<译> 简单的代数数据类型

发布时间:2019-06-26 发布网站:脚本宝典
脚本宝典收集整理的这篇文章主要介绍了<译> 简单的代数数据类型脚本宝典觉得挺不错的,现在分享给大家,也给大家做个参考。

原文见 http://bartoszmilewski.com/20...

-> 上一篇:『积与余积

我们已经了解了两种类型组合方式:积与余积。编程中,仅通过这两种类型就可以构造出大部分数据结构。正是因为这一点,保证了数据结构的许多性质都是可复合的。例如,如果知道如何比较两种基本类型的值是否相等,并且知道如何将这种比较方法推广到积与余积类型,那么你就能够自动派生出支持相等运算的复合类型。在 Haskell 中,大部分复合类型能够自动继承相等比较、大小比较以及与字符串的相互转换等运算能力。

现在,我们先近距离的看看编程中的积类型与和类型。

积类型

编程语言中,对于两个类型的积,官方实现是序对(Pair)。在 Haskell 中,序对是基本的类型构造子;在 C++ 中,积表现为标准库中所定义的相对复杂一些的模板。

<img tITle="<译> 简单的代数数据类型" alt="<译> 简单的代数数据类型" data-src="/img/bVqH5s" src="https://static.segmentfault.COM/v-5cc2cd8e/global/img/squares.svg" style="cursor: pointer;">

序对并非严格可交换的:不能用序对 (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 是由 ab 参数化的类型的名字;p 是数据构造子的名字。要定义一个序对类型,只需向 Pair 类型构造子传递两个类型。要构造一个序对类型的值,只需向数据构造子 P 传递两个合适类型的值。例如,定义一个序对类型的值 stmt,其对应的序对类型为 StringBool 的积:

stmt :: Pair String Bool
stmt = P "This statements is" False

上述代码的第一行是类型声明,即使用 StringBool 类型替换了 Pair 泛型定义中的 ab。第二行向数据构造子 P 传递了具体的字符串与布尔值,从而定义了一个序对类型的值 stmt。类型构造子用于构造类型;数据构造子用于构造值。

因为类型构造子与数据构造子的命名空间是彼此独立的,因此二者可以同名:

data Pair a b = Pair a b

如果你足够学究,就可以发现 Haskell 内建的序对类型只是这种声明的一种变体,前者将 数据构造子 Pair 替换为一个二元运算符 (,)。如果将这个二元运算符像正常的数据构造子那样用,照样能创建序对类型的值,例如:

stmt = (,) "This statement is" False

类似的,可以用 (,,) 来创建三元组,以此类推。

如果不用泛型序对或元组,也可以定义特定的有名字的积类型,例如:

data Stmt = Stmt String Bool

这个类型虽然也是 StringBool 的积,但是它有自己的名字与构造子。这种风格的类型声明,其优势在于可以为相同的内容定义不同的类型,使之在名称上具备不同的意义与功能,以避免彼此混淆。

在编程中,只依赖元组以及多参数的构造子会让代码混乱,容易出错,因为只能靠我们的脑袋来记忆各个数据成员的含义。若是能对数据成员进行命名,结果会好一些。支持数据成员命名的积类型也是有的,在 Haskell 中称为记录,在 C 语言中称为 struct

记录@H_338_360@

来看一个简单的例子:用两个字符串表示化学元素的名称与符号,用一个整型数表示原子量,将这些信息组合到一个数据结构中。可以用元组 (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 ee 中检出 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 代码中的构造子 NilCons,在 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 同构么?例如,是否存在一个 IntVoid 构成的序对?

要创建序对,需要两个值。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 的值,因此只要二者有一个有值即可。逻辑运算 andor 也能形成半环,它们也能映射到类型理论:

<译> 简单的代数数据类型

这是更深刻的类比,也是逻辑与类型理论之间的 Curry-Howard 同构的基础。以后在讨论函数类型时,对此再作探讨。

挑战

1. 证明 Maybe aEither () 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,然后创建两个类 CircleRect,并以虚函数的形式实现 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 审阅此文并提出了宝贵意见。

-> 下一篇:『函子

脚本宝典总结

以上是脚本宝典为你收集整理的<译> 简单的代数数据类型全部内容,希望文章能够帮你解决<译> 简单的代数数据类型所遇到的问题。

如果觉得脚本宝典网站内容还不错,欢迎将脚本宝典推荐好友。

本图文内容来源于网友网络收集整理提供,作为学习参考使用,版权属于原作者。
如您有任何意见或建议可联系处理。小编QQ:384754419,请注明来意。