Haskell/Curry-Howard 同构

Curry-Howard 同构 是一个惊人的关系，它连接了两个看似无关的数学领域——类型论和结构逻辑。

简介

Curry-Howard 同构，以下简称为 CH，告诉我们为了证明任何数学定理，我们只需要构造一个反映该定理本质的特定类型，然后找到一个具有该类型的值。这在一开始听起来非常奇怪：类型与定理有什么关系？然而，正如我们将看到的，这两者之间有着密切的关系。在我们开始之前，需要简单说明一点：在这些介绍性段落中，我们忽略了像 error 和 undefined 这样的表达式的存在，它们的语义学 是 ⊥。它们起着极其重要的作用，但我们将适时单独考虑它们。我们还忽略了像 unsafeCoerce# 这样的绕过类型系统的函数。

我们可以使用 Haskell 的 高阶函数 功能构建极其复杂的类型。我们可能想问这样一个问题：给定一个任意类型，在什么条件下存在一个具有该类型的值（我们说该类型是可居住的）？第一个猜测可能是“一直存在”，但这很快就会在例子中被打破。例如，不存在类型为 a -> b 的函数，因为我们没有办法将类型为 a 的东西转换成完全不同的类型 b 的东西（除非我们事先知道 a 和 b 是哪些类型，在这种情况下我们谈论的是一个单态函数，例如 ord :: Char -> Int）。

令人难以置信的是，事实证明，一个类型只有在它对应于数学逻辑中的一个真命题时才是可居住的。但这种对应关系的本质是什么？像 a -> b 这样的类型在逻辑的背景下意味着什么？

形式逻辑速成课程

在我们开始探索类型论与形式逻辑之间的关系之前，我们需要了解一些形式逻辑的背景知识。这是一个非常简短的介绍；为了更广泛的了解，我们建议你参考有关该主题的入门教科书。

在日常语言中，我们使用了很多“如果...那么...”句子。例如，“如果今天天气好，那么我们就去镇上散步”。这些类型的陈述在数学中也经常出现；我们可以说像“如果x为正，那么它就有（实数）平方根”这样的事情。形式逻辑是一种表示语句的方法，这些语句用布尔逻辑来近似英语含义，我们可以对其进行计算。我们使用符号 A→B（读作“A 蕴涵 B”）表示只要 A 为真，B 就为真。例如，我们之前的陈述可以重新表述为“x 为正 → x 具有实数平方根”，这意味着该数字的正性意味着存在所需类型的根。我们通常使用字母来代表整个语句，因此例如如果W是“天气很好”的语句，而T是“我们将去镇上散步”的语句，那么我们就可以说W→T。

我们对 P→Q 的定义存在一些缺陷。如果Q是某些总是为真的语句，无论是什么情况——比如“太阳很热”——那么P是什么并不重要。P甚至可以是错误的语句，如果P为真，Q仍然为真，因此蕴涵P→Q不被认为是错误的。当P为假且Q为真时，P→Q被定义为真。因此，→ 并不真正代表任何因果关系；像“天空是粉红色的 → 太阳很热”这样的语句被定义为真。除了布尔逻辑之外，还有其他逻辑代数试图解决这些“问题”，我们也可以在 Haskell 中构建它们。

在日常语言和数学中经常出现的其他事物被称为合取和析取。前者代表包含“和”的语句，后者代表包含“或”的语句。我们可以用符号 $(M\wedge S)\to B$ 来表示语句“如果这本杂志有货，而且我有足够的钱，我就买它”，其中M = “我有足够的钱”，S = “杂志有货”，B = “我会买这本杂志”。本质上，可以将符号 $\wedge$ 简单地读作“和”。类似地，可以将符号 $\vee$ 读作“或”，因此语句“我会步行或乘火车去上班，或者两者都做”可以表示为 $W\vee T$，其中W = “我会步行去上班”，而T = “我会乘火车去上班”。

使用这些符号，以及我们在过程中会介绍的几个其他符号，我们可以生成任意复杂的符号串。这些符号串有两类：表示真语句的符号串，通常称为定理；以及表示假语句的符号串，称为非定理。请注意，符号串是定理还是非定理取决于字母代表的内容，因此 $P\vee Q$ 如果P代表语句“现在是白天”而Q代表语句“现在是晚上”（忽略像黄昏这样的例外情况）就是一个定理，但如果P是“树是蓝色的”而Q是“所有鸟都能飞”，那它就是一个非定理。如果我们不知道符号串是定理还是非定理，我们通常将其称为命题。

