一个函数只有签名 List[A] => List[A]，能不能据此断定它只会调整元素顺序？不能。它可以丢弃、复制元素，甚至总是返回空表。但如果它对所有类型统一工作、不观察元素内部结构，而且是纯且全的，那么它受到比普通业务函数强得多的限制。这些限制可以转化成测试性质，也可以帮助判断哪些优化允许移动到调用边界之外。

本篇用一个可手算的自然性等式展开参数性，再用 Scala 中的 null、运行时类型检查和效果记录拆开其假设。Scala 的高阶类型与组合定律保留类型类背景，简单类型 λ 演算保留类型判断背景。两篇都不替代这里对工程语言例外的检查。完整系列从导读与能力自测进入。

从“缺少操作”推导约束

考虑 def choose[A](a: A): A。如果没有其他 A 值，没有运行时类型分析，没有不安全转换，没有空值、异常与无限循环，并要求全函数，那么实现只能返回这个输入。它不知道 A 是数字、地址还是支付方式，不能凭空调用加法或创建一个业务值。

删除任一前提都可能扩大实现集合。throw 可以在不给出 A 的情况下满足 Scala 的返回类型；无限递归也一样。未启用 explicit-nulls 的语言环境中，空值相关操作会提供理想参数模型中不存在的观察方式。类型擦除更不等于无法观察任何运行时信息，isInstanceOf[String] 仍可以识别字符串实例。

参数多态是语法和类型系统提供的量化能力；参数性是关于程序如何保持关系的语义性质。这两个词不能互换。Wadler 的作者资料页在Theorems for free!条目中说明了从多态类型导出定理与 Reynolds 抽象定理的联系。应用到 Scala 前，还需要确定被分析的子语言、全性条件与允许的观察。

实验用编译器拒绝一个最直接的越界实现：

1
2
3
import scala.compiletime.testing.typeCheckErrors
val rejected = typeCheckErrors("def invent[A]: A = 42")
assert(rejected.nonEmpty)

这说明普通整数不能冒充任意 A，不说明所有具有该签名的方法都必然纯或者终止。编译失败检查与语义定理承担不同任务：前者封住一个具体类型错误，后者需要描述所有允许的实现和输入。

把关系具体化为一次map

设 t[A]: List[A] => List[A] 是满足上述条件的统一变换，f: A => B 是纯全函数。候选性质为：

1
t(xs).map(f) = t(xs.map(f))

左边先改列表结构，再变换元素；右边先变换元素，再按同一个多态算法改结构。关键是两次调用 t 分别实例化在 A 与 B，但必须遵守相同规则。不能在左边选择整数版业务逻辑，在右边选择字符串版业务逻辑。

用图关系 R={(a,f(a))} 可以看清推导。xs 与 xs.map(f) 按相同位置相关。参数性要求 t 将相关输入带到相关输出，因此输出的长度与对应位置也须匹配 R。这个关系正好表达左侧输出映射后等于右侧输出。它不要求 f 可逆；即使 f 把所有整数都映成同一字符串，该性质仍应成立。

实验选择 reverse，输入 [1,2,3]，令 f(n)="n="+n。两侧都是 ["n=3","n=2","n=1"]。输入为空时两侧仍为空；输入有重复元素时，顺序变化与元素相等不能混为一谈，因此测试还包含重复与负数。四个列表与三个转换函数共检查十二个组合。

reverse 只是一个实例。取前三个、重复每个元素两次、总返回空表也能满足同一等式，所以通过该性质无法证明实现就是反转。实现的业务规格仍需诸如长度、位置以及反转两次复原等额外性质。free theorem 提供的是由类型约束带来的共同规律，不会替代具体需求。

也不应把自然性等同于元素不能被观察的充分条件。某个含特殊逻辑的程序可能在这十二组输入上碰巧通过。有限测试适合找到反例或回归退化；若要证明对所有类型成立，必须给出语义论证或在合适的形式系统中证明。

三个可以直接运行的反例

第一个函数删除 null。取 xs=List(null,"x")，令 f 把 null 转为字符串 "missing"，其他值保持不变。先删除再映射得到 ["x"]；先映射再删除得到 ["missing","x"]。这个变换利用了元素里某种特殊值的可观察性，已不满足统一不透明处理的假设。

反例没有证明“所有带 null 的代码都破坏所有 free theorem”。它只证明这个签名不足以在当前语言模型中自动保证此处自然性。若把领域限制成非空类型，并保证调用边界不注入 null，那么可以重新讨论受限领域上的性质。边界限制必须是可检查的契约，不能只写在注释里。

第二个函数按运行时字符串类型筛选。对整数列表先筛选会得到空表，随后映射仍为空；先把整数转成字符串再筛选，则保留所有元素。代码没有强制类型转换，依然破坏关系保持。这说明“没有 asInstanceOf”不是充分的审查规则；类型反射和模式匹配同样影响假设。

第三个反例保持返回值不变，却改变执行轨迹。令 f 将整数写入一个缓冲区再返回其字符串。对 [1,2]，先 reverse 再 map 的记录为 2,1；先 map 再 reverse 的记录为 1,2。结果列表相等，而效果顺序不同。

