有两种ADT一种是abstract data types,另一种叫algebraic data types,前者常常在OO的语言出现,一般是各种泛型,比如一些容器类。而后者代数数据类型则是来自函数式编程。

正如其名,代数数据类型代表相应的数据结构应该满足一定的数学属性,利用相应的关系,我们可以用来证明类型实现的正确定,进一步证明程序的正确性。另一方法,它鼓励合理利用composition去构建更复杂的数据结构和算法。

不要看下去了,去看大神的博客吧。

Product Types and Sum Types

有两中基本的方法可以combining types,即productcoproduct。基本类型的组合有着重要的意义,一方面可以方便的构造新的类型,另一方面可以直接获得诸如equalitytoString这种函数。

Product Types

一个常见的典型的product type就是pair。在Haskell和Scala都是原生支持(Int, Bool)这种写法,在C++里面,stl中也有Pair

在Scala里面,大多数情况下,case class都是product types。比如定义一个Person

1
case class Person(name: Name, age: Age)

这样你得到的可能的Person的数目应该是Name类型实例的个数乘上Age类型实例的个数。既然是乘法,那么就应该有01。实际上我们有()或者叫Unit包含0个元素。比较一下下面这个类型。

1
case class unitTimesPerson(name: Name, age: Age, Unit)

我们好像并没有获得更多的Person,这就像乘上了一。对于这两种类型,可以称为isomorphic即同构的。 至于0,其实有0个元素就意味着无法实例化,而在Scala中正有一个无法实例化的类型Nothing。具体Nothing的实现也很有意思。可以看由于为了实现ADT很多时候都需要Nothing类型,即需要一个是所有类的子类的类。比如

1
2
3
sealed trait List[+A] 
case object Nil extends List[Nothing]
case class Cons[+A](head: A, tail: List[A]) extends List[A]

这里定义了List类型,首先List类型应该满足协变,即A是B的子类,那么List[A]也可以看做List[B]的子类。然后空的List,即Nil应该是任何List[A]的子类,因为它可以被接在任何类型的List类型的后面,即Cons(anyList, Nil),都应该是合法的。

与之相对的,在Haskell里面也有类似的语法,相对来说更简单

1
data Pair a b = P a b

这里定义了一个类型Pair,以ab两个类型参数,P是data constructor的名字。然后你就可以通过P来生成一个Pair了。

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

第一句是声明类型,第二行则利用P生成了相应的类型。

Sum Types

Sum Types的一个典型的例子是Enumeration,对于枚举值由于是无序的所以加入新的值也只是增加了一个值而已。

另一个常见的类型在Haskell里面是

1
data Either a b = Left a | Right

或者在Scala里面

1
2
3
sealed trait Either[+E,+A] 
case class Left[+E](get: E) extends Either[E,Nothing]
case class Right[+A](get: A) extends Either[Nothing,A]

显然每一个类型只对应一个data constructor,所以它们其实是可交换的。而Nothing则是其中的0,考虑

1
Either[Nothing, A]

其和A本身应该是isomorphic的,因为这样你就只能构造Right A而无法构造Left Nothingc++中的

1
enum { Red, Green, Blue};

也是相似的意思。值得注意的是,之前举例看到的List本身也是sum types。把它翻译成c++就是

1
2
3
4
5
6
7
template<class A>
class List {
Node<A> *_head;
List(): _head(nullptr) {} //这里可以看做Nil
List(A a, List<A> tail) // 这里可以看做Cons
: _head(new Node<A>(a, tail)){}/
}

Properties Of Algebraic Data Types

简单来说,一个algebraic可以通过下面这三个方面定义:

  1. A set of objects: 这个objects不是OO的那个对象,完全不是同一维度的东西。有时候也有人叫symbols.

  2. A set of operations:其中元素是怎么组合构件新的元素的。其实从这篇文章能看出来,这里的Operations并不是常见的函数,所有的Type constructors都可以是Operation。A category consists of objects and arrow that go between them.然后在此之上,可以定义出对偶的products以及coproducts。然后,products导致了product typescoproducts导致了sum types。什么鬼!

  3. A set of laws: 这些laws定义了objects以及operations应该满足的规则。

像交换律等常见的规律都是很容易证明的,我们先详细看看分配律distributive law

a * (b + c) = a * b + a * c

转换成我们的类型应该是(a, Either b c) = Either (a, b) (a, c)

我们可以实现一个函数

1
2
3
4
5
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)

回顾离散数学里面的内容,如果一个集合定义了加法和乘法,但是没有减法,我们就可以叫它半环。

这篇东拼西凑的文章写出来,其实发现有更多的问题。ADT是FP组织代码形式,Category Theory用个不恰当的比如可以看做OO的设计模式。 在库的设计上有着重要的作用,最近也在看一些库设计方面的论文,好吧,我很不务正业。之后趁着元旦的时候尽量整理一个靠谱一点的。(明天开会,我还是没干什么活




X