Let us try to code the Natural Numbers ℕ (sometimes one writes Nat) from scratch.

Comments:

  1. -- at the beginning affects the line
  2. An opening {- followed by -} comments a block

The following

{-# OPTIONS --without-K --safe #-}

is a comment. However, the particular syntax {-# … #-} is a directive to the Agda compiler. We can give options to it without having to include them on the command line.

The directive --without-K, although not strictly needed here, puts Agda in a mode (concerning propositional equality) that is compatible with Homotopy Type Theory.

Important: every file is a module and the top module name must match the file name: 
module simplenat where

This is our first judgements:

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

Set is Agda’s notion of Type, or 𝕌—we should not think of it as Set Theory. (This is only the fist level, but more about this later.)

So, in the first line we made the judgement that \(ℕ\) is a type. The context is empty.

Moreover, we have two more:

  1. zero is a term of type ℕ

  2. suc is a term of type ℕ → ℕ: our judgement is n : ℕ ⊢ suc n : ℕ.

    You would be right to expect that we should interpret this as the successor of \(n\), and that it should simply mean \(n+1\).

In short, we are doing Peano’s arithmetic.

Why don’t we build the Booleans, while we’re at it:

data 𝔹 : Set where
  t : 𝔹
  f : 𝔹

For efficiency, it is best to let the system be aware that the naturals we are building had better be the same thing as the builtin naturals of the underlying Haskell compiler and hence of the underlying machine:

{-# BUILTIN NATURAL ℕ #-}

In this way we can write 0, 1, 2, … instead of zero, suc (zero), suc (suc (zero)), ….

Let us define addition and Multiplication of natural numbers:

_+_ : ℕ → ℕ → ℕ
zero + m = m
suc n + m = suc (n + m)

_*_ : ℕ → ℕ → ℕ
zero * m = zero
suc n * m = m + (n * m)

You will have noticed the both were defined by recursion on the first variable. It will have some practical consequences on the mechanics of some proofs. More interesting facts:

  1. The functions are defined by pattern matching on the variable(s)

  2. Oh, wait, did I say function?

    1. We are constructing a term as follows: n : ℕ, m : ℕ ⊢ (n + m) : ℕ. This is a “function” of two variables that Agda (and other similar proof assistants) parse as the following type:

      ℕ → ℕ → ℕ = ℕ → (ℕ → ℕ)

      This is called Currying, in honor of the mathematician Haskell Curry, after whom the language Haskell is also named.

    2. The notation is worth thinking about: we are using an infix one, with the function “body,” the plus sign, in the middle, right than in front of the variables. So the expressions below are exactly the same:

      n + m = _+_ n m = (_+_ n) m

      (Why?) Technically, we refer to such a function as being “infix,” as opposed to prefix.

Pattern matching, infix and even postfix function names, with the liberal use of whitespace that goes with them, are cornestones of the Agda idiomatic writing style. Here is another example:

if_then_else_ : {A : Set} → 𝔹 → A → A → A
if t then x else y = x
if f then x else y = y

In the above code, we have that if_then_else_ is of type {A : Set} → 𝔹 → A → A → A. The novel feature is the expression {A : Set}: with it we signal that A is a type, but that it is declared as an implicit variable: we do not mention it in the actual body of the function, because Agda can figure out that A is a type if x and y are judged to be of type A.

A standard example of implicit variables occurs in the identity function:

id : {A : Set } → A → A
id x = x

We can implement a simple min function for the Natural numbers as follows. First, let’s define an order:

_≤_ : ℕ → ℕ → 𝔹
zero ≤ _ = t
suc _ ≤ zero = f
suc n ≤ suc m = n ≤ m

then define minℕ to return the minimum of two natural numbers n and m

minℕ : ℕ → ℕ → ℕ
minℕ n m = if n ≤ m
           then n
           else m

One can go along way with operations like the one above.

However, what if we want to prove that, say, addition is commutative? Well, we cannot simply test

n : ℕ, m : ℕ ⊢ (n + m) = (m + n) --Wrong!!!

The equal sign = is what Agda uses for definitional equality in the underlying type theory, meaning we cannot test for it. What we need is a proposition in order to state that to things are equal, and a term of said proposition to conclude that it is indeed true that they are equal. In other words, we need a notion of propositional equality, which we will typically denote by ≡.