多相ヴァリアントを触っていたときに気づいた小ネタの紹介。
ある再帰的コード
let rec x = `N[x; `M] in x
ここで `N[x; `M] は `N([x; `M]) のようにコンストラクタ `N にリストを適用しただけのコード。
これは μ記法 を使うと μx. `N [x; `M] とかける。最初に `N が来て、そのあとは [`N[...]; `M] と続く無限木（あるいはグラフ）を表す。
単一化ベースの型推論に対する(私の)過剰な期待
多相ヴァリアントの熱烈なファンとしては、この「最外は`Nのみ」という性質が型に現れてほしいところだが、OCaml処理系は次のように推論する：
[> `M | `N of 'a list ] as 'a
最外にも `M が出現しうると推論されてしまう。 これは型推論の過程で x の出現と x の定義に同じ型変数を割り当ててしまうため、といったらよいのだろうか。
ただし上のようなケースが現実のプログラミング場面で頻繁に現れるかといえばかなり疑問ではある。
意外なコーナーケース以上のものではない、かもしれない。
どう直す
x を1回展開して
let rec x = `N([`N[x; `M]; `M]) in x
[`N(...); `M] の部分に結び目を移して、`N を再帰定義の外に出す。
let rec y = [`N(y); `M] in `N(y)
こうすれば、推論される型は期待通り
[> `N of [> `M | `N of 'a ] list as 'a ]
となる。
余談
ICFP'16 の Set-Theoretic Types for Polymorphic Variants (Castagna et al.) ではサブタイピングと HM(X) による型推論が提案されており、より精密な型が推論されるようになっている。
型推論器はこちらで触ってみることができる：
リストがないので if 文で似たようなコードを書いてみると、
# recfun f x -> `n (if x then f x else `m);;
- : Bool -> `n(X1) where X1 = `n(X1) | `m
- = <fun>
のように、期待通りの型が推論される。面白い。
とはいえ、こんなコーナーケースを見つけたのは初めてだし、私は今の OCaml の型推論には満足している。