A Taste of Agda

The objective of this section is to provide a first glimpse of Agda with some small examples. The first one is a demonstration of dependently typed programming, and the second shows how to use Agda as a proof assistant. Finally, we build a complete program and compile it to an executable program with the GHC and Javascript backends.

Preliminaries

Before proceeding, make sure that you installed Agda and a compatible version of the standard library.

Agda programs are typically developed interactively, which means that one can type check code which is not yet complete but contain “holes” which can be filled in later. Editors with support for interactive development of Agda programs include Emacs via the Emacs mode, Atom via the agda mode for Atom, Visual Studio Code via the agda mode for VSCode, and Vim via agda-vim.

Hint

If you want a sneak peek of Agda without installing it, try the Agda Pad

Note

In this introduction we use several of Agda’s interactive commands to get information from the typechecker and manipulate code with holes. Here is a list of the commands that will be used in this tutorial:

• C-c C-l: Load the file and type-check it.

• C-c C-d: Deduce the type of a given expression.

• C-c C-n: Normalise a given expression.

• C-c C-,: Shows the type expected in the current hole, along with the types of any local variables.

• C-c C-c: Case split on a given variable.

• C-c C-SPC: Replace the hole with a given expression, if it has the correct type.

• C-c C-r: Refine the hole by replacing it with a given expression applied to an appropriate number of new holes.

• C-c C-x C-c (C-x C-c in VS Code): Compile an Agda program.

See Notation for key combinations for a full list of interactive commands (keybindings).

Programming With Dependent Types: Vectors

In the code below, we model the notion of vectors (in the sense of computer science, not in the mathematical sense) in Agda. Roughly speaking, a vector is a list of objects with a determined length.

module hello-world-dep where

open import Data.Nat using (ℕ; zero; suc)

data Vec (A : Set) : ℕ → Set where
  []  : Vec A zero
  _∷_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (suc n)

infixr 5 _∷_

Paste or type the code above in a new file with name hello-world-dep.agda. Load the file (in Emacs C-c C-l). This also saves the file. If the agda source code was loaded correctly, you should see that the code is highlighted and see a message *All done* .

Note

If a file does not type check Agda will complain. Often the cursor will jump to the position of the error, and the error will (by default) be underlined. Some errors are treated a bit differently, though. If Agda cannot see that a definition is terminating/productive it will highlight it in light salmon, and if some meta-variable other than the goals cannot be solved the code will be highlighted in yellow (the highlighting may not appear until after you have reloaded the file). In case of the latter kinds of errors you can still work with the file, but Agda will (by default) refuse to import it into another module, and if your functions are not terminating Agda may hang. See Background highlighting for a full list of the different background colors used by Agda.

Tip

If you do not like the way Agda syntax or errors are highlighted (if you are colour-blind, for instance), then you can tweak the settings by typing M-x customize-group RET agda2-highlight RET in Emacs (after loading an Agda file) and following the instructions.

Agda programs are structured into modules. Each Agda file has one top-level module whose name must match the name of the file, and zero or more nested modules. Each module contains a list of declarations. This example has a single top-level module called hello-world-dep, which has three declarations:

1. An open import statement that imports the datatype ℕ and its constructors zero and suc from the module Data.Nat of the standard library and brings them into scope,

2. A data declaration defining the datatype Vec with two constructors: the empty vector constructor [] and the cons constructor _∷_,

3. And finally an infixr declaration specifying the precedence for the cons operation.

Tip

Agda uses Unicode characters in source files (more specifically: the UTF-8 character encoding), such as ℕ, →, and ∷ in this example. Many mathematical symbols can be typed using the corresponding LaTeX command names. To learn how to enter a unicode character, move the cursor over it and enter M-x describe-char or C-u C-x =. This displays all information on the character, including how to input it with the Agda input method. For example, to input ℕ you can type either \Bbb{N} or \bN. See Unicode input for more details on entering unicode characters.

The datatype Vec

Let us start by looking at the first line of the definition of Vec:

data Vec (A : Set) : ℕ → Set where

This line declares a new datatype and names it Vec. The words data and where are keywords, while the part Vec (A : Set) : ℕ → Set determines the type of Vec.

Vec is not a single type but rather a family of types. This family of types has one parameter A of type Set (which is the sort of small types, such as ℕ, Bool, …) and one index of type ℕ (the type of natural numbers). The parameter A represents the type of the objects of the vector. Meanwhile, the index represents the length of the vector, i.e. the number of objects it contains.

