【翻译】代数数据类型的代数结构（中）

原文链接

我以此题目在2012年11月的伦敦Haskell会议上做了演讲。演讲的视频见 YouTube ，幻灯片见 GitHub 。这篇是系列的第二部分；你可以在这里阅读第一部分

上一次我介绍了单位类型 Unit 或者 () 以及零类型 Void 。我同时还介绍了类型运算符 Add 和 Mul ，以及函数类型 a->b 。

在这篇文章中，我将同时使用Haskell记号和数学记号。下面这个表可以帮助你在这两者之间转换。

$$\begin{aligned} \operatorname{Void} && \leftrightarrow && 0 \\ () \,, \operatorname{Unit} && \leftrightarrow && 1 \\ \operatorname{Add} \; a \; b && \leftrightarrow && a + b \\ (a,b) \,,\; \operatorname{Mul} \; a \; b && \leftrightarrow && a \cdot b \\ a \rightarrow b && \leftrightarrow && b ^ a \end{aligned}$$

在这篇文章中我将着眼于递归类型，并展示如何在以各种方式使用类型代数来推导出关于类型的有趣事实。

Maybe 类型构造子

让我们通过探索 Maybe a 来放松一下。这表示它这个类型可能包含类型 $a$ 的一个值，也可能为空。它定义如下：

1

data Maybe a = Nothing | Just a

竖线表示这是一个和类型，所以如果我们已经定义了类型 Nothing 和 Just a ，我们可以使用我们上次定义的类型 Add 来写。它看起来就像下面这样：

1
2
3
4

data Nothing = Nothing
data Just a  = Just a

type Maybe a = Add Nothing (Just a)

看我们是怎么把 data 声明替换为 type 声明的？这意味着 Maybe a 不再是一个新类型 —— 而只是一个已知类型的同义词。

但我们可以更进一步。注意到 Nothing 只具有一个值，所以它等价于 () 。类似的，Just 是类型 $a$ 的一个单一值的容器，故它等价于 $a$ 。因而我们有

1

type Maybe a = Add () a

也就是说，Maybe $a$ 与 1 + $a$ 是一样的。Maybe 所做的事就是给一个类型添加一个可能的值。

递归类型

列表

Haskell中基本的列表是 链式表 。一个列表 $as$ 要么是空的，记作 [] ，要么是将单个 $a$ 附加到另一个列表 $as$ 上而构成的，记作 a : as 。如果我们想要自己定义一个列表，我们可以写成

1

data List a = Nil | Cons a (List a)

让我们来花点时间看一下这个声明的结构。和 Maybe 一样，List 类型是两种更简单类型的和。

加数是 Nil ，是一个等价于 () 的无参构造子。

被加数是 Cons a (List a) ，是一个包含 $a$ 和列表 $as$ 的乘积。

如果我们将列表写作 $L(a)$ ，那么它的代数形式是

$$L(a) = 1 + a \cdot L(a)$$

这好像意味着我们可以在Haskell中将列表类型写作

1

type List a = Add () (a, (List a))

但实际上这不能通过编译。其原因是类型别名会在类型检查之后，编译之前的编译期被展开。这个定义永远不会停止展开 —— 它会像下面这样一直展开

1

Add () (a, Add () (a, Add () (a, ...)))

等等。这不行的原因与Haskell处理递归类型定义的方式有关（和大多数具有复杂的类型系统的语言一样，它使用 同构递归类型而不是等同递归类型 ^[1] ）

它的方式是使用 newtype 声明替代 type 声明，并将类型包装在一个新的类型构造子 L 中：

1

newtype List a = L (Add () (a, List a))

这样只是为了满足类型检查器 —— 当代码被编译时，额外的构造子会被优化掉，我们所剩的与上面使用 type 的声明相同。

如果我们将类型 List a 写作 $L(a)$ ，那么这个列表的声明就是说

$$L(a) = 1 + a \cdot L(a)$$

为了看清列表 实际上 是什么，我们可以开始通过反复替代来展开定义。在展开式中，无论何时我看见了具有 $a\cdot a$ 形式的类型，我都会用 $a^2$ 替代以节省空间。

