函数式编程中的ADT有哪些代数特性？

Question

我在一本Scala书中读到了这样的内容：

For example, this code is an ADT:

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

......并且它进一步表示：

ADTs中的“代数”在Haskell wiki上的描述如下：

“代数”是指代数数据类型由“代数”操作创建的属性。 这里的“代数”是类型的“和”和“积”。

但是在上面的代码片段中，这些'代数'操作在哪里？

- Mandroid

---

我对Scala没有了解，但是这段代码看起来像是一个和类型。Bool 是 True 和 False 的和。 - VLAZ

没有上下文的情况下，你可能会把“ADT”理解为抽象数据类型。 - chepner

这是一篇关于ADTs的优秀介绍：http://tomasp.net/blog/types-and-math.aspx/ - Mark Seemann

Answer 1

但是上面代码片段中的那些“代数”操作在哪里？

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

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)

抽象数据类型中的“代数”是什么

术语“代数”源于数学领域的抽象代数。它研究不同对象及其上的不同运算，并希望找到它们之间的共同行为。大致上，就是去掉某些东西，看剩下什么。就像孩子们用苹果学习数数和算术一样。在某个时候，你“拿走”了这些苹果，留下来的是“数字”，它们表现出与苹果相同的方式。优点在于，现在你学到的用于苹果算术的规则和法律也适用于橙子等其他物品的算术。但数学家更进一步，会问像“如果我们连数字本身都拿走了会发生什么”这样的疯狂问题？另一个看待它的方式是，你写下一些方程式，比如

a + b = b + a       (commutativity law)

在某种抽象意义下定义了加法运算符“+”，现在尝试找到任何满足条件的对象。例如，整数、实数等均满足条件，但事实证明，某些数据类型（如和类型）也适合这个方程式。于是，数学家们声明所有在某种意义下与加法操作一起工作并且其操作结果是可交换的对象类作为一种代数结构，并赋予其一些重要的命名，如阿贝尔群。这大致解释了“代数数据类型”中“代数”的词源。

- Mario Galic

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。

- chepner

Answer 3

在Haskell中，您可以使用“广义”ADT语法编写ADT，例如：

{-# LANGUAGE GADTs #-}

data Bool where
  False :: Bool
  True :: Bool

这段代码看起来更像是Scala版本，而不是等价的标准Haskell表示法：

data Bool = False | True

关于这个问题为什么要使用代数学： Bool 是和类型的一个例子。其中最通用的是:

{-# LANGUAGE TypeOperators, GADTs #-}

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

标准版的是

data Either a b = Left a | Right b

通用的产品类型应该是：

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

等等。作为一项练习，请证明每个名称都有与其所示数量相同的合法值。

- leftaroundabout