Sum-Types
Disjoint sum (union)
We add up (put together) elements, not multiply them.
Sums (and sum-types) are “linear”, while products are build “dimensions”.
We use the symbol | to emphasize partitioning of a disjoint union.
Rotation
commutative (same notion) \[(a \mid b) \cong (b \mid a)\]
Nested pairs
isomorphic \[((a \mid b) \mid c) \cong (a \mid (b \mid c))\]
Disjoint sum
Think of it as adding up without morphing into one. \[a \mid b \cong a + b\]
Unit
\(\emptyset\) as a unit - adding nothing change nothing.
Logically it is an uninhabited type Void - there are no instances (or
values) of a void.
\[a + 0 = a \cong a \mid \emptyset = a\]
partitions
These are type-level notions, not an instance (value) level.
either True or False
data Bool = True | False
The empty/non-empty aspect of a list
data Maybe a = Nothing | Just a
Recursive disjoint sum (of tuples)
data List a = Nil | Cons a (List a)
a List is either empty, or it is a singleton, or a pair, or a triple or an n-tuple, made out of Conses, which are nested Pairs.
Pattern-matching
“Universal” (everywhere) pattern-matching on sum-types of the ML-family of languages is the most important innovation in programming languages.
It breaks disjount sums apart in a systematic, uniform way, with proper nesting.
Languages without universal pattern-matching are simply inferior.