Hindley-Milner型推論の仕組み

なぜ注釈なしで型が決まるのか

ML や Haskell では let id = \x -> x と書くだけで、コンパイラが id の型を a -> a と割り出します。注釈は一切いりません。これを支えるのが Hindley-Milner（HM）型推論です。HM の凄みは、書ける式に対して必ず最も一般的な型（principal type、主要型）が存在し、しかもそれを機械的に一意に求められる点にあります。動的型付けのように実行時へ検査を遅らせるのではなく、コンパイル時に全式の型を決め切ります。

原理は二つの柱に分解できます。式から型の等式制約を集めて解く**単一化（Unification）と、let で束縛した定義を多くの型で使い回せるようにするlet多相（let-polymorphism）**です。順に分解します。

制約を集める：型変数を置く

HM はまず、型が未知の箇所に型変数（慣例で a, b, t0, t1）を仮置きします。そして式の構造から、型が満たすべき等式を機械的に書き出します。たとえば関数適用 f x を見たら、「f の型は 引数の型 -> 結果の型 でなければならない」という制約が生まれます。

-- 推論したい式
\f -> \x -> f (f x)

ここで f : t_f、x : t_x と置くと、内側の適用 f x から「t_f = t_x -> t1」、外側の f (f x) から「t_f = t1 -> t2」という制約が出ます。型推論とは、こうして集めた制約をすべて満たす型変数への代入を求める作業に他なりません。

単一化（Unification）：制約を解くエンジン

単一化とは、二つの型を「等しくするための最小限の代入」を見つけるアルゴリズムです。t_x -> t1 と t1 -> t2 を単一化するなら、対応する位置を突き合わせて t_x = t1、t1 = t2 を導きます。規則はごく単純です。

• 同じ型構築子同士（-> と ->、List と List）なら、引数の型を再帰的に単一化する。
• 型変数 a と任意の型 t なら、a := t という代入を作る（a を t に束縛）。
• 構築子が食い違う（Int と Bool、Int と a -> b）なら型エラー。これが型不一致の正体です。

求まる代入は **MGU（most general unifier、最汎単一化子）**と呼ばれ、「等式を満たす中で最も束縛が少ない＝最も一般的な解」になります。HM が主要型を導けるのは、単一化が常に MGU を返すからです。

let多相：同じ定義を複数の型で使う

ここからが HM の核心です。次の式を考えます。

let id = \x -> x
in (id 1, id "hello")

id は整数にも文字列にも適用されています。もし id の型変数を単一化で固定すると、id 1 で a = Int に縛られ、続く id "hello" が型エラーになってしまいます。これを救うのが let多相です。

let で束縛を作るとき、HM はその定義の型に含まれる「他で固定されていない型変数」を**一般化（generalize）し、forall a. a -> a という型スキーム（多相型）へ持ち上げます。そして id を使うたびに、forall の変数を新しい型変数で具体化（instantiate）**します。id 1 では a := Int、id "hello" では別個に a := String と、呼び出しごとに独立した型が割り当てられるため、両立します。

let多相とラムダ束縛の違い

同じ「変数に値を束縛する」でも、let と**ラムダ引数（関数の仮引数）**では多相の扱いが正反対です。ここは資格試験でも実務でも誤解されがちな要点です。

\id -> (id 1, id "hello") が通らないのは、引数 id の型を一般化できず、id 1 で Int に固定された瞬間に id "hello" が矛盾するためです。第一級の多相を引数に渡したいときは rank-N 多相という拡張が要りますが、それは推論の決定可能性を犠牲にし、明示注釈を要求します。素の HM が型注釈なしで決定可能なのは、多相を let の位置に限定しているからこそです。

Algorithm W の全体像

ここまでの部品を組み上げたのが、Damas と Milner による Algorithm W です。式を再帰的にたどり、次を行います。

1. 変数参照なら、型環境から型スキームを引き、forall を新しい型変数へ具体化する。
2. ラムダ \x -> e なら、x に新鮮な型変数を割り当て（単相のまま）本体を推論し、引数型 -> 本体型 を組む。
3. 適用 f x なら両者を推論し、f の型を x型 -> 新変数 と単一化する。
4. let x = e1 in e2 なら e1 を推論し、その型を一般化して環境に入れ、e2 を推論する。

結果として得られる代入を全体に適用すれば、注釈ゼロでも全式の型が確定します。複雑な値の分類自体は変数とデータ型、検査をいつ行うかという軸は型システム（静的型付け vs 動的型付け）で扱っています。

HM の限界と実務での位置づけ

HM は強力ですが万能ではありません。素の HM は部分型（サブタイピング）や型クラス、第一級多相（rank-N）を直接は扱えません。Haskell は型クラスを、辞書渡しと制約付き型スキーム（Ord a => a -> a -> Bool の形）で HM に上乗せして実現しています。また let を再帰や相互再帰へ広げると、単一化が単純には終わらず、束縛グループごとに一般化する工夫が要ります。

実務的には、HM 系の推論は「注釈は要所だけ、残りは導出」という快適さの源泉です。型を引数化する発想はジェネリクス（総称型）と地続きで、forall a. a -> a はまさに総称型の数理的な姿です。コンパイル時に型を解き切るという点では、解析と検査のタイミングを論じたコンパイルとインタプリタとも響き合います。原理を押さえれば、推論が詰まったときに「どの制約が衝突したか」を自力で追えるようになります。