为什么我们需要和类型？ [英] Why do We Need Sum Types?
问题描述
data颜色=白色|黑色|蓝色
我们会有
pre > 数据白色=白色
数据黑色=黑色
数据蓝色=黑色
类型颜色=白色：|：黑色：|：蓝色
其中：|：（这里不是 | | 以避免与总和类型混淆）是一个内置类型联合运算符。模式匹配将以相同的方式工作
show :: Color - >字符串
显示白色=白色
显示黑色=黑色
显示蓝色=蓝色
正如您所看到的，与副产品相比，它会产生扁平结构，因此您无需处理注射。并且，与sum类型不同，它允许随机地组合类型，从而获得更大的灵活性和粒度：
type ColorsStartingWithB = Black：|：蓝色
我相信构建递归数据类型也不是问题。
data无=无
数据缺点a =缺点a（列表a）
类型列表a =缺点a | ：无
我知道联合类型存在于TypeScript和其他语言中，但为什么Haskell委员会他们选择了ADTs？
Haskell的总和类型与您的非常相似：|：
两者之间的区别在于Haskell和类型 | 是一个标记为 union，而您的总和类型：|：是未标记的。
实例是唯一的 - 你可以distonguish Int | Int > Int （实际上，这适用于任何 a ）：
data EitherIntInt = Left Int | Right Int
在这种情况下： Int Int 比 Int 带有 more 信息，因为可以存在 Left 和右 Int 。
在您的：| ：，你不能区分这两个：
type EitherIntInt = Int：|：Int
你怎么知道它是左边还是右边 Int
有关以下部分的扩展讨论，请参阅评论。
标记工会还有另一个优势：编译器可以验证你是否作为程序员处理了所有的情况，这对于一般未加标签的联合来说依赖于实现。你是否处理过 Int中的所有情况：|：Int ？要么按照定义同构 Int ，要么编译器必须决定选择哪个 Int （左或右）这是不可能的，如果他们无法区分。
考虑另一个例子：
类型（积分a，数字b）=> IntegralOrNum a b = a：|：b - 未标记的
数据（积分a，数字b）=> IntegralOrNum ab =标记为
什么是 5 :: IntegralOrNum Int Double 在untagged union中？它既是 Integral 和 Num 的一个实例，所以我们无法确定并且必须依赖实现细节。另一方面，带标签的联合会确切地知道 Left 或 Right 。
至于命名：Haskell中不相交的联合是工会类型。 ADT只是实现这些功能的一种手段。
Imagine a language which doesn't allow multiple value constructors for a data type. Instead of writing
data Color = White | Black | Blue
we would have
data White = White
data Black = Black
data Blue = Black
type Color = White :|: Black :|: Blue
where :|: (here it's not | to avoid confusion with sum types) is a built-in type union operator. Pattern matching would work in the same way
show :: Color -> String
show White = "white"
show Black = "black"
show Blue = "blue"
As you can see, in contrast to coproducts it results in a flat structure so you don't have to deal with injections. And, unlike sum types, it allows to randomly combine types resulting in greater flexibility and granularity:
type ColorsStartingWithB = Black :|: Blue
I believe it wouldn't be a problem to construct recursive data types as well
data Nil = Nil
data Cons a = Cons a (List a)
type List a = Cons a :|: Nil
I know union types are present in TypeScript and probably other languages, but why did the Haskell committee chose ADTs over them?
Haskell's sum type is very similar to your :|:.
The difference between the two is that the Haskell sum type | is a tagged union, while your "sum type" :|: is untagged.
Tagged means every instance is unique - you can distunguish Int | Int from Int (actually, this holds for any a):
data EitherIntInt = Left Int | Right Int
In this case: Either Int Int carries more information than Int because there can be a Left and Right Int.
In your :|:, you cannot distinguish those two:
type EitherIntInt = Int :|: Int
How do you know if it was a left or right Int?
See the comments for an extended discussion of the section below.
Tagged unions have another advantage: The compiler can verify whether you as the programmer handled all cases, which is implementation-dependent for general untagged unions. Did you handle all cases in Int :|: Int? Either this is isomorphic to Int by definition or the compiler has to decide which Int (left or right) to choose, which is impossible if they are indistinguishable.
Consider another example:
type (Integral a, Num b) => IntegralOrNum a b = a :|: b -- untagged
data (Integral a, Num b) => IntegralOrNum a b = Either a b -- tagged
What is 5 :: IntegralOrNum Int Double in the untagged union? It is both an instance of Integral and Num, so we can't decide for sure and have to rely on implementation details. On the other hand, the tagged union knows exactly what 5 should be because it is branded with either Left or Right.
As for naming: The disjoint union in Haskell is a union type. ADTs are only a means of implementing these.
这篇关于为什么我们需要和类型？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
