3. Types, Constructors, And Cases

Consider the natural numbers.

Instead of beginning with an already completed collection $\{0,1,2,3,\ldots\}$ we can use the familiar constructive description of the natural numbers.

There are two constructors:

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

Starting from zero, repeated use of suc gives:

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

This constructive presentation is central to approaches such as Martin-Löf type theory, which develops ideas connected to intuitionism, type theory, and the propositions-as-types tradition.

Every natural number constructed in this way has one of two forms.

It is either

zero

or

suc(k)

for some smaller natural number k.

That gives us a finite set of cases even though there are infinitely many natural numbers.

A function on natural numbers can be defined by considering these forms.

For a function of one natural-number argument, there are two cases:

zero
suc(k)

For a function of two natural-number arguments, there are four combinations:

zero, zero
zero, suc(l)
suc(k), zero
suc(k), suc(l)

This is where a table becomes possible.

Recursive calls can also move to structurally smaller data.

If a recursive definition handles suc(k) by making a recursive call on k, the recursive call is made on structurally smaller data.

For example: $f(suc(k)) \mapsto f(k)$

removes one suc.

Starting with $f(suc(suc(suc(zero))))$ we move to $f(suc(suc(zero)))$, then $f(suc(zero))$, then $f(zero)$.

A structurally recursive definition has two features worth watching:

Every constructor case must be handled.

Recursive calls must move toward smaller inputs.

A recursion table can make both visible.