函数式编程中 ADT 的代数是什么？

Question

在一本 Scala 书中我读到：

例如，这段代码是一个 ADT：

sealed trait Bool 
case object True extends Bool 
case object False extends Bool

....进一步说：

Haskell wiki 上这样描述 ADT 中的“代数”：

“代数”是指代数数据类型由“代数”运算创建的属性。这里的“代数”是“和”和“产品”（类型）。

但是上面代码 sn-p 中的那些“代数”运算在哪里？

Answer 1

但是上面代码 sn-p 中的那些“代数”运算在哪里？

它们隐含在语言的语法中。 “加法”的概念运算

A + B

可以在 Scala 中编码为

sealed trait T 
case object A extends T 
case object B extends T

乘法的概念运算

A x B

可以在 Scala 中编码为

case class T(a: A, b: B)

什么是关于 ADT 的代数

“代数”一词源于名为abstract algebra 的数学领域。这是一项研究不同对象和对这些对象的不同操作并希望找到它们之间的共同行为的努力。粗略地说，这是拿走东西并看到剩下的东西的过程。就像你小时候学习数数和用苹果做算术一样。在某些时候，你“拿走”了苹果，剩下的就是“数字”，它们的行为方式与苹果相同。这样做的好处是，现在你在苹果算术中学到的相同规则和法则，可以推广到橙子的算术及其他方面。但数学家走得更远，他们会问一些疯狂的问题，比如如果我们连数字本身都拿走会发生什么？另一种看待它的方法是写下一些方程式，例如

a + b = b + a       (commutativity law)

其中加法+ 是在某种抽象意义上定义的，现在尝试找到满足它的任何类型的对象。例如，整数以及实数等都满足它，但事实证明，某些类型的数据类型（如 sum 类型）也适合该等式。因此，数学家将所有对象的类统称为集体，它们在某种意义上与加法运算一起工作，使得运算的结果是可交换的，作为代数结构，并给它一些宏伟的名称，如阿贝尔群等。这大致是“代数数据类型”中“代数”的词源。

Answer 2

布尔类型可以看作是单位类型和单位类型的总和。很抱歉用 Haskell 而不是 Scala 编写以下代码：

type MyBool = Either () ()

由于()只有一个值，所以Either () ()类型只有两个值，这取决于我们是在()上使用Left还是Right来构造一个值。

Bool 和 Either () () 同构的证明如下：

我们可以定义两个函数来将Bool 转换为Either () ()，反之亦然。

b2e :: Bool -> Either () ()
b2e True = Right ()
b2e False = Left ()

e2b :: Either () () -> Bool
e2b (Right ()) = True
e2b (Left ()) = False

我们可以简单地证明b2e 和e2b 是同构的。

e2b (b2e True) == e2b (Right ()) == True
e2b (b2e False) == e2b (Left ()) == False
b2e (e2b (Right ())) == b2e True == Right ()
b2e (e2b (Left ())) == b2e False == Left ()

因此e2b . b2e == b2e . e2b == id。

Answer 3

在 Haskell 中，您也可以使用 通用 ADT 语法编写 ADT：

{-# LANGUAGE GADTs #-}

data Bool where
  False :: Bool
  True :: Bool

...看起来更像 Scala 版本，而不是等效的标准 Haskell 表示法：

data Bool = False | True

至于这是如何代数的：Bool 是 sum 类型的示例。其中最普遍的一种是

{-# LANGUAGE TypeOperators, GADTs #-}

data (+) a b where
  Left :: a -> (a+b)
  Right :: b -> (a+b)

其中的标准版本是

data Either a b = Left a | Right b

通用的product类型应该是

data (*) a b where
  Both :: a -> b -> (a*b)

与(a,b)同构。

现在你可以定义一些有限类型了：

data One = One
type Two = One + One
type Three = One + Two
type Four = Two * Two

等等。等等。作为一个练习，证明它们中的每一个都具有与名称所暗示的一样多的不同法律价值。