为什么我们需要总和类型？

Question

想象一种语言,它不允许数据类型的多个值构造函数.而不是写作

data Color = White | Black | Blue

我们会有

data White = White
data Black = Black
data Blue = Black
type Color = White :|: Black :|: Blue

where :|:(这里不是|为了避免与sum类型混淆)是一个内置的类型union运算符.模式匹配可以以相同的方式工作

show :: Color -> String
show White = "white"
show Black = "black"
show Blue = "blue"

正如您所看到的,与副产品相比,它会产生扁平结构,因此您无需处理注射.而且,与sum类型不同,它允许随机组合类型,从而产生更大的灵活性和粒度:

type ColorsStartingWithB = Black :|: Blue

我相信构造递归数据类型也不是问题

data Nil = Nil
data Cons a = Cons a (List a)
type List a = Cons a :|: Nil

我知道联合类型存在于TypeScript和其他语言中,但为什么Haskell委员会选择ADT而不是它们呢？

Answer 1

Haskell的总和类型非常类似于你的:|:.

两者之间的区别在于Haskell和类型|是标记的并集,而您的"和类型" :|:是未标记的.

标记意味着每个实例都是唯一的 - 你可以Int | Int从Int(实际上,这适用于任何实例)中解脱出来a:

data EitherIntInt = Left Int | Right Int

在这种情况下:Either Int Int携带更多的信息,而不是Int因为可以有Left和Right Int.

在你的:|:,你无法区分这两个:

type EitherIntInt = Int :|: Int

你怎么知道它是左还是右Int？

有关以下部分的扩展讨论,请参阅注释.

标记的联合具有另一个优点:编译器可以验证您是否作为程序员处理了所有情况,这对于一般未标记的联合是依赖于实现的.你处理过所有案件了Int :|: Int吗？Int根据定义,这是同构的,或者编译器必须决定选择哪个Int(左或右),如果它们无法区分则是不可能的.

考虑另一个例子:

type (Integral a, Num b) => IntegralOrNum a b = a :|: b    -- untagged
data (Integral a, Num b) => IntegralOrNum a b = Either a b -- tagged

什么是5 :: IntegralOrNum Int Double在未标记的工会吗？它既是实例Integral和Num,所以我们不能决定肯定和必须依靠实施细则.另一方面,标记的联合确切地知道5应该是什么,因为它被标记为Left或者Right.

至于命名:Haskell中的不相交联合是一个联合类型.ADT只是实现这些的一种手段.

Answer 2

我将尝试扩展@BenjaminHodgson提到的分类论证.

Haskell可以看作是类别Hask,其中对象是类型,而态射是类型之间的函数(忽略底部).

我们可以将产品定义Hask为元组 - 从语义上说它符合产品的定义:

的乘积a和b的类型为c配有凸起p和q使得p :: c -> a与q :: c -> b和任何其他候选c'配备p'和q'存在一个态射m :: c' -> c,使得我们可以写p'为p . m和q'为q . m.

请阅读Bartosz的"程序员类别理论"中的更多信息.

现在对于每个类别,存在相反的类别,它具有相同的态射但反转所有箭头.因此,副产品是:

的副产物c的a和b是类型c配备注射i :: a -> c和j :: b -> c使得对于所有其他候选人c'与i'和j'存在一个态射m :: c -> c',使得i' = m . i和j' = m . j.

让我们看看给定此定义的标记和未标记联合如何执行:

无标记的联合,a并且b是这样的类型a :|: b:

• i :: a -> a :|: b被定义为i a = a和
• j :: b -> a :|: b 被定义为 j b = b

但是,我们知道这a :|: a是同构的a.基于该观察,我们可以定义产品的第二个候选者,其a :|: a :|: b具有完全相同的态射.因此,没有一个统一的最佳人选,因为态射m之间a :|: a :|: b和a :|: b为id.id是一种双射,这意味着它m是可逆的并且以任何一种方式"转换"类型.该论证的直观表示.更换p用i和q用j.

限制自己Either,因为您可以通过以下方式验证自己:

• i= Left和
• j = Right

这表明产品类型的分类补充是不相交的联合,而不是基于集合的联合.

set union是不相交联合的一部分,因为我们可以将它定义如下:

data Left a = Left a
data Right b = Right b
type DisjUnion a b = Left a :|: Right b

因为我们已经在上面说明了集合并不是两种类型的副产品的有效候选者,所以我们会失去许多"自由"属性(从参数中得到leftroundabout),而不是选择类别中的不相交联合Hask(因为那里)将不是副产品).

Answer 3

这是我对自己的想法很多的一个想法:一种具有"一流类型代数"的语言.我们确信我们可以像Haskell那样做所有事情.当然,如果这些分离是像Haskell替代品那样标记的工会; 然后你可以直接重写任何ADT来使用它们.事实上GHC可以为你做到这一点:如果你派生一个Generic实例,一个变体类型将由一个:+:构造表示,这实际上只是Either.

我不确定未标记的工会是否也会这样做.只要您要求参与总和的类型明显不同,显式标记原则上不应该是必要的.然后,该语言需要一种方便的方法来在运行时匹配类型.听起来很像动态语言的作用 - 显然有很多开销.
最大的问题是,如果两边的类型:|:必须不相等,那么你就失去了参数,这是Haskell最好的特性之一.