OCamlのlocally abstract typeに関するメモ２ （構文）

Locally abstract typeについてメモを続けていく。今回は構文について。

locally abstract typeに関する構文は４つある。そのうち３つは糖衣構文と言っていい。

基本構文

まず一番基本の構文

fun (type a) -> e

ぱっと見では関数式のように見えるが、上記の構文ではfun (type a) -> ...の部分はあくまでlocally abstract typesを導入しているだけでeには関数だけではなく任意の式が入る（型検査が通るかは別問題だが・・・）。そしてfun (type a) -> eを評価するとeは即座に評価される。

この「ぱっと見では関数式に見えるけど違う」というのは公式リファレンスでもかなり初めの方で：

Note that contrary to what the syntax could suggest, the expression fun ( type typeconstr-name ) -> expr itself does not suspend the evaluation of expr as a regular abstraction would. The syntax has been chosen to fit nicely in the context of function declarations, where it is generally used.

と言い訳的な説明が入る。"where it is generally used"とある通り関数以外でのうまい使用例は知らないが、構文上は関数に限定されていない。

ちなみにこの構文は言語開発者の間でもなんとなく微妙だと思われているようで、Gabriel Schererがredditのスレで「ほとんど使われないような機能だろうから構文がちょっと微妙でもいいだろうと考えていたら、時が経つにつれてみんな使うようになってしまった」と書いていた：

Finally: at the time where this feature was introduced, it was understood to be useful only in combination with advanced/arcane constructs that most OCaml programmers would rarely, if ever, encounter. So the fact of being slightly convoluted was not such a big issue. As time goes on, features thought of as "advanced" get internalized by more and more people and end up in more codebases.

関数用の糖衣構文２つ

実際に使うとなるとeは関数式であることが多い。そうするとfun (type a) -> fun (x : t) -> e（ただしtやeにaが出てくる）となってかなり冗長だ。

それを避けるための糖衣構文が二つ用意されている。

まず第一：

fun (type a) (x : t) -> e

fun (type a) -> fun (x : t) -> eの最初の二つのfunを合わせて一つにしている。

第二の糖衣構文はlet f = fun x -> eをlet f x -> eと書けるのと同じ理屈:

let f (type a) (x : t) = e

明示的な多相型注釈との組み合わせ

最後の糖衣構文は、locally abstract typeを導入するだけではなく関数に明示的な多相型注釈をつける場合。

糖衣構文なしだと

let f : 'a. t = fun (type a) (x : u) -> e

といった形になるのが

let f : type a. t' = fun (x : u) -> e

と表現できる（t'はtの中の'aをaに置換したもの）。

OCamlで関数に明示的な多相型注釈をつける必要があるのは大抵（常に？）多相な再帰関数なので、この糖衣構文は「多相な再帰関数にlocally abstract typesを導入する必要がある」ケース、例えばGADTに対する再帰などで活躍する。

次回

次はどのような状況でlocally abstract typesが必要になってくるのかを見ていく。