最近这里有点安静！我几乎把所有写作时间都花在了Logic for Programmers上，整个脑子都变成书的形状了。相信我，你肯定不想看我那篇长达 2000 字、关于 Sphinx 构建后 LaTeX 定制的抱怨。但过去一周我一头扎进了历史的兔子洞，挖到了些东西，必须分享一下。

一切始于Algebraic [Data] Types are not Scary, Actually。那篇文章更详细地介绍了 AlgDT¹，这里先做个快速概览：

• 积类型像是 (Int, Bool) 或 Dog(name: str, owner: Person, age: Int) 这样的类型。它们在每个字段上都有一个值。几乎所有现代语言都有积类型，通常叫作“结构体”或“记录”或“值对象”之类。

• 和类型是“带标签联合”，像是 Int + Nothing、Result + ErrorType 或 Address + Number + Email 这样的类型。它们是在若干选项中做选择。“标签”意味着我们不会合并重叠的选项。Bool + Bool 有四种可能的值，通俗地说就是 Left True, Right True, Left False, Right False。在现代编程语言中，除了函数式编程和像 Rust 这样的少数领域外，和类型相对少见。

这些名字是怎么来的？常见的解释是源于它们的基数（可能取值的数量）：如果 #T 表示类型 T 的基数，那么 #(S + T) == #S + #T 且 #(S, T) == #S * #T。如果你不太确定，可以拿 Bool + Weekday 和 (Bool, Weekday) 试试。

但也可能是因为类型的“和”与“积”在行为上就像数字的加法与乘法！我觉得这点算得上众所周知，只是在介绍 AlgDT 的文章里很少提及。例如：数字的加法满足结合律，即 a + (b + c) == (a + b) + c。这告诉我们 Int + (String + Null) 与 (Int + String) + Null 是同构（≅）的：我们可以在这两种类型之间转换值而不丢失任何有用信息。

一个更有意思的例子是，AlgDT 满足分配律 a*(b + c) == a*b + a*c。如果我们有一个类型为 Account(name: str, contact: (Email + Phone)) 的值，就可以把它转换成类型为 EmailAccount(name, email) + PhoneAccount(name, number) 的值。这相当巧妙！

于是我产生了好奇：到底是 AlgDT 的哪一条性质让“和”与“积”得名的，又有哪些性质是后来才被发现的？随着研究的深入，这篇博客逐渐膨胀，最终成了一篇关于代数数据类型的早期历史。

寻找源头

通常要追溯术语的起源简直是噩梦，但这属于典型的学术圈故弄玄虚，所以相关内容总能在某篇论文里找到。我常用的有两种研究方法：

1. 找一篇肯定用过这些术语的论文，看它引用了什么，再去读那些被引用的论文，如此反复
2. 去ACM 数字图书馆搜索一个术语，然后从最早的论文开始一篇篇读起。²

通常我发现把两种方法结合起来效果最好。最终我找到了约翰·麦卡锡（LISP 的发明者）的“A Basis for a Mathematical Theory of Computation”，发表于 1961 年。就我所能查到的来看，这是对 AlgDT 最早的论述，无论以何种形式。

麦卡锡的论文

首先，这篇论文完全没有使用（计算机科学意义上的）“类型”或“代数”这些词，甚至严格说来也不是在讲计算机科学。但它确实讨论了“通过给定的基础空间来定义新的数据空间的方法”，其中一种新的数据空间就是“真值的 Π，其仅有的元素是 T（真）和 F（假）”，也就是布尔值。不过他肯定是熟悉类型的，毕竟是ALGOL-60 委员会的成员，所以我猜他在这里是刻意回避了“类型”这个词。

整篇论文讨论的是程序函数及其性质的一个简单数学模型。在第 2.6 节，他定义了两种从已有数据空间生成新数据空间的方式：

1. 两个集合 A 和 B 的笛卡尔积 A × B 是所有有序对 (a · b) 的集合，其中 a ∈ A 且 b ∈ B。如果 A 和 B 是有限集，且 n(A) 和 n(B) 分别表示 A 和 B 的元素个数，那么 n(A × B) = n(A) · n(B)。