这里必须先说清等号观察什么。若只比较最后的不可变列表，两个结果相同；若观察日志、计费请求或状态写入，它们不同。不能先用“只看返回值”完成等式，再将这个等式用于重排带效果代码。相同数值结果既不能证明幂等，也不能证明动作次数和故障时点一致。

1
2
3
4
val trace = scala.collection.mutable.ArrayBuffer.empty[Int]
def observed(n: Int): String =
  trace += n
  n.toString

函数的 Int => String 类型并未显示 trace。把观察到的依赖移入 State、Writer 或 IO 可以使组合规则更明确，但效果类型不会自动恢复原来的纯函数定理。新的函数类型已经不同，应对新结构重新推导。

等式如何帮助工程决策

假定数据管道的 t 只做取固定前缀，f 是昂贵但纯的编码函数。满足自然性时，可以先取前缀再编码，减少对被丢弃元素的计算。若编码可能验证失败，移动顺序会改变是否发现后部非法输入；若它记录审计事件，移动顺序会改变记录数量。这种优化是否合法，取决于是否允许改变这些观察，而不只是输出集合是否相同。

另一个常见误判是把输入类型限制误当作多态性。List[Order] => List[Order] 可以读取订单价格，并按价格筛选；[A] => List[A] => List[A] 在理想参数模型中不能获得这种领域操作。若签名额外传入 A => Boolean，筛选当然成为合法能力，但等式必须同时规定谓词如何沿 f 转换，不能继续套用没有谓词时的原式。

类型类约束同样会提供能力。[A: Ordering] 允许排序；两个实例化类型的 Ordering 未必与 f 保持顺序。因此为通用方法增加一个看似无害的上下文参数，可能使原来的推导失效。评审时需要一起检查显式参数、隐式实例和闭包捕获的环境。

全性也有工程代价。一个函数对十个样本都返回，不能证明对全部输入返回。数组越界、溢出检查、异常与递归都需要额外处理。对于普通项目，常用做法是把定理作为带前提的设计依据，用性质测试覆盖重要输入，再明确记录未证明的范围，而不是给接口贴上“参数化”标签就放弃测试。

非单射转换能排除哪些实现

自然性里的 f 不必一一对应，这让性质比“换一种显示格式”更强。取两个不同整数，把它们都映射成同一个字符串。假设 t 会根据元素相等性去重：先对整数去重可能保留两个元素，再映射得到两个相同字符串；先映射再去重却只剩一个。这样的 t 即使没有业务专用字段，也利用了理想参数模型没有提供的元素比较能力。

由此可以看出，列表长度是一种允许观察的结构信息，元素的任意相等比较却不一定允许。一个函数可以根据列表长度决定保留前半部分；它对元素类型仍一视同仁。另一个函数虽然只调用通用 equals，也可能区分映射前后的元素关系。检查“有没有访问字段”不足以代替检查“有哪些观察能力”。

把输入进一步改成 List[(A,Int)]，情况又不同。函数可以依据明确提供的整数标签筛选，因为标签不在抽象类型 A 内部。此时需要推导的是只映射 A 分量、保持标签不变的性质。如果连标签也一起改变，原有关系就不是同一个关系。类型中的哪一部分被量化，是每次推导都要准确写出的起点。

对多参数函数，也要同时考虑每个参数。例如 pick[A](left:A,right:A):A 在纯全且不观察 A 的模型中只能选择已有参数，但选择哪一个可以受额外 Boolean 参数控制。若没有 Boolean，签名仍不区分总选左与总选右。类型限制实现空间，却未必唯一确定实现；把这种限制讲成“看类型就能知道所有代码”会误导接口使用者。

free theorem 还不能替代安全策略。即使编码器对所有元素统一处理，也可能把敏感字段全部序列化出去；即使组合保持自然性，也可能有高复杂度或过多内存分配。这些问题属于具体数据和资源规格。代数性质适合约束组合与重排，不会从任意泛型参数自动推导隐私、权限或性能结论。

实际评审可先写一个条件句：在有效非空值、无类型分析、纯全变换且仅观察返回列表的前提下，允许把该映射移过该结构变换。随后逐项对照实现。发现日志或异常时，应重新选择观察范围或者禁止该次优化；不能在说明里保留理想假设，却在代码中继续利用已经排除的能力。

实验记录与验收题

运行 node examples/functional-programming/run.mjs E02。Scala 3.3.7 实际执行输出：

1
2
naturality=12; null-counterexample=true; runtime-type-counterexample=true
effect-traces=2,1/1,2; invalid-invent=rejected

Main.scala包含全部输入与正反断言；result.json保存命令、退出码与源文件哈希。反例断言期待两侧不等，因此它们成功不是实验失败，而是对假设失效的明确验证。

手算题：t 取列表前两个元素，f 把整数取绝对值，输入 [-2,1,3]，两侧为什么都得到 [2,1]？如果 t 改成删除负数，该签名还具有原先要求的全称类型吗？答案是它已经使用整数特有能力，不能装作同一个任意 A 上的变换。

修改题：给实验增加“每个元素复制两次”的 t，沿用三个 f 和四组输入验证自然性，再增加独立的长度翻倍断言。然后将 f 改成每调用一次就增加计数，比较 take(2) 的两种计算顺序。验收必须同时报告输出值与计数，解释为何原先的纯等式不再足以批准重排。