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为真，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, b)来表示符号串$A\wedge 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
   

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

   empty x = case x of { }
   

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

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

否定

逻辑中的 ¬ 操作将定理转换为非定理，反之亦然：如果 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 演算文章中所述，当试图确定标识符的自由出现的概念时，困难就出现了。组合子演算是由美国数学家哈斯凯尔·卡里（以他命名的某种编程语言）发明的，就是因为这些困难。组合子演算有许多变体，但我们这里考虑最简单的变体之一。我们从两个所谓的组合子开始

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

你应该将第一个函数识别为const。第二个更复杂，它是((->) e)幺半群中的单子函数ap（本质上是 Reader）。这两个组合子构成了整个 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 。