毫不意外，积类型正是以笛卡尔积命名的。记录 Dog(name: str, owner: Person, age: Int) 就是笛卡尔积 Str × Person × Int 的带标签版本。在这里我们也看到，用我们的行话来说，#(A, B) == #A * #B。

1. 集合 A 和 B 的直接并 A ⊕ B 是两个互不相交集合的并，其中一个与 A 一一对应，另一个与 B 一一对应。如果 A 和 B 是有限集，那么 n(A ⊕ B) = n(A) + n(B) 即使 A 和 B 相交也是如此 [为原文强调]。A ⊕ B 的元素可以写成来自 A 或 B 的元素，并以下标标明其来源集合，即 a_A 或 b_B

据我所知，“直接并”是麦卡锡首创的说法，但它完全对应于不交并。麦卡锡随后将这两者称为“直接和与笛卡尔积”。他并没有把它们命名为“和类型与积类型”，但我认为，它们的名字源于对应的不交并和笛卡尔积这两种集合运算，是可信的。至于那些集合运算本身的名字历史，我就不深究了，不过我猜它们也是类比算术中的加法与乘法而得名的。

在定义直接和与笛卡尔积后不久³，麦卡锡又定义了数据空间之间的同构：

我们不会把集合 A × (B × C) and (A × B) × C 视为同一个集合，但它们之间存在一个典范的一一映射……我们将写作 (A × B) × C ≅ A × (B × C) 来表示这些集合是典范同构的。

接着他展示了若干同构，包括我觉得非常巧妙的分配律 A × (B ⊕ C) ≅ A × B ⊕ A × C。这些“代数数据类型”的所有性质从一开始就已被知晓，即便当时还没有这样称呼它们。

就是从这里传播开的吗？

在研究过程中，我发现了一篇奇怪的文章，叫“Some Observations Concerning Large Programming Efforts”（1964）。作者几乎在敏捷宣言提前 50 年就提出了敏捷宣言的思想！却从未有人引用过它，作者也再没有发表过其他东西。

我想说的是，就算你是第一个想到某个点子的人，如果没人听说过，那也无关紧要。

那么，让我们继续追溯代数类型的演进。1964 年，麦卡锡发表了Definition of new data types in ALGOL x。⁴他在其中提议在下一版 ALGOL 中加入两种新类型——“笛卡尔”与“联合”。值得注意的是，这是我们第一次看到“带标签”的代数类型，即和类型与积类型都带有字符串标签。ALGOL-68 后来实现了这两者，但在语言史上却是一个奇特的死胡同，对现代编程语言几乎没有产生什么影响。

历史从这里开始变得错综复杂。为了寻找下一步线索，我找到了两篇引用过麦卡锡的重要论文：托尼·霍尔的Notes on Data Structuring（1970）和罗德·伯斯托尔的Proving properties of programs by structural induction（1968）。它们分别对应着命令式语言与函数式语言的分流，因此我将分开讨论。

霍尔的论文

霍尔似乎是独立想出了和类型与积类型的概念。在“A contribution to the development of ALGOL”（1966）中，他提出了用“类”作标签的记录，以及用 union 关键字将互不相交的类合并为单一超类型的方案。不过，他并未给出记录或联合的任何代数性质。到了《Notes on Data Structuring》时，他的术语已经转向与麦卡锡保持一致：

我们所关心的类型，正是数学家们早已熟悉的那些，即笛卡尔积、可辨识联合、集合、函数、序列和递归结构。

他的“笛卡尔积”和“可辨识联合”都是带标签的，与我们今天使用代数类型的方式一致。由于他主要关注数据存储，并未列出任何代数性质，但作为如何最有效地存储这些类型的讨论的一部分，他确实提到了它们的基数。

这篇论文也可能是首次将和类型作为在编译期检测错误的手段来讨论：

如果程序员试图将一个可辨识联合的值转换回它并非来源的那个类型，这是一个严重的编程错误，可能导致无意义的结果。这种错误只能通过运行时检查来检测，即在每次显式或隐式调用此类转换时检查标签字段。这样的检查既耗时，一旦失败又极不方便。因此，我们寻求一种记法技巧，能够保证这种错误绝不会在运行的程序中出现；而这种保证仅通过检查程序文本即可给出，无需了解任何运行时处理的值。如果有自动化的编译器，这样的保证就可以由编译器提供。

