Free theorem

形式陈述 ​

free theorem 不是检查函数体后发现的偶然性质，而是把多态类型代入关系参数性公理库关系参数性Relational parametricity · Reynolds parametricity · Abstraction theorem多态项必须统一保持类型之间任意关系的抽象定理及其行为约束。所得的行为定理。推导通常包含四步：把类型翻译成关系命题；为类型变量选择能表达目标函数的关系；应用参数性基本结论；最后把关系成员关系化简成程序等式。

以

$$f:\mathrm{\forall }\alpha .\mathsf{List}(\alpha )\to \mathsf{List}(\alpha )$$

为例。给定函数公理库函数Function · Map · Mapping由定义域、陪域和单值图共同组成，并把每个输入送到唯一输出的映射。 $g:A\to B$，选择它的图关系

$$R_g=\{(a,g(a))\mid a\in A\}\subseteq A\times B.$$

列表把关系逐元素提升；于是

$$(xs,ys)\in \mathsf{List}(R_g)⟺ys=\mathsf{map}gxs.$$

参数性说明 $f[A]$ 与 $f[B]$ 保持 $\mathsf{List}(R_g)$。把相关输入取为 $xs$ 与 $\mathsf{map}gxs$，可得

$$\mathsf{map}g(f[A]xs)=f[B](\mathsf{map}gxs).$$

因此带完整类型实例的自然性等式是

$$\mathsf{map}g\circ f[A]=f[B]\circ \mathsf{map}g.$$

复合次序来自图关系的方向，不能左右互换；省略 $[A],[B]$ 只是一种排版简写。等号表示在已指定纯、总求值语义下的观察等价或外延相等，不要求两个程序拥有相同语法、机器步骤或内存表示。

对 $h:\mathrm{\forall }\alpha .\alpha \to \alpha$，任取 $a:A$，用从单位值到 $a$ 的单点图关系实例化参数性。单位侧的总函数只能返回单位值，关系保持遂迫使 $h[A](a)=a$。由于 $A,a$ 任意，在纯、总、无类型反射的语言中，$h$ 观察等价于多态恒等函数。

直觉 ​

多态签名像一份信息预算。f 能看到列表是空还是非空、能重排或删减结构，却看不到元素究竟是数字、字符串还是对象。若先用 $g$ 改写所有元素再运行 f，与先运行 f 再改写元素应得到相同外部结果，因为 f 没有合法手段对 $g$ 改变的元素表示作出不同选择。

“免费”指结论主要由类型和语言的参数性定理支付，而不是完全没有证明成本。使用者仍要确认语言满足哪一版参数性、关系选择方向正确，并把关系结论推到所需观察等式。

例子与边界 ​

reverse : ∀α.List α→List α 满足

$$\mathsf{map}g(\mathsf{reverse}xs)=\mathsf{reverse}(\mathsf{map}gxs),$$

因为反转只依赖列表结构。元素排序却需要比较元素；在纯 System F 中，它不可能具有毫无限制的 $\mathrm{\forall }\alpha .\mathsf{List}(\alpha )\to \mathsf{List}(\alpha )$ 类型。实际语言会要求 Ord α、比较函数或其他字典参数，这些新增输入允许实现观察元素，原 free theorem 也随之改变。

若语言允许 bottom，类型 $\mathrm{\forall }\alpha .\alpha \to \alpha$ 还可能由永不返回的程序居住；朴素的“只能是恒等函数”便不成立。Haskell 的 seq 能观察求值程度，异常能提前退出，引用与指针相等能观察身份，类型反射和 unsafe cast 更可直接检查或伪造表示。这些语言可能拥有以 admissible relation、近似序、严格性条件或部分等价表达的修正版，而不是完全失去所有参数性推理。

从任意泛型语法不能直接推出 free theorem。重载、类型类字典、运行时类型标签和单态化本身会向程序提供额外可观察输入；必须先证明相应核心语言的参数性，再从准确的关系解释导出结论。

推论与应用 ​

free theorem 可用于验证重构、改写融合与库优化。例如自然性等式允许把某些 map 穿过多态结构变换，减少中间列表；优化正确性仍以观察等价为准，并需遵守语言的严格性和效果顺序。

该方法也能快速排除不可能实现：若需求要求函数检查未知元素的数值，却给出完全无约束的多态类型，类型本身已经暴露接口缺口。此时应补充比较能力或收窄类型，而不是编造一个违反参数性的实现。

参考资料

• Philip Wadler, “Theorems for Free!” FPCA, 1989。
• John C. Reynolds, “Types, Abstraction and Parametric Polymorphism,” in Information Processing 83, 1983。
• Janis Voigtländer, “Free Theorems Simply, via Dinaturality,” 2009，refinements and derivation techniques for free theorems。