OCamlで使える同値再帰型 (equi-recursive types) は恐ろしいけど、すごい
この記事は OCaml Advent Calendar 2012 の 17日目の記事です。
同値再帰型が何であるか知りたい方は、今後発売される TAPL日本語版を読むと良いと思います（私も翻訳しています。*1）。 Wikipedia英語版にもありますね。
同値再帰型は、再帰型の定式化の方法のひとつで、「型の再帰構造が外からまる見えな型」といった風情の型です。例えば無限リストは、普通の(同型)再帰型なら
type 'a inflist = InfList of 'a * 'a inflist let rec ones = InfList(1, ones)
などと、ヴァリアント等を介さないと定義できませんが、 -rectypesオプションで同値再帰型が有効になっている場合、タプルを組み合わせるだけで無限リストを作れます。
let rec ones : int * 'a as 'a = 1, ones;;
この int * 'a as 'a が同値再帰型で、上の Wikipedia の記事の記法では μα. int * α などと表記されています。
この同値再帰型 FOOBAR as 'a は、 FOOBARに出現する 'a を自分自身に置き換えて展開した型もすべて同じ型とみなされます。つまり int * 'a as 'a と int * (int * 'a) as 'a と int * (int * (int * 'a)) as 'a 等は すべて同じ型とみなされます。型推論もちゃんと効くようです。すごいですね。
無限リストでなくても、任意の再帰型を同様の方法で作れます。例えばintのリストμα.(1+ int*α) と同様の構造をもつ型は、OCamlでは直和の部分を option で表現すれば (int * 'a) option as 'a という型で表現でき、次のように扱えます:
# let intlist = Some (0, (Some (1, (Some (2, None)))));; val intlist : (int * (int * (int * 'a option) option) option) option = Some (0, Some (1, Some (2, None))) # let rec map f = function Some (hd, tl) -> Some (f hd, map f tl) | None -> None;; val map : ('a -> 'b) -> (('a * 'c) option as 'c) -> (('b * 'd) option as 'd) = <fun> # map (fun x -> x+1) intlist;; - : (int * 'a) option as 'a = Some (1, Some (2, Some (3, None))) #
もちろん木構造も表現できます（やってみましょう！）
フリーダムすぎる同値再帰型
恐らくメジャーな言語ではOCamlくらいにしか備わっていない同値再帰型(equi-recursive types)。
面白いですが、あまりにも自由すぎるせいで、恐らくプログラマが意図しない式にも型がついてしまいます。
$ ocaml
OCaml version 4.00.1
# #rectypes;; (* 同値再帰型を有効にするコマンド *)
# let f x x = x x;;
val f : 'a -> ('b -> 'c as 'b) -> 'c = <fun>
# let f x = x::x;;
val f : ('a list as 'a) -> 'a list = <fun>
# let rec i = (i, i);;
val i : 'a * 'a as 'a =
(((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((...),
(...)),
(何か良くわからない括弧の山)
このように弊害が大きいので、OCamlでも-rectypesはデフォルトではオフになっています。サブタイピングと組み合わせたとき、理論的な扱いがとても難しくなる（TAPLでも余帰納法を導入する等、そのあたりが一つの大きな山になっている。興味のある方はチャレンジしてみてください。）のも、あまり他の言語で実装されていない理由の一つのようです。
が、多相バリアントやオブジェクト型では -rectypes 無しでも同値再帰的な型付けになります。というか、同値再帰のおかげでこれらが有用になっている、言ってみればOCamlのひとつの神髄は同値再帰にあり、といっても過言ではない側面があります。それについてはまた。
