Data types in programming come in all flavours, and to many programmers, the theories behind them pass unnoticed. In this post I will explain one of these theories: algebraic data types. Have you ever used a struct/record in your favourite programming language? That is an algebraic data types. Have your ever hard about "sum types"? That is also an algebraic data type!
Algebraic data types (ADT) are a way of modelling the combination of data types
using algebra as an analogy. More specifically, the analogy is about the
cardinality of types, i.e. total number of elements belonging to the type.
As an example, a struct/record is also called product type because a record
C that combines type A and type B has cardinality equals A's multiplied
by B's cardinality, i.e. |C| = |A| * |B|. This is a very similar concept to
an ordered pair in set theory.
Another example of algebraic data type is a sum type. As the name indicates, a
sum type C combining types A and B has a total number of elements equals to the
sum of total elements of A and total elements of B, i.e. |C| = |A| + |B|.
This corresponds to disjoint unions in set theory, but not to regular unions.
In fact, in contrary to set theory's unions, summing a type with itself produces
a new type, as we'll see in a section below.
There are other types, such as exponential types (whose cardinality you all might have guessed), unitary types and nullary types. As the names suggest, unitary types have one element, nullary types have no elements. In the following sections all of this will be explored in more details.
| Names | Notations | Cardinality Formula |
|---|---|---|
| void type, bottom type, never type, nothing type | 0, ⊥ |
|0| = 0 |
| unitary type, unit type, top type, void type (C-like) | 1, ⊤, () |
|1| = 1 |
| sum type, variant type, tagged union, discriminated union | A + B |
|A + B| = |A| + |B| |
| product type, struct, record | A * B, (A, B) |
|A * B| = |A| * |B| |
| exponential type, function type | B ^ A, A -> B |
|B ^ A| = |B| ^ |A| |
| dependent sum type, dependent record | Σ(x : A). B(x),(x : A, B(x)) |
|Σ(x : A). B(x)| = Σ(x : A). |B(x)| |
| dependent product type, dependent function | Π(x : A). B(x),(x : A) -> B(x) |
|Π(x : A). B(x)| = Π(x : A). |B(x)| |