逻辑学还有很多微妙之处（包括当我们说“如果你吃晚饭，你就能得到甜点”时，实际上意味着“只有如果你吃晚饭，你才能得到甜点”）。如果这个主题让你感兴趣，市面上有很多教科书全面地涵盖了这个主题。

命题是类型

因此，给定一个类型 a -> b，在符号逻辑中它意味着什么？方便地，它只是意味着 a → b。当然，只有当 a 和 b 是可以进一步解释为符号逻辑的类型时，这才有意义。这就是 CH 的本质。此外，正如我们之前提到的，a → b 是一个定理，当且仅当 a -> b 是一个可居住类型。

让我们用最简单的 Haskell 函数之一来举例说明。const 的类型是 a -> b -> a。翻译成逻辑，我们得到 a → b → a。这必然是一个定理，因为类型 a -> b -> a 被值 const 所居住。现在，另一种表达 a → b 的方式是“如果我们假设 a 为真，那么 b 必须为真”。因此，a → b → a 意味着如果我们假设 a 为真，那么如果我们进一步假设 b 为真，那么我们可以得出结论 a。这当然是一个定理；我们假设了 a，因此 a 在我们的假设下为真。

⊥ 的问题

我们已经提到，如果一个类型被居住，那么它对应于一个定理。然而，在 Haskell 中，每个类型都由值 undefined 所居住。实际上，更普遍地，任何具有类型 forall a. a 的值，其语义为 ⊥，都是一个问题。⊥ 在类型论中对应于逻辑中的不一致性；我们可以使用 Haskell 类型证明任何定理，因为每个类型都被居住。因此，Haskell 的类型系统实际上对应于一个不一致的逻辑系统。然而，如果我们使用 Haskell 类型系统的一个有限子集，特别是禁止多态类型，那么我们有一个一致的逻辑系统，我们可以用它来做一些很酷的事情。此后，假设我们在这个类型系统中工作。

现在我们已经了解了 CH 的基本知识，我们可以开始更深入地了解类型和命题之间的关系。

逻辑运算及其等价物

符号逻辑的本质是一组命题，例如 P 和 Q，以及组合这些命题的不同方式，例如 Q → P 或 $P\vee Q$。这些组合命题的方式可以被认为是对命题的操作。根据 CH，命题对应于类型，因此我们应该有这些命题组合器的 CH 等价物是类型操作，通常称为类型构造器。我们已经看到了一个例子：逻辑中的蕴涵运算符 → 对应于类型构造器 (->)。本节的其余部分将继续探讨其余的命题组合器并解释它们的对应关系。

合取和析取

为了使 $A\wedge B$ 成为一个定理，A 和 B 都必须是定理。因此，$A\wedge B$ 的证明相当于证明 A 和 B。请记住，为了证明命题 A，我们找到类型为 A 的值，其中 A 和 A 是 CH 对应物。因此，在这种情况下，我们希望找到一个包含两个子值的值：第一个子值的类型对应于 A，第二个子值的类型对应于 B。这听起来非常像一个对。实际上，我们将符号串 $A\wedge B$ 表示为 (a, b)，其中 a 对应于 A，b 对应于 B。

析取与合取相反。为了使 $A\vee B$ 成为一个定理，A 或 B 必须是一个定理。同样，我们寻找一个包含类型为 A 的值或类型为 B 的值的值。这就是 Either。Either A B 是对应于命题 $A\vee B$ 的类型。

假

在我们的逻辑系统中，有时需要表示一个假语句。根据定义，一个假语句是无法被证明的语句。因此，我们正在寻找一个不可居住的类型。虽然这些类型中没有一个存在于默认库中（不要与 () 类型混淆，该类型恰好有一个值），但我们可以定义一个（或者对于不支持 Haskell2010 的旧版本 GHC，我们打开 -XEmptyDataDecls 标记）

data Void

省略构造函数的效果意味着 Void 是一个不可居住的类型。因此，Void 类型对应于我们逻辑中的非定理。这里有一些方便的推论

1. (Void, A) 和 (A, Void) 都是对于任何类型 A 的空类型，对应于 $F\wedge A$ 和 $A\wedge F$ 都是非定理，如果 F 是一个非定理。
2. Either Void A 和 Either A Void 本质上与 A 相同，对于任何类型 A， 对应于 $F\vee A$ 和 $A\vee F$，其中 F 是一个非定理，只有当 A 是一个定理时才成立。
3. 任何对应于非定理的类型都可以替换为 Void。这是因为任何非定理类型必须是空类型，所以用 Void 替换它不会改变任何内容。Void 实际上等价于任何非定理类型。

