1 Demo: Agda in Action

\(\newcommand{\la}{\lambda} \newcommand{\Ga}{\Gamma} \newcommand{\ra}{\rightarrow} \newcommand{\Ra}{\Rightarrow} \newcommand{\La}{\Leftarrow} \newcommand{\tl}{\triangleleft} \newcommand{\ir}[3]{\displaystyle\frac{#2}{#3}~{\textstyle #1}}\)

\(\newcommand{\la}{\lambda} \newcommand{\Ga}{\Gamma} \newcommand{\ra}{\rightarrow} \newcommand{\Ra}{\Rightarrow} \newcommand{\La}{\Leftarrow} \newcommand{\tl}{\triangleleft} \newcommand{\ir}[3]{\displaystyle\frac{#2}{#3}~{\textstyle #1}}\)

This chapter contains a brief demonstration of Agda, the language used in PLFA and in CS 747. I won’t be explaining everything in detail, and you shouldn’t expect to understand everything fully. We’ll go over everything more carefully later.

Interactions with Agda take place within the text editor Emacs, using short keyboard sequences. One sequence brings in the demonstration file (842demo.agda, linked on the Handouts page; we’re using the starter version) and another activates Agda, checking syntax and providing highlighting.

The file starts with these lines:

module 842demo where

open import Relation.Binary.PropositionalEquality
open import Data.Nat

These lines start the module defined by the file, and import library code for using equality and natural numbers. These very basic notions are not built into Agda; they are constructed, and later we will see how this is done.

Next we have a datatype definition.

data List (A : Set) : Set where
  empty : List A
  add   : A → List A → List A

This is a definition of a polymorphic list datatype, parameterized by the type of elements A. It has two data constructors, empty and add. empty represents the empty list. add can be applied to an element and an existing list, and creates a new list with the element added to the existing list. We can build longer lists by applying add repeatedly, and there’s an example in the file. The only reason I imported natural numbers was to have something to put into an example list.

To apply a constructor or function to arguments, we simply list its name followed by its arguments. Applying the add constructor to arguments 2 and empty is just add 2 empty. The file has a longer example.

-- The list 1, 3, 2

ex1 : List ℕ
ex1 = add 1 (add 3 (add 2 empty))

Two hyphens (–) make the rest of the line into a comment. The next two lines declare the constant ex1 to be a list of natural numbers, and provide its definition. Reading the definition from the inside out, we start with the empty list, add 2, then add 3, and finally 1.

We’d like to define computations on lists, and the example we’ll use is the function append that produces the result of appending one list to another. For example, appending the list 2, 4 to the end of the list 1, 5, 3 should produce the list 1, 5, 3, 2, 4. Written in Agda, append (add 1 (add 5 (add 3 empty))) (add 2 (add 4 empty)) should produce the result  (add 1 (add 5 (add 3 (add 2 (add 4 empty))))).

The file declares append as a polymorphic function that consumes two lists of type A and produces one of the same. The right-hand side of the definition is incomplete.

append : {A : Set} → List A → List A → List A
append xs ys = {!!}

In the starter file, a question mark (?) is used as shorthand for {!!}, which is a "hole" to be filled in. With Agda activated, the exclamation marks (!!) are replaced with a highlight, and the hole is numbered. This is an active zone where interactive development is possible.

We can, for example, do a case analysis on the parameter xs. It is either empty or add applied to two arguments. To do this case analysis, we type xs into the hole and issue a two-chord keyboard command. This creates the two cases. Agda has chosen names for the two things that add was applied to, but we can change them, if we want.

append empty ys = {!!}
append (add x xs) ys = {!!}

In the first case, we know that the result is just ys. We can put this into the hole and ask Agda to accept it.

append empty ys = ys
append (add x xs) ys = {!!}

The second case takes a little more work. But we know that x is the first element of the result, so we can type add x into the hole and ask Agda to refine it (accept it as a partial answer).

append (add x xs) ys = add x {!!}

The hole should be filled in with the rest of the result. This is the rest of the first argument of append (which Agda called xs) with all of the second argument appended. That is, we do a recursive application of append. Here’s the full definition.

append : {A : Set} → List A → List A → List A
append empty ys = ys
append (add x xs) ys = add x (append xs ys)

This takes much longer to read (and even longer for me to typeset) than it does to do in Emacs. Here’s a short asciicast that illustrates real-time development. It’s a recording of a command-line terminal session, which captures characters and escape sequences for cursor movement and colours. It is played with a JavaScript player in your browser. I have a short separate page with more details, including keyboard controls for the player.

The Emacs frame normally has two windows, the main one above for editing the Agda file, and a smaller one below for information and other responses. I have added a third window to the right, which is logging commands that I type, since the asciicast is silent and I can’t explain what I’m doing (most of the explanation is written out above each asciicast). Some common commands are filtered out of the log (e.g. standard cursor movements). You can safely ignore the third window for now.

We can test that our code works for the example above. The method may be a little different from your past experience.

ex2 : append (add 1 (add 5 (add 3 empty)))
             (add 2 (add 4 empty))
      ≡
      (add 1 (add 5 (add 3 (add 2 (add 4 empty)))))
ex2 = refl

The type of ex2 is a statement that the result of applying append to our chosen examples is equal to our expected result. Agda’s type system is strong enough to express logical statements, which is a huge advantage. The proof of our statement is on the definition line. refl is short for "reflexivity", and it will work if the expressions on the left and right sides of the equality symbol (which is ≡, as = is reserved for definitions) reduce to the same value when all computation is carried out.

Here’s a more general theorem about append. It says that append empty xs is just xs, for any xs. In Agda, this theorem is a function that consumes xs and produces a proof that append empty xs equals xs.

append-empty-left : {A : Set} →
  forall (xs : List A) → append empty xs ≡ xs
append-empty-left xs = {!!}

What would the proof look like? Looking at the first line of the definition of append, we can see that computing append empty xs will result in xs. So refl will work as the proof.

append-empty-left : {A : Set} →
  forall (xs : List A) → append empty xs ≡ xs
append-empty-left xs = refl

But the next theorem, about appending empty on the right, does not have as obvious a proof.

append-empty-right : {A : Set} →
  forall (xs : List A) → append xs empty ≡ xs
append-empty-right xs = {!!}

Just to be clear about the theorem being a function, here is an example of its use. To show that appending the empty list to the list 1, 3, 2 results in the list 1, 3, 2, we apply theorem append-empty-right to the list 1, 3, 2.

ex3 : append (add 1 (add 3 (add 2 empty))) empty
      ≡
      (add 1 (add 3 (add 2 empty)))
ex3 = append-empty-right (add 1 (add 3 (add 2 empty)))

This example will only work when we finish the definition of append-empty-right. But we can’t just supply refl as the proof, because the definition of append does not have a case for append xs empty. That definition does a case analysis on its first argument. So to be able to make progress using that definition, we should do the case analysis also. Entering xs in the hole in the definition of append-empty-right and asking Agda to split into cases, we get:

append-empty-right : {A : Set} →
  forall (xs : List A) → append xs empty ≡ xs
append-empty-right empty = {!!}
append-empty-right (add x xs) = {!!}

What is the type of what we need to fill in for the first hole? We might expect it to be append empty empty ≡ empty. But Agda can do the computation on the left, and if we ask it what it wants, it will say empty ≡ empty. That we can prove with refl.

append-empty-right : {A : Set} →
  forall (xs : List A) → append xs empty ≡ xs
append-empty-right empty = refl
append-empty-right (add x xs) = {!!}

For the remaining hole, we would expect the type to be append (add x xs) empty ≡ add x xs. But once again, Agda can make progress on the computation on the left, because it is the second case in the definition of append. The simplified type is add x (append xs empty) = add x xs. There is a recursive application of append on the left. What does the recursive application of the function append-empty-right give us? It gives us append xs empty ≡ xs. We can ask Agda to rewrite the type of what needs to go into the hole using this equality.

append-empty-right (add x xs)
  rewrite append-empty-right xs = {!!}

Now the type expected by Agda in the hole is add x xs ≡ add x xs, and this can be proved with refl.

append-empty-right (add x xs)
  rewrite append-empty-right xs = refl

Here’s the completed definition of our theorem.

append-empty-right : {A : Set} →
  forall (xs : List A) → append xs empty ≡ xs
append-empty-right empty = refl
append-empty-right (add x xs)
  rewrite append-empty-right xs = refl

And here’s the asciicast of the interactive development.

You may recognize this as a proof by structural induction on the list xs. But since a logical statement can be a type, and a proof of it can be a value inhabiting that type, the inductive proof in this case is naturally expressed as a function, with the inductive hypothesis being the recursive application of the function. Proving in Agda is programming.

To summarize, Agda’s type system and computational model are strong enough to define complex datatypes, computations on them, and theorems about those computations, all with the same powerful mechanisms. This makes it a useful tool in which to both write programs and verify their properties.