形式陈述

Hindley–Milner（HM）系统为带 let 的 lambda 演算提供秩一参数多态：lambda 绑定变量单态使用，而 let x=e_1 in e_2 可把 $e_1$$e_1$ 推得的、未受环境约束的类型变量泛化成类型方案 $\forall\bar\alpha.T$$\mathrm{\forall }\overline{\alpha }.T$。Algorithm W 递归生成类型约束，以带 occurs check 的一阶合一求最一般合一子，并返回主类型：任何其他合法类型都是主类型的实例。纯 HM 的类型推断无需程序员写类型标注且可判定。

直觉

程序先产生“这些类型必须相同”的方程，合一求出最少承诺的解；let 边界再把不依赖环境的未知量安全地推广为可重复实例化的泛型。

例子与边界

let id = fun x -> x in (id 0, id true) 可让两次 id 分别实例化为 Int→Int 与 Bool→Bool。表达式 fun x -> x x 会要求 $\alpha=\alpha\to\beta$$\alpha =\alpha \to \beta$，occurs check 拒绝无限类型。加入可变引用时，无限制 let 泛化会不安全，ML 通常采用值限制；高秩多态、子类型和类型类也需扩展算法。

推论与应用

HM 奠定 ML 系语言的自动类型推断和主类型接口。它展示了表达力与可推断性的精确折中：比单态系统通用，又避开 System F 一般类型重建的不可判定性。

参考资料

• Benjamin C. Pierce, Types and Programming Languages, MIT Press, 2002，Ch. 22, type reconstruction and let-polymorphism。
• Robert Harper, Practical Foundations for Programming Languages, 2nd ed., Cambridge University Press, 2016，Ch. 10, type inference and polymorphism。