形式陈述

Algorithm W 对表达式结构递归，返回类型替换 $S$ 与推断类型 $\tau$。 变量使用时实例化环境中的类型方案；应用 $e_1{e}_2$ 时分别推断函数与实参，并统一函数类型与 ${\tau }_2\to \alpha$；let x=e_1 in e_2 在应用替换后的环境中泛化 $e_1$ 的类型，再推断 $e_2$。 在标准纯 Hindley–Milner 语言中，算法可靠且完备，并产生主类型。

直觉

语法递归产生等式约束，统一持续求解并把结果回写环境；泛化只发生在具有共享语义的 let 边界。

例子与边界

$\lambda f.\lambda x.fx$ 推得 $(\alpha \to \beta )\to \alpha \to \beta$。加入可变引用、子类型、高阶多态或类型类后，原始 W 的结论和实现都需要扩展或限制。

推论与应用

它解释 ML 系语言无需类型标注仍能得到最一般静态类型的原因。

参考资料

• Robin Milner, A Theory of Type Polymorphism in Programming (1978), algorithm W.
• Luis Damas, Robin Milner, Principal Type-Schemes for Functional Programs (1982), principal type schemes.