Hindley-Milner型推論

Hindley-Milner (HM) 型推論は、明示的な型注釈なしに完全な型無しλ項へ主要型 (principal type) を割り当てる型推論。let多相 (let-polymorphism) を実現する型システム上で動く。

アルゴリズム

• Algorithm W: top-down なアプローチ。単一化 (unification) を使いながら型変数の代入を求める。TaPL 22章のものとは異なり型注釈を許さず、完全な型無し項に主要型を付ける。
• Algorithm M: bottom-up なアプローチ。期待型を伝播させながら推論する。
• 派生として Algorithm DW もある。
• 部分型 (subtyping) には素朴な HM は対応せず、$F_{<:}$ 等の拡張が要る。

実装

• Haskell 実装（STRef で単一化）、Julia 実装（MinCaml の型推論段）、Rust 実装 (type-theory-rs) などで写経されている。MinCaml ではこの型推論を入れるとレイトレが書ける。

関連

• 載せる型システムはtype-theory-lambda-cube、部分型拡張はsubtyping-variance。
• λ項の表現はlambda-calculus。
• _moc-prog-lang