这也是我能找到的、首次有人把和类型称为“可辨识联合”的地方。⁵随后芭芭拉·利斯科夫用“可辨识联合”来描述 CLU 的 oneof 和类型，尼克劳斯·维尔特则用“可辨识联合”来解释Pascal 为何没有和类型。正因如此，我推测命令式语言世界最初是从霍尔的这次讲座中了解到和类型的，而霍尔则受到了麦卡锡的影响（但并非完全源于他）。⁶

在此之后，和类型便从命令式编程中消失了。20 世纪后期的命令式语言主要受 Pascal 和 C 的影响。Pascal 没有和类型，是因为维尔特认为它们不如无标签联合灵活。C 可能没有和类型，则是因为它沿用了 IBM 的 PL/I 的类型系统。PL/I 于 1964 年首次发布，拥有积类型（当时称为 structs），但只有无标签联合。近年来的命令式语言反而是从函数式编程世界重新引入了和类型，这就又把我们带回到“Proving properties of programs by structural induction”。

伯斯托尔的论文

研究伯斯托尔让人非常头疼。他的讣告列出了数量庞大的论文和极具影响力的学生，可见他在函数式编程的早期发展中扮演了重要角色。但这些论文中极少能在网上找到，因此我能轻松查到的资料存在巨大空白。以下是我尽力还原他在历史中的作用的尝试。

这篇论文讨论的是如何证明递归类型（如列表和树）的性质。他是这样定义列表的：

我建议，每个构造操作都引入一种新类型，而这些类型的析取也应是类型，（大致遵循 Landin 1964）

一个 cons 拥有一个原子和一个列表，一个 nil 没有组成部分，一个 list 是 cons 或 nil。

伯斯托尔说他的记法来自 P. J. 兰丁的“The Mechanical Evaluation of Expressions”（1964）。兰丁的用法似乎并不完全是和类型——不清楚他是否有机制在类型取值重叠时加以区分。相反，在我看来，伯斯托尔“遵循”的只是兰丁书写递归定义的方式。不过，仅凭几次阅读很难下定论，我也完全可能是错的。

不过伯斯托尔确实拥有和类型，这一点可以从他对树的定义中看出。一棵树是“一个 node 或一个 tip 或一个 niltree”，但一个 tip 是“拥有一个 item”，而非“就是一个 item”。随后，他给出了这样的伪代码：

cases t:
    niltree(): nil()
    tip(i): i::nil()
    node(t1, i1, i2): concat(flatten(t1), flatten(t2))

伯斯托尔还说他的想法“基于约翰·麦卡锡的工作”，并引用了那篇数学理论论文。伯斯托尔受到麦卡锡“直接并”概念的启发，也并非不可能。

截至 2025 年，这篇论文已被引用超过 500 次。伯斯托尔后来还作出了更大的贡献，但那要到 1980 年，所以我们得先讲 ML。

米尔纳的论文

到目前为止，我们已经看到了代数数据类型的定义以及“笛卡尔积”的常见用法，但还没有出现“和类型”和“积类型”这些术语。就我所知，这些术语来自罗宾·米尔纳的ML，具体见于“A Theory of Type Polymorphism in Programming”（1977）：

ML 的完全确定类型（即单态类型）是由一组基础类型（int、bool 等）通过二元中缀运算符 x（笛卡尔积）、+（不交和）与 ->（函数类型）以及一元后缀运算符 list 构造而成的。

关于这篇论文有几点值得注意。首先，它当然是用“不交和”来描述类型的构造，并使用了 + 符号。其次，与霍尔和麦卡锡不同，它既没有对“不交和”作解释，也没有给出定义。到这个时候，对米尔纳的读者而言，这或许已是常识。最后，论文声称和类型与积类型在 ML 中已至少实现了两年。

我们没有最早版本 ML 的完整规范，但我们有 ML 所服务的 LCF 证明器的已发布源代码。相关代码在files.ml 中：

