Church编码、参数化与Yoneda引理

# 丘奇编码、参数性与米田引理 来源：https://blog.wybxc.cc/blog/parametricity/ 我依然记得多年前初次接触函数式编程时的震撼。那一刻我得知，自然数可以仅在语言内部构造出来： `` data Nat = Zero | Succ Nat `` 接着我了解到，所有计算都可以通过函数来表达（Lambda演算），而递归本身可以被编码为令人着迷的Y组合子： `` Y = λf. (λx. f (x x)) (λx. f (x x)) `` 还有丘奇数，每个数都变成一个函数： `` 0 = λs. λz. z 1 = λs. λz. s z 2 = λs. λz. s (s z) `` 丘奇编码将自然数表示为函数；每个数 `n` 接受一个后继函数和一个初始点，然后将后继应用 `n` 次。 但这背后的逻辑是什么？为什么偏偏是这些Lambda项？ 列表也有丘奇编码： `` nil = λc. λn. n cons = λx. λxs. λc. λn. c x (xs c n) `` 模式看似相似，但细节不同。很长一段时间里，我认为事情就是这样：一个聪明的技巧，每遇到新情况就重新发现一次。 经过多年学习，我终于理解了更深层的故事。丘奇编码展现了数据类型、多态性和范畴论之间的深层联系。一旦你看到这些联系，编码的形式就不可避免了，其结果比技巧本身更优雅。 在这篇文章中，我想追溯这些联系。我们将从类型化环境中最简单的数据类型开始，观察一种模式的浮现，然后逐步构建起一系列工具（参数性、代数数据类型、F-代数和米田引理），直到丘奇编码呈现出它是由数学所要求的。 ### System F 为了捕捉丘奇编码背后的模式，我们需要类型。无类型Lambda演算给出了项，但没有词汇来描述这些“项”是什么。这就是简单类型Lambda演算（STLC）出现的原因——每个项都有一个类型。纯STLC中唯一的类型构造子是函数箭头 `A → B`¹。但STLC几乎立刻碰壁。一个丘奇数必须接受“任何”类型作为其载体：关键在于 `2` 无论是用来数苹果还是函数都应该表现相同。STLC无法表达这一点。STLC中的每个函数都有固定的、单态的类型。 ²但STLC几乎立刻碰壁。一个丘奇数必须接受“任何”类型作为其载体：关键在于 `2` 无论是用来数苹果还是函数都应该表现相同。STLC无法表达这一点。STLC中的每个函数都有固定的、单态的类型。 这就是说，有经验的程序员会警觉：我们需要“泛型”。我们需要对类型而言是多态的函数。给予我们这一点的演算是“System F”，即多态Lambda演算。 思路是这样的：在System F中，函数可以将类型作为参数。类型抽象写作 `ΛX.t`，类型应用写作 `f[X]`。System F的类型包括类型变量 `X`、函数类型 `A → B` 和全称量化 `∀X.A`²。如你所见，我们的System F始于一个空宇宙。在STLC中，我们会声明像 `Unit` 和 `Bool` 这样的基类型来起步。但在System F中，有趣的事发生了：我们可以仅用函数和多态性从零开始构造这些类型！我们可以将 `Unit` 和 `Bool` 编码为多态函数，而不需要任何数据类型专用语法。 让我陈述一个原则：一个数据类型可以通过它的消费方式来等价地表示。我暂时无法解释这个说法背后的逻辑，但让我们先把它放在一边，看看它对 `Unit` 是如何起作用的³。 如果你持有一个 `Unit` 类型的值，你能用它做什么？消费 `Unit` 值的唯一方式就是忽略它，然后返回某个与它无关的东西。 假设你想写一个通用的消费者：对于任何目标类型 `X`，它将一个 `Unit` 转化为一个 `X`。因为我们不知道 `X` 的任何信息，我们无法凭空捏造出一个 `X` 类型的新值。我们唯一能做的就是返回一个我们已经拥有的 `X`。但我们从哪里获得一个 `X` 呢？我们没有！我们应该将它作为一个参数接收进来。因此，`Unit` 的通用消费者的类型签名是： `∀X. X → X`，读作：“对于任何类型 `X`，给我一个 `X`，我还你一个 `X`。” 这个类型有什么居民？可以轻松想到一个：恒等函数⁴。它接受一个 `X` 并原样返回： `` id = ΛX. λx. x `` 这个函数就是 `Unit` 的丘奇编码。 让我们对 `Bool` 尝试同样的推理。`Bool` 有两个构造子：`True` 和 `False`。 消费一个 `Bool` 需要什么？你需要一个目标类型 `X`，并且需要 `True` 和 `False` 各自的解释：两个 `X` 类型的值。然后，根据实际的 `Bool` 值代表哪个构造子，你返回对应的解释。 作为类型签名： `` ∀X. X → X → X `` 读作：“对于任何类型 `X`，给我两个 `X`，我还你一个 `X`。” 我们可以找到这个类型的两个居民，对应消费 `Bool` 的两种方式： `` true = ΛX. λx. λy. x false = ΛX. λx. λy. y `` 一个选择第一个参数，另一个选择第二个参数。它们恰好对应 `Bool` 的两个值。 观察这两个例子，一种模式浮现出来： 总结一下目前的模式：System F中数据类型的丘奇编码是一个多态函数，其参数与构造子匹配。它是该类型的一个通用消费接口。这个调查对 `Unit` 和 `Bool` 非常完美，因为它们的构造子不携带数据。但是像 `Nat` 这样的类型呢？它的 `Succ` 构造子有一个递归参数。我们会在后续章节讨论如何处理，但在此之前，我们需要理解使这个模式起作用的机制。 ### 参数性 真正令人瞩目的是，对于 `∀X. X → X` 我们只能找到一个实现，即恒等函数。同样，对于 `∀X. X → X → X`，我们只能找到两个实现：`true` 和 `false`。System F的类型系统不允许其他实现。 一旦你接受了这个事实，我们继续。 要理解“为什么”类型系统如此精确地限制居民，我们需要审视System F多态性背后的机制。System F中的多态性是“参数化”的：一个多态函数得到一个类型参数，但它不能检查它。它不能根据“我处理的是 `Int` 还是 `Bool`”来分支。它必须将类型视为黑箱。这个限制恰恰是巨大力量的来源。 John Reynolds 在1983年证明了“参数性定理”（也称“抽象定理”）。这里给出一个紧凑的陈述： > 令 `f: ∀X. τ(X)` 为System F的封闭项，其中 `τ(X)` 是一个类型表达式。对于任意类型 `A, B` 以及任意关系 `R ⊆ A × B`，令 `τ(R) ⊆ τ(A) × τ(B)` 为从 `τ` 的结构递归定义的关系提升。如果 `(a, b) ∈ τ(R)`，则 `(f[A] a, f[B] b) ∈ τ(R)`。 这个表述可能看起来很抽象，但其核心信息很简单：一个多态函数必须“保持”你与类型参数相关联的任意关系。它无法检测它所实例化的具体类型结构。一个推论是，你可以从类型签名本身推导出函数必须满足的方程，而无需参考实现。Philip Wadler 后来称这些为“免费定理”。 让我们从一个你可以亲手验证的特例开始。 **主张**：`∀X. X → X` 只有恒等函数，即任何 `f: ∀X. X → X` 必须满足对所有 `A` 和 `a` 有 `f[A] a = a`。 **证明**：我们来看看参数性对 `f: ∀X. X → X` 说了什么。取两个任意类型 `A` 和 `B`，并在它们之间选择任意关系 `R ⊆ A × B`。定理要求我们将 `R` 提升通过类型表达式 `τ(X) = X → X`。提升是这样工作的：两个函数 `hA: A → A` 和 `hB: B → B` 被 `τ(R)` 关联起来，恰好当它们把 `R` 相关的输入映射到 `R` 相关输出时，即如果 `(x, y) ∈ R`，则 `(hA(x), hB(y)) ∈ R`。直观上说，`hA` 和 `hB` 同步地保持 `R`。 现在，参数性说：因为 `f` 是多态的，它在 `A` 和 `B` 处的实例化必须被这个提升后的关系关联。用符号表示：`(f[A], f[B]) ∈ τ(R)`。展开来说：对任意 `(x, y) ∈ R`，有 `(f[A] x, f[B] y) ∈ R`。 关键步骤来了。固定一个类型 `A` 和一个值 `a: A`。我们的目标是证明 `f[A] a = a`。定义一个非常具体的关系： `R = {(a, a)} ⊆ A × A` 这个关系只将 `a` 与自身配对。取 `B = A`。由于 `(a, a) ∈ R`，参数性条件迫使： `(f[A] a, f[A] a) ∈ R` 但 `R` 恰好只包含一个对：`(a, a)`。因此 `f[A] a` 必须是 `a`。证毕。 注意刚才发生了什么：参数性迫使 `f` 成为恒等函数，即使 `f` 对它被应用的类型一无所知。仅凭类型签名就没有给它其他选择。 类似的论证对 `∀X. X → X → X` 也有效。这个类型的函数接收两个未知类型 `X` 的值，必须返回一个 `X`。由于对 `X` 没有任何可用操作，唯一可能的行为是“总是返回第一个参数”或“总是返回第二个”。这就是 `true` 和 `false`⁵。 现在是关键部分。参数性对一般形式 `f: ∀X. (F X → X) → X` 说了什么？这里 `F` 是任何类型算子；可以把它看作是描述数据类型的结构。我们得到的免费定理是：对于任何 F-代数同态⁶ `h: (A, fA) → (B, fB)`， `h (f[A] fA) = f[B] fB` 这个方程在后文中扮演核心角色，我们将用它证明丘奇编码与其编码的数据类型等价。 ### 代数数据类型与函子 手握参数性工具，我们现在回到主线。回忆一下我们停在哪里：`Unit` 和 `Bool` 揭示了一种模式（丘奇编码是一个多态函数，其参数与构造子匹配），但我们还没有办法处理像 `Nat` 这样的递归类型。为了扩展这个模式，我们需要一种系统性的语言来描述数据类型的结构，使构造子及其参数的构成显式化。这就引入了“代数数据类型”（ADT）。 我们知道元组是“积类型”，而带标签的联合是“和类型”。一个代数数据类型从根本上说就是由这两种运算构建的，即“积的和”。每个构造子是其字段的积；整个类型是构造子之间的和。如果一个构造子不携带数据，那么它就是空积，也就是 `Unit` 类型。 我们可以用一个简单的代数记号来精确表达： - 1（单元类型 `Unit`）：有恰好一个值的类型。它是积的幺元：`1 × A ≅ A`。 - `A + B`（和类型）：一个值要么是 `A` 要么是 `B`，并带有标签。 - `A × B`（积类型）：一个 `A` 和一个 `B` 的对。 在这个记号下： ``` Unit = 1 Bool = 1 + 1 Nat = 1 + Nat ``` 最后一行读作：自然数要么是 `Zero`（`1` 分支，不携带信息），要么是 `Succ`（包装另一个 `Nat`）。这个方程是递归的，我们用 `μ` 绑定器来理解： ``` Nat = μX. 1 + X ``` 同样的方法适用于列表： ``` List(a) = μX. 1 + a × X ``` 这里 `Nil` 是 `1` 分支，`Cons` 是 `a × X` 分支。 但代数不仅限于记号。类型惊人地遵循熟悉的代数定律。例如，分配律： ``` a × (b + c) ≅ a × b + a × c ``` 这里 `≅` 表示类型同构：存在双向见证等价性的函数。 将这条定律读作类型：`(a, Either b c)` 同构于 `Either (a, b) (a, c)`。证据是我们可以编写以下函数： `` f :: (a, Either b c) -> Either (a, b) (a, c) f (a, Left b) = Left (a, b) f (a, Right c) = Right (a, c) g :: Either (a, b) (a, c) -> (a, Either b c) g (Left (a, b)) = (a, Left b) g (Right (a, c)) = (a, Right c) `` 那函数类型呢？我们能将其表示为代数运算吗？ 让我宣布：“函数就是指数。”考虑两个有限类型 `A` 和 `B`，分别有 `|A|` 和 `|B|` 个居民。有多少个函数 `A → B` 存在？对于每个输入 `a ∈ A`，我们可以独立地从 `B` 中选择任意一个输出。那就是 `|B|` 种选择重复 `|A|` 次：`|B|^|A|` 种可能性。这提示我们将函数类型写为指数： ``` A → B ≅ B^A ``` Currying 于是就变成了熟悉的指数定律： ``` C^{A × B} ≅ (C^B)^A ``` 而走出和类型的函数遵循自己的分配律： ``` C^{A + B} ≅ C^A × C^B ``` 现在让我们回到自然数的丘奇编码。我们在无类型 Lambda 演算中见过丘奇数： `` 0 = λs. λz. z 1 = λs. λz. s z 2 = λs. λz. s (s z) `` 我们想给它们在 System F 中赋予类型。假设 `z` 的类型是 `X`。我们期望 `0` 和 `1` 的类型相同，因此 `s z` 应该与 `z` 具有相同的类型。所以 `s` 必须具有类型 `X → X`。这就给出了自然数丘奇编码的类型： ``` ChurchNat = ∀X. X → (X → X) → X ``` 它看起来与 `Unit` 和 `Bool` 的丘奇编码类型有些许不同。第二个参数是一个函数而不是一个值。是否存在一个单一的形式可以涵盖所有这些？ 让我们更仔细地检查编码的内部部分。 Currying 告诉我们，一个函数 `X → (X → X) → X` 等价于一个函数 `(X, X → X) → X`。而我们已经知道元组 `(A, B)` 可以写作 `A × B`，函数类型 `A → B` 可以写作 `B^A`。然后我们可以做一些代数操作： ``` X → (X → X) → X ≅ X × X^X → X ≅ X^{1+X} → X // 因为 X^1 = X, X^(1+X) ≅ X^1 × X^X ≅ ((1+X) → X) → X // 反过来 ``` 因此完整的丘奇编码变成： ``` ChurchNat ≅ ∀X. ((1+X) → X) → X ``` 现在看看表达式 `1+X`。这正是 `Nat = μX. 1+X` 递归类型定义的主体。换句话说，丘奇编码的形式是： ``` ∀X. (F X → X) → X ``` 其中 `F X = 1+X`。这里的 `F` 是一个“函子”，它捕获了数据类型形状的轮廓。让我们验证一下这对我们之前的例子是否成立： - 对于 `Unit`：函子为 `F X = 1`。那么 `(F X → X) → X = (1 → X) → X ≅ X → X`。匹配 `∀X. X → X`。 - 对于 `Bool`：函子为 `F X = 1+1`。那么 `(F X → X) → X = (1+1 → X) → X ≅ (X × X) → X ≅ X → X → X`。匹配 `∀X. X → X → X`。 这里我们得到了一个通用模式：对于代数数据类型 `T = μX. F X`，其丘奇编码为 `∀X. (F X → X) → X`。 在下一节中，我们将看到丘奇编码 `∀X. (F X → X) → X` 是 **F-代数** 通用消费者的类型，正是这个视角，通过参数性和米田引理，将引领我们对丘奇编码的真实含义达成最深刻的理解。 ### F-代数 我们已经来到了一个转折点。上一节以 `∀X. (F X → X) → X` 这个统一了 `Unit`、`Bool` 和 `Nat` 丘奇编码的形式收尾。但这个形式仍然像是凭空而来。为什么偏偏是这个符号排列？为了回答这个问题，我们需要给各个部分命名。这就是范畴论登场的时刻。 我们从小的开始。一个“范畴”是一族对象和它们之间的箭头，并满足组合和恒等的合理规则。对程序员而言，最自然的例子是 `Set` 范畴：对象是类型，箭头是函数，组合是函数组合，恒等箭头是 `id`。 一个“函子” `F` 是范畴之间的映射。在我们的世界中，`F` 将每个类型 `A` 映射到类型 `F A`，将每个函数 `f: A → B` 映射到函数 `F f: F A → F B`，并且保持组合和恒等： ``` F (g ∘ f) = F g ∘ F f F id = id ``` 这正是 `F X = 1+X` 一直以来在做的事：它从一个旧类型构建新类型，“并且”提升函数来作用于该结构内部⁷。 一个“自然变换” `η` 介于两个函子 `F` 和 `G` 之间，是将 `F` 的形状转换为 `G` 的形状的一种方式，且不依赖于具体的值。