练习 ：表达式 $a^2$ 可以用序对 $(a,a)$ 或函数 $2\rightarrow a$ 表示。证明它们是一样的。

$$\begin{aligned} L(a) & = 1 + a \cdot L(a) \\ & = 1 + a \cdot (1 + a \cdot L(a)) \\ & = 1 + a + a ^ 2 \cdot (1 + a \cdot L(a)) \\ & = 1 + a + a ^ 2 + a ^ 3 \cdot (1 + a \cdot L(a)) \\ & = \ldots \\ & = 1 + a + a ^ 2 + a ^ 3 + a ^ 4 + a ^ 5 + \cdots \end{aligned}$$

这告诉我们 $a$ 的列表要么是空列表，要么是包含单个 $a$ 的列表，要么是包含两个 $a$ 的列表，要么是包含三个 $a$ 的列表，等等。也许你已经知道这一点 —— 但代数告诉我们的更加简洁！

但现在，这有一件确实很酷的事情。让我们从列表的方程式开始，而不是使用反复替代的方法，同时忘掉一会儿我们的对象是类型，并假装它们是任意的表达式。这意味着我们有理由使用任何我们喜欢的技巧来“求解 $L(a)$ ”。

首先在等式两边同时减去 $L(a)$ ：

$$L(a) - a \cdot L(a) = 1$$

然后分解出等式左侧的因子：

$$(1 - a) \cdot L(a) = 1$$

最后，两边同时除以 $1-a$ ：

$$L(a) = \frac{1}{1-a}$$

这看起来没有意义，因为我们不知道一个类型减去另一个类型是什么意思，也不知道一个类型除以另一个类型是什么意思。但是它一点有意思的事都不能告诉我们吗？

如果你学习过微积分，你也许记得许多函数都可以按照 泰勒级数 进行展开。我们可以 问一问 Wolfram Alpha $1/(1-a)$ 的泰勒级数是什么，然后它会告诉我们：

$$L(a) = 1 + a + a ^ 2 + a ^ 3 + a ^ 4 + \cdots$$

也就是说，$L(a)$ 的级数展开，恰恰就是我们通过反复替代化简得到的式子。尽管我们通过对类型进行了一些完全不合理的操作，极大地滥用了代数，但还是得到了一个合理的结果。

树

考虑节点处有值的二叉树。在Haskell中你可以像这样写

1

data Tree a = Empty | Node a (Tree a) (Tree a)

以一种可能令人熟悉的方式，我们可以将它看作两个类型的和 —— 一个等价于 () 的无参类型，和一个积类型。这一次它是三个项的乘积，但这并不是个问题 —— 我们可以使用嵌套的乘积，其形式为 (a, (b, c)) 。

根据我们所知道的运算关系（再一次，我们使用 newtype 来获得一个递归的定义），其定义为

1

newtype Tree a = T (Add () (a, (Tree a, Tree a)))

在代数的语言中，如果把 $T(a)$ 作为树的类型，我们可以写出

$$T(a) = 1 + a\cdot T(a)^2$$

为了更好地解决树是什么，我们可以采用与列表相同的方式进行重复替换，但那会更加麻烦。相对的，我们可以用重新排列方程的技巧来求解 $T(a)$ 吗？

首先，将所有东西移到方程的同一侧：

$$a \cdot T(a)^2 - T(a) + 1 = 0$$

我们可以看出它是关于 $T(a)$ 的 二次方程 ，因此我们可以使用二次方程求根公式求出

$$T(a) = \frac{1 - \sqrt{1 - 4 a}}{2a}$$

这比列表类型的方程更没意义。取一个类型的平方根是个什么意思？但是，不要慌张，我们再一次 问问 Wolfram Alpha 它的级数展开，然后它会告诉我们

$$T(a) = 1 + a + 2a ^ 2 + 5a ^ 3 + 14a ^ 4 + \cdots$$

那么我们如何理解它呢？前两项告诉我们，一个树可以是空的（如果它是 Empty ），或者可以有一个类型为 $a$ 的值（如果它是 Node a Empty Empty ）。

