TIL: OCamlで再帰とlet多相

これは相互再帰ではないですが、
let main = id(3);
let id(n) = n;
のようなプログラムの時に、main: Int -> Int, id: a -> aと型推論したいのですが、現在(単相型推論)の場合構文解析時にトップレベルで定義された変数名を記録しておいて、型推論時に予め型環境に上記変数名とフレッシュな型変数続き

— taka2 (@Jj1Fxh) December 8, 2022

こちらの話が大変興味深かったのでOCamlでどうなっているか試した。

結論からいうと、順序関係なく単相化されてしまう：

utop # let rec id x = x
and main () = id 3;;
val id : int -> int = <fun>
val main : unit -> int = <fun>

考えてみたら相互再帰じゃなくても

utop # let rec f b x =
  if b then x else (ignore (f true 5); x);;
val f : bool -> int -> int = <fun>

のように単相化されてしまう。

明示的に全称型な型注釈をつければ大丈夫：

utop # let rec f : 'a. bool -> 'a -> 'a = fun b x ->
  if b then x else (ignore (f true 5); x);;
val f : bool -> 'a -> 'a = <fun>

ただしOCamlの場合はHaskellと違って相互再帰な可能性のある範囲が非常に狭い（let rec ... and ... and ...と指定された範囲のみ）のでこの挙動がlet多相化の邪魔をする可能性はそこまで高くない。Haskellだとスコープ全体で再帰の可能性があるので強連結成分を算出してそれらの依存関係を出して、その順番で型推論していく必要などが生じるのだろうか。

と思って調べたらそういう話がredditで出ていた

www.reddit.com

そして今ふと思い出したのだけどcamlspotter's blogでもこの話に触れられていた：

camlspotter.hatenablog.com

「SCC を計算すればいいのにサボっている」は間違い

これは、値の使用グラフを作ってその SCC (Strongly Connected Component) を計算すれば let/let rec の区別は付くはずなので、let/let rec の区別は必要ない。必要なのは型推論器の実装に手を抜いているから、という意見だ。

Haskell ユーザーはついこの批判をしてしまうように見受けられる。(実際私もこの主張を日本語であれ英語であれ何度か見ている。) なぜなら Haskell では実際に SCC を計算する事で let束縛の入れ子をフラットにしたまま多相的なプログラムを書くことが出来るからだ。

OCamlはサボってるわけではないが、自作言語ではlet rec相応のものを入れて遠慮なくサボりたい所存。