OCaml の弱い型変数についての解説

弱い型変数.md

ML の型システムには 2 種類の型変数があります。多相型の型変数と単相型の型変数です。OCaml では多相型の型変数のことを単に型変数と言い、単層型の型変数のことを弱い型変数と言います。

弱い型変数が現れるプログラム例を見てみましょう。

let id x = x in id id

関数 id のラムダ計算での表記は $\lambda x.x$ です。$(\lambda x.x)(\lambda x.x)\rightarrow_{\beta}\lambda x.x$ なので、id id の型も id と同じになるように思われます。しかし、実際には id の型は 'a -> 'a であるのに対し、id id の型は '_weak -> '_weak になります。('_weak は弱い型変数)

id id の前半の id を id1、後半の id を id2 とおきます。id1 の引数の型は 'a であり、実引数である id2 の型は 'b -> 'b です。整合性をとるために 'a と 'b -> 'b を単一化します。

Note

ふたつの項 $s,t$ が与えられたときに、$\theta s=\theta t$ を満たすような代入 $\theta$ を求めることを単一化と言います。単一化可能であれば、条件を満たす代入は無限に存在しますが、基本的には最も一般的な代入を考えます。

結果として、'a を '_weak -> '_weak にして、'b を '_weak にするような代入が得られます。型の単一化が行われると、多相型は単相型に変化します。このため、普通の型変数ではなく弱い型変数が代入されます。実際に代入をすると、id1 の型は ('_weak -> '_weak) -> ('_weak -> '_weak) になり、id1 id2 の型は '_weak -> '_weak になります。