关系参数性

形式陈述 ​

在纯、总的 System F公理库System FSystem F · Polymorphic lambda calculus具有显式类型抽象与类型应用的二阶多态 λ 演算。 中，关系环境 $\eta$ 为每个类型变量 $\alpha$ 指定两个闭类型 $A_1,A_2$ 及其值之间的关系 $R_{\alpha }$。这是一种按类型递归的二元逻辑关系公理库逻辑关系Logical relation · Logical predicate · Reducibility relation按类型结构定义值与计算之间的关系，用于把局部类型规则提升为终止、等价或参数性结论。。变量和箭头分支为

$$\begin{array}{rl}\mathcal{V}[[\alpha {]]}_{\eta }& =R_{\alpha },\\ \mathcal{V}[[A\to B{]]}_{\eta }& =\{(f_1,f_2)\mid \mathrm{\forall }(a_1,a_2)\in \mathcal{V}[[A{]]}_{\eta },\\ & (f_1{a}_1,f_2{a}_2)\in \mathcal{E}[[B{]]}_{\eta }\}.\end{array}$$

全称类型要求保持每一种可选关系：

$$\begin{array}{rl}(v_1,v_2)\in \mathcal{V}[[\mathrm{\forall }\alpha .A{]]}_{\eta }\text{当且仅当}& \mathrm{\forall }{B}_1,B_2,R\subseteq \mathsf{Val}(B_1)\times \mathsf{Val}(B_2),\\ & (v_1[B_1],v_2[B_2])\in \mathcal{E}[[A{]]}_{\eta [\alpha \mapsto (B_1,B_2,R)]}.\end{array}$$

关系参数性或 abstraction theorem 是逻辑关系基本定理公理库逻辑关系基本定理Fundamental theorem of logical relations · Fundamental lemma良类型项在点对点相关的环境替换下产生逻辑相关结果的核心引理。在这套解释上的实例：若 $\mathrm{\Gamma }⊢e:A$，则对相关的类型实例化和项环境，两份实例化后的 $e$ 在 $\mathcal{E}[[A]]$ 下相关。闭合多态项因此与自身跨任意类型关系相关。这里的“自身”仍包含左右两侧不同的类型实例，不是逐字复制后得到的平凡等式。

参数多态公理库参数多态Parametric polymorphism程序对类型参数统一工作而不依赖其具体表示的多态。是一种类型系统能力；关系参数性是关于该语言全部良类型项的元定理。重载或 ad-hoc polymorphism 可以按类型选择不同实现，不满足上述“任意关系都保持”的前提，不能只因语法里有泛型参数就套用本定理。

直觉 ​

一个对未知 $\alpha$ 工作的程序没有类型专属的观察手段。若输入元素在某个任意关系下配对，它只能通过类型允许的统一结构搬运、丢弃或组合这些元素，不能突然识别“左边是整数、右边是字符串”。把“不了解表示”精确化为“保持所有关系”，便从类型签名得到强行为约束。

关系环境比只比较相同类型更有力。它可以把编码不同、值集合不同的两个类型联系起来；多态程序若仍保持该关系，就说明其行为不依赖任何一侧的具体表示。

例子与边界 ​

设 $f:\mathrm{\forall }\alpha .\alpha \to \alpha$。任取类型 $A$ 与值 $a:A$，再选择只把某个辅助值与 $a$ 配对的关系；参数性迫使 $f[A]a$ 仍与该辅助值对应，因此在纯、总、无类型反射的语义中，$f$ 只能观察等价于恒等函数的行为。这个结论依赖总性：若允许发散，f 还可能永不返回。

对 $g:\mathrm{\forall }\alpha .\mathsf{List}(\alpha )\to \mathbb{N}$，逐元素关系会把形状相同的两条列表配对，而完全不限制相关元素的具体表示。参数性于是要求 $g$ 对这两条列表返回同一自然数；它可以依赖空/非空、长度等列表形状，却不能检查元素是零、字符串还是某个对象身份。

底值、异常、引用、指针相等、类型反射、不安全转换以及 Haskell 风格 seq 都会改变可观察行为或允许程序探查本应抽象的信息。相应语言可能仍有经过 admissibility、world、step index 或部分性修正的参数性定理，但不能无条件沿用经典 Reynolds 版本。

推论与应用 ​

关系参数性支撑表示隐藏、程序等式和从多态类型导出的自然性条件。所谓 free theorem 是进一步选择特定关系并把关系结论化为程序等式的应用；推导时仍要写明总性、纯度和观察等价，不能把“代码复用”当成形式证明。

编译器若做类型擦除或多态优化，也可用参数性说明程序不能观察被擦除的类型信息。不过当源语言暴露运行时类型表示或字典参数时，证明必须把这些额外值纳入关系，而不是假定所有泛型语言都与纯 System F 相同。

参考资料

• John C. Reynolds, “Types, Abstraction and Parametric Polymorphism,” in Information Processing 83, 1983。
• Philip Wadler, “Theorems for Free!” FPCA, 1989。
• Robert Harper, Practical Foundations for Programming Languages, 2nd ed., Cambridge University Press, 2016，parametricity and abstraction。