参数多态

参数多态把类型当作接口占位符：程序知道某些值类型相同，却不知道它们究竟是整数、字符串还是树。正因为缺少类型专有操作，代码被迫保持统一行为；一个纯函数若类型是 $\mathrm{\forall }\alpha .\alpha \to \alpha$，除了返回输入外几乎没有别的总行为。它不同于重载：重载可为不同类型选择不同实现；也不同于子类型公理库子类型Subtyping允许某类型值在期望其上界类型的位置使用的可替代关系。多态，后者依赖类型层次中的替代关系。类型限制为何能推出这些行为结论，由关系参数性及其具体实例负责证明。

多态恒等函数为 $\mathrm{\Lambda }\alpha .\lambda x:\alpha .x$，类型是 $\mathrm{\forall }\alpha .\alpha \to \alpha$；实例化为整数或布尔类型仍使用同一函数体。多态映射 map : ∀A.∀B.(A→B)→List A→List B 不能凭空制造 $B$，只能把给定函数应用到列表元素并保留结构。

边界是 printType : ∀A.A→String 一类能反射类型参数的原语：它可按 $A$ 分支，不再满足纯 System F 的经典关系解释。不安全强制转换、指针相等、非终止和效果也会改变可推出的等式；这不影响“程序可对类型抽象”的基础定义，却要求使用相应语言版本的参数性定理。

参数多态是泛型库、集合算法和类型安全复用的基础。System F公理库System FSystem F · Polymorphic lambda calculus具有显式类型抽象与类型应用的二阶多态 λ 演算。提供显式的高阶多态核心，Hindley–Milner 则以秩一类型方案公理库类型方案Type scheme · Polytype通过显式量化类型变量表示一族单态类型的多态对象。和 let 泛化提供可推断的隐式版本。

关系参数性可证明程序等价，表示独立性公理库表示独立性Representation independence · Representation independence theorem两个实现若由保持接口操作的表示关系连接，则任何只依赖接口的良类型客户端都无法区分它们。再把相关实现提升为客户端不可区分；在Curry–Howard 对应公理库Curry–Howard 对应Curry–Howard correspondence · Propositions as types把命题对应为类型、证明对应为程序、证明化简对应为程序求值。下，全称类型对应二阶全称量化。