同値再帰型で相互再帰する

同値再帰型(Equirecursive types)とは，再帰型の一種で，再帰的なデータの型である．
同値再帰型を用いて型付けできる構造には，たとえば，

• Yコンビネータ
• リストなどの再帰的構造

などがある．

事例1: Yコンビネータ

OCaml トップレベルでは， -rectypes オプションを用いることで有効にできる．
utop でも -rectypes オプションを使うと有効にできる．

$ utop -rectypes
utop # let y f = (fun x -> f (x x)) (fun x -> f (x x));;
val y : ('a -> 'a) -> 'a = <fun>

(正格評価なので) この y は実行しても無限ループするだけなのでなんの意味もないが，型をつけることはできる．

事例2: リスト

多相バリアントと組み合わせると，なんと型宣言なしでリストを始めとした様々な構造を使うことができる．

utop # let rec map f = function
    `Nil -> `Nil
  | `Cons(x,xs) -> `Cons(f x, map f xs);;
val map : ('a -> 'b) -> ([< `Cons of 'a * 'c | `Nil ] as 'c) -> ([> `Cons of 'b * 'd | `Nil ] as 'd) = <fun>

Isorecursive types について

同値再帰型(Equirecursive types)と似たものに， Isorecursive types というものがある．
Equirecursive types は暗黙のうちに roll/unroll する． Isorecursive types は roll/unroll を明示する． (ちなみに，roll/unroll は fold/unfold と呼ばれることもある)

本題

さて，このように同値再帰型はすごいものであって，これでさまざまな構造が表すことができるので，いろいろ表してみたくなる．ところが，ここでひとつ問題が生じる．相互再帰的な構造をどう表すのかということだ．

具体例．たとえば， JavaScript の AST を表す型をつくるとする．
JavaScript の次のようなコードについて考える:

(function (x) { return x; })

これは，素直に考えるとこうなるはずだ:

type ident = string
type expr = Ident of ident | FuncLit of ident list * stmt list
 and stmt = Return of expr
let ast = FuncLit(["x"], [Return (Ident "x")])

expr の定義に stmt が現れ，かつ stmt の定義に expr が現れている．このような定義を相互再帰という．

再帰型でこのような構造を表すのはちょっと難しい．

しかし，これをうまく表す方法がある．相互再帰する型を，型変数として受け取るのである．つまり:

type ident = string
type ('expr,'stmt) expr1 = Ident of ident | FuncLit of ident list * 'stmt list
type ('expr,'stmt) stmt1 = Return of 'expr
type expr = ('expr, ('expr,'stmt) stmt1 as 'stmt) expr1 as 'expr
type stmt = (('expr,'stmt) expr1 as 'expr, 'stmt) stmt1 as 'stmt
let ast : expr = FuncLit(["x"], [Return (Ident "x")])

これでよし．

参考文献

• Stone Christopher A. (2005) "Equational Theories with Recursive Types", p17 2015年2月25日アクセス．