Hindley–Milner 类型推断

HM 的巧妙之处是让程序员省略类型参数和多数注解，编译器却仍能找到最一般的答案。应用产生“函数参数类型必须等于实参类型”的方程，统一算法传播这些等式；let 则把与外部环境无关的未知类型泛化，使同一函数在不同位置独立实例化。主类型像约束信息的最小承诺：它没有过早选定具体类型，却能生成所有合法特例。秩一限制牺牲了把任意多态函数作为参数的表达力，换来可判定、完备的推断。

对组合函数 λf. λg. λx. f (g x)，推断得到

它是所有具体组合函数类型的主类型。let id = λx.x in (id 0, id true) 通过 let 泛化成立，而把 id 改成普通 λ 参数时不再自动获得多态实例。

边界来自效果与更高阶多态。若把一次可变引用分配的结果任意泛化，可能在同一位置写入不同类型的值，因此 ML 类语言采用值限制。多态递归和高秩类型一般不能由标准 HM 自动推断，需要注解或更强约束求解。

HM 奠定 ML、OCaml、Haskell 核心类型推断的基础。类型方案公理库类型方案Type scheme · Polytype通过显式量化类型变量表示一族单态类型的多态对象。表达 let 多态，一阶统一公理库一阶统一First-order unification · Syntactic unification寻找使若干一阶项在替换后相等的最一般替换。求解约束，Algorithm W 给出构造性主类型算法。

主类型支持模块化错误定位和泛型库复用；现代语言常让 HM 推断服务于代数数据类型公理库代数数据类型Algebraic data type · Algebraic datatype以有限构造子的和、每个构造子字段的积以及可选递归组合数据形状的类型。构造与模式，但和、积、递归的数据定义不是 HM 核心推断规则的前置。双向类型检查公理库双向类型检查Bidirectional type checking · Bidirectional typing把类型综合与给定类型下的检查分开，并用局部注解连接两种方向的算法化类型判断。则以局部的 synthesis/checking 方向和必要注解组织信息，区别于 HM 通过全局约束统一寻找主类型。类型类、行多态与效应等扩展还需分别管理它们对可判定性和主类型的影响。