Algorithm W

W 沿语法树一边走一边积累“到目前为止必须成立的类型等式”。每遇到未知值就生成新鲜类型变量，每遇到应用就让统一算法校准插头与插座，所得替换立即改写后续世界。let 是唯一的多态关口：先把局部求出的类型中不受环境约束的变量封装成方案，之后每次使用再新鲜实例化。它不是试遍所有类型，而是始终维护最一般解，因此一次运行就得到整个类型族。

对 λf. λx. f x，W 为 $f,x$ 分配新鲜类型 $\alpha ,\beta$，应用处统一 $\alpha$ 与 $\beta \to \gamma$，最终得到 $(\beta \to \gamma )\to \beta \to \gamma$。对

let id = λx.x in (id 0, id true)，

绑定处得到 $\alpha \to \alpha$ 并泛化为 $\mathrm{\forall }\alpha .\alpha \to \alpha$，两次使用分别新鲜实例化，因此可同时接受整数和布尔值。

边界是省略 occurs check：推断 λx. x x 时会产生 $\alpha =\alpha \to \beta$，标准有限类型下应失败。W 也不推断任意高秩或多态递归类型；给它加入语言特性后，主类型和完备性可能不再成立。

复合不是合并映射 ​

令 $S_1=\{\alpha \mapsto \beta \}$、$S_2=\{\beta \mapsto \mathsf{Int}\}$。正确复合把 $\alpha ,\beta$ 都送到 Int；简单字典并集却在一次同时替换下仍把 $\alpha$ 送到 $\beta$。计算 $S_2\circ S_1$ 时应先用 $S_2$ 改写 $S_1$ 的每个像，再为不在 $\mathrm{dom}(S_1)$ 的变量补入 $S_2$ 的映射。这也覆盖两个定义域相交的情形，因为原变量首先经过 $S_1$。

嵌套 let 的完整替换账本 ​

考虑闭项

λf.
  let id = λx.x in
  let y = f (id 0) in
  let keep = λz.y in
  (id true, keep (id 0))

令 $f$ 的初始单态类型为 $\alpha$。id 的参数类型取新鲜 $a$，故得到 $a\to a$；$a$ 不自由出现于环境 $f:\alpha$，于是方案为 $\mathrm{\forall }a.a\to a$。下表按实际从左到右的推断次序，记录所有应用处新增的统一约束与替换。每行替换都左复合到此前累积替换，并作用于后续环境。

两处 let 的处理发生在表的第二行之后，不能跳过：

1. 绑定 y 时，环境已含 $f:\mathsf{Int}\to d$，所以 $d\in \mathrm{FTV}({\mathrm{\Gamma }}_1)$。y 的类型是 $d$，没有可泛化变量，方案仍是单态 $d$。
2. 推断 λz.y 时，为 $z$ 取新鲜 $e$，得到 $e\to d$。此时环境含自由 $d$，但不含 $e$，故 keep 的方案为 $\mathrm{\forall }e.e\to d$。表末调用把量化的 $e$ 新鲜化为 $i$，并保留共享的 $d$。

最后一行的 $d\mapsto \ell$ 必须继续更新 $f$、y 和 keep 的自由部分。最终累积替换对所有已引入变量的非恒等作用为

这里 $a,e$ 在各自方案中被量化，不是后续统一可以全局改写的共享槽位。二元组类型为 $\mathsf{Bool}\times \ell$；最外层 λ 要用更新后的 $S\alpha$，因此闭项的主方案为

取 $\ell =\mathsf{Int}$ 或 $\ell =\mathsf{Bool}$ 都得到合法实例。若让 keep 泛化共享的 $d$，便错误允许它把同一个 y 返回为任意类型；若忘记更新 λ 参数，则结果还会保留不受约束的 $\alpha$，同样不可靠。

统一器维护的是全部解的因子分解 ​

对原方程集合 $E_0$，统一器维护残余集合 $E$ 和累积替换 $S$，初态为 $(E_0,\mathrm{Id})$。用 $\mathrm{Sol}(E)$ 表示所有满足 $E$ 的有限类型替换，核心不变量是

每次取一条当前方程，按以下顺序处理：相同类型删去；同一箭头或积构造器分解成两个分量方程；若一侧为变量 $\alpha$，把它朝向左侧，对另一侧 $\tau$ 做 occurs check，再令 $T=\{\alpha \mapsto \tau \}$，把状态改为 $(T{E}_{\mathrm{rest}},T\circ S)$。其余构造器冲突则失败。变量左右互换在这一分支中一次完成，不另作可来回翻转的循环步骤。[3]

删除、分解和朝向不改变解集。变量消去的关键等式是

从右往左：$\alpha$ 不在 $\tau$ 中，故 $T\tau =\tau$，于是 $R\circ T$ 让两侧都成为 $R\tau$；残余方程也由假设满足。从左往右：若 $Q$ 满足原方程，则 $Q\alpha =Q\tau$，从而 $Q\circ T=Q$；它也满足 $T{E}_{\mathrm{rest}}$，取 $R=Q$ 即可。这证明新约束没有删除任何可进一步实例化的解。

终止时 $E=\varnothing$，恒等替换满足它，所以累积 $S$ 本身统一 $E_0$；不变量还说明所有其他统一子都在 $S$ 后继续替换，故 $S$ 是 MGU。遇到不同构造器时，替换无法改变外层符号，解集为空。若 $\alpha$ 真出现在 $\tau \ne \alpha$ 内，任何有限解都会让 $Q\alpha$ 成为 $Q\tau$ 的真子树，二者不可能相同；这证明 occurs-check 拒绝可靠。应先删 $\alpha =\alpha$，不能把这条恒等式误判成递归类型。

算法终止也有单独度量：先比较残余方程中不同变量的个数，再比较全部类型树节点数。消去变量严格减少第一项，即使替换展开使第二项增加也无妨；删除和构造器分解在第一项不减时严格减少第二项。两项均为自然数，按字典序不可能无限下降。W 的递归调用又只处理原表达式的真子式，每次统一终止，故整个推断过程终止。

两种失败：循环类型与共享约束 ​

对 λx. x x，$x$ 只有一个单态类型 $\alpha$。应用要求 $\alpha =\alpha \to \beta$，occurs check 可靠失败。循环类型图可能表示 rational tree，但那已改变本页有限 HM 类型的对象，不能用它偷偷接受该项。

再看

λf. let g = f in (g 0, g true)

f 的 $\alpha$ 已自由出现于环境，所以 g 不能得到 $\mathrm{\forall }\alpha .\alpha$，只能保持同一个单态 $\alpha$。第一次应用把它统一为 $\mathsf{Int}\to \beta$；第二次应用要求该同一函数接受 Bool，分解得到 $\mathsf{Int}=\mathsf{Bool}$，因此失败。let 不会仅因换了一个变量名就创造多态。

W 把类型方案理路类型方案Type scheme · Polytype通过显式量化类型变量表示一族单态类型的多态对象。、一阶统一理路一阶统一First-order unification · Syntactic unification寻找使若干一阶项在替换后相等的最一般替换。和HM 推断理路Hindley–Milner 类型推断Hindley–Milner type inference · HM type system为带 let 的秩一参数多态 λ 演算提供主类型性质与可判定类型推断的系统。组合成可实现算法。编译器可据此补全省略的类型、生成错误信息，并在中间表示中插入显式类型信息。

实际实现常用约束生成与求解分离、union–find、等级或区域标记来高效实现泛化；但这些优化必须保持 W 的主类型语义。

成功判断的证明按项结构归纳：变量取方案实例；常量直接定型；λ 用更新后的参数类型；应用对两个归纳结果施加后续替换，再由统一等式接上函数消去；二元组逐分量组合。let 则先在更新环境中泛化不属于环境的变量，再检查其作用域。最一般性还需在这项归纳中同时维护环境因子分解及新鲜实例化义务；MGU不变量解释统一步骤为何不作多余承诺，完整HM主类型定理见文献。[1] 不能只证明统一器输出一个解，就把let的泛化正确性当作已经证明。