let instintype insttylist ty = inst ty whererec inst ty =
    fst(revassoc ty insttylist)
    ?(failwith phylumoftype ty
   ??``consttype vartype`` ty
   ??``funtype`` mkfuntype((inst # inst)(destfuntype ty))
   ??``sumtype`` mksumtype((inst # inst)(destsumtype ty))
   ??``prodtype`` mkprodtype((inst # inst)(destprodtype ty))
     )  ;;

看，这就是“和”与“积”类型！不过它们还不是带标签的。李耀夏的文章Where does the name “algebraic data type” come from?提到“早期版本并未包含数据类型（见爱丁堡 LCF 的第一版）”，我理解这指的是带标签的代数类型；ML 有 abstype 关键字用于为构造出的类型命名。你可以把 EmailOrAddress 定义为 Str + Str，但无法把左边的 Str 称为“email”。

《“A Theory of Type Polymorphism in Programming”》并未引用麦卡锡的论文，也没有引用霍尔或伯斯托尔的论文，因此不清楚米尔纳是受到了他们的影响，还是独立发展出了 AlgDT。有一些初步证据来自后续论文“A Metalanguage for Interactive Proof in LCF”（1978），他在其中感谢了三位人士的贡献：

我们感谢 Dana Scott 为我们的工作提供了大部分理论基础；感谢约翰·麦卡锡在斯坦福对本项目前身的鼓励；感谢 Richard Weyhrauch 对该项目作出的巨大贡献；感谢托尼·霍尔和 Jerry Schwarz 在 ML 抽象类型概念上的帮助；感谢 Avra Cohn 在最终设计阶段通过实验给予的帮助；感谢罗德·伯斯托尔及爱丁堡的众多同事富有启发性的讨论。

好了，还剩三门语言要讲。

Hope、VAX ML 与 Miranda

大约在这一时期，伯斯托尔正将范畴论应用于软件规约，最终促成了 HOPE 的诞生。“HOPE: An experimental applicative language”（1980）标志着带标签联合首次被引入函数式编程，但带标签积类型尚未出现：

要定义一个“数字树”类型，我们可以这样写

data numtree == empty ++ tip(num) ++ node(numtree#numtree)

（符号 # 表示类型的笛卡尔积。）

除此之外，这篇论文还引入了几个重要思想。第一是编译器可以穷尽地检查和类型中的所有互斥分支是否都已被处理：

每种数据类型都将拥有一组互不相交的子类型，每种子类型对应不同的构造器函数；例如，列表由 cons 或 nil 构造。针对这些构造器进行分支分析应当是容易的，编译器也应能轻易检查这种分析是否穷尽。这可以避免诸如忘记对空列表进行检测之类的错误。

此外，论文还提出，通过模式匹配可以极大地简化对和类型的使用。这并非结构化模式匹配在编程语言中的首次出现（Prolog 最早拥有它），但却是模式匹配在函数式编程中的首次亮相。

与 HOPE 大致同时，伯斯托尔的再传弟子卢卡·卡尔代利⁷正致力于将 ML 移植到 VAX 和 Unix，并在这一过程中加入了记录类型和变体类型。据我所知，这是带标签的和类型与带标签的积类型首次同时出现在函数式编程语言中。

所有这些思想后来都被纳入Standard ML，奠定了人们今天所认为的代数类型的核心特性：标签、基于编译器的穷尽性检查以及模式匹配。

最后，再次引用李耀夏的观点，“Miranda: A non-strict functional language with polymorphic types”（1985）是首篇真正使用“Algebraic Data Type”这一术语的论文。强烈推荐阅读李耀夏的文章以了解更多信息。

一个非常不牢靠的小结

• 麦卡锡在论文中首次提出了代数数据类型的概念与性质，尽管他并未如此称呼。
• 这至少对托尼·霍尔和罗德·伯斯托尔产生了一定影响，他们各自写出了有影响力的论文。
• AlgDT 在 ALGOL-68、CLU 和 ML 中得到了实现。尚不清楚米尔纳是否了解麦卡锡的理论，但我倾向于认为他很可能知道。
• Pascal 和 C 阻碍了和类型在命令式编程中立足。
• 伯斯托尔和卢卡·卡尔代利补全了 AlgDT 的主要特性，使其成为类型化函数式编程的基石。

这已是我在现有时间和资源下能做到的最好程度。如果你发现任何错误，请告诉我！

如果你喜欢这篇文章，欢迎订阅我的新闻通讯！我每周都会在那里发布新文章。

我为企业提供形式化方法培训，让软件开发更快、更便宜、更安全。点击这里了解更多。