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

我以此题目在2012年11月的伦敦Haskell会议上做了演讲。演讲的视频见 YouTube ，幻灯片见 GitHub 。

在本系列文章中，我将在不提及范畴论和高等数学的情况下解释Haskell的数据类型为什么被称为 代数的。

你高中所学的代数始于数字（例如：1、2、3……）和运算符（例如：加法和乘法）。运算符给你一种组合数字并从中产生新数字的方法。例如：将1和2通过加法运算结合起来将得到一个新数字3，我们通常将这个事实表述为

1 + 2 = 3

当你稍微长大一点之后，你会学到能够代替数字的变量（例如： $x$ 、 $y$ 、 $z$ ……）。在你更大一些之后，你会知道一些代数遵循的法则，诸如

\begin{aligned} 0 + x &= x \\ 1 \cdot x &= x \end{aligned}

它们对于 $x$ 的任何值都成立。此外还有一些其它的规则来定义数字和运算的性质。

当数学家们谈论代数时，他们意味着的是比这更普遍的东西。一个数学上的代数包含三个部分：

对象是代数的“事物”。对象的集合定义了我们要讨论的是什么。
运算给出将旧事物结合成新事物的方法。
规则是对象和操作间的关系。

在中学的代数中，数字是对象，而加法、乘法和友谊是运算。

Haskell类型的代数

在Haskell类型的代数中，对象是类型，例如 Bool 和 Int。运算符从已有的类型中产生新的类型。一个实例是类型构造子 Maybe 。它本身不是类型，但你可以使用它产生类型 —— 例如 Maybe Bool 和 Maybe Int，而它们是类型。另一个例子是 Either，它从两个旧有类型中产生新类型 —— 例如 Either Int Bool。

计数

通过对类型可能具有的值进行计数，我们可以看到它与我们熟悉的数字代数的联系。我们取 Bool 的定义为

1	data Bool = False \| True

一个类型为 Bool 的对象有两种可能的取值 —— 它要么是 False 要么是 True （技术上来讲，它还有可能会是 undefined ，但我会在后文中忽略这个事实）。不严谨地说，类型 Bool 就对应于数字代数中的“2”。

如果说 Bool 是2，那么什么是1呢？它应当是一个只有唯一取值的类型。在计算机科学文献中，这种类型通常称为 Unit 并有如下定义

1	data Unit = Unit

在Haskell中已经存在一种只有唯一取值的类型了 —— 它是 () （读作“Unit”）。你不能自己定义它，但如果你可以，它大概长这样

1	data () = ()

使用这种计数方法类推，Int 对应于数字 $2^{32}$ ，这正是类型 Int 所具有的值的数目（至少在我的机器上是这样的）。

加法

原则上我们可以有对应于3、4、5等等的类型。有时我们可能真的需要这样做 —— 比如对应于7的类型可以用于编码一周的七天。但是，如果我们可以从旧的类型建立起新的类型岂不是更好。这就需要我们请出代数中的运算符

一个对应于加法的类型是

1	data Add a b = AddL a \| AddR b

也就是说，类型 $a+b$ 是一个具有标签的联合体^[1]，它可以是 $a$ 或 $b$ 。要了解为什么这对应于加法，我们可以重新审视一下计数法。让我们假设 $a$ 是 Bool 而 $b$ 是 ()，那么 $a$ 有2种取值而 $b$ 有1种取值。至于类型 Add Bool () 有多少种取值呢？我们可以将他们列出一个表：

1	addValues = [AddL False, AddL True, AddR ()]

这其中有三个值，而 3 = 2 + 1 。这通常被称为是一个 和类型。在Haskell中，和类型通常使用 Either，它的定义为

1	data Either a b = Left a \| Right b

但我坚持使用 Add。

乘法

一个对应于乘法的类型是

1	data Mul a b = Mul a b

也就是说，类型 $a\cdot b$ 是一个容纳 $a$ 和 $b$ 的容器。通过计数法可以证明其与乘法间的对应关系 —— 如果我们把 $a$ 和 $b$ 都定为 Bool，那么类型 Mul Bool Bool 可能的值为

1	mulValues = [Mul False False, Mul False True, Mul True False, Mul True True]

这其中有四个值，即 $4 = 2 \times 2$ 。这通常被称为 积类型。在Haskell中乘积是序对类型：

1	data (,) a b = (a, b)

但我坚持使用 Mul。

零

使用加法和乘法我们可以产生任何1以上的数字所对应的类型 —— 但是0呢？它应当是一个没有任何值的类型。这听起来很奇怪，但你可以定义这样的类型：

data Void

注意到在数据的定义中没有构造子，因此无法构造 Void 类型的值 —— 它有零个值，这正是我们想要的！

Haskell类型的代数中的规则

我们前面定义的类型有什么规则？就如同数字代数里那样，有一道规则能够断言两个对象是否相等 —— 在我们这，对象就是指类型。

然而，当我谈论到 相等性 时，我的意思不是Haskell中函数 (==) 的意义下的相等，而是两种类型之间存在着一一对应的关系 —— 也就是说，当我说 $a$ 和 $b$ 两种类型相等时，我的意思是你可以写出两个函数

1 2	from :: a -> b to :: b -> a

它将 $a$ 的值与 $b$ 的值配对，因此下面的等式总是成立的（这里的 == 是真正的Haskell式的相等）

1 2	to (from a) == a from (to b) == b

比如，我认为类型 Bool 与类型 Add () () 等价的。因为我可以通过如下的函数证明它们的等价性：

to :: Bool -> Add () ()
to False = AddL ()
to True  = AddR ()

from :: Add () () -> Bool
from (AddL _) = False
from (AddR _) = True

后面，我会使用三等号，===，来表示类型之间的这种等价关系。

加和类型的运算法则

加法有两条运算规则：

1	Add Void a === a

意即类型 Add Void a 与类型 a 具有相同数目的值，而

1	Add a b === Add b a

意味着你求和是什么次序无关紧要。这可以两条法则写成你可能更为熟悉的算数代数的形式

\begin{aligned} 0 + x &= x \\ x + y &= y +x \end{aligned}

假如你喜欢做练习，你可以在 Haskell 代数中证明上述法则的正确性 —— 无论是采用计数法，还是通过写出 from 和 to 函数。

乘积类型的运算法则

乘法有三个有用的法则：

1	Mul Void a === Void

意味着任何类型与 Void 相乘，你都会得到 Void ，

1	Mul () a === a

意即与 () 不改变任何东西，而

1	Mul a b === Mul b a

意味着你做乘积是什么次序无关紧要。这些法则更让人熟悉的形式是

\begin{aligned} 0 \cdot x &= 0 \\ 1 \cdot x &= x \\ x \cdot y &= y \cdot x \end{aligned}

两个小练习：（1）证明上述法则在 Haskell 代数中的有效性，（2）解释为什么我们不需要下面这样的法则

1 2	Mul a Void === Void Mul a () === a

此外，我们还有一条联系加法和乘法运算的法则：

1	Mul a (Add b c) === Add (Mul a b) (Mul a c)

这一条推理起来可能有点棘手，但写出对应的 from 和 to 函数并不太难。这条法则的算术版长得比较友好

a \cdot (b + c) = a \cdot b + a \cdot c

它被称为分配律。

函数类型

除了像 Int 和 Bool 这样的实体类型，Haskell 中还有函数类型，如 Int -> Bool 或 Double -> String 。如何将它们也纳入到这种代数里面？

为了解决这个问题，我们重新回到计数法。类型 $a\rightarrow b$ 包含多少种函数？

让我们具体来看，把 $a$ 和 $b$ 都定为 Bool。值 False 可以映射到 True 或者 False，对于值 True 也是如此 —— 因此，有 $2 \cdot 2 = 2 ^{2} = 4$ 种可能的 Bool -> Bool 函数。为了真正的明确它们，我们可以将其枚举如下

f1 :: Bool -> Bool -- 等价于 'id'
f1 True  = True
f1 False = False

f2 :: Bool -> Bool -- 等价于 'const False'
f2 _     = False

f3 :: Bool -> Bool -- 等价于 'const True'
f3 _     = True

f4 :: Bool -> Bool -- 等价于 'not'
f4 True  = False
f4 False = True

如果 $b$ 仍然是（只有两个值的）Bool 类型，而 $a$ 是具有三个值的类型，如

1	data Trio = First \| Second \| Third

那么每个 First 、Second 和 Third 可以映射到两个可能值，因而总共有 $2 \cdot 2 \cdot 2 = 2^{3} = 8$ 种 Trio -> Bool 类型的函数。

采用同样的方法可以得到一般的规律。如果 $A$ 是类型 $a$ 的值的个数， $B$ 是类型 $b$ 的值的个数，那么类型 $a\rightarrow b$ 值的个数为

B^{A}

这说明了使用 指数类型 作为函数类型的常用术语的理由。

函数的运算法则

这里有两条关于单位类型的函数类型的运算法则。它们是

1	() -> a === a

这意味着有和类型 a 的值一样多的函数 () -> a ，以及

1	a -> () === ()

这意味着只存在唯一的一个函数 a -> () —— 特别地，它就是 const () 。这两条规则的算术形式是

\begin{aligned} a^{1} &= a \\ 1^{a} &= 1 \end{aligned}

还有允许提取出共同参数的法则：

1	(a -> b, a -> c) === a -> (b,c)

其算术形式为

b^{a} \cdot c^{a} = (bc)^{a}

以及关于返回其它函数的函数

1	a -> (b -> c) === (b,a) -> c

其算术形式为

(c^{b})^{a} = c^{b \cdot a}

当右侧部分的变量顺序切换，同时删除左侧的括号后，最后这条法则可能会变得更为令人熟悉

1	a -> b -> c === (a,b) -> c

这也就是我们所谓的柯里化和非柯里化的函数。再说一次，通过写出对应的 from 和 to 函数来证明所有的这些法则是一项有趣的练习。

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

此处原文为 “… the type a + b is a tagged union …” 。具有标签的联合体（tagged union）这个翻译可能不是很准确，但网上也没找到其它合适的翻译，特此注明。 ↩︎