代数数据类型和基类型之间有什么区别？

Question

我理解GADT是什么,但是GADT和基本类型(在Haskell或其他地方)有什么区别？

Answer 1

我不确定你是指使用GADTs扩展的常规data声明与类型Int或广义代数数据类型,所以如果这不能回答你的问题那么请澄清.

正常data声明允许您创建属于产品(this和that)和sums(this或that)组合的类型.

一些例子是:

data Color = Red | Green | Blue                      -- a sum type
data Person = Person { name :: String, age :: Int }  -- a product type
data Address = Mail Street City Country | Email String -- both!

GADT允许您更具体地了解每个构造函数的类型.这是我最喜欢的例子:

-- helper types to encode natural numbers
data Z     -- zero
data S n   -- successor

-- a list that encodes its size in its type
data List a n where
  Nil :: List a Z
  Cons :: a -> List a n -> List a (S n)

-- head that cannot be called on an empty list!
head :: List a (S n) -> a
head (Cons h _) = h

-- tail that cannot be called on a empty list!
tail :: List a (S n) -> List a n
tail (Cons _ t) = t

请注意,我们无法使用常规数据声明来完成此操作

data List a n = Nil | Cons a (List a n)

因为没有办法指定Nil类型是什么,List a Z并且Cons将列表的大小增加1.