3. Types, Constructors, and Destructors

Stefan Kober

Recursion tables only make sense once we are clear about the kind of objects they apply to.

Consider the natural numbers. Instead of thinking of them as a set of given objects, we can describe how they are constructed. This perspective is central to dependent type theory, where mathematical objects are understood through the rules by which they are constructed. It grew out of intuitionism and the Curry-Howard correspondence, and later found technical expression in work by Per Martin-Löf and others.

There are two rules:

  • $zero$ is a natural number
  • if $n$ is a natural number, then $suc(n)$ is a natural number

Starting from $zero$, repeated application of $suc$ generates all natural numbers:

$zero$
$suc(zero)$
$suc(suc(zero))$
...

Every natural number is built in this way. There are no other cases.

That is why $zero$ and $suc$ are called the constructors of the natural numbers.

To define a function on such values, we must also be able to take them apart. This is done by inspecting how a value was built.

For natural numbers, there are again two possibilities:

  • the value is $zero$
  • the value is $suc(k)$ for some $k$

A function definition proceeds by handling these cases. In the $zero$ case, we give a direct result. In the $suc(k)$ case, we typically define the result in terms of $k$, which is a simpler value.

This step can be seen directly.

The number $4$, for example, is built as

$suc(suc(suc(suc(zero))))$.

If we apply a function defined by recursion, the case $suc(k)$ reduces the problem to $k$:

$$ f(suc(k)) \mapsto f(k). $$

In this example, that means:

$$ f(suc(suc(suc(suc(zero))))) \mapsto f(suc(suc(suc(zero)))). $$

Each step removes one layer of construction. Repeating this process, we eventually reach $f(zero)$, where a direct value is given.

By construction we can be sure that we end up with a value after a finite amount of function applications.

This is what we mean when we say that numbers become simpler.

We will now look at a concrete example where all of this comes together.