Hindley–Milner 型推論

type-theorycomputer-science

ML / Haskell 系の古典的型推論。型注釈なしで最も一般的な型（principal type）を一意に自動導出する。実装の代表が Algorithm W（Damas–Milner, 1982）。parametric 多相に let 多相 を足した体系。

仕組み

  1. 各部分式に型変数を割り当てる
  2. 構文から制約（等式）を集める
  3. 単一化（unification, Robinson）で制約を解き、代入（substitution）を得る
let id = \x -> x in (id 1, id True)
-- id :: ∀a. a -> a に一般化され、各使用箇所で a を Int / Bool に具体化

let 多相（核心）

これにより同じ id を Int にも Bool にも使える。λ束縛の引数は一般化されない（単相）点が要。

principal type の保証

HM では「最も一般的な型が必ず一意に存在する」（完全性）。だから人間が注釈を書かなくても、コンパイラが過不足ない型を決められる。

限界

ランクN多相・部分型・GADT・HKT・篩型では完全推論が決定不能・困難になり、双方向型検査や明示注釈が要る。現代の実装は substitution ベースの W から、制約生成と求解を分離した方式（HM(X), GHC の OutsideIn(X)）へ。

関連

Graph

Backlinks