Together, this line tells us that, for any concrete type B : Set and any natural number m : ℕ, we are declaring a new type Vec B m, which also belongs to Set.

The constructors [] and _∷_

Each constructors of a datatype is declared on a separate line and indented with a strictly positive number of spaces (in this case two).

We chose the name [] for the first constructor. It represents the empty vector, and its type is Vec A 0, i.e. it is a vector of length 0.

The second constructor is a mixfix operator named _∷_ (pronounced cons). For any number n : ℕ, it takes as input an object of A and a vector of length n. As output, it produces a vector with length suc n, the successor of n. The number n itself is an implicit argument to the constructor _∷_.

The final declaration with keyword ìnfixr does not belong to the datatype declaration itself; therefore it is not indented. It establishes the precedence of the operator _∷_.

Tip

You can let Agda infer the type of an expression using the ‘Deduce type’ command (C-c C-d). First press C-c C-d to open a prompt, enter a term, for instance 3 ∷ 2 ∷ 1 ∷ [], and press return. Agda infers its type and return the type Vec ℕ 3, meaning that the given term is a vector with 3 objects of type ℕ.

Note

Almost any character can be used in an identifier (like α, ∧, or ♠, for example). It is therefore necessary to have spaces between most lexical units. For example 3∷2∷1∷[] is a valid identifier, so we need to write 3 ∷ 2 ∷ 1 ∷ [] instead to make Agda parse it successfully.

The total function lookup

Now that Vec is defined, we continue by defining the lookup function that given a vector and a position, returns the object of the vector at the given position. In contrast to the lookup function we could define in most (non-dependently typed) programming languages, this version of the function is total: all calls to it are guaranteed to return a value in finite time, with no possibility for errors.

To define this function, we use the Fin datatype from the standard library. Fin n is a type with n objects: the numbers 0 to n-1 (in unary notation zero, suc zero, …), which we use to model the n possible positions in a vector of length n.

Now create a new file called hello-world-dep-lookup.agda file and type or paste:

module hello-world-dep-lookup where

open import Data.Nat using (ℕ)
open import Data.Vec using (Vec; _∷_)
open import Data.Fin using (Fin; zero; suc)

variable
  A : Set
  n : ℕ

lookup : Vec A n → Fin n → A
lookup (a ∷ as) zero = a
lookup (a ∷ as) (suc i) = lookup as i

The Vec type that we saw before is actually already in the module Data.Vec of the standard library, so we import it instead of copying the previous definition.

We have declared A and n as generalizable variables to avoid the declaration of implicit arguments. This allows us to use A and n in the type of lookup without binding the names explicitly. More explicitly, the full type of lookup (which we can get by using C-c C-d) is:

lookup : {A : Set} {n : ℕ} → Vec A n → Fin n → A

Warning

zero and suc are not the constructors of ℕ that we saw before, but rather the constructors of Fin. Agda allows overloading of constructor names, and disambiguates between them based on the expected type where they are used.

The definition of the lookup function specifies two cases:

• Either the vector is a ∷ as and the position is zero, so we return the first object a of the vector.

• Or the vector is a ∷ as and the position is suc i, so we recursively look up the object at position i in the tail as of the vector.

There are no cases for the empty vector []. This is no mistake: Agda can determine from the type of lookup that it is impossible to look up an object in the empty vector, since there is no possible index of type Fin 0. For more details, see the section on coverage checking.

Agda as a Proof Assistant: Proving Associativity of Addition

In this section we state and prove the associativity of addition on the natural numbers in Agda. In contrast to the previous section, we build the code line by line. To follow along with this example in Emacs, reload the file after adding each step by pressing C-c C-l.

Statement of associativity

We start by creating a new file named hello-world-proof.agda. Paste or type the following code:

module hello-world-proof where

Now we import the datatype ℕ and the addition operation _+_, both defined in the Agda Builtin library.

open import Data.Nat using (ℕ; _+_)

Next, we import the propositional equality type _≡_ from the module Relation.Binary.PropositionalEquality.

open import Relation.Binary.PropositionalEquality using (_≡_)

Under the Curry-Howard correspondence, the type x ≡ y corresponds to the proposition stating that x and y are equal objects. By writing a function that returns an object of type x ≡ y, we are proving that the two terms are equal.

Now we can state associativity: given three (possibly different) natural numbers, adding the first to the addition of the second and the third computes to the same value as adding the addition of the first and the second to the third. We name this statement +-assoc.

+-assoc : Set
+-assoc = ∀ (x y z : ℕ) → x + (y + z) ≡ (x + y) + z

