参数多态

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

多态恒等函数为 $\mathrm{\Lambda }\alpha .\lambda x:\alpha .x$，类型是 $\mathrm{\forall }\alpha .\alpha \to \alpha$；实例化为整数或布尔类型仍使用同一函数体。在纯、总且不带类型反射的语言中，∀A.∀B.(A→B)→List A→List B 型函数不能凭空制造任意 $B$；输出元素只能来自给定函数对输入元素的应用。但这个类型并不强制保持列表长度或次序：总返回空列表、重复结果或逆序输出都可定型。通常的 map 逐项应用函数并保留列表结构，是其具体定义的保证；参数性给出的自然性等式不能代替这项算法规格。

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

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

若通用代码还需未知类型上的专属操作，可以用受约束类型方案理路受约束类型方案Qualified types · Constrained type scheme在多态方案中保留操作所需的谓词条件，以独立的蕴涵和实例解析判断调用是否有证据。保留Eq a等前提，而不是假装所有a都自带比较。字典传递翻译理路类型类的字典传递翻译Type class dictionary passing · Dictionary translation把类型类条件编译为方法记录参数，并区分译后类型正确与不同证据选择的语义一致性。把该前提变成方法记录参数；两份同类型字典可能产生不同结果，因此译后类型正确与隐式证据选择一致是两项不同责任。

关系参数性可证明程序等价，表示独立性理路表示独立性Representation independence · Representation independence theorem以自然数和单位列表计数器为例，逐项证明接口关系，再对纯传值客户端的全部构造归纳，覆盖高阶调用与抽象状态递归。再把相关实现提升为客户端不可区分；在Curry–Howard 对应理路Curry–Howard 对应Curry–Howard correspondence · Propositions as types把命题对应为类型、证明对应为程序、证明化简对应为程序求值。下，全称类型对应二阶全称量化。