A Gentle Introduction to Agda

A very easy introduction to Agda for working programmers.

I want you, as a programmer, to clear your mind. Better yet, close your eyes and imagine looking up at a star-studded night sky.

What you see in your mind is a universe filled with stars. Now, imagine a universe filled with natural numbers. This universe contains nothing but. If you were the creator of such a universe, an obvious question is how would you go about creating the very first natural number.

Well, to be realistic, nothing can be created out of thin air. There has to be a baseline. Something that is universally true and known to exist as a creation tool without the need for further proving.

In the case of natural numbers, we agree that zero is that baseline. It’s our universe’s Big Bang. We call it our axiom.

In order to classify natural numbers, we write ℕ as a type of all natural numbers. We say that all natural numbers are members of a natural number set ℕ.

We can write down a definition for natural numbers as follows:

--------------
zero : ℕ
m : ℕ
--------------
succ m : ℕ

Our baseline, or base case, is zero is a first natural number or ℕ. Our inductive case is if m is ℕ, then succ m must also be ℕ. At this point, we assume that succ stands for successor, or what comes after m. But there is absolutely nothing in the definition that states so. The only fact is succ m is a natural number ℕ.

These rules provide the only two ways of creating natural numbers, aka zero and succ. Therefore, these are all natural numbers (can you guess what these numbers’ equivalents in integers are?)

zero
succ zero
succ (succ zero)
succ (succ (succ zero))

To create a type in Agda, we start by writing a signature data Nat : Set which reads, “new type Nat of type Set”. In Agda, everything has a type, including types themselves, such as Nat. Set happens to be the mother of all types.

Next, we define the possible constructors for our newly created Nat. The first one is, of course, zero. We also want a way to create more natural numbers out of zero. We name the second constructor succ, for successor. succ has a type of Nat -> Nat, or a function that maps a Nat to a Nat. succ is effectively a way to define the next natural number from an existing one m.

data ℕ : Set where
  zero : ℕ
  succ : ℕ -> ℕ

Next, we can define addition on natural numbers as a recursive function:

_+_ : ℕ -> ℕ -> ℕ
zero + y = y
(succ x) + y = succ (x + y)

The function _+_ is an infix operator where the underlines are placeholders for operands. In this case, within the function body, x and y are two inferred operands.

The function starts by pattern-matching the operands. The base case is when an operand is zero and another is any natural number y. Because we know as an axiom that zero is an additive identity, we can conclude that zero + y = y.

The inductive case is when the first operand is any natural number succ x and the second is another natural number y. Due to associativity in addition, (succ x) + y = succ (x + y). If you replace succ x with 1 + x, (1 + x) + y = 1 + (x + y). Thus, this case holds true.

Note that the inductive case takes a recursive spin, calling itself (_+_) on the right-hand side.

When evaluated in Agda, (succ zero) + (succ zero) will results in succ (succ zero). We finally have a mean to create natural numbers and an + operator to add them together at will.