4. 正如我们在第一部分中提到的，蕴含 P → Q 为真，如果 Q 为真，无论 P 的真值如何。所以我们应该能够找到一个具有类型 Void -> a 的项。事实上确实存在，但解释起来有点复杂：答案是空函数。我们可以将函数 f :: A -> B 定义为（可能无限的）一对的集合，其第一元素是 A（定义域）的元素，第二元素是 f 对该项的输出，B（值域）的元素。例如，自然数的后继函数表示为 {(0,1), (1,2), (2,3), ...}。请注意，为了成为一个（完全定义的）函数，我们必须为每个类型为 A 的项 a 精确地包含一对 (a, f a)。

   空函数，我们称之为 empty，用空集表示。但由于我们必须为定义域中的每个元素都有一对，而我们的表示中没有一对，因此定义域类型必须为空，即 Void。值域类型呢？empty 永远不会产生任何输出，因此对值域类型没有任何限制。因此，假设值域类型具有任何类型是有效的，所以我们可以说 empty :: forall a. Void -> a。不幸的是，在 Haskell 中无法写出这个函数；理想情况下我们想要写出类似的东西

   empty :: Void -> a
   

   到这里就停止了，但这在 Haskell 中是违法的。我们能做到的最接近的是以下内容

   empty :: Void -> a
   empty _ = undefined
   

   或者

   empty :: Void -> a
   empty = empty
   

   另一种合理的方法是写（在 GHC 中使用 EmptyCase 扩展有效）

   empty x = case x of { }
   

   case 语句完全形成，因为它处理了 x 的所有可能值。

   请注意，这完全安全，因为这个函数的右侧永远不会被访问到（因为我们没有东西传递给它）。因此，所有这些的结论是 Void -> a 是一个可居住类型，就像 P → Q 在 P 为假时为真一样。

否定

逻辑中的 ¬ 操作将定理转换为非定理，反之亦然：如果 A 是一个定理，那么 ¬A 是一个非定理；如果 A 是一个非定理，那么 ¬A 是一个定理。我们如何在 Haskell 中表示它？答案很狡猾。我们定义一个类型别名

type Not a = a -> Void

所以对于一个类型 A，Not A 就是 A -> Void。这是如何运作的？嗯，如果 A 是一个定理类型，那么 A -> Void 必须是不可居住的：任何函数都无法返回任何值，因为返回值类型 Void 没有值（函数必须为 A 的所有居民提供值）！另一方面，如果 A 是一个非定理，那么 A 可以用 Void 替换，正如我们在上一节中探讨的那样。然后函数 id :: Void -> Void 是 Not A 的居民，所以 Not A 是一个定理，正如所要求的那样（函数不需要提供任何值，因为它的定义域中没有居民。尽管如此，它仍然是一个函数——具有一个空图）。

公理化逻辑和组合子演算

到目前为止，我们只使用了一些 Haskell 类型系统中非常基本的功能。事实上，我们提到的逻辑的大部分功能都可以使用一种非常基本的“编程语言”组合子演算来探索。为了充分理解 CH 如何将这两个数学领域紧密联系在一起，我们需要公理化我们对形式逻辑和编程语言的讨论。

公理化逻辑

我们从关于 → 操作应该如何表现的两个公理开始（从现在开始，我们假设 → 是一个右结合函数，即 A → B → C 表示 A → (B → C))

1. A → B → A
2. (A → B → C) → (A → B) → A → C

第一个公理说，给定任何两个命题 A 和 B，如果我们假设 A 和 B 都成立，那么我们知道 A 为真。第二个公理说，如果 A 蕴含 B 蕴含 C（或等效地，如果 C 在 A 和 B 都为真时为真），并且 A 本身蕴含 B，那么知道 A 为真就足以得出 C 为真的结论。这可能看起来很复杂，但稍微思考一下就会发现它很合乎常理。想象我们有一组各种颜色的盒子，有些有轮子，有些有盖子，所有有轮子的红色盒子也有盖子，所有红色盒子都有轮子。选择一个盒子。令 A = “正在考虑的盒子是红色的”，B = “正在考虑的盒子有轮子”，C = “正在考虑的盒子有盖子”。那么第二定律告诉我们，因为 A → B → C（所有有轮子的红色盒子也有盖子），并且 A → B（所有红色盒子都有轮子），那么如果 A（如果盒子是红色的），那么 C 必须为真（盒子有盖子）。

我们还允许一个推理法则，称为肯定前件

1. 如果 A → B，并且 A，那么 B。

这条法则允许我们从旧定理中创建新定理。这应该相当明显；它本质上是 → 的含义的定义。这个小的基础提供了一个足够简单的逻辑系统，表达能力足以涵盖我们大多数讨论。以下是在我们的系统中对定律 A → A 的示例证明

首先，我们知道两个公理都是定理

• A → B → A
• (A → B → C) → (A → B) → A → C

你会注意到第二个公理的左侧看起来有点像第一个公理。第二个公理保证，如果我们知道 A → B → C，那么我们可以得出结论 (A → B) → A → C。在这种情况下，如果我们令 C 与 A 相同，那么我们就有，如果 A → B → A，那么 (A → B) → A → A。但我们已经知道 A → B → A，那是第一个公理。因此，我们有 (A → B) → A → A 是一个定理。如果我们进一步令 B 为命题 C → A，对于另一个命题 C，那么我们就有，如果 A → C → A，那么 A → A。但同样地，我们知道 A → C → A（它又是第一个公理），所以 A → A，正如我们所期望的。

这个例子演示了，给定一些简单的公理和一个从旧定理生成新定理的简单方法，我们可以推导出更复杂的定理。这可能需要一段时间才能实现——这里我们有几行推理来证明显而易见的语句 *A* → *A* 是一个定理！——但我们最终会实现。这种形式化很有吸引力，因为我们本质上定义了一个非常简单的系统，并且很容易研究该系统的工作原理。

组合子演算

lambda 演算 是一种从非常简单的基础定义简单编程语言的方法。如果您还没有阅读刚刚链接的章节，我们建议您至少阅读关于演算无类型版本的介绍部分。以下是一些复习内容，以防您感觉生疏。lambda 项是以下三种事物之一

• 一个 *值*，*v*。
• 一个 *lambda 抽象* $\lambda x.t$，其中 *t* 是另一个 lambda 项。
• 一个 *应用* $(t_{1}t_{2})$，其中 $t_{1}$ 和 $t_{2}$ 是 lambda 项。

也只有一个约简规则，称为 *beta-约简*

• $((\lambda x.t_{1})t_{2})$ → $t_{1}[x:=t_{2}]$，其中 $t_{1}[x:=t_{2}]$ 表示将 $t_{1}$ 中所有 *x* 的自由出现用 $t_{2}$ 替换。

如 lambda 演算 文章中所述，当试图确定标识符自由出现的概念时，就会遇到困难。组合子演算是由美国数学家 Haskell Curry（以某种编程语言命名）发明的，因为这些困难。组合子演算有许多基本变体，但我们这里只考虑最简单的一种。我们从两个所谓的 **组合子** 开始

• **K** 接受两个值并返回第一个。在 lambda 演算中，$\mathbf {K} =\lambda xy.\ x$.
• **S** 接受一个二元函数、一个一元函数和一个值，并将传递到一元函数中的值和该值应用于二元函数。同样，在 lambda 演算中：$\mathbf {S} =\lambda xyz.\ xz(yz)$.

您应该认识到第一个函数是 const。第二个函数更复杂，它是在 ((->) e) 单子（本质上是 Reader）中的单子函数 ap。这两个组合子构成了整个 lambda 演算的完整基础。每个 lambda 演算程序都可以仅使用这两个函数编写。

直觉主义逻辑与经典逻辑

到目前为止，我们证明的所有结果都是直觉主义逻辑的定理。让我们看看当我们试图证明经典逻辑的基本定理 Not Not A -> A 时会发生什么。回想一下，这转化为 ((A -> Void) -> Void) -> A 。因此，给定一个类型为 (A -> Void) -> Void 的函数，我们需要一个类型为 A 的函数。现在，类型为 (A -> Void) -> Void 的函数的存在恰好是因为类型 A -> Void 是空的，或者换句话说，类型 A 是有人居住的。因此，我们需要一个函数，它接受任何有人居住的类型，并返回该类型的一个元素。虽然在计算机上执行此操作足够简单——我们只需要找到每个类型的“最简单”或“第一个”居民——但无法使用标准的 lambda 演算或组合子技术来执行此操作。因此，我们看到，此结果无法使用这两种技术证明，因此，其基础逻辑是直觉主义逻辑而不是经典逻辑。

相反，考虑一个传统的错误处理函数，它在发生错误时调用 throw，并将计算转移到 catch。throw 函数会取消来自原始函数的任何返回值，因此它的类型为 A -> Void，其中 A 是其参数的类型。然后，catch 函数将 throw 函数作为其参数，并且如果 throw 触发（即返回 Void），它将返回 throw 函数的参数。因此，catch 的类型为 ((A -> Void) -> Void) -> A 。