为什么和类型称为和类型？

Question

在学习 Haskell 的过程中，我阅读了关于代数数据类型、求和类型和乘积类型的内容。虽然乘积类型类似于笛卡尔积并且“乘积”对我来说立即有意义，但我不明白为什么和类型（又名变体类型，又名标记联合，又名歧视联合，又名不相交联合）被称为和类型。

维基百科说：

sum 类型对应于 Curry-Howard 对应关系下的直觉逻辑析取。

好的，我明白了：析取类似于布尔代数中的 OR，这种看起来像总和，因为

 OR |   | +
-----------
0 0 | 0 | 0 
0 1 | 1 | 1
1 0 | 1 | 1
1 1 | 1 | 0 (mismatch here)

但由于 1 + 1，它并不真正适合。

我找到了关于什么是乘积和总和类型的各种解释，我想我明白了。总和类型是一件事或另一件事。

但是为什么它被称为和类型呢？仅仅因为将符号 + 用于 OR 运算符是一种约定？还是因为“和类型是乘积类型的对偶。”？

（同样，除非我错过了一些大的东西，请不要解释 sum/product type。我想我明白了这个概念。我只想知道为什么它被称为sum type。）

Answer 1

这就是所谓的和类型，因为值的数量的A + B是值的数量的总和A和B。