recursive module で polymorphic recursion を書く

OCaml 3.12.0 より明示的に型を書くことで polymorphic recursion (多相再帰) が簡単に書けるようになりました:

let rec len : 'a. 'a sep -> int = function
  | Nil -> 0
  | Cons (_, sep) -> 1 + 2 * len sep

let rec ... in ... で定義される値は、in の後では polymorphic でも、定義の中では monomorphic。異なる複数の型で使うことは出来ません。でも、ほとんど普通は違った型で使ったりしないので、不便ありません。でもタマ〜に、定義中でも polymorphic だったら嬉しいな、ということがあります。例えば、Chris Okasaki の本

Purely Functional Data Structures

Purely Functional Data Structures

でも書いてある complete binary tree の data type とか。持ってない人は http://www.dcc.ufmg.br/~camarao/sblp2003.pdf の3ページ目とか見てください:

type 'a sep = Nil | Cons of 'a * ('a * 'a) sep

この型が何かってのは本や論文を見てもらうとして、この型でノード数を調べる関数 len は普通定義できません:

# let rec len = function
    | Nil -> 0
    | Cons (_, sep) -> 1 + 2 * len sep
  ;;
                                   ^^^
Error: This expression has type ('a * 'a) sep but is here used with type 'a sep

len は 'a sep -> int という型で定義されている所なのに、('a * 'a) sep -> int として使っている。なのでエラー。

さて、この let rec からこの制限を無くして、定義内部でも sep を他の型でも、つまり polymorphic に使えるようにしたものを polymorphic recursion と言います。Polymorphic recursion の型推論は undecidable なので一般的には出来ません。*1でも型チェックは出来るので、len の polymorphic な型を与えてやれば大丈夫です。例えば Haskell だと

len :: Sep a -> int
len Nil = 0
len (Cons (_, sep)) = 1 + 2 * len sep

みたいに書ける。(細かいシンタックスは知らんよ。)

で、OCaml でも出来るというのが本題です。Recursive module を使います:

module rec M : sig
  val len : 'a sep -> int
end = struct
  open M
  let (* rec はいらない *) len = function
    | Nil -> 0
    | Cons (_, sep) -> 1 + 2 * len sep
end
let len = M.len

めんどくさいけど。もうちょっと綺麗にしようと思って、

let len = 
  let module rec M : sig
    val len : 'a sep -> int
  end = struct
    open M
    let len = function
      | Nil -> 0
      | Cons (_, sep) -> 1 + 2 * len sep
  end in
  M.len

としたら、 let module rec は無いそうです。じゃあ、

let len = 
  let module N = struct
    module rec M ...
    include M
  end in
  N.len

としようとしたら、expansive だと言われて polymorphic になりませんでした。痛し痒し。η変換するのもなんだかすっきりしない。という訳で、一番始めの例で我慢。

いちいち書き下すのもなんだから、p4 マクロでも書こうかしらん。

*1:そこをなんとかして一部のありがちな物に関しては型推論できるようするっていう研究が幾つもありますけど、それには触れません。