然后下一项告诉我们，一个树可以以两种不同的方式包含两个类型为 $a$ 的值。而再下一项告诉我们，一个树可以以五种不同的方式包含三个类型为 $a$ 的值。

但我们确实可以看出这些，如果我们枚举所有二叉树，并且将他们按所包含的值的个数分组。有一棵树没有值，有一棵树有一个值，有两棵树有两个值，有五棵树有三个值 —— 正如这个图片中描述的（从 Flajolet 和 Sedgewick 所著的优秀书籍 《解析组合数学》 中摘来的）。

方程能计算可以存在的不同二叉树的数目！这一计数属性与我们在第一篇文章中看到的简单计数实例有关，也与 组合种类（combinatorial species） ^[2] 有关，正如 Brent Yorgey 所写的有关拓展。种类（species）和类型（types）有许多的共同点，尽管它们并不是同一样东西。

七树合一（Seven Trees In One）

如果我们限制树只包含单位类型，例如 Tree () ，那么 $T(a)$ 中的 $a$ 就等于 1 ，然后我们可以写出树的定义式方程

$$T = 1 + T^2$$

通过代数方法，重复地使用公式 $T ^ 2 = T - 1$ ，我们可以化简为

$$\begin{aligned} T^6 & = (T-1) ^ 3 \\ & = T ^ 3 - 3T ^ 2 + 3T - 1 \\ & = T (T - 1) - 3T ^ 2 + 3T - 1 \\ & = - 2T ^ 2 + 2T - 1 \\ & = -2(T-1) + 2T - 1 \\ & = 1 \end{aligned}$$

当你把它解释为语言的类型时，这表示一个树的六元组与单位类型等价。换句话说，只存在一个树的六元组。

这显然是无意义的，那么是哪里出了问题呢？更神秘的是如果我们在等式两边同时乘 $T$ ，我们会得到

$$T ^ 7 = T$$

这并 不是 没有意义的 —— 它表明一个树的七元组和单个树等价。

乍一看，这不是一个深刻的结果。任何两个具有 可数无限多 个可能值的类型都是等价的 —— 这就是可数的意思。

然而，还有比这更巧妙的。在论文 七树合一（Seven Trees In One） 中，Andreas Blass 不仅展示了如何找到七个树到一个树的确切映射和逆映射（实质上，他就是告诉你如何写出前一篇所说的 from 和 to 函数），而且还表明，这些函数从来都不需要再任何树上深入四层以上。

最后，他解释了为什么 $T ^ 7 = T$ 是有效的，而 $T ^ 6 = 1$ 却不是。事实上，通过我上面给出的使用减法的方法，派生出类似的方法，你可以转换为不使用减法的“诚实的”证明，因此对于类型也是有效的 —— 但当你开始所用的 $T$ 的幂必须是一个大于6的倍数的幂。因此你可以将 $T ^ 7$ 化简为 $T$（因为 7 = 6 + 1 ），而不能将 $T ^ 6$ 化简为 1 。

一个解释？

如果你认为这篇文章提出的问题比提供的答案还要多，这是十分公正的。例如：

• 类型的减法、除法和开方是什么意思？
• 对于仍然具有意义、可计算、可解释的类型方程，我们还可以做什么？
• 为什么对类型方程进行不合理的操作却可以得到有意义的答案？

作为最后一个问题的预热，一个可以给类型建模的数学结构叫 半环 。这也就是说，你可以加或乘对象，并且你有对应于 0 和 1 的对象。这里有一篇 Marcelo Fiore 和 Tom Leinster 的论文，表明如果你从一个 复数 $T$ 开始，它由方程

$$t = p(t)$$

定义 ，其中 $p$ 是一个多项式，并且化简为

$$q_1(t) = q_2(t)$$

其中 $q_1$ 和 $q_2$ 不是常量（他们不能只是 1 ），那么同样的结果对于半环也是正确的。特别地，它对于类型也是正确的，也就是你可以找到一个不使用减法以及其它对于类型而言非法的运算的证明。

下一次，我将解释拉链（zippers）数据结构是什么，然后描述如何对类型进行微积分。