Algebraic Data Types

A type tells us which values may appear in a program. For a finite type $\tau$, write $|\tau|$ for the number of values in that type.

The type bool has two values, so $|\mathbf{bool}|=2$. The type order has three values, so $|\mathbf{order}|=3$. For this reason, we sometimes use the natural number $2$ as a name for any type with two values and $3$ as a name for any type with three values.

A value of type $A\times B$ is a pair $(a,b)$ with $a:A$ and $b:B$. For every choice from $A$, we may choose any value from $B$. Therefore

$$|A\times B|=|A|\times|B|.$$

For example, bool * order contains six values:

Thus $|\mathbf{bool}\times\mathbf{order}|=2\times3=6$.

The type unit has exactly one value, written () in Standard ML. It acts as the multiplicative identity:

$$A\times\mathbf{unit}\simeq A\qquad\mathbf{unit}\times A\simeq A.$$

The symbol $\simeq$ means that the two types contain the same information. More precisely, they are isomorphic.

To prove $A\simeq B$, give a total function $f:A\to B$ and a total function $g:B\to A$ such that applying one after the other returns the original input:

$$g(f(x))=x\qquad f(g(y))=y.$$

These equations say that $f$ and $g$ are inverses. They establish a bijection between the values of the two types.

Associativity of products

$$A\times(B\times C)\simeq(A\times B)\times C.$$

The functions only change the grouping of the pair. No value is created, forgotten, or duplicated.

Commutativity of products

$$A\times B\simeq B\times A.$$

The function swap is its own inverse.

A value of type $A+B$ contains either a value from $A$ or a value from $B$. Tags record which choice was made.

The constructors introduce values into the sum:

$$\frac{\Gamma\vdash e:A}{\Gamma\vdash\mathsf{Left}\;e:A+B}\qquad \frac{\Gamma\vdash e:B}{\Gamma\vdash\mathsf{Right}\;e:A+B}.$$

Case analysis eliminates a sum. Since the input may use either constructor, both cases are required.

There are $|A|$ values tagged Left and $|B|$ values tagged Right. The groups do not overlap, so

$$|A+B|=|A|+|B|.$$

For example, $|\mathbf{bool}+\mathbf{order}|=2+3=5$.

An option contains either one value of type $A$ or no such value.

The constructor SOME contributes $|A|$ possibilities. The constructor NONE contributes one more. Therefore

$$|A\;\mathbf{option}|=|A|+1.$$

This is the same structure as $A+\mathbf{unit}$:

$$A\;\mathbf{option}\simeq A+\mathbf{unit}.$$

For example, a function that searches for an element can return SOME x when it succeeds and NONE when it does not. The type records both possibilities, so callers must account for failure.

Products distribute over sums:

$$(A\times B)+(A\times C)\simeq A\times(B+C).$$

We prove this with two inverse functions.

This law is also a useful refactoring principle. If every case stores the same value of type $A$, store that value once outside the choice.

Addition has an identity value, zero. The corresponding type is the empty type, also called void. It has no values, so $|\mathbf{void}|=0$.

If we somehow receive a value of this type, we may produce a value of any type:

$$\frac{\Gamma\vdash e:\mathbf{void}}{\Gamma\vdash\mathsf{absurd}(e):A}.$$

This rule is safe because there is no value that can be supplied as the argument. Standard ML can encode the empty type recursively:

A finite value cannot be built because constructing Void v first requires another value v of type void.

$$A+\mathbf{void}\simeq A.$$

A total function from $A$ to $B$ chooses one output from $B$ for every input from $A$. Each input gives $|B|$ choices, and there are $|A|$ inputs. Therefore

$$|A\to B|=|B|^{|A|}.$$

For example, there are $2^2=4$ total functions from bool to bool. They are the constant false function, the constant true function, the identity function, and Boolean negation.

The familiar exponent law $(C^B)^A=C^{A\times B}$ appears as currying:

$$A\to(B\to C)\simeq A\times B\to C.$$

Currying changes how arguments are supplied, but it does not change the information in the function.

A recursive type refers to itself in its own definition. Lists are the central example.

A list is either Nil, which carries unit information, or Cons, which carries an element and another list. If $L(A)$ is the type of lists whose elements have type $A$, then

$$L(A)\simeq\mathbf{unit}+A\times L(A).$$

Substituting the same equation into itself reveals every possible finite length:

$$\begin{aligned} L(A)&=1+A\times L(A)\\ &=1+A\times(1+A\times L(A))\\ &=1+A+A^2+A^3+\cdots. \end{aligned}$$

The term $1$ describes the empty list. The term $A$ describes lists of length one. The term $A^2$ describes lists of length two, and so on.

Natural numbers

A natural number is either zero or the successor of another natural number:

$$\mathbf{nat}\simeq\mathbf{unit}+\mathbf{nat}.$$

Repeated expansion gives $1+1+1+\cdots$. This explains why the type contains infinitely many values. It also explains the isomorphism $\mathbf{nat}\simeq\mathbf{nat}\;\mathbf{option}$.

A recursive definition does more than describe data. It also determines how functions consume that data and how proofs reason about it.

For lists, every value was built by exactly one of two constructors. A complete proof about all lists must therefore have two cases:

1. Prove the property for Nil.
2. Assume the property for a list xs, then prove it for Cons (x, xs).

The first case is the base case. The second is the inductive step. Every constructor becomes one proof case.

Example: appending Nil

We want to prove that append (xs, Nil) = xs for every list xs.

For the base case, append (Nil, Nil) evaluates to Nil.

For the inductive step, assume append (xs, Nil) = xs. Then

$$\begin{aligned} \mathsf{append}(\mathsf{Cons}(x,xs),\mathsf{Nil}) &=\mathsf{Cons}(x,\mathsf{append}(xs,\mathsf{Nil}))\\ &=\mathsf{Cons}(x,xs). \end{aligned}$$

The second equality uses the inductive assumption. The proof follows the same structure as the list itself.

The shape of the data determines the shape of the program and the shape of the proof.

Type construction	Counting operation	Meaning
$A+B$	$|A|+|B|$	Choose a tagged value from either type
$A\times B$	$|A|\times|B|$	Choose one value from each type
$A\to B$	$|B|^{|A|}$	Choose one output for every input
$\mathbf{unit}$	$1$	Exactly one value
$\mathbf{void}$	$0$	No values

These correspondences explain the name algebraic data type. Equations from ordinary algebra become type isomorphisms, but every equation must be witnessed by concrete inverse functions.

Recursive types extend this picture. They describe lists, trees, and natural numbers, guide recursive programs, and supply induction principles. This is why algebraic data types matter both for programming and for theorem proving.