TIL：OCamlコンパイラのrectypesフラグ

再帰型についてTaPLなどを読み返していて、ようやく再帰型の「2大流派」であるisorecursiveとequirecursiveの違いなどがわかってきた。調べている間にOCamlコンパイラの-rectypesというフラグについて知ったのでメモ。

OCaml（そしてほとんどの関数型プログラミング言語）はisorecursiveな観点で再帰型を実装している。

型システム実装シリーズでもこの制約に少し当たっている：

zehnpaard.hatenablog.com

new_tvar内で定義されているfがTVar nと共にf (n+1)を返している。しかしこれを実現するためにはただのタプルだとOCamlの型検査を通らないのでtype new_tvar = NewTVar ...と新しい型とコンストラクタを定義している。

の部分で、新しい型とコンストラクタを定義することによってisorecursiveな再帰型が導入されている。もしOCamlがequirecursiveな再帰型をサポートしていたらただのタプルでも型レベルの再帰が可能（なはず）。

実はOCamlコンパイラは-rectypesというフラグを受け取り、これがあると全般的にequirecursiveな型が受け入れられるようになるらしい。

とりあえず手元のshellで試してみる。

まずはnew_tvarを簡略化した関数を定義した：

experiment$ echo "let rec f n () = (n, f(n+1))" > testrec.ml

簡単なカウンタ関数で、インクリメントされていく数字と「次に呼ぶべき関数」を返している。

普通にocamlcでコンパイルしようとする：

experiment$ ocamlc testrec.ml
File "testrec.ml", line 1, characters 21-27:
1 | let rec f n () = (n, f(n+1))
                         ^^^^^^
Error: This expression has type unit -> int * 'a
       but an expression was expected of type 'a
       The type variable 'a occurs inside unit -> int * 'a

occursチェックで失敗しているのがわかる。

今度は-rectypesフラグ付き：

experiment$ ocamlc -rectypes testrec.ml
experiment$ ls
a.out       testrec.cmi testrec.cmo testrec.ml

型検査を通ってコンパイルが完了している。

このコードだと実行しても何も起きないので、実際にこのf関数を使うよう変えてみる：

let rec f n () = (n, f(n+1))

let () =
  let (n, g) = f 0 () in
  let (m, g) = g () in
  let (p, _) = g () in
  print_endline @@ string_of_int (n+m+p)

コンパイル＆実行してみると以下の通り：

experiment$ ocamlc -rectypes testrec.ml
experiment$ ./a.out
3

うまくいっているようだ。

ただ本当にequirecursiveな再帰型を許容したいかというと微妙なところで、どちらかというと変なバグを型エラーとして検出できなくなる側面の方が強いようだ。まあ「こういうものもある」と頭に留めておくくらいのものだろうか。