This is not yet a proof, we have merely written down the statement (or enunciation) of associativity.

Proof of associativity

The statement +-assoc is a member of Set, i.e. it is a type. Now that we have stated the property in a way that Agda understands, our objective is to prove it. To do so, we have to construct a function of type +-assoc.

First, we need to import the constructors zero and suc of the already imported datatype ℕ and the constructor refl (short for reflexivity) and function cong (short for congruence) from the standard library.

open import Data.Nat using (zero; suc)
open import Relation.Binary.PropositionalEquality using (refl; cong)

To prove +-assoc we need to find an object of that type. Here, we name this object +-assoc-proof.

+-assoc-proof : ∀ (x y z : ℕ) → x + (y + z) ≡ (x + y) + z

If we load now the file, Agda gives an error: “The following names are declared but not accompanied by a definition: +-assoc-proof”. Indeed, we have only declared the type of +-assoc-proof but not yet given a definition. To build the definition, we need to know more about holes and case splitting.

Holes and case splitting

We can let Agda help us to write the proof by using its interactive mode. To start, we first write a simple clause so the file can be loaded even if we still do not know the proof. The clause consists of the name of the property, the input variables, the equals symbol = and the question mark ?.

+-assoc-proof x y z = ?

When we reload the file, Agda no longer throws an error, but instead shows the message *All Goals* with a list of goals. We have now entered the interactive proving mode. Agda turns our question mark into what is called a hole { }0 with a label 0. Each hole stands as a placeholder for a part of the program that is still incomplete and can be refined or resolved interactively.

Note

You are not supposed to enter a hole such as { }0 manually, Agda takes care of the numbering when you load the file. To insert a hole, write either ? or {! !} and load the file to make Agda assign a unique number to it.

To get detailed information about a specific hole, put the cursor in it and press C-c C-,. This displays the type of the hole, as well as the types of all the variables in scope. In this example we get the information that the goal type is x + (y + z) ≡ x + y + z, and there are three variables x, y, and z in scope, all of type ℕ.

Note

You might wonder why Agda displays the term (x + y) + z as x + y + z (without parenthesis). This is done because of the infix statement infixl 6 _+_ that was declared in the imported Agda.Builtin.Nat module. This declaration means that the _+_ operation is left-associative. More information about mixfix operator like the arithmetic operations. You can also check this associativity example.

To continue writing our proof, we now pick a variable and perform a case split on it. To do so, put the cursor inside the hole and press C-c C-c. Agda asks for the name of the pattern variable to case on. Let’s write x and press return. This replaces the previous clause with two new clauses, one where x has been replaced by zero and another where it has been replaced by suc x:

+-assoc-proof zero y z = {  }0
+-assoc-proof (suc x) y z = {  }1

Important

The x in the type signature of +-assoc-proof is not the same as the x pattern variable in the last clause where suc x is written. The following would also work: +-assoc-proof (suc x₁) y z = { }1. The scope of a variable declared in a signature is restricted to the signature itself.

Instead of one hole, we now have two. The first hole has type y + z ≡ y + z, which is easy to resolve. To do so, put the cursor inside the first hole labeled 0 and press C-c C-r. This replaces the hole by the term refl, which stands for reflexivity and can be used any time we want to construct a term of type w ≡ w for some term w.

+-assoc-proof zero y z = refl
+-assoc-proof (suc x) y z = {  }1

Now we have one hole left to resolve. By putting the cursor in it and pressing C-c C-, again, we get the type of the hole: suc x + (y + z) ≡ suc x + y + z. Agda has already applied the definition of _+_ to replace the left-hand side (suc x + y) + z of the equation by suc (x + y + z), and similarly replaced the right-hand side suc x + (y + z) by suc (x + (y + z)).

Tip

You can use the go-to-definition command by selecting the definition that you want to check eg. _+_ and pressing M-. in Emacs or C-M-\ in Atom. This takes you to the definition of _+_, which is originally defined in the builtin module Agda.Builtin.Nat.

Tip

You can ask Agda to compute the normal form of a term. To do so, place the cursor in the remaining hole (which should not contain any text at this point) and press C-c C-n. This prompts you for an expression to normalize. For example, if we enter (suc x + y) + z we get back suc (x + y + z) as a result.

Proof by induction

If we now look at the type of the remaining hole, we see that both the left-hand side and the right-hand side start with an application of the constructor suc. In this kind of situation it suffices to prove that the two arguments to suc are equal. This principle is called congruence of equality _≡_, and it is expressed by the Agda function cong.

To use cong we need to apply it to a function or constructor, in this case suc. If we ask Agda to infer the type of cong suc by pressing C-c C-d and entering the term, we get back the type {x y : ℕ} → x ≡ y → suc x ≡ suc y. In other words, cong suc takes as input a proof of an equality between x and y and produces a new proof of equality between suc x and suc y. We write cong suc in the hole and again press C-c C-r to refine the hole. This results in the new line

+-assoc-proof (suc x) y z = cong suc {  }2

where the new hole with number 2 is of type x + (y + z) ≡ x + y + z.

To finish the proof, we now make a recursive call +-assoc-proof x y z. Note that this has type x + (y + z) ≡ (x + y) + z, which is exactly what we need. To complete the proof, we type +-assoc-proof x y z into the hole and solve it with C-c C-space. This replaces the hole with the given term and completes the proof.

Note

When we define a recursive function like this, Agda performs termination checking on it. This is important to ensure the recursion is well-founded, and hence will not result in an invalid (circular) proof. In this case, the first argument x is structurally smaller than the first argument suc x on the left-hand side of the clause, hence Agda allows us to make the recursive call. Because termination is an undecidable property, Agda will not accept all terminating functions, but only the ones that are mechanically proved to terminate.

The final proof +-assoc-proof is defined as follows:

+-assoc-proof zero y z = refl
+-assoc-proof (suc x) y z = cong suc (+-assoc-proof x y z)

When we reload the file, we see *All Done*. This means that +-assoc-proof is indeed a proof of the statement +-assoc.

Here is the final code of the ‘Hello world’ proof example, with all imports together at the top of the file:

module hello-world-proof where

open import Data.Nat using (ℕ; zero; suc; _+_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)

+-assoc : Set
+-assoc = ∀ (x y z : ℕ) → x + (y + z) ≡ (x + y) + z

+-assoc-proof : ∀ (x y z : ℕ) → x + (y + z) ≡ (x + y) + z
+-assoc-proof zero y z = refl
+-assoc-proof (suc x) y z = cong suc (+-assoc-proof x y z)

Tip

You can learn more details about proving in the chapter Proof by Induction of the online book Programming Language Foundations in Agda.

Building an Executable Agda Program

Agda is a dependently typed functional programming language. This means that we can write programs in Agda that interact with the world. In this section, we write a small ‘Hello world’ program in Agda, compile it, and execute it. In contrast to the standalone example on the Hello World page, here we make use of the standard library to write a shorter version of the same program.

Agda Source Code

First, we create a new file named hello-world-prog.agda with Emacs or Atom in a folder that we refer to as our top-level folder.

{-# OPTIONS --guardedness #-}

module hello-world-prog where

open import IO

main : Main
main = run (putStrLn "Hello, World!")

A quick line-by-line explanation:

• The first line is a pragma (a special comment) that specifies some options at the top of the file.

• The second line declares the top-level module, named hello-world-prog.

• The third line imports the IO module from the standard library and brings its contents into scope.

• A module exporting a function main of type Main (defined in the IO module of the standard library) can be compiled to a standalone executable. For example: main = run (putStrLn "Hello, World!") runs the IO command putStrLn "Hello, World!" and then quits the program.

Compilation with GHC Backend

Once we have loaded the program in Emacs or Atom, we can compile it directly by pressing C-c C-x C-c and entering GHC. Alternatively, we can open a terminal session, navigate to the top-level folder and run:

agda --compile hello-world-prog.agda

The --compile flag here creates via the GHC backend a binary file in the top-level folder that the computer can execute.

Finally, we can then run the executable (./hello-world-prog on Unix systems, hello-world-prog.exe on Windows) from the command line:

$ cd <your top-level folder>
$ ./hello-world-prog
Hello, World!

Compilation with JavaScript Backend

The JavaScript backend translates the Agda source code of the hello-world-prog.agda file to JavaScript code.

From Emacs or Atom, press C-c C-x C-c and enter JS to compile the module to JavaScript. Alternatively, open a terminal session, navigate to the top-level folder and run:

agda --js hello-world-prog.agda

This creates several .js files in the top-level folder. The file corresponding to our source code has the name jAgda.hello-world-prog.js.

Hint

The additional --js-optimize flag can be used to make the generated JavaScript code faster but less readable. Moreover, the --js-minify flag makes the generated JavaScript code smaller and even less readable.

Where to go from here?

There are many books and tutorials on Agda. We recommend this list of tutorials.

Join the Agda Community!

Get in touch and join the Agda community, or join the conversation on the Agda Zulip.