Hindley-Milner 类型推断

定义

Hindley-Milner（HM）类型系统是一种支持参数化多态的类型系统，以逻辑学家 J. Roger Hindley 与计算机科学家 Robin Milner 命名，配套的 Algorithm W 由 Milner 提出、经 Luis Damas 形式化，故也称 Damas-Milner 系统。

核心性质

HM 最重要的性质是主类型（principal type）定理：任何可类型化的表达式都存在一个最一般的类型，所有其他合法类型都是它的实例。推断过程完全可判定，程序员无需书写任何类型标注，编译器通过合一（unification）算法自动求解类型约束。

机制

关键机制是 let 多态：在 let 绑定处对类型变量做泛化（generalization），在使用处做实例化，从而让同一个函数以多种类型被复用。

应用

ML、OCaml、Haskell、Elm 等语言的类型推断均以 HM 为基础；Rust、Swift 等语言采用其局部化变体。