形式陈述

Hindley–Milner 系统中的类型方案通常写作

$$\mathrm{\forall }{\alpha }_1\cdots {\alpha }_k.\tau .$$

实例化把量化变量替换为新鲜类型变量；泛化在 let 绑定处量化类型中不自由出现于环境的变量。 环境保存变量到类型方案的映射，而 λ 绑定参数通常仍获得单态类型。

直觉

类型方案不是运行时携带的万能值，而是允许每次使用绑定变量时选择一个一致的单态实例。

例子与边界

恒等函数可有方案 $\mathrm{\forall }\alpha .\alpha \to \alpha$，一次使用于整数、另一次使用于布尔值。若错误地泛化环境中受约束变量，会产生不可靠类型。

推论与应用

它区分 let 多态与 λ 参数多态，并是主类型方案和 Algorithm W 的直接前置。

参考资料

• Benjamin C. Pierce, Types and Programming Languages (2002), let-polymorphism and type schemes.
• Robin Milner, A Theory of Type Polymorphism in Programming (1978), type polymorphism.