形式陈述

参数多态允许一段程序对所有类型参数使用同一实现。典型类型为

$$ \forall\alpha.\,T(\alpha), $$$$\mathrm{\forall }\alpha .T(\alpha ),$$

值通过类型抽象构造，并可在具体类型 $A$$A$ 处实例化为 $T(A)$$T(A)$。其“参数性”要求程序不能依赖未知类型的具体表示；在纯语言中，关系参数性把这一要求形式化，并从类型导出自由定理。它不同于按类型选择实现的特设多态，也不同于由包含关系驱动的子类型多态。

直觉

类型变量是调用者稍后填入的占位符，而程序必须在不知道其具体内容时仍统一工作，所以可做的事情受到强约束。

例子与边界

纯粹、总定义的函数若类型为 $\forall\alpha.\,\alpha\to\alpha$$\mathrm{\forall }\alpha .\alpha \to \alpha$，参数性迫使它等同行为；多态恒等函数可用于整数、布尔值或任意其他类型。带类型反射、异常、非终止或可变引用时，朴素自由定理可能需修正。重载的 + 在整数与浮点数上调用不同实现，不是这种统一参数多态。

推论与应用

参数多态支持通用容器、组合子和抽象接口，并让类型本身提供程序等价性质。它是 System F 和 Hindley–Milner 系统的共同核心，但两者在量词位置和类型推断能力上不同。

参考资料

• Benjamin C. Pierce, Types and Programming Languages, MIT Press, 2002，Ch. 23, universal types and parametricity。
• Robert Harper, Practical Foundations for Programming Languages, 2nd ed., Cambridge University Press, 2016，Chs. 10–11, polymorphism and abstraction。