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 ∣ b) ≅ (b ∣ a)$

Nested pairs

isomorphic $((a ∣ b) ∣ c) ≅ (a ∣ (b ∣ c))$

Disjoint sum

Think of it as adding up without morphing into one. $a ∣ b ≅ 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 ≅ a ∣ \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.