In the course of learning Haskell I read about Algebraic Data Types, sum types and product types. While product types are analogous to the Cartesian product and "product" immediately made sense to me I don't understand why sum types (aka variant types aka tagged union aka discriminated union aka disjoint union) are called sum types.
Wikipedia says:
The sum type corresponds to intuitionistic logical disjunction under the Curry–Howard correspondence.
OK, I get it: Disjunction is analogous to OR in boolean algebra and this kind of looks like sums because
OR | | +
-----------
0 0 | 0 | 0
0 1 | 1 | 1
1 0 | 1 | 1
1 1 | 1 | 0 (mismatch here)
But it does not really fit because of 1 + 1.
I found various explanations on what product and sum types are and I think I get it. The sum type is either one thing OR the other thing.
But why exactly is it called sum type? Just because it is a convention to use the symbol + for the OR operator? Or because "Sum types are the dual of product types."?
(Again, unless I missed something big, please don't explain sum/product type. I think I get the concept. I only want to know why it is called sum type.)
It's called a sum type because the number of values of A + B is the sum of the number of values of A and B.