类型方案

类型方案不是一个“包含未知量的单类型”，而是一份可反复生成单态实例的模板。每次使用多态变量都要把量化变量换成新的类型变量，否则两次调用会被错误地强迫成同一类型。泛化时排除环境中的自由变量同样关键：这些变量代表外部已经共享的约束，擅自量化会把一份单态资源伪装成多态。类型方案位于可推断性与表达力的折中点，只提供外层全称量化，却足以覆盖大量泛型代码。

恒等函数的方案是 $\mathrm{\forall }\alpha .\alpha \to \alpha$。在 let id = λx.x in (id 0, id true) 中，两次读取 id 分别实例化为 $\mathbb{Z}\to \mathbb{Z}$ 与 $\mathbb{B}\to \mathbb{B}$，因此整个表达式良类型。

边界是 λ 绑定参数：标准 Hindley–Milner 不会把 λf.(f 0, f true) 中的 f 自动视为多态方案，因而该项不可定型。多态递归和高秩参数也超出普通类型方案推断，需要显式注解或更强系统。

类型方案是Hindley–Milner 类型推断公理库Hindley–Milner 类型推断Hindley–Milner type inference · HM type system为带 let 的秩一参数多态 λ 演算提供主类型性质与可判定类型推断的系统。中 let 多态的表示，Algorithm W公理库Algorithm WAlgorithm W为 Hindley–Milner 语言递归推导主类型方案的统一算法。在变量处实例化、在 let 处泛化。一阶统一公理库一阶统一First-order unification · Syntactic unification寻找使若干一阶项在替换后相等的最一般替换。只求解生成的单态约束，量化边界由方案机制管理。

在实现上，方案使泛型函数无需复制源代码即可安全复用；带可变状态的语言还需值限制，避免把具有分配效果的表达式不安全地泛化。