13

想象一种不允许数据类型使用多个值构造函数的语言。而不是写

data Color = White | Black | Blue

我们会有

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

where :|:（这里不是|为了避免与 sum 类型混淆）是一个内置类型联合运算符。模式匹配将以相同的方式工作

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 而不是它们？

4

4 回答 4

16

Haskell 的 sum 类型与您的:|:.

两者之间的区别在于 Haskell 求和类型|是标记的联合，而您的“求和类型”:|:是未标记的。

标记意味着每个实例都是唯一的 - 您可以区分Int | Int（Int实际上，这适用于任何a）：

data EitherIntInt = Left Int | Right Int

在这种情况下：Either Int Int携带更多信息，Int因为可以有 aLeft和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未标记的联合中有什么？它既是 and 的实例Integral，Num所以我们不能确定，必须依赖实现细节。另一方面，被标记的 union 确切地知道5应该是什么，因为它被标记为Leftor Right。

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

于 2016-11-15T22:34:06.747 回答
14

我将尝试扩展@BenjaminHodgson 提到的分类论点。

Haskell 可以看作是类Hask，其中对象是类型，态射是类型之间的函数（不管底部）。

我们可以将产品定义Hask为元组 - 明确地说它符合产品的定义：

和的乘积是配备投影a和的b类型，对于任何其他配备和的候选，存在一个态射，我们可以写成和。cpqp :: c -> aq :: c -> bc'p'q'm :: c' -> cp'p . mq'q . m

产品

阅读Bartosz 的程序员类别理论以获取更多信息。

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

和的联积c是配备注入的类型和使得对于所有其他具有和的候选者存在这样的态射和。abci :: a -> cj :: b -> cc'i'j'm :: c -> c'i' = m . ij' = 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 :|: ba :|: bididmpiqj

副产品未标记

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

  • i=Left和
  • j=Right

这表明产品类型的分类补是不相交并集，而不是基于集合的并集。

集合并集是不相交并集的一部分，因为我们可以将其定义如下：

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

因为我们在上面已经表明，集合并集不是两种类型的联积的有效候选者，所以如果不选择类别中的不相交并集，我们将失去许多“自由”属性（这些属性来自参数化Hask，如 leftroundabout 提到的） （因为不会是副产品）。

于 2016-11-16T00:35:01.480 回答
5

这是我想了很多关于自己的想法：一种具有“一流类型代数”的语言。很确定我们可以像在 Haskell 中那样做所有事情。当然，如果这些分离像 Haskell 替代方案一样被标记为联合；那么你可以直接重写任何 ADT 来使用它们。事实上 GHC 可以为你做到这一点：如果你派生一个Generic实例，一个变体类型将由一个:+:构造表示，它本质上就是Either.

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

于 2016-11-15T22:52:48.590 回答
1

鉴于您提到了 TypeScript，看看它的文档对它的联合类型有什么看法是很有启发性的。那里的例子从一个函数开始......

function padLeft(value: string, padding: any) { //etc.

...有一个缺陷：

问题在padLeft于其填充参数的类型为any. 这意味着我们可以使用既不是 anumber也不是 a的参数来调用它string

然后提出了一种合理的解决方案，但被拒绝了：

在传统的面向对象代码中，我们可以通过创建类型层次结构来抽象这两种类型。虽然这更加明确，但也有点矫枉过正。

相反，该手册建议...

代替，我们可以为参数any使用联合类型padding：

function padLeft(value: string, padding: string | number) { // etc.

至关重要的是，联合类型的概念是这样描述的：

联合类型描述的值可以是多种类型之一。

TypeScript 中的string | number值可以是string类型或number类型，作为string子number类型string | number（参见 Alexis King 对问题的评论）。然而，Haskell 中的Either String Int值既不是String类型也不是Int类型——它唯一的单态类型是Either String Int. 这种差异的进一步影响显示在讨论的其余部分：

如果我们有一个联合类型的值，我们只能访问联合中所有类型共有的成员。

在大致类似的 Haskell 场景中，如果我们有一个Either Double Int，我们不能(2*)直接应用它，即使两者都有Double和Int的实例Num。相反，类似的东西bimap是必要的。

当我们需要具体知道我们是否有一个Fish? [...] 我们需要使用类型断言：

let pet = getSmallPet();

if ((<Fish>pet).swim) {
    (<Fish>pet).swim();
}
else {
    (<Bird>pet).fly();
}

这种向下转换/运行时类型检查与 Haskell 类型系统通常的工作方式不一致，即使它可以 使用完全相同的类型系统来实现（也参见 leftaroundabout 的答案）。相比之下，在运行时没有什么需要弄清楚的类型：案例分析发生在值级别，并且由于运行时类型不匹配，Either Fish Bird不需要处理任何失败和产生Nothing（或更糟， ）的事情。null

于 2016-11-16T00:03:13.103 回答