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 也不推断任意高秩或多态递归类型；给它加入语言特性后，主类型和完备性可能不再成立。

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

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