关系参数性

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

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

设闭项 $f:\mathrm{\forall }\alpha .\alpha \to \alpha$。为方便推导，可保守地加入只有一个值 $\ast$ 的单位类型 $\mathbf{1}$。任取类型 $A$ 与值 $a:A$，选择关系 $R=\{(\ast ,a)\}$。输入 $(\ast ,a)$ 相关，参数性便要求 $f[\mathbf{1}]\ast$ 与 $f[A]a$ 的返回值也在 $R$ 中。左侧只能返回 $\ast$，而与它相关的右侧值只有 $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 相同。