Sum Type

A sum type is the result of the sum operation on two or more algebraic types. In most programming languages, this is expressed with a pipe character. For example in purescript the type Boolean can be expressed as

data Boolean = True | False

The cardinality of a sum type is the sum of all the cardinailities of it's constructors. $|Boolean| = 2$

data Maybe a = Nothing | Just a

$$|Maybe a| = 1 + |a|$$

The monoidal identity of the sum operation is the void type, as $|Void| = 0$.

References

• Book: Thinking with Types