Building the Naturals in Agda

A years-long interest in the foundations of mathematics has led me to want to formalize what I’ve learned in a functional programming language called Agda. The promise is that, by formalizing mathematical truths, one gains a deeper understanding of how mathematics is built from the ground up.

While there are a few tutorials on Agda on the web, in my experience, most assume a lot of background information. The learning curve is quite steep, such that even after 3 months, I’m still stuck on the basics. I’ve had to revise my notes over and over, as I keep finding mistakes and gaps in my understanding.

⚠ The following are notes that I’ve decided to make public in order to force myself to make them as tidy as possible. They are not meant to be a tutorial, nor can I guarantee that they are free from errors! I’m here simply applying the so-called Feynman technique of imagining that I have an audience to whom I’m explaining the material.¹

I will be following the tutorial from the online book Programming Language Foundations in Agda by Wadler et al.

Preliminaries

The mathematical theory behind Agda is dependent type theory, which deals with types and their terms in a similar way that set theory deals with sets and their elements. But unlike set theory, where an element can be said to “belong” to more than one set, a term “belongs” to a unique type. And instead of writing \(x \in A\), we express the idea that a term \(a\) is of type \(A\) as \(a: A\). Here \(A\) is an atomic type, and \(a\) is an atomic term. In addition to atomic types and terms, we have function types like \(A \to B\) and function terms like \(f: A \to B\).

The naturals

The sequence of natural numbers (ℕ) starts with \(0,1,2,3, \dots,\) and on to infinity. In Agda (and type theory in general), the naturals ℕ are an (atomic) type, and each natural number is an (atomic) term of that type. In Agda code, we express this as follows:

data ℕ : Set

(For some reason, in Agda a type is called a Set. Go figure!)

Our first order of business is to generate all those terms of type ℕ. How do we do that? We use special functions called constructors. The only two constructors needed to generate the naturals are called “zero” and “successor”:

This says that the constructors may be derived freely. Usually one has one ore more premises above the line, from which we may infer the conclusion below the line. No premises means that the conclusion needs no justification.

So, given the type \(\mathbb{N}\), we may freely assume the term \(\mathtt{zero}\).

How do we get all the other terms of \(\mathbb{N}\)? That’s where \(\mathtt{suc}\) (short for “successor”) comes in. It’s a unary function, meaning that it takes one single argument (in this case, a natural number) and returns a natural number. Since the only term we have (thus far) is \(\mathtt{zero}\), \(\mathtt{suc}\) will take \(\mathtt{zero}\) and return the successor of zero, which is \(1\). So now we have two natural numbers: zero and \(1\). And if we “feed” \(1\) to \(\mathtt{suc}\), it will give us the successor of \(1\), which is \(2\). And so on ad infinitum.

Hidden details

Now, initially I had a hard time understanding this, for how is \(\mathtt{zero}\) a constructor? We said that a constructor is a function, which is a term but of the function type. The constructor \(\mathtt{suc}\), for example, is of this type \(\mathbb{N \to N}\). So why isn’t \(\mathtt{zero}\), as a constructor, declared similarly? This is not often mentioned, but \(\mathtt{zero}\) is a nullary function, that is, one that accepts no arguments and just returns a constant term of type \(\mathbb{N}\). In fact, a nullary function is also just called a constant. That constant term can be whatever we want. Here, we obviously want \(\mathtt{zero}\) to return the number zero as the constant term. Still, there is something strange about it, because we seem to be blurring the line between a constructor and the thing constructed, between a function that returns a constant and the constant itself. But perhaps it is no more strange than the very concept of the number \(0\) or the empty set \(\varnothing\).

One other thing to keep in mind is that \(\mathtt{suc}\), when taking \(\mathtt{zero}\), actually returns the term \(\mathtt{suc(zero)}\). Feeding this term back to \(\mathtt{suc}\) gives us the next term \(\mathtt{suc(suc(zero))}\), and so on. We use the symbols \(1\) and \(2\) as abbreviations for these terms.

Seven

Lastly, let’s construct the number \(7\):

seven : ℕ
seven = suc (suc (suc (suc (suc (suc (suc zero))))))

In the signature (the first line), we declare a new term of type \(\mathbb{N}\) with the name “seven” (note that we can’t use the numeral \(7\) as a name, Agda doesn’t like that). On the second line, we show what this new term equates to, or, equivalently, how we can construct the new term.

So far so good. Constructing the natural numbers is pretty straightforward. Things get a little hairy when we turn to addition, however.