Hindley–Milner 类型推断

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

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

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

边界首先来自效果。值限制理路值限制与安全泛化Value restriction · Relaxed value restriction限制带引用的let泛化，阻止同一存储单元被独立实例化为不兼容类型。用同一个引用先写整数列表、再误读成布尔列表的执行，说明为什么一次分配结果不能任意泛化；λ工厂则通过每次新建单元避免错误共享。

多态递归理路多态递归Polymorphic recursion · Milner–Mycroft recursion让递归定义内部的每次自调用重新实例化显式全称签名，以处理参数类型随结构层次变化的数据。让递归体内的自调用在不同元素类型上实例化，例如从Perfect a递归到Perfect(a×a)。高秩参数理路高秩多态与局部检查Higher-rank polymorphism · Rank-n polymorphism把全称量词放进函数参数类型，并用实例化、刚性变量与逃逸检查验证多态承诺。则把全称量词保留在函数箭头左侧，使同一个参数能在一次调用里处理Int与Bool。这两项都超出标准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 通过全局约束统一寻找主类型。类型类、行多态与效应等扩展还需分别管理它们对可判定性和主类型的影响。