原文见 http://bartoszmilewski.com/2015/01/13/simple-algebraic-data-types/
-> 上一篇:『积与余积』
我们已经了解了两种类型组合方式:积与余积。编程中,仅通过这两种类型就可以构造出大部分数据结构。正是因为这一点,保证了数据结构的许多性质都是可复合的。例如,如果知道如何比较两种基本类型的值是否相等,并且知道如何将这种比较方法推广到积与余积类型,那么你就能够自动派生出支持相等运算的复合类型。在 Haskell 中,大部分复合类型能够自动继承相等比较、大小比较以及与字符串的相互转换等运算能力。
现在,我们先近距离的看看编程中的积类型与和类型。
编程语言中,对于两个类型的积,官方实现是序对(Pair)。在 Haskell 中,序对是基本的类型构造子;在 C++ 中,积表现为标准库中所定义的相对复杂一些的模板。
序对并非严格可交换的:不能用序对 (Bool, Int)
去替换序对 (Int, Bool)
,即使它们承载相同的信息。然而,在同构意义上,序对是可交换的—— swap
可给出这种同构关系:
swap :: (a, b) -> (b, a) swqp (x, y) = (y, x)
你可以将序对看作是采用了不同的格式存储了相同的数据,这有点像大根堆 vs 小根堆。
可以通过序对的嵌套,将任意个数的类型组合到积内,但是更简单的方法是利用:嵌套的序对与元组(Tuple)相等。因为嵌套的序对与元组是同构的。如果你想将 a
, b
, 与 c
这三种类型组合为积,有两种办法可以做到:
((a, b), c)
或
(a, (b, c))
这两种类型是不同的——你不能将其中一种类型传递给一个需要另一种类型的函数——但是它们所包含的元素是壹壹对应的。有一个函数可以将其中一种类型映射为另一种:
alpha :: ((a, b), c) -> (a, (b, c)) alpha ((x, y), z) = (x, (y, z))
并且,这个函数是可逆的:
alpha_inv :: (a, (b, c)) -> ((a, b), c) alpha_inv (x, (y, z)) = ((x, y), z)
因此,这是一种同构,即用了不同的方式封装了相同的数据。
可以将积类型的构造解释为作用于类型的一种二元运算。从这个角度来看,上述的同构关系看上去有些像幺半群中的结合律:
(a * b) * c = a * (b * c)
只不过,在幺半群的情况中,这两种复合为积的方法是等价的,而上述积类型的构造方法只是在『同构条件下』等价。
如果是在同构的条件下,不再坚持严格的相等性的话,我们可以走的更远,而且还能揭示 unit 类型 ()
类似于数字乘法中的 1
。类型 a
的值与一个 unit 值所构成的序对,除了 a
值之外,什么也没有包含。因此,这种类型
(a, ())
与 a
是同构的。如果不相信,我们可以为它们构造出同构关系:
rho :: (a, ()) -> a rho (x, ()) = x rho_inv :: a -> (a, ()) rho_inv x = (x, ())
如果用形式化语言描述这些现象,可以说 Set (集合的范畴)是一个 幺半群范畴 ,亦即这种范畴也是一个幺半群,这意味着你可以让对象相乘(在此,就是笛卡尔积)。以后我会再多讲讲幺半群范畴,并给出完整的定义。
在 Haskell 中有一种更通用的办法来定义积类型——特别是,过一会就可以看到,这种积类型可由加类型复合而成。这种积类型可以用带有多个参数的构造子来定义,例如可将序对定义为:
data Pair a b = P a b
在此, Pair a b
是由 a
与 b
参数化的类型的名字; p
是数据构造子的名字。要定义一个序对类型,只需向 Pair
类型构造子传递两个类型。要构造一个序对类型的值,只需向数据构造子 P
传递两个合适类型的值。例如,定义一个序对类型的值 stmt
,其对应的序对类型为 String
与 Bool
的积:
stmt :: Pair String Bool stmt = P "This statements is" False
上述代码的第一行是类型声明,即使用 String
与 Bool
类型替换了 Pair
泛型定义中的 a
与 b
。第二行向数据构造子 P
传递了具体的字符串与布尔值,从而定义了一个序对类型的值 stmt
。类型构造子用于构造类型;数据构造子用于构造值。
因为类型构造子与数据构造子的命名空间是彼此独立的,因此二者可以同名:
data Pair a b = Pair a b
如果你足够学究,就可以发现 Haskell 内建的序对类型只是这种声明的一种变体,前者将 数据构造子 Pair
替换为一个二元运算符 (,)
。如果将这个二元运算符像正常的数据构造子那样用,照样能创建序对类型的值,例如:
stmt = (,) "This statement is" False
类似的,可以用 (,,)
来创建三元组,以此类推。
如果不用泛型序对或元组,也可以定义特定的有名字的积类型,例如:
data Stmt = Stmt String Bool
这个类型虽然也是 String
与 Bool
的积,但是它有自己的名字与构造子。这种风格的类型声明,其优势在于可以为相同的内容定义不同的类型,使之在名称上具备不同的意义与功能,以避免彼此混淆。
在编程中,只依赖元组以及多参数的构造子会让代码混乱,容易出错,因为只能靠我们的脑袋来记忆各个数据成员的含义。若是能对数据成员进行命名,结果会好一些。支持数据成员命名的积类型也是有的,在 Haskell 中称为记录,在 C 语言中称为 struct
。
来看一个简单的例子:用两个字符串表示化学元素的名称与符号,用一个整型数表示原子量,将这些信息组合到一个数据结构中。可以用元组 (String, String, Int)
来表示这个数据结构,只不过需要我们记住每个数据成员的含义。现在要用一个函数检查化学元素符号是否为其名称的前缀(例如 He 是否为 Helium 的前缀),这需要通过模式匹配从元组中抽取数据成员:
startsWithSymbol :: (String, String, Int) -> Bool startsWithSymbol (name, symbol, _) = isPrefixOf symbol name
这样的代码很容易出错,并且也难于理解与维护。更好的办法是用记录:
data Element = Element { name :: String , symbol :: String , atomicNumber :: Int }
上述的元组与记录是同构的,因为二者之间存在可逆的转换函数:
tupleToElem :: (String, String, Int) -> Element tupleToElem (n, s, a) = Element { name = n , symbol = s , atomicNumber = a } elemToTuple :: Element -> (String, String, Int) elemToTuple e = (name e, symbol e, atomicNumber e)
注意,记录的数据成员的名字本身也是访问这些数据成员的函数。例如, atomicNumber e
从 e
中检出 atomicNumber
的值。也就是说, atomicNumber
是个函数:
atomicNumber :: Eelement -> Int
使用 Element
的记录语法去实现 startsWithSymbol
函数,可读性更好:
startsWithSymbol :: Element -> Bool startsWithSymbol e = isPrefixOf (symbol e) (name e)
还可以用一下 Haskell 的小花招,将 isPrefixOf
作为中缀运算符,可以让 startsWithSymbol
的实现几乎接近人类的语言:
startsWithSymbol e = symbol e `isPrefixOf` name e
原来的两对括号被省略了,因为中缀运算符的优先级低于函数调用。
就像集合的范畴中的积能产生积类型那样,余积能产生和类型。Haskell 官方实现的和类型如下:
data Either a b = Left a | Right b
类似序对, Either
在同构意义下是可交换的,也是可嵌套的,而且在同构意义下,嵌套的顺序不重要。因此,我们可以定义与三元组相等的和类型:
data OneOfThree a b c = Sinistral a | Medial b | Dextral c
可以证明 Set 对于余积而言也是个(对称的)幺半群范畴。二元运算由不相交和(Disjoint Sum)来承担,unit 元素由初始对象来扮演。用类型术语来说,我们可以将 Either
作为幺半群运算符,将 Void
作为中立元素。也就是说,可以认为 Either
类似于运算符 +
,而 Void
类似于 0
。这与事实是相符的,将 Void
加到和类型上,不会对和类型有任何影响。例如:
Either a Void
与 a
同构。这是因为无法为这种类型构造 Right
版本的值——不存在类型为 Void
的值。 Either a Void
只能通过 Left
构造子产生值,这个值只是简单的封装了一个类型为 a
的值。这就类似于 a + 0 = a
。
在 Haskell 中,和类型相当普遍,而 C++ 中的与之相对应的联合(Union)与变体(Variant)类型则不是那么常见。这是有原因的。
首先,最简单的和类型是枚举,在 C++ 中可以用 enum
来实现,在 Haskell 中与之等价的和类型是:
data Color = Red | Green | Blue
在 C++ 中相应的枚举类型为:
enum {Red, Green, Blue};
其实 Haskell 中还有更简单的和类型:
data Bool = True | False
它与 C++ 中内建的 bool
类型等价。
在 C++ 中,要控制一个值在和类型中出现与否,有各种各样的实现,需要借助一些特殊技巧以及一些『不可能』的值,例如空字串、负数、空指针等等。在 Haskell 只需使用 Maybe
类型即可解决这一问题:
data Maybe a = Nothing | Just a
Maybe
类型是两个类型的和。可以将两个构造子分开来看。只观察第一个构造子,其形态如下:
data NothingType = Nothing
它是一个叫做 Nothing
的单值的枚举。换句话说,它是一个单例,与 unit 类型 ()
等价。
第二个构造子
data JustType a = Just a
的作用就是封装类型 a
。
于是,我们可以将 Maybe
表示为:
data Maybe a = Either () a
在 C++ 中,更复杂一些的和类型往往要使用指针。一个指针可以为空,也可以指向某种特定类型。例如,Haskell 中的列表类型,它被定义为一个(递归)的和类型:
List a = Nil | Cons a (List a)
要将它翻译为 C++ 代码,需要使用空指针来模拟空列表:
template<class A> class List { Node<A> * _head; public: List() : _head(nullptr) {} // Nil List(A a, List<A> l) // Cons : _head(new Node<A>(a, l)) {} };
注意,上述 Haskell 代码中的构造子 Nil
与 Cons
,在 C++ 代码中对应于 List
构造函数的重载。虽然 List
类不需要用标签来区分和类型的两个成员,但是它需要用 nullptr
将 _head
弄成类似 Nil
这样的东西。
Haskell 与 C++ 类型之间主要的区别是 Haskell 的数据结构不可变。如果你使用特定的构造子创建了一个对象,这个对象会永远记住它是由哪个构造子创建的,以及这个构造子接受的参数是什么。因此由 Just "energy"
创建的 Maybe
对象,永远也不会变成 Nothing
。类似的,一个空的列表永远都是空的,一个有三个元素的列表永远有相同的三个元素。
正是这种数据的不变性使得数据的构造是可逆的。给定一个对象,你总是能够使用它的构造函数将它大卸八块。这种解构过程可以通过模式匹配来实现。
List
类型有两个构造子,因此任意一个 List
的解构可以使用与这两个构造子相对应的模式匹配来实现。一个模式可以匹配 Nil
列表,另一个模式可匹配 Cons
构造的列表。例如,下面是一个作用于 List
的简单函数:
maybeTail :: List a -> Maybe (List a) maybeTail Nil = Nothing maybeTail (Cons _ t) = Just t
maybeTail
定义的第一部分使用了 Nil
构造子作为模式,以 Nothing
作为结果返回。第二部分使用了 Cons
构造子作为模式,并使用通配符 _
对其第一个参数进行匹配,之所以如此,是因为我们对第一个参数不感兴趣。 Cons
的第二个参数值会被绑定到变量 t
上(虽然称之为变量,但事实上它们是永远都不变的:一旦它们被绑定到表达式,它们就不会再变化了),返回结果是 Just t
。你的 List
是如何创建的, maybeTail
总有一个『从句』能够与之相匹配。如果 List
是由 Cons
创建,那么 Cons
所接受的两个参数就会被 maybeTail
检出(第一个参数会被忽略)。
C++ 中可以通过多态类的继承方式实现更复杂一些的和类型。有共同祖先的类族可以看作是一个可变的类型,虚函数表的扮演了一个隐含的标签的角色。C++ 多态类是通过虚函数表查找要被调用的虚函数来实现多态,而 Haskell 总是可以基于构造子的模式匹配来完成同样的事。
很少看到 C++ 代码中会使用联合类型作为和类型,因为联合类型存在很多限制。譬如,你不能将 std::string
放入联合中,因为字符串具有 copy 构造函数。
积类型与和类型,单独使用其中一个就可以定义一些有用的数据结构,但是二者组合起来或更加强大。我们再度祭出复合的能量。
先总结一下到现在为止已经见识过的东西。我们已经见识了类型系统中两种可交换的幺半群结构:用 Void
作为中性元素的和类型,用 ()
作为中性元素的积类型。可以将这两种类型比喻为加法与乘法。在这个比喻中, Void
相当于 0
,而 ()
相当于 1
。
现在来思考如何增强这个比喻。例如,与 0 相乘的结果为 0 么?换句话说,一个积类型中的一个成员是 Void
,那么这个积类型与 Void
同构么?例如,是否存在一个 Int
与 Void
构成的序对?
要创建序对,需要两个值。 Int
值很容易获得,但是 Void
却没有值。因此,对于任意类型 a
而言, (a, Void)
是不存在的——它没有值——因此它等价于 Void
。换句话说, a * 0 = 0
。
另外一件事,加法与乘法在一起的时候,存在着分配律:
a * (b + c) = a * b + a * c
那么对于积类型与和类型而言,是否也存在分配律?是的,不过一般是在同构意义下存在。上式的左半部分相当于:
(a, Either b c)
右半部分相当于:
Either (a, b) (a, c)
下面给出一个方向的转换函数:
prodToSum :: (a, Either b c) -> Either (a, b) (a, c) prodToSum (x, e) = case e of Left y -> Left (x, y) Right z -> Right (x, z)
另一个方向的转换函数为:
sumToProd :: Either (a, b) (a, c) -> (a, Either b c) sumToProd e = case e of Left (x, y) -> (x, Left y) Right (x, z) -> (x, Right z)
case of
语句用于函数内部的模式匹配。每个模式后面是箭头所指向的可求值的表达式。例如,如果将下面的值作为 proToSum
的参数:
prod1 :: (Int, Either String Float) prod1 = (2, Left "Hi!")
case e of
中的 e
就等于 Left "Hi!"
,它会匹配到模式 Left y
,所以 y
就会被绑定到 "Hi!"。因为
x 已经匹配到
2 了,因此
case of 从句的结果,也就是整个函数的结果将会是
Left (2, "Hi!")`。
我不打算证明上面的这两个函数互逆,不过如果你对此有所疑虑,可以肯定的说,它们肯定互逆!因为它们只不过是将相同的数据用了不同的形式进行了封装。
数学家们为这种相互纠缠的幺半群取了个名字:半环(Semiring)。之所以不叫它们全环,是因为我们无法定义类型的减法。这就是为何半环有时也被称为 rig 的原因,因为『Ring without an n(negative,负数)』。不过,在此不关心这些问题,我们关心的是怎么描述自然数运算与类型运算之间的对应关系。这里有一个表,给出了一些有趣的对应关系:
列表类型相当有趣,因为它被定义为一个方程的解,因为我们要定义的类型出现在方程两侧:
List a = Nil | Cons a (List a)
如果将 List a
换成 x
,就可以得到这样的方程:
x = 1 + a * x
不过,我们不能使用传统的代数方法去求解这个方程,因为对于类型,我们没有相应的减法与除法运算。不过,可以用一系列的替换,即不断的用 (1 + a*x)
来替换方程右侧的 x
,并使用分配律,这样就有了下面的结果:
x = 1 + a*x x = 1 + a*(1 + a*x) = 1 + a + a*a*x x = 1 + a + a*a*(1 + a*x) = 1 + a + a*a + a*a*a*x ... x = 1 + a + a*a + a*a*a + a*a*a*a...
最终会是一个积(元组)的无限和,这个结果可被解释为:一个列表,要么是空的,即 1
;要么是一个单例 a
;要么是一个序对 a*a
;要么是一个三元组 a*a*a
;……以此类推,结果就是一个由 a
构成的字符串。
对于列表而言,还有更有趣的东西,等我们了解函子与不动点之后,再来观察它们以及其他的递归数据结构。
用符号变量来解方程,这就是代数!因此上面出现的这些数据类型被称为:代数数据类型。
最后,我应该谈一下类型代数的一个非常重要的解释。注意,类型 a
与类型 b
的积必须包含类型 a
的值与类型 b
的值,这意味着这两种类型都是有值的;两种类型的和则要么包含类型 a
的值,要么包含类型 b
的值,因此只要二者有一个有值即可。逻辑运算 and 与 or 也能形成半环,它们也能映射到类型理论:
这是更深刻的类比,也是逻辑与类型理论之间的 Curry-Howard 同构的基础。以后在讨论函数类型时,对此再作探讨。
1.
证明 Maybe a
与 Eigher () a
同构。
2.
用 Haskell 定义一个和类型:
data Shape = Circle Float | Rect Float Float
要为 Shape
定义一个 area
函数,可以用 Shape
的两个构造子形成的模式匹配:
area :: Shape -> Float area (Circle r) = pi * r * r area (Rect d h) = d * h
请在 C++ 或 Java 中以接口的形式实现 Shape
,然后创建两个类 Circle
与 Rect
,并以虚函数的形式实现 area
。
3.
继续上一题,在不改变 Shape
定义的条件下,很容易增加一个新函数 circ
,用于计算 Shape
的周长:
circ :: Shape -> Float circ (Circle r) = 2.0 * pi * r circ (Rect d h) = 2.0 * (d + h)
请为你的 C++ 或 Java 实现也增加 circ
函数。原来的代码有哪部分不得不作修改?
4.
继续上一题,在 Shape
中增加一个新的形状 Square
,并对代码作相应的更新。在 Haskell vs C++ 或 Java 的实现中,有哪些代码需要变动?(即使你并非 Haskell 程序猿,代码的变动应该也是相当明显的。)
5.
证明 a + a = 2 * a
在类型系统中(在同构意义下)也成立。记住,在上面给出的表中, 2
相当于 Bool
。
感谢 Gershom Bazerman 审阅此文并提出了宝贵意见。