为什么我们需要 Sum 类型?

Why do We Need Sum Types?

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

data Color = White | Black | Blue

我们会

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

其中:|:(这里不是|,以免与求和类型混淆)是内置类型联合运算符。模式匹配的工作方式相同

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

如您所见,与联积相比,它会产生扁平结构,因此您不必处理注入。而且,与求和类型不同,它允许随机组合类型,从而获得更大的灵活性和粒度:

type ColorsStartingWithB = Black :|: Blue

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

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

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

Haskell的求和类型和你的:|:.

非常相似

两者的区别在于Haskell和类型|tagged联合,而你的"sum type":|: 未标记。

标记意味着每个实例都是唯一的 - 您可以将 Int | IntInt 区分开来(实际上,这适用于任何 a):

data EitherIntInt = Left Int | Right Int

在这种情况下:Either Int IntInt携带更多信息,因为可以有LeftRightInt.

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

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 应该是什么,因为它被标记为 LeftRight.


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

这是我自己想了很多的一个想法:一种具有“第一个class类型代数”的语言。很确定我们可以像在 Haskell 中那样做所有事情。当然,如果这些分离是 Haskell 替代方案,tagged 联合;然后你可以直接重写任何 ADT 来使用它们。事实上 GHC 可以为你做这件事:如果你派生一个 Generic instance, a variant type will be represented by a :+: 结构,它本质上只是 Either.

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

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

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

...有缺陷:

The problem with padLeft is that its padding parameter is typed as any. That means that we can call it with an argument that’s neither a number nor a string

然后提出了一个合理的解决方案,但被拒绝了:

In traditional object-oriented code, we might abstract over the two types by creating a hierarchy of types. While this is much more explicit, it’s also a little bit overkill.

相反,手册建议...

Instead of any, we can use a union type for the padding parameter:

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

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

A union type describes a value that can be one of several types.

TypeScript 中的 string | number 值可以是 string 类型或 number 类型,因为 stringnumber 是 [= 的子类型19=](参见 Alexis King 对问题的评论)。然而,Haskell 中的 Either String Int 值既不是 String 类型,也不是 Int 类型——它唯一的单态类型是 Either String Int。在讨论的其余部分中会出现这种差异的进一步含义:

If we have a value that has a union type, we can only access members that are common to all types in the union.

在大致类似的 Haskell 场景中,如果我们有一个 Either Double Int,我们不能直接在其上应用 (2*),即使 DoubleIntNum 的实例。相反,像 bimap 这样的东西是必要的。

What happens when we need to know specifically whether we have a Fish? [...] we’ll need to use a type assertion:

let pet = getSmallPet();

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

这种 downcasting/runtime 类型检查是 with how the Haskell type system ordinarily works, even though it can be implemented 使用完全相同的类型系统(也参见 leftaroundabout 的回答)。相比之下,在运行时没有什么需要弄清楚 Either Fish Bird 的类型:案例分析发生在值级别,并且不需要处理任何失败并产生 Nothing(或更糟, null) 由于运行时类型不匹配。

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

Haskell可以看作范畴Hask,其中对象是类型,态射是类型之间的函数(无视底部)。

我们可以将Hask中的一个积定义为元组——断然符合积的定义:

A product of a and b is the type c equipped with projections p and q such that p :: c -> a and q :: c -> b and for any other candidate c' equipped with p' and q' there exists a morphism m :: c' -> c such that we can write p' as p . m and q' as q . m.

阅读 Bartosz' Category Theory for Programmers 了解更多信息。

现在对于每一个范畴,都存在相反的范畴,它具有相同的态射,但反转了所有的箭头。因此,副产品是:

The coproduct c of a and b is the type c equipped with injections i :: a -> c and j :: b -> c such that for all other candidates c' with i' and j' there exists a morphism m :: c -> c' such that i' = m . i and j' = m . j.

让我们看看在给定此定义的情况下标记和未标记联合的执行情况:

ab 的未标记联合是类型 a :|: b 使得:

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

然而,我们知道 a :|: aa 同构。基于该观察,我们可以为乘积 a :|: a :|: b 定义第二个候选,它配备了完全相同的态射。因此,没有单一的最佳候选,因为 a :|: a :|: ba :|: b 之间的态射 midid 是一个双射,这意味着 m 是可逆的,而 "convert" 是任何一种类型。该论点的直观表示。将 p 替换为 i,将 q 替换为 j

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

  • i = Left
  • j = Right

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

集合并集是不相交并集的一部分,因为我们可以这样定义它:

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

因为我们在上面已经证明集合并集不是两种类型的余积的有效候选者,所以我们会失去很多 "free" properties(来自 parametricity如 leftroundabout 所述)不选择类别 Hask 中的不相交并集(因为不会有余积)。