范畴论图解：类型
Category Theory Illustrated - Types
在范畴论语境下，“类型”不仅是编程中的基础构件，更指向一种深刻的数学基础理论。本文从习以为常的“集合”概念切入，揭示了这种直观思维潜藏的深层危机——罗素悖论。当试图定义“所有不包含自身的集合”时，朴素集合论便陷入了无法自洽的逻辑死循环。面对这一困境，数学界分化出两条路径：其一是以ZFC集合论为代表，通过增添诸多限制性公理来“打补丁”，代价是牺牲了集合论原本引以为傲的简单性；其二则是罗素本人的选择，即完全抛弃集合，另起炉灶构建一种在底层设计上就天然免疫悖论的全新体系——类型理论。本文以清晰的逻辑脉络，引导读者跳出“以集合为中心”的思维定势，一窥类型理论作为替代性数学基础语言的严谨与优雅。
类型
在本章中我们将讨论类型。如果你期望学习尽可能多的 新 范畴（在你甚至都未怀疑它们真的是范畴，直到意外揭晓之前），这可能会让你感到失望——从第一章起，我们就一直在讨论给定编程语言中的类型范畴（category of types），而且我们已经知道它们是如何形成一个范畴的。然而，类型不仅仅关乎编程语言。它们也不仅仅是另一个范畴。它们还处于一个被称为 类型理论（type theory） 的数学理论的核心。
作为数学的基础语言，类型理论是集合论（set theory）以及范畴论本身的替代方案，并且它和那些形式化体系中的任何一个一样，都是强大的工具。
集合、类型与罗素悖论
我们又开始了谈论集合。大多数关于范畴论（以及一般数学）的书都以集合开头，并且经常回到集合。即使在一本像这样关于范畴论的书中，大多数数学对象的标准定义也涉及集合。确实，在听到幺半群（monoids）是单对象范畴的定义时，一个只懂集合的人可能会说：
“忘掉那个吧！你见过集合吗？这是同一回事，只不过你还有这个二元运算。”
或者对于作为单态射范畴的 序（orders）：
“你见过集合吗？这是同一回事，只不过某些元素比其他元素大。”
这种 “以集合为中心” 的观点普遍存在的原因其实很简单：集合很容易理解，特别是当我们在入门材料惯有的概念层面上进行操作时。
例如，我们都会把给定活动所需的一组用品归拢在一起（例如，数学课上的 量角器、圆规 和 铅笔，或者画画时的 纸、颜料罐 和 画笔），以免忘记其中的某一些。或者我们将经常一起闲逛的人归为这个或那个群体。因此，当我们在几样东西周围画一个圈时，每个人都知道我们在谈论什么。
然而，这种对集合的初步理解有些 过于简单 了（或者如数学家所称的，朴素（naive）），因为当仔细审视它时，它会导致一堆不易解决的悖论，其中最著名的就是罗素悖论。
罗素悖论
罗素悖论本身就很有趣，除此之外，它也是创建类型理论的动机之一，因此我们将通过理解它是如何以及为何发生的来开始本章。
我们见过的大多数集合（如空集和单元素集合）都不包含 它们自己。
然而，由于集合的元素本身也是集合，一个集合可以包含它自己。
这种能力是罗素悖论的根本原因。
当我们试图将 所有不包含自身的集合的集合 可视化时，这个悖论就出现了。在最初的集合记法中，它可以被定义为这样一个集合：它包含所有满足 $x$ 不是 $x$ 的成员（即 $x \mid x \notin x$）的集合 $x$。
然而，这幅图有些问题——如果我们看看定义，我们会发现我们刚刚定义的这个集合 也不包含它自己，因此它也属于那里。
嗯，这里也有点不对劲——因为我们所做的新的调整，我们的集合现在 包含了它自己。
而移除这个集合，使其不再是自身的元素，只会把我们带回到起点，所以我们无路可走——这就是罗素悖论。
用集合解决悖论
不包含自身的集合的集合听起来不像是一个非常有用的集合。而且它确实不是——事实上，除了构建罗素悖论之外，我没见过它因为任何其他原因被提及。因此，大多数人在了解罗素悖论时的最初反应会是这样的：
“等等，难道我们不能直接加一些规则，说你不能画出不包含自身的集合的集合吗？”
这正是数学家 Ernst Zermelo 和 Abraham Fraenkel 着手做的事情（无意双关）。他们添加的额外规则导致了集合论的一个新定义，被称为 Zermelo–Fraenkel 集合论（Zermelo–Fraenkel set theory），或 ZFC（末尾的 C 是另外的故事），这是一个没有悖论的集合论版本。ZFC 取得了成功，并且至今仍在使用，然而它妥协了集合所拥有的最好的特性之一，即它们的 简单性。
我们这是什么意思？嗯，集合论的最初表述（如今被称为朴素集合论（naive set theory））仅仅基于一条（相当模糊的）规则/公理：“给定一个性质 P，存在一个集合，包含所有具有该性质的对象”，即任何一堆对象都可以形成一个集合。
相比之下，ZFC 由数量更多（且更具限制性）的公理来定义，例如，配对公理（axiom of pairing），它指出给定任何两个集合，存在一个包含它们作为元素的集合。
……或者并集公理（the axiom of union），它指出如果你有两个集合，你也就有了一个包含它们所有元素的集合。
总共有大约 8 条这样的公理（取决于理论的流派）。它们以一种允许我们构建所有有趣的集合，同时又无法构建那个臭名昭著的包含自身的集合的方式被策划出来。然而，接受 ZFC 将意味着接受集合论并不像它看起来那样简单直接。
确实，它比范畴论更复杂，也比我们稍后将要学习的另一种理论更复杂……
用类型解决悖论
当 Zermelo 致力于完善集合论的公理以避免罗素悖论时，Russell 本人采取了一条不同的路线来解决他的悖论，并决定完全抛弃集合，开发一个在 设计上 就没有悖论的全新数学概念——一个你不需要用额外的公理来打补丁以避免出现不合逻辑的构造的概念。因此，在 1908 年，即 Zermelo 发布 ZFC 第一个版本的同年，Russell 提出了他的 类型理论（theory of types）。
类型理论与集合论完全不相似，但同时，它与集合论也并非完全不同，因为 类型（types） 和 项（terms） 的概念明显让人联想到 集合 和 元素 的概念。
| 理论 | 集合论 | 类型理论 |
|---|---|---|
| 元素 | 项 | |
| 属于一个 | 集合 | 类型 |
| 记法 | $a \in A$ | $a : A$ |
当涉及 结构 时，两者之间最大的区别在于项绑定到了它们的类型上。
因此，虽然在集合论中，一个元素可以是许多集合的成员
在类型理论中，一个项只能拥有一个类型。（注意小圆圈里的红球与大圆圈里的红球是不同的）
由于这条定律，类型不能包含它们自己，因此罗素悖论被完全避免了。
这条定律听起来可能很奇怪，例如因为一个项只能属于一个类型，在类型理论中，自然数 1 被记为 $1 : \mathbb{N}$，并且它是与整数 1（记为 $1 : \mathbb{Z}$）完全独立的对象
只有当我们意识到我们总是可以使用我们在第一章学到的像函数（image function）将值的一个版本转换为另一个版本时，它才开始变得有些道理。
正如您很快就会看到的，类型的概念与函数的概念有很大关系。
什么是类型理论
“每一个命题函数（propositional function）φ(x)——人们如此主张——除了它的真值范围（range of truth）之外，还有一个意义范围（range of significance），也就是说，如果 φ(x) 根本上要成为一个命题（无论真假），x 必须落在该范围内。这是类型理论的第一个要点；第二个要点是，意义范围构成了类型，即，如果 x 属于 φ(x) 的意义范围，那么就会存在一个对象类，即 x 的类型，该类中的所有对象也必定属于 φ(x) 的意义范围” — 罗素 - Principles of Mathematics
在上一节中，我们差点掉进把类型解释为“像集合，但是……”的陷阱中（例如，它们像集合，但一个项只能是一个类型的成员）。然而，尽管这在技术层面上可能是对的，任何这样的解释都完全不合时宜，因为，虽然类型最初是作为集合的替代方案出现的，它们最终却变得相当不同。因此，用集合来思考是走不远的。确实，如果我们把上一节中那位典型的集合论学者请出来，问他们关于类型的事，他们真实的回答必定会是：
“你见过集合吗？好吧，这跟它一点关系都没有。”
那么，让我们看看如何正当地定义一个类型理论。
但首先……
在我们开始之前，让我们先把这段长长的免责声明解决掉：
请注意，在上一句话中我们说的是 a type theory（一种类型理论），而不是“type theory”或“the type theory”。这是因为，并不存在唯一的一种类型理论，而是有许多不同（尽管相互关联的）类型理论的表述，令人困惑的是，它们被称为类型 theories（而不那么令人困惑的叫法是类型系统），例如简单类型 lambda 演算或多态 Lambda 演算。出于这个原因，谈论 a type theory 是有道理的。
我把你们弄糊涂了吗？没有？
在某些语境下，“type theory”这一术语（不可数）指的是研究类型理论的整个领域，就像范畴论是研究范畴的一样。但是，（深吸一口气）你有时可以把不同的类型系统看作“类型理论的不同版本”，因此，当人们谈论一组给定的、所有类型系统共有的特征时，他们有时会使用“type theory”一词来指代任何具有这些特征的随意的类型系统。
什么是类型？
无论如何，让我们回到我们的主题（不管我们想怎么称呼它）。正如我们所说，类型理论诞生于罗素的探索，他试图找到一种方法来定义所有有趣的对象集合，而又不会意外地定义出把我们引入歧途的集合（例如，导致他那个同名的悖论），且无需凭空捏造大量额外的公理（像 ZFC 那样）。
他思考了很多（至少我想象他思考了），并设法设计出了一个符合所有这些标准的形式系统，基于一个革命性的新想法……这基本上就是处于范畴论核心的同一个想法（我不知道为什么他从未因为是一个范畴论先驱而获得赞誉）。这个想法如下：那些有趣的集合，那些我们首要想谈论的集合，就是作为函数源和目标的集合。我们或许可以这样说。
类型是可以作为箭头的源和/或目标的事物。
（为了使定义更通用，我们使用了更通用的术语——“箭头”，但目前你可以把箭头想象成函数。）
让我们再想一想那个不包含自身的所有集合的集合。除了是罗素悖论的起因之外，这个集合相当无用（除非我们把引发悖论算作有用）。如果我们深入挖掘，最终会发现原因：没有任何（有趣的）函数从任何其他集合指向这个集合，所以我们无法从任何地方到达它。反过来，我们也无法从它到达任何地方（也没有以它为源的函数）。这个集合就像是沙漠中心的一片绿洲……或者是大绿洲中心的一片小沙漠……如果你能想到什么好比喻，请联系我。
构建类型
我们看到，就其产生的结构而言，类型理论与集合论并没有太大区别——所有的类型（至少在第一层级上）都是集合，尽管并非所有的集合都是类型。而所有的函数都是……嗯，函数。然而，就结构产生的方式而言，类型理论与集合论截然不同，就像逻辑的直觉主义方法不同于经典方法一样（顺便说一句，如果这个比喻让类型理论和直觉主义逻辑之间的联系对你来说太明显了，帮个忙，请不要提及它，并在我们明确指出它时装出惊讶的样子）。
在集合论中，（特别是在其朴素版本中）所有可能的集合和函数从一开始就在那里了，就像柏拉图的理念世界一样。我们所做的仅仅是探索那些我们感兴趣的。
在类型理论中，我们从一个空的空间开始。
[图表省略]
从那里，我们必须构建我们的类型。一个接一个。用我们的双手（好吧，我们确实有一些很酷的数学工具来协助我们）。
类型形成、项引入与项消去
“通常，我们可以把数据看作是由选择器和构造器的某种集合定义的，加上这些过程为了成为有效表示而必须满足的特定条件。” — Harold Abelson, Gerald Jay Sussman, Julie Sussman — Structure and Interpretation of Computer Programs
在介绍构建类型的具体公式之前，我想详细说明一下总体思路。在上一节中，我们说到：
类型是可以作为箭头的源和/或目标的事物。
这个定义可能看起来有点模糊，但当我们看看计算机编程中类型是如何定义的时，它就变得微不足道了。很明显，即使是通过传统命令式语言的视角来看，类型的定义也包含了用于构造函数（以及更一般的箭头）的规则的定义。
class MyType<A> {
a: A;
constructor(a) {
this.a = a;
}
getA() {
return this.a;
}
}
哪些种类的规则？我们可以将它们分为三类。
首先，一个类型必须有一个定义来指明它是什么。请注意，这个箭头与我们通常认为的箭头不同——它不是一个值级箭头（从一个类型指向另一个类型），而是一个类型级箭头（从一个类型范畴指向另一个）。这被称为类型形成规则。
接下来，一个类型必须至少有一个指向这个新类型的箭头。这被称为项引入规则（“项”是“值”的对应词）。在编程中，它被称为构造器，并且它是一个值级箭头（例如函数）。
最后，由于我们不想仅仅为了构造新类型而构造类型，一个类型必须至少有一个从这个新类型出发的箭头。这是一个被称为项消去规则的值级箭头（函数）（就好像我们通过用方法的结果替换掉该类型，从而“消去”了它一样）。
综上所述
一个类型是通过定义以下三个箭头来定义的：
- 一个类型级箭头（类型形成）。
- 至少一个以该类型为目标的值级箭头（项引入）。
- 至少一个以它为源的值级箭头（项消去）。
好了，我觉得我们在没有真正定义类型理论的情况下，试图去定义类型理论走得有点太远了，所以我们将继续讲公式……在我们的第二段长免责声明之后。
正如我们在第一段长免责声明中所说，并不存在唯一的一种类型理论，而是有许多类型理论。所以如果我们想要做类型理论，我们必须首先挑选 a type theory（如果这句话让你困惑，请重读第一段免责声明）。
选择一个类型理论（或者我们称之为类型系统），也涉及到选择一个用来描述该理论的语言。当听到关于语言时，程序员可能会想到流行的、功能丰富的编程语言，如 TypeScript 或 Java。另一方面，类型理论家有不同的偏好——因为他们感兴趣的是类型系统，而不是语言，他们并不真正关心语言特性，因此他们大多数人选择的语言是可能存在的最简单、最极简的语言，即 Lambda Calculus（Lambda 演算）。如果你没听说过它，这是一种只有（匿名）函数而别无其他的语言。
为了让双方都满意，（同时也让双方都感到恼火），我们将采用一种介于两者之间的语言——即（一个子集）Haskell。这在理论上不会有太大区别，因为 Haskell 是基于 Lambda 演算的，但会让程序员更容易接受：与只有函数的 Lambda 演算不同，Haskell 支持将积构造器定义为原语（这从形式化的角度来看本身没有区别，因为我们可以通过柯里化和反柯里化轻松地从积转换到函数）。
另外，最后但同样重要的是，Haskell 的构造器和函数可以拥有名称（相信我，这很有帮助）。
既然我们选择了 Haskell，我们将在 Haskell 的类型理论/类型系统中工作。这是一个由 Jean-Yves Girard 在 1972 年发现的类型系统，被称为 Polymorphic Lambda Calculus（多态 Lambda 演算）或 System F。
Unit 类型
我们从一个空的空间开始，此时什么都没有定义，除了单例类型，在 Haskell 中被称为 $U n i t$ 类型。
一种只有一个值的类型，我们可以用作起点。
$U n i t$ 类型（$1$）是具有一个值的类型。
Lambda 类型
实际上还有一个不太容易解释的前提：即针对每一对对象的箭头类型（arrow types），被称为 Lambda 类型。在 Lambda 演算中，类型之间的箭头也是类型（这一特征在编程语境中有时被称为“一等函数”）。
对于任意类型 $A$ 和 $B$，存在一个类型 $A \rightarrow B$，称为 $A$ 和 $B$ 的 Lambda 类型，它以所有连接 $A$ 和 $B$ 的箭头作为值。
我们在这里不会详述，因为 Lambda 类型的定义与工作方式与上一章所定义的直觉主义逻辑中的蕴涵对象相同。正如你将学到的，它也发挥着相同的作用。
基本类型。布尔类型
一旦有了一个起点，我们就可以定义一些类型。但如何定义呢？让我们从基本类型开始，比如布尔值。对于它们，这个过程非常简单，因为我们可以直接列出它们的值。
$$ \begin{aligned} \mathsf{Bool} & : \mathsf{Type} \\ \mathsf{True} & : \mathsf{Bool} \\ \mathsf{False} & : \mathsf{Bool} \end{aligned} $$
让我们过一遍这个定义：
类型形成
首先，$\mathsf{Bool} : \mathsf{Type}$ 表示存在一个我们称之为“Bool”的类型。
项引入
然后，$\mathsf{True} : \mathsf{Bool}$ 表示“$\mathsf{True}$ 是一个布尔值”，即它为这个新创建的数据类型添加了一个值。在图中，我们将把它表示为一个从单元素类型（在 Haskell 中称为 $\mathsf{Unit}$ 类型）出发的箭头，正如第 2 章中集合范畴的基本理论所述。
而 $\mathsf{False} : \mathsf{Bool}$ 创建了另一个这样的值。
看哪，我们刚刚定义了一个类型！
项消去
等等，划掉那句。实际上我们还没有定义一个类型。或者说我们确实定义了一个，但它毫无用处。因为只有当我们定义了至少一个从它出发的箭头时，它才会变得有用（否则，它只是一条单行道）。对于布尔类型，这个函数通常被称为 $\mathsf{ifElse}$。
$$ \begin{aligned} \mathsf{ifElse} &: \forall a . \mathsf{Bool} \rightarrow a \rightarrow a \rightarrow a \\ \mathsf{ifElse}\ \mathsf{True}\ a\ b &= a \\ \mathsf{ifElse}\ \mathsf{False}\ a\ b &= b \end{aligned} $$
你可以看到，在 Haskell 中定义函数非常基础——你只需将一个类型的每个单独的值映射到另一个类型的值。
以下是一些使用该函数的表达式，并附有它们返回值的说明（-- 是 Haskell 的注释语法）
ifElse True 1 2 --1
ifElse False 1 2 --2
类型之间的同构
但是为什么（冒着重复自己的风险）这个特定的类型必须是布尔类型呢？是什么阻止了我们的同事 Bobby——那个总是想按自己的方式做一切事情的人——去定义他们自己的布尔版本并在他们的项目中使用它呢。
$$ \begin{aligned} \mathsf{BobbysBool} & : \mathsf{Type} \\ \mathsf{BobbysTrue} & : \mathsf{BobbysBool} \\ \mathsf{BobbysFalse} & : \mathsf{BobbysBool} \end{aligned} $$
答案是“什么都没有”。但这并不是什么大问题——我们可以直接迅速拼凑出一个函数，将他们的 Bool 转换为我们的：
$$ \begin{aligned} \mathsf{convertBobbysBool} &: \mathsf{BobbysBool} \rightarrow \mathsf{Bool} \\ \mathsf{convertBobbysBool}\ \mathsf{BobbysTrue} &= \mathsf{True} \\ \mathsf{convertBobbysBool}\ \mathsf{BobbysFalse} &= \mathsf{False} \end{aligned} $$
这个函数也是可逆的。这意味着这两个类型是同构的，即它们是同一个类型，相差一个（唯一的）同构。
其他基本类型
差点忘了：就像我们构造布尔类型一样，我们可以构造任何其他有限/基本类型，比如球的类型。
$$ \begin{aligned} \mathsf{Ball} & : \mathsf{Type} \\ \mathsf{OrangeBall} & : \mathsf{Ball} \\ \mathsf{RedBall} & : \mathsf{Ball} \\ \mathsf{YellowBall} & : \mathsf{Ball} \end{aligned} $$
多态类型。Maybe 类型
现在，我们将定义在 Haskell 中被称为 $M a y b e$ 的类型（在其他语言中通常被称为 $O p t i o n$）。如果你没有遇到过它，Haskell 文档提供了一个非常好的描述：
The Maybe type encapsulates an optional value. A value of type Maybe a either contains a value of type a (represented as $J u s t \left[\right. a \left]\right.$), or it is empty (represented as $N o t h i n g$). Using $M a y b e$ is a good way to deal with errors or exceptional cases without resorting to drastic measures such as error.
但是，一旦你学会了阅读它，类型定义本身就已经足够清晰了：
$$ \begin{aligned} \mathsf{Maybe} & : \mathsf{Type} \rightarrow \mathsf{Type} \\ \mathsf{Nothing} & : \forall a . \mathsf{Maybe}[a] \\ \mathsf{Just} & : \forall a . a \rightarrow \mathsf{Maybe}[a] \end{aligned} $$
类型形成
$M a y b e$ 看起来很像 $B o o l$，但是，与 $B o o l$ 不同，$M a y b e$ 是一个多态类型，正如我们通过查看类型形成规则所能看出的那样
$$ \mathsf{Maybe} : \mathsf{Type} \rightarrow \mathsf{Type} $$
Maybe 是多态的，即不仅有一个 $M a y b e$，而是有许多 $M a y b e$——每个类型 a 对应一个。例如，让我们以类型 $B o o l$ 为例。因为 $B o o l$ 是一个类型，那么（根据这条规则）$M a y b e \left[\right. B o o l \left]\right.$ 也是一个类型。
多态类型是从类型宇宙（universe of types）到其自身的箭头（即 $M a y b e$ 的 kind 是 $T y p e \rightarrow T y p e$），而 $B o o l$ 只是一个 $T y p e$。
项引入：Nothing
现在，是时候填充我们的类型了。
第一行与我们之前在布尔类型中看到的类似。
$$ \mathsf{Nothing} : \forall a . \mathsf{Maybe}[a] $$
它表示对于所有的 $M a y b e$ 类型，都有一个名为 $N o t h i n g$ 的值（这就是 $\forall$ 的含义——“对于所有”）。
项引入：Just
当然，如果所有的 $M a y b e$ 都一样，那么拥有许多 $M a y b e$ 就毫无意义。这就是第二行发挥作用的地方。
$$ \mathsf{Just} : \forall a . a \rightarrow \mathsf{Maybe}[a] $$
构造器 $J u s t$ 表示一个从类型 $a$ 到类型 $M a y b e \left[\right. a \left]\right.$ 的箭头，例如从 $B o o l e a n$ 到 $M a y b e \left[\right. B o o l e a n \left]\right.$。
使用 Maybe
$M a y b e$ 类型用于处理错误，即用于定义偏函数。假设我们想要定义一个函数，该函数并不为源中的所有值都提供箭头。这是否意味着这个函数无法被定义？
不，我们只需将目标类型包裹在 $M a y b e$ 中，它就变成了一个常规函数。
项消去
为了结束这个话题，我们定义了一个用于解构/消去类型 maybe 的函数，即通过使用一个转换其底层类型的函数，将其转换为其他东西。
$$ \begin{aligned} \mathsf{maybe} &: \forall a b . b \rightarrow (a \rightarrow b) \rightarrow \mathsf{Maybe}[a] \rightarrow b \\ \mathsf{maybe}\ n\ f\ \mathsf{Nothing} &= n \\ \mathsf{maybe}\ n\ f\ (\mathsf{Just}\ x) &= f\ x \end{aligned} $$
请注意，这个函数定义了一个从类型 $M a y b e \left[\right. a \left]\right.$ 到任意类型 $b$ 的箭头，前提是提供了一个函数 $a \rightarrow b$ 和一个 $b$ 的值。
归纳类型：自然数类型
初学数学时可能会感到不知所措：面对如此庞大甚至无限的知识体系，你或许不知从何入手。但事实证明答案很简单：你从知道 0 件事开始。然后，你学了 1 个理论——恭喜，你学到了你的第一个理论，因此总共会知道 1 个理论。然后，你又学了 1 个理论，于是你总共已经知道了 2 个理论。接着再学 1 个理论，然后再学 1 个，只要给予足够的时间和投入，你可能会学到所有的理论。
可以说，这个论证不仅适用于数学理论，也适用于所有其他“可数”的事物。因为这是自然数数学定义的基础，正如 19 世纪意大利数学家 Giuseppe Peano 所著名总结的那样：
- $0$ 是自然数。
- 如果 $n$ 是自然数，$n + 1$ 是自然数。
或者如 Haskell 程序员所说：
$$ \begin{aligned} \mathbb{N} & : \mathsf{Type} \\ \mathsf{Zero} & : \mathbb{N} \\ \mathsf{Succ} & : \mathbb{N} \rightarrow \mathbb{N} \end{aligned} $$
让我们顺着箭头看。
类型形成
第一行表明自然数类型是一个普通的非多态，或者说“单态”（monomorphic）的类型。
$$ \mathbb{N} : \mathsf{Type} $$
项引入：零（Zero）
第一条规则同样显而易见。
$$ \mathsf{Zero} : \mathbb{N} $$
它允许我们构造一个值，称为零（Zero）
即这是对 Giuseppe Peano 第一条公理的逐字重复。
- $0$ 是自然数。
项引入：后继（Successors）
第二条规则更有趣些。
$$ \mathsf{Succ} : \mathbb{N} \rightarrow \mathbb{N} $$
它说存在一个称为“后继”的构造器 $Succ$（或者按我们的叫法 +1），即这等价于
- 如果 $n$ 是自然数，$n + 1$ 是自然数。
$Succ$ 是一个从自然数类型指向自身的箭头，这意味着给定一个自然数，$Succ$ 会构造出另一个。
但现在我们只有自然数类型的一个项（值）：$Zero$。我们画出 $Succ$ 箭头并构造出另一个，$Succ Zero$（在某些语境下称为 $1$。
现在，我们多了一个值，所以必须再画一个 $Succ$ 箭头。这次的结果是 $Succ Succ Zero$，即二。
我们像这样继续下去，以至无限，创造出一条无尽的值链。
嗯，这种记法有点笨拙，要是能有更好的方式来表示这些值就好了……哦，等等。
这就是你定义归纳类型（inductive type）（或者我们也可以称之为递归类型（recursive type））的方式。
项消去
等等，还有消去规则，我总是忘记消去规则，它们在这里。
$$ \begin{aligned} \mathsf{foldNat} &: \mathbb{N} \rightarrow a \rightarrow (a \rightarrow a) \rightarrow a \\ \mathsf{foldNat}\ \mathsf{Zero}\ z\ s &= z \\ \mathsf{foldNat}\ (\mathsf{Succ}\ n)\ z\ s &= s\ (\mathsf{foldNat}\ n\ z\ s) \end{aligned} $$
这允许我们，例如，将我们的 Nat 转换为普通的 Haskell Nat：
foldNat (Succ (Succ Zero)) 0 (+ 1) -- 2
任何其他将自然数转换为其他类型的规范函数（canonical function），也都可以使用消去规则来定义。
复合类型：列表类型
没有复合类型（composite types），类型的风景将会是一个真正的……平坦之地。那些是允许你将其他类型的多个值合并为一个的类型。
终极的复合类型是列表。具体来说，链表（linked list）是一件美妙的事物：
$$ \begin{aligned} \mathsf{List} & : \mathsf{Type} \rightarrow \mathsf{Type} \\ \mathsf{Nil} & : \forall a . \mathsf{List}[a] \\ \mathsf{Cons} & : \forall a . a \rightarrow \mathsf{List}[a] \rightarrow \mathsf{List}[a] \end{aligned} $$
让我们拆解来看：
类型形成
类型形成规则告诉我们，$List$（像 $Maybe$ 一样）是一个复合类型。
$$ \mathsf{List} : \mathsf{Type} \rightarrow \mathsf{Type} $$
这意味着，不止一个，而是有许多 $List$ 类型，例如 $List \left[\right. N a t \left]\right.$ $List \left[\right. B o o l \left]\right.$ 等（如果你考虑列表的列表（的列表），则有无限多个）。它们通常被读作“自然数列表”、“布尔值列表”等。
项引入：Nil
现在，让我们看看构造器。第一个定义了一个静态值，每个列表一个，代表空列表。
$$ \mathsf{Nil} : \forall a . \mathsf{List}[a] $$
我们将这个值称为 $Nil$（原生 Haskell 列表使用 [] 符号）。
项引入：Cons
现在来看更有趣的部分：$Cons$，我们的第二个项引入规则（顺便说一句，$Cons$ 是 construct 的缩写），可以被视为将值 $a$ 添加到列表（并返回该列表）的操作。
$$ \mathsf{Cons} : \forall a . a \rightarrow \mathsf{List}[a] \rightarrow \mathsf{List}[a] $$
乍一看，$Cons$ 看起来与我们见过的归纳构造器 $Succ$ 非常相似。事实上，就像 $Succ$ 一样，$Cons$ 是一个归纳/递归构造器，会生成无限数量的项。
然而，与签名为 $X \rightarrow X$ 的 $Succ$ 不同（即对于每个 $X$，都有另一个），$Cons$ 的签名是 $a \rightarrow \left(\right. X \rightarrow X \left.\right)$ ——对于类型 $a$ 的每个值，都有一个 List 构造器。我们可以将 $Cons$ 可视化为一个指向另一个箭头的箭头。
为什么我们能够有来自其他箭头的箭头？也许这里应该提醒你，在 Lambda 演算中，类型之间的箭头本身也是类型。
那么，让我们从基础值 $Nil$ 开始，绘制这些箭头。
如前所述，$List$ 类型是归纳的，即你画的每个箭头都会生成更多的箭头（在这里，我们只画了其中的一部分（那些来自橙色球的箭头））。
结果是一个其值为……嗯，其他值的列表的类型，
项消去
现在，让我们写出项消去规则。
$$ \begin{aligned} \mathsf{foldList} &: (b \rightarrow a \rightarrow b) \rightarrow b \rightarrow \mathsf{List}[a] \rightarrow b \\ \mathsf{foldList}\ f\ z\ \mathsf{Nil} &= z \\ \mathsf{foldList}\ f\ z\ (\mathsf{Cons}\ x\ xs) &= \mathsf{foldList}\ f\ (f\ z\ x)\ xs \end{aligned} $$
这个规则也是操作列表最有用的函数。
**任务 1：**存在一种从 $L i s t$ 到 $B o o l e a n$ 的特定映射，它非常有用，以至于某些 Lisp 方言根本没有 $B o o l e a n$ 类型，而仅仅依赖这个映射。请画出它。
**任务 2：**在 Haskell 中定义这个映射（在 List 和 Bool 之间）。先从头写一个函数定义一次，再使用 foldList 函数定义一次。
f :: (Bool -> a -> Bool)
f = undefined
foldList f False
**任务 3：**我向你展示类型 $L i s t U n i t$（其中 $U n i t$ 是单例类型（singleton type），即只有一个值的类型）。请画出 $L i s t U n i t$ 的值，直到你画不出为止。
任务 4：$L i s t U n i t$ 类型实际上与我们在这里回顾过的另一个类型同构（isomorphic）。找出它是哪个。
正类型与负类型。Either 与元组（Tuples）。
现在，我们将快速介绍另外两个类型，（嗯……我感觉我实际上以前见过它们）。
Either
$E i t h e r$ 类型是一个有趣的类型。
它是一个由两个类型 $a$ 和 $b$ 参数化的类型，并有两个构造器/项引入规则——一个称为 $L e f t$ 的构造器，接收一个 $a$ 的值。另一个称为 $R i g h t$，接收一个 $b$。下面是 Either 的定义（不包括项消去规则）。
$$ \begin{aligned} \mathsf{Either} & : \mathsf{Type} \rightarrow \mathsf{Type} \rightarrow \mathsf{Type} \\ \mathsf{Left} & : \forall a b . a \rightarrow \mathsf{Either}[a,b] \\ \mathsf{Right} & : \forall a b . b \rightarrow \mathsf{Either}[a,b] \end{aligned} $$
元组（Tuple）
我们将要介绍的下一个类型是 $T u p l e$ 类型，它同样由 $a$ 和 $b$ 参数化，但它的每一个值都同时包含一个 $a$ 的值和一个 $b$ 的值。
在这里我们将做一些不同的事情——不给出定义，而是直接展示类型消去规则。
$$ \begin{aligned} \mathsf{first} &: \forall a b . \mathsf{Tuple}[a,b] \rightarrow a \\ \mathsf{second} &: \forall a b . \mathsf{Tuple}[a,b] \rightarrow b \end{aligned} $$
**任务 5：**写一个 Tuple 的构造器。为 Either 写一个 fold 函数。
正类型与负类型
$E i t h e r$ 类型由其引入规则唯一定义，即消去规则可以从引入规则中推导出来。
$$ \begin{aligned} \mathsf{Left} & : \forall a b . a \rightarrow \mathsf{Either}[a,b] \\ \mathsf{Right} & : \forall a b . b \rightarrow \mathsf{Either}[a,b] \end{aligned} $$
另一方面，$T u p l e$ 由其消去规则定义，即引入规则可以从它们中推导出来：
$$ \begin{aligned} \mathsf{first} &: \forall a b . \mathsf{Tuple}[a,b] \rightarrow a \\ \mathsf{second} &: \forall a b . \mathsf{Tuple}[a,b] \rightarrow b \end{aligned} $$
像 $E i t h e r$ 这样由其引入规则定义的类型被称为正类型（positive types）。由其消去规则定义的类型是负类型（negative types）。到目前为止我们见过的所有类型（除了 $T u p l e$）都是正类型。
正类型与负类型彼此对偶。
正/负类型对应于范畴论中极限（limit）/余极限（colimit）的概念，但我们稍后会学到更多关于它们的知识。
**任务 6：**除了 $T u p l e$，还有一个非常重要的负类型，我们在本章（以及各种其他地方）已经介绍过。
小结
在本节中，我们几乎从无开始——仅仅是 $U n i t$ 类型。然后我们非常快速地定义了许多东西。
人们可以看到，程序员使用的一些类型仍然缺失，但它们可以用与我们已定义类型几乎相同的方式来定义：例如 $c h a r$ 只是一个基本类型，$s t r i n g$ 只是 $L i s t \left[\right. c h a r \left]\right.$ 等等。
Church 编码：从 Haskell 到 Lambda 演算
在上一节中，我们确实非常快速地定义了许多东西，但我们依赖于 Haskell 的广义代数数据类型（Generalized Algebraic Datatypes，GADTs），并且用仅有的函数实现同样的事情并非显而易见。然而，这是可能的：存在一种将每个类型编码为函数的机制，被称为 Church 编码（Church encoding），得名于 Lambda 演算的创造者阿隆佐·邱奇（Alonzo Church）。
基本类型。布尔类型（Boolean type）
考虑布尔类型，我们这样定义它：
$$ \begin{aligned} \mathsf{Bool} & : \mathsf{Type} \\ \mathsf{True} & : \mathsf{Bool} \\ \mathsf{False} & : \mathsf{Bool} \end{aligned} $$
这是相同事物的另一个版本，仅使用函数。
$$ \begin{aligned} \mathsf{type}\ \mathsf{Bool} & = \forall a . a \rightarrow a \rightarrow a \\ \mathsf{false} & : \mathsf{Bool} \\ \mathsf{false}\ a\ b &= b \\ \mathsf{true} & : \mathsf{Bool} \\ \mathsf{true}\ a\ b &= a \end{aligned} $$
在这里 $B o o l$ 只是函数 $\forall a . a \rightarrow a \rightarrow a$ 的简写，该函数对于所有的 $a$ 接收两个类型为 $a$ 的值并返回另一个值。我们可以看到，在这个定义下，$T r u e$ 是一个返回第一个 $a$ 的函数，而 $F a l s e$ 是一个返回第二个的函数。
不相信这些可以作为布尔值使用？这里是 $i f E l s e$ 函数的一个实现：
$$ \begin{aligned} \mathsf{ifElse} &: \forall a . \mathsf{Bool} \rightarrow a \rightarrow a \rightarrow a \\ \mathsf{ifElse}\ v\ a\ b &= v\ a\ b \end{aligned} $$
这个实现是微不足道的，因为数据类型本身在做这些工作。这是所谓的“Church 编码”数据类型背后的主要原则之一——数据类型编码了项消去规则。
以下是你如何使用它的方式：
ifElse true "True" "False" -- "True"
ifElse false "True" "False" -- "False"
多态类型。Maybe 类型
布尔类型当然是一个基本类型。所以，让我们考虑更复杂的 $M a y b e$ 类型：
$$ \begin{aligned} \mathsf{Maybe} & : \mathsf{Type} \rightarrow \mathsf{Type} \\ \mathsf{Nothing} & : \forall a . \mathsf{Maybe}[a] \\ \mathsf{Just} & : \forall a . a \rightarrow \mathsf{Maybe}[a] \end{aligned} $$
$M a y b e$ 更复杂，因为它可以在其内部包含另一个值（通过 $J u s t$ 构造器）。在这里我们学到了 Church 编码的另一个重要原则：使用柯里化函数来保存值。
$$ \begin{aligned} \mathsf{type}\ \mathsf{Maybe}[a] & = \forall m . m \rightarrow (a \rightarrow m) \rightarrow m \\ \mathsf{nothing} & : \mathsf{Maybe}[a] \\ \mathsf{nothing}\ n\ j &= n \\ \mathsf{just} & : a \rightarrow \mathsf{Maybe}[a] \\ \mathsf{just}\ val\ n\ j &= j\ val \end{aligned} $$
一般原则
到现在为止，你可能已经看到，类型的 Church 编码与“普通”类型具有相同的构造器——区别仅仅在于它将它们作为参数接收。
如果我们有一个类似 $M a y b e$ 的类型，但只有一个值（像 $1$ 类型）……
$$ \begin{aligned} \mathsf{Nothing} & : \forall a . \mathsf{Maybe}[a] \end{aligned} $$
……它的 Church 编码将会是……
$$ \forall m . m \rightarrow m $$
（这确实是 $1$ 类型的 Church 编码）
然后，如果我们扩展该类型使其也拥有 $J u s t$ 构造器……
$$ \begin{aligned} \mathsf{Nothing} & : \forall a . \mathsf{Maybe}[a] \\ \mathsf{Just} & : \forall a . a \rightarrow \mathsf{Maybe}[a] \end{aligned} $$
……编码像这样扩展……
$$ \forall m . m \rightarrow \left(\right. a \rightarrow m \left.\right) \rightarrow m $$
这就是为什么 Church 编码类型的签名与用于消去它的 $f o l d$ 函数的签名几乎完全相同：
$$ \begin{aligned} \mathsf{foldMaybe} & : \forall a m . m \rightarrow (a \rightarrow m) \rightarrow \mathsf{Maybe}[a] \rightarrow m \end{aligned} $$
而 $f o l d$ 函数本身是微不足道的。通常，类型的 Church 编码基本上就是一个柯里化的 $f o l d$ 函数，一个给定与“折叠”函数相同参数、从而产生相同结果的函数。
Church 编码的一般原则是，一个类型完全由你能用它做什么来表征，因此，我们不是为类型提供构造器然后再用 $f o l d$ 消去它们，而是直接跳到 $f o l d$。
**任务 7：**写一个自然数类型（natural numbers type）的 Church 编码版本
多态 Lambda 演算——形式化定义
到目前为止，我们看到了 Lambda 演算是如何运作的。现在，我们即将看到它是如何被形式化定义的。答案是，和所有类型系统一样，它是由类型规则定义的。那么什么是类型规则呢？基本上，它们也是箭头。（惊讶吗？）
自然演绎
是的，Haskell 的类型规则确实是箭头，但它们是用一种不同于 Haskell 的语言定义的，称为自然演绎。自然演绎就像 Haskell，但它使用一种将前提和结论用水平横线隔开的语法，例如，不是写……
$$ a \rightarrow b $$
……我们写……
$$ \frac{a}{b} $$
除此之外，自然演绎和 Haskell 之间没有太大的区别。以布尔类型为例。我们在 Haskell 中这样定义它：
$$ \begin{aligned} \mathsf{Bool} & : \mathsf{Type} \\ \mathsf{True} & : \mathsf{Bool} \\ \mathsf{False} & : \mathsf{Bool} \end{aligned} $$
如果我们想使用自然演绎来定义它，使其成为类型系统本身一部分的“原始”类型之一（就像在大多数编程语言中定义的那样），它看起来会是这样的。
$$
$$
这意味着有一个叫做 Bool 的类型（严格来说，这不是一条类型规则，而是一条“kinding”规则（因此使用了双冒号））。
$$
$$
$$
$$
$True$ 和 $False$ 是布尔值。
哦我忘了，在自然演绎中，允许没有前提的结论。
**任务 8：**使用自然演绎定义布尔类型的消去规则。
上下文
这是否太简单了？让我们把类型上下文（或类型环境）的概念加入进来。
情况是这样的：类型和变量必须被存储在某个地方。因此，给定一组值（例如 $x$, $y$, $z$ 等）和一组类型（例如 $A$, $B$, $C$ 等），一个上下文就是所有变量及其类型的一个集合（哎呀，我又这么说了），例如 $\left(\right. x , A \left.\right) , \left(\right. y , B \left.\right) , \left(\right. z , C \left.\right) \ldots$。
我们通常用字母 $\Gamma$ 表示上下文，并使用 $\vdash$ 符号表示从该上下文中得出的东西（哦，不，又不是另一个箭头吧），例如 $\Gamma \vdash a : b$ 意味着在上下文 $\Gamma$ 中，存在一个变量 $a$ 具有类型 $b$。）。
因此，当我们考虑上下文时，上述定义变成
$$
$$
即上下文包含类型 $Bool$
$$
$$
即上下文包含类型为 $Bool$ 的值 $True$
$$
$$
即上下文包含类型为 $Bool$ 的值 $False$
因此，我们直接将布尔类型定义为上下文的一部分。
值级箭头
以此，我们列出 Lambda 演算的公理，其中只不过包含了值级箭头（函数）的类型定义。
我们必须定义几条类型规则，从平凡的规则 Var 开始，它声明如下：如果我们之前说过 $x$ 具有类型 $A$，那么 $x$ 具有类型 $A$。
$$ \frac{x : A \in \Gamma}{\Gamma \vdash x : A} $$
现在，我们继续定义箭头的类型。
我们从类型形成规则（type formation rule）（或 kinding 规则）开始。
$$ \frac{\Gamma \vdash A :: \mathsf{Type},\ \Gamma \vdash B :: \mathsf{Type}}{\Gamma \vdash A \rightarrow B :: \mathsf{Type}} $$
然后是两条类型规则。一条是 lambda 项的项引入（term introduction），称为抽象（或 Abs）。
$$ \frac{\Gamma , x : A \vdash y : B}{\Gamma \vdash \lambda z : A \rightarrow B} $$
（即，如果我们有一种方式，给定一个类型为 $A$ 的值 $x$ 来获得一个类型为 $B$ 的值 $y$，那么我们就得到了一个函数 $A \rightarrow B$）。
还有 lambda 的项消去（term elimination），即函数应用（App）。
$$ \frac{\Gamma \vdash z : A \rightarrow B , \Gamma \vdash x : A}{\Gamma \vdash z x : B} $$
为了理解这些规则是如何工作的，让我们以函数 $l e n g t h : s t r i n g \rightarrow i n t$ 为例。这个函数的抽象规则将是：
$$ \frac{\Gamma,\ x : \mathsf{string} \vdash y : \mathsf{int}}{\Gamma \vdash \lambda \mathsf{length} : \mathsf{string} \rightarrow \mathsf{int}} $$
而应用规则将是
$$ \frac{\Gamma \vdash \mathsf{length} : \mathsf{string} \rightarrow \mathsf{int},\ \Gamma \vdash x : \mathsf{string}}{\Gamma \vdash \mathsf{length}\ x : \mathsf{int}} $$
这些规则就是你定义值级箭头所需要的全部。
简单类型 Lambda 演算
到目前为止我们回顾的规则并没有定义多态 Lambda 演算，而是定义了一个更简单的类型系统，恰如其分地称为简单类型 Lambda 演算。
简单类型 Lambda 演算（STLC）是只有一种类型构造器——函数（lambda）的类型系统，具有类型规则 Abs 和 App（用于项引入和项消去）。它还具有 Var 类型规则。
多态
简单类型 lambda 演算就像多态 Lambda 演算，除了……它不是多态的，即我们不能定义像 $M a y b e$ 这样的多态类型。
$$ \begin{aligned} \mathsf{Maybe} & : \mathsf{Type} \rightarrow \mathsf{Type} \\ \mathsf{Nothing} & : \forall a . \mathsf{Maybe}[a] \\ \mathsf{Just} & : \forall a . a \rightarrow \mathsf{Maybe}[a] \end{aligned} $$
我们能做的最好的事情就是定义该类型的单独版本，例如，一个仅适用于 $int$ 的版本。
$$ \begin{aligned} \mathsf{MaybeInt} & : \mathsf{Type} \\ \mathsf{NoInt} & : \mathsf{MaybeInt} \\ \mathsf{JustInt} & : \mathsf{int} \rightarrow \mathsf{MaybeInt} \end{aligned} $$
还有一个适用于 $string$ 的版本
$$ \begin{aligned} \mathsf{MaybeString} & : \mathsf{Type} \\ \mathsf{NoString} & : \mathsf{MaybeString} \\ \mathsf{JustString} & : \mathsf{string} \rightarrow \mathsf{MaybeString} \end{aligned} $$
此外，在 STLC 中，我们不能定义适用于多态 $M a y b e$ 的函数（无论它们持有的是什么类型），因此我们不仅必须重新定义类型，还必须重新定义所有使用它们的函数。
为了解决这个问题，并将我们自己从简单类型提升到多态 Lambda 演算（又名 System F），我们定义了类型级箭头。
但是，实际上我们应该先谈谈 kind……
kind
在表达式 “ $x : A$ ” 中，“ $A$ ” 表示值的类型。那么在表达式 “ $A :: T y p e$ ” 中，$T y p e$ 又是什么呢？我们不能说 $T y p e$ 是一个类型，因为我们会看到罗素正潜伏在我们身后，带着他同名的悖论。在 Lambda 演算中，它是通过以下方式解决的：
- 值具有类型（用单冒号注释 – $:$）
- 类型具有类型的类型，即 kind（用双冒号注释 – $::$）
- kind 具有……好吧，我们先停在这里……
这意味着除了类型系统和类型规则之外，我们还有一个 kind 系统（kind-system）和 kinding 规则。但是，请不要把这本书扔出窗外——STLC 的 kinding 系统非常容易定义：只有一个 kind，我们称之为 $Type$（有时用 $*$ 标记）。
$$
$$
然后类型定义规则像这样被定义（即，一切都是 kind $Type$：
$$
$$
而对于多态 Lambda 演算，我们将在下一节看到。
类型级箭头
我们通过使用平凡的 Var 类型规则定义值级变量，开始了 STLC 的定义，
$$ \frac{x : A \in \Gamma}{\Gamma \vdash x : A} $$
在多态 Lambda 演算中，我们还有类型级变量，它们用类似的 TVar kinding 规则定义。
$$ \frac{A :: K \in \Gamma}{\Gamma \vdash A :: K} $$
现在，让我们继续定义箭头本身的类型。
在多态 Lambda 演算中，就像在 STLC 中一样，我们有将值转换为其他值的值级箭头……
$$ \frac{\Gamma \vdash A :: \mathsf{Type},\ \Gamma \vdash B :: \mathsf{Type}}{\Gamma \vdash A \rightarrow B :: \mathsf{Type}} $$
而且，我们还有将类型转换为其他类型的类型级箭头。它们用这条 kinding 规则定义：
$$ \frac{\Gamma,\ (\alpha :: A) \vdash (B :: \mathsf{Type})}{\Gamma \vdash \forall (\alpha :: A) . (B :: \mathsf{Type})} $$
例如，对于 $M a y b e$ 类型，这条规则会说
$$ \frac{\Gamma,\ (\alpha :: \mathsf{Type}) \vdash \mathsf{Maybe}[\alpha] :: \mathsf{Type}}{\Gamma \vdash \forall (\alpha :: \mathsf{Type}) . \mathsf{Maybe}[\alpha] :: \mathsf{Type}} $$
多态函数
多态更有趣（也更难）的部分是增强值级箭头以使其与多态类型一起工作，即拥有除了值之外还接受一个类型作为参数的函数。
例如，如果我们在 STLC 的上下文中工作，并使用我们在上一节中定义的 $M a y b e S t r i n g$ 类型（它只适用于字符串），我们可以定义一个具有以下类型签名的函数
$$ z :: \mathsf{string} \rightarrow \mathsf{MaybeString} $$
利用多态 Lambda 演算的能力，我们可以抽象出类型 $S t r i n g$（使用规则 TAbs 来构建一个多态函数，它看起来像这样。
$$ z^{'} :: \forall \alpha . \alpha \rightarrow \mathsf{Maybe}\ \alpha $$
然后，我们使用 TApp 将类型参数 $S t r i n g$ 应用于抽象函数，以获得我们的原始函数。
$$ z = z^{'}[\mathsf{String}] $$
（这不是真正的 Haskell 语法，因为 Haskell 会自动进行类型应用——你只需提供值，语言就会从中推断出类型）。
以下是多态函数本身的类型规则：
类型抽象（或 TAbs）
$$ \frac{\Gamma,\ (\alpha :: A) \vdash z : C}{\Gamma \vdash (\Lambda \alpha :: A . z) : \forall (\alpha :: A) . C} $$
以及类型应用（TApp）
$$ \frac{\Gamma \vdash z^{'} : \forall (\alpha :: A) . C,\ \Gamma \vdash (X :: A)}{\Gamma \vdash z^{'}[X] : C[\alpha := X]} $$
至此，我们结束了 System F 的定义。
多态 Lambda 演算（System F）是只拥有一个类型构造器——多态 lambda 的类型系统，带有类型规则 Abs 和 App（用于项的引入与消去）以及 kinding rules（kinding rules）TAbs 和 TApp（用于类型的引入与消去）。它也具有 Var 类型规则和 TVar kinding 规则。
现在我们准备好去看看它与我们的主要主题有何关联。
类型系统即范畴
我们已经在类型理论与范畴论之间建立了一些平行联系，但这绝不仅仅是单纯的平行：透过恰当的视角来看，类型系统就是某种范畴。而且不仅如此：我们已经知道是哪一种！
类型即对象，箭头即态射
让我们从基础开始。
每个类型都是一个对象。
每个值级箭头（函数）都是一个态射。
现在来看一些不那么平凡的东西——值。
值也是态射
我们说过范畴论全是关于箭头的。在这里，我们似乎背离了这一点，又开始画值和内部图，例如自然数类型。
但这里并不矛盾。我们说过在类型理论中，“唯一的值是那些作为箭头源点和目标的实体”。在自然数的情况下，就是 $s u c c e s s o r$ 箭头和 $z e r o$ 箭头。
这意味着值实际上只是表示箭头的另一种方式。
例如，自然数类型可以在外部这样表示。
这里我们回到了在第二章学过的关于集合/类型元素的一个简单定理：
任何集合 $X$ 的每个元素都同构于一个函数 $1 \rightarrow X$（其中 $1$ 表示单例集合）。
因此，对于某个类型 $X$，从 $1 \rightarrow X$ 的箭头，在将其视为集合时，等价于 $X$ 的一个值。
这意味着我们称之为 $0$ 的从 $1 \rightarrow \mathbb{N}$ 的箭头，同构于值 $0$。
除了 $1 \rightarrow \mathbb{N}$ 之外，我们还有一个箭头 $s : \mathbb{N} \rightarrow \mathbb{N}$。那么，当我们把这两者组合起来会发生什么？我们得到了另一个 $1 \rightarrow \mathbb{N}$ 箭头——$s \circ 0$，$0$ 的后继，即 $1$。
如果我们再这样做一次，就会得到 $s \circ s \circ 0$。
我们可以看到，它的展开方式与旧定义相同。我们并没有退回到值，而是兜了一个完整的圈子，发现（或者重新发现，因为我们从集合范畴的初等理论中已经知道了这一点）值只是画箭头的一种更方便的方式。
简单类型 lambda 演算作为笛卡尔闭范畴
好了，我们明白了：如果我们将类型视为对象，将箭头和值视为态射，那么整个类型理论/类型系统就可以被视为一个范畴。但是是哪个范畴呢？为了理解这一点，我们回顾一下 Lambda 演算具有的特殊特征：我们知道它有 Lambda 类型，也就是函数类型，因此我们需要一个带有函数类型的范畴。要定义它，你还需要终端对象（$1$ 对象）和积，因此我们要寻找的是一个必须具备这些特征的范畴。令人惊讶的是，我们已经知道哪个范畴具备所有这些特征了。我们在上一章讨论逻辑时已经研究过它。
简单类型 lambda 演算可以被视为一个笛卡尔闭范畴——元组和 either 类型是“与”和“或”操作，Unit 和 Empty 类型是值“真”和“假”，而 Lambda 类型是指数对象。
无类型 Lambda 演算作为笛卡尔闭幺半群
我们不会深入探讨它，但我认为值得一提的是，还存在一种叫做无类型 Lambda 演算的东西。这是一种只有一种类型的语言——函数，并且每个函数都接受任何其他函数作为参数。
那么，无类型 Lambda 演算如何融入我们的图景中呢？它完美地契合了：它对应于笛卡尔闭幺半群（简称 C-幺半群）。这些是只有一个对象的笛卡尔闭范畴。
多态 Lambda 演算作为……
我们已经确定值级箭头对应态射。
但是类型级箭头（也就是多态类型）呢？它们对应什么？
我们将在下一章继续探讨这个问题！
Curry-Howard-Lambek 对应
在结束本节之前，让我们思考一下这个问题：为什么 Lambda 演算和直觉主义逻辑对应于几乎相同类型的范畴——笛卡尔闭范畴。
为了理解这一点，我们回顾一下在上一章中研究过的逻辑与范畴之间的对应关系。
直觉主义逻辑的逻辑系统可以被视为一个双笛卡尔闭范畴——“与”和“或”操作是积/余积，值“真”和“假”是初始/终端对象，而蕴涵操作是指数对象。
这与我们现在关于类型的定义几乎完全相同（唯一的区别在于，Lambda 演算可以在没有余积和初始对象的情况下工作，所以它是一个笛卡尔闭范畴，而直觉主义逻辑需要它们，所以它是双笛卡尔的）。
这意味着直觉主义逻辑与 Lambda 演算之间的相似性并不仅仅止于它们都是“范畴式的”。它们实际上是同一回事：
- 逻辑命题可以被视为类型。
- 给定命题的证明无非是对应类型的一个值。 - Lambda 类型是蕴涵对象。
- 函数应用（App）是假言推理。
| 直觉主义逻辑 | 简单类型 lambda 演算 | 笛卡尔闭范畴 |
|---|---|---|
| 命题 | 类型 | 对象 |
| 蕴涵 | 箭头 | 态射 |
| 基本命题 | 类型 A 的值 | 态射 1 → A（全局元素） |
| 蕴涵对象 (A → B) | Lambda 类型 (A → B) | 指数对象 B^A |
| 与 (A ∧ B) | 元组 (A × B) | 积 A × B |
| 或 (A ∨ B) | Either (A + B) | 余积 A + B |
| 真 (⊤) | Unit 类型 | 终端对象 (1) |
| 假 (⊥) | Empty 类型 | 初始对象 (0) |
| 否定 A → ⊥ | 函数 A → Empty | 态射 A → 0 |
简而言之，在上一章中，我们讨论了直觉主义逻辑与笛卡尔闭范畴之间的对应关系（被称为 Curry-Howard-Lambek 对应），现在我们正在为这种对应关系加上第三个分支——Lambda 演算。
附录：Haskell 中的定义
关于是以可执行的 Haskell 代码还是以公式（即等宽字体或现代排版）的形式来提供基本类型的定义，我考虑了很久。最后，我决定公式更好，但它们确实都是 Haskell 代码，只是有几个需要注意的地方：
首先，我们想从空白状态开始。在 Haskell 中，我们可以通过移除标准库（叫做“Prelude”）来做到这一点，它通常是隐式导入的。
{-# LANGUAGE NoImplicitPrelude #-}
并且我们还要再使用一个扩展，它允许我们编写更明确一些的类型定义。
{-# LANGUAGE GADTs, NoImplicitPrelude #-}
差不多就是这样了。除此之外就是使用 forall 代替 $\forall$ 符号。
{-# LANGUAGE GADTs, NoImplicitPrelude #-}
import qualified Prelude as P
data Bool where
True :: Bool
False :: Bool
deriving (P.Show)
ifElse :: forall a. Bool -> a -> a -> a
ifElse True a b = a
ifElse False a b = b
data Either a b where
Left :: forall a b. a -> Either a b
Right :: forall a b. b -> Either a b
deriving (P.Show)
foldEither :: forall a b c. (a -> c) -> (b -> c) -> Either a b -> c
foldEither fa fb (Left val) = fa val
foldEither fa fb (Right val) = fb val
data Tuple a b where
Tuple :: forall a b. a -> b -> Tuple a b
deriving (P.Show)
first :: Tuple a b -> a
first (Tuple a b) = a
second :: Tuple a b -> b
second (Tuple a b) = b
data Maybe a where
Nothing :: forall a. Maybe a
Just :: forall a. a -> Maybe a
deriving (P.Show)
foldMaybe :: forall a b. b -> (a -> b) -> Maybe a -> b
foldMaybe n _ Nothing = n
foldMaybe _ f (Just x) = f x
data List a where
Nil :: forall a. List a
Cons :: forall a. a -> List a -> List a
deriving (P.Show)
foldList :: (b -> a -> b) -> b -> List a -> b
foldList f z Nil = z
foldList f z (Cons x xs) = foldList f (f z x) xs
data Nat where
Zero :: Nat
Succ :: Nat -> Nat
deriving (P.Show)
foldNat :: Nat -> a -> (a -> a) -> a
foldNat Zero z s = z
foldNat (Succ a) z s = s (foldNat a z s)
plus :: Nat -> Nat -> Nat
plus Zero n = n
plus (Succ m) n = Succ (plus m n)
not :: Bool -> Bool
not False = True
not True = False
main = do
P.print (ifElse True 1 2) --1
P.print (ifElse False 1 2) --2
P.print (foldNat (Succ (Succ Zero)) 0 (P.+ 1)) -- 2
答案
任务 1： 存在一种从 List 到 Boolean 的映射，非常直观。直观到某些 Lisp 方言根本没有 Boolean 类型，完全依赖这种映射。试着猜猜这种映射。
任务 2： 在 Haskell 中定义这个映射（在 List 和 Bool 之间）。从零写一个函数定义一次，使用 foldList 函数再定义一次。
任务 3： 我向你展示 List Unit 类型，其中 Unit 是单例类型，记作 $1$（一个只有一个值的类型）。画出 List Unit 的值，直到画满空间。
好的，它们在这里（我们将只画出最终结果，不画箭头）。
任务 4： List Unit 类型实际上与我们这里回顾过的另一个类型同构。找出是哪一个。
它与自然数类型（Nat）同构。List 和 Nat 都是归纳类型，两者之间唯一的区别是，List 的归纳构造器 Cons 由一个类型参数化，即对于该类型的每个值都有一个构造器，而 Nat 只有一个 Succ 构造器。因此，一个只有一个值的类型（如 Unit）的列表，与 Nat 同构。
任务 5： 写一个 Tuple 的构造器。为 Either 写一个 fold 函数。
首先是元组的构造器。这非常直接，为了能够有输出 a 和 b 的函数，你必须在构造器中输入一个 a 和一个 b。
data Tuple a b where
Tuple :: forall a b. a -> b -> Tuple a b
Either 的 fold 函数也很直接，尽管第一眼看上去可能并非如此：顾名思义，一个 Either a b 要么是一个 a，要么是一个 b，所以为了转换 Either a b -> c，你必须提供 (a -> c) 和 (b -> c)。
foldEither :: forall a b c. (a -> c) -> (b -> c) -> Either a b -> c
foldEither fa fb (Left val) = fa val
foldEither fa fb (Right val) = fb val
任务 6： 除了 Tuple 之外，还有一种非常重要的负类型，我们将在本章（以及各种其他地方）介绍它。
它就是函数类型。我们可以将函数视为“可以被求值的对象”，这意味着，像元组一样，它们由其项消去规则表征：一个函数 a -> b（连同值 a）可以被化简为一个值 b。
任务 7： 写出自然数类型的 Church 编码版本
如下所示
$$ \begin{aligned} \mathsf{type}\ \mathbb{N} & = \forall b . b \rightarrow (b \rightarrow b) \rightarrow b \\ \mathsf{zero} & : \mathbb{N} \\ \mathsf{zero}\ z\ s &= z \\ \mathsf{succ} & : \mathbb{N} \rightarrow \mathbb{N} \\ \mathsf{succ}\ n\ z\ s &= s\ (n\ z\ s) \end{aligned} $$
$$ \begin{aligned} \mathsf{foldNat} & : \forall a b . b \rightarrow (b \rightarrow b) \rightarrow \mathbb{N} \rightarrow b \\ \mathsf{foldNat}\ z\ s\ n &= n\ z\ s \end{aligned} $$
任务 8： 使用自然演绎定义布尔类型的消去规则。
以类型规则表达的消去规则（即 $\mathsf{ifElse}$ 函数）如下：
$$ \frac{\Gamma \vdash b : \mathsf{Bool} \quad \Gamma \vdash x : a \quad \Gamma \vdash y : a}{\Gamma \vdash \mathsf{ifElse}\ b\ x\ y : a} $$
给定一个布尔值 $b$，以及某个类型 $a$ 的两个值，我们可以产生一个类型为 $a$ 的值。
术语表
| 原文 | 中文 |
|---|---|
| abstraction | 抽象 |
| Alonzo Church | 阿隆佐·邱奇 |
| application | 应用 |
| arrow types | 箭头类型 |
| axiom of pairing | 配对公理 |
| Bicartesian Closed Category | 双笛卡尔闭范畴 |
| Boolean type | 布尔类型 |
| C-monoids | C-幺半群 |
| canonical function | 规范函数 |
| Cartesian Closed Monoid | 笛卡尔闭幺半群 |
| category of types | 类型范畴 |
| Church encoding | Church 编码 |
| colimit | 余极限 |
| composite types | 复合类型 |
| conclusion | 结论 |
| constructor | 构造器 |
| Curry-Howard-Lambek correspondence | Curry-Howard-Lambek 对应 |
| currying | 柯里化 |
| Elementary Theory of the Category of Sets | 集合范畴的初等理论 |
| Generalized Algebraic Datatypes (GADTs) | 广义代数数据类型（GADTs） |
| Gerald Jay Sussman | Gerald Jay Sussman |
| global element | 全局元素 |
| Harold Abelson | Harold Abelson |
| image function | 像函数 |
| implication object | 蕴涵对象 |
| inductive type | 归纳类型 |
| intuitionistic logic | 直觉主义逻辑 |
| isomorphic | 同构 |
| Jean-Yves Girard | Jean-Yves Girard |
| Julie Sussman | Julie Sussman |
| kind | kind |
| kinding rules | kinding rules |
| Lambda Calculus | Lambda 演算 |
| limit | 极限 |
| linked list | 链表 |
| modus ponens | 假言推理 |
| monoids | 幺半群 |
| monomorphic | 单态 |
| naive | 朴素 |
| naive set theory | 朴素集合论 |
| natural deduction | 自然演绎 |
| natural numbers type | 自然数类型 |
| negative types | 负类型 |
| partial functions | 偏函数 |
| polymorphic functions | 多态函数 |
| Polymorphic Lambda calculus | 多态 Lambda 演算 |
| positive types | 正类型 |
| premise | 前提 |
| product constructors | 积构造器 |
| propositional function | 命题函数 |
| range of significance | 意义范围 |
| range of truth | 真值范围 |
| recursive type | 递归类型 |
| Russell | 罗素 |
| set theory | 集合论 |
| Simply-typed lambda calculus | 简单类型 lambda 演算 |
| singleton type | 单例类型 |
| System F | System F |
| term elimination rule | 项消去规则 |
| term introduction rule | 项引入规则 |
| terms | 项 |
| the axiom of union | 并集公理 |
| theory of types | 类型理论 |
| Tuples | 元组 |
| type abstraction | 类型抽象 |
| type application | 类型应用 |
| type constructor | 类型构造器 |
| type formation rule | 类型形成规则 |
| type systems | 类型系统 |
| type theory | 类型理论 |
| type-level arrows | 类型级箭头 |
| type-level variables | 类型级变量 |
| types | 类型 |
| typing context | 类型上下文 |
| typing environment | 类型环境 |
| typing rules | 类型规则 |
| uncurrying | 反柯里化 |
| universe of types | 类型宇宙 |
| Untyped Lambda calculus | 无类型 Lambda 演算 |
| value-level arrows | 值级箭头 |
| Zermelo–Fraenkel set theory | Zermelo–Fraenkel 集合论 |
| ZFC | ZFC |
此文章由 AI 翻译