algebraic-data-types - 为什么和类型称为和类型？

Question

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

维基百科说:

The sum type corresponds to intuitionistic logical disjunction under the Curry–Howard correspondence.

好的，我明白了:析取类似于 bool 代数中的或，这种看起来像求和，因为

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

但是因为1+1所以不太合适

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

但为什么它被称为 sum 类型？ 只是因为 OR 运算符使用符号 + 是一种约定？或者因为“总和类型是产品类型的对偶。”？

(再次声明，除非我遗漏了一些大的东西，否则请不要解释 sum/product 类型。我想我明白了这个概念。我只想知道为什么它被称为 sum 类型。)

Answer 1

之所以称为求和类型，是因为A + B 的值数 是A 和B.