Martin Escardo. Notes originally written for the module Advanced Functional Programming of the University of Birmingham, UK.

Introduction to Agda

Everything defined and briefly discussed in this introduction will be redefined and discussed in more detail in other handouts.

Initial examples of types in Agda

Here are some examples of types:

data Bool : Type where
 true false : Bool

data ℕ : Type where
 zero : ℕ
 suc  : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

data List (A : Type) : Type where
 []   : List A
 _::_ : A → List A → List A

infixr  _::_

The pragma BUILTIN NATURAL is to get syntax sugar to be able to write 0,1,2,3,… rather than the more verbose

• zero
• suc zero
• suc (suc zero)
• suc (suc (suc zero))
• ⋯

We pronounce suc as “successor”.

Examples of definitions using the above types

not : Bool → Bool
not true  = false
not false = true

_&&_ : Bool → Bool → Bool
true  && y = y
false && y = false

_||_ : Bool → Bool → Bool
true  || y = true
false || y = y

infixr  _||_
infixr  _&&_

if_then_else_ : {A : Type} → Bool → A → A → A
if true  then x else y = x
if false then x else y = y

_+_ : ℕ → ℕ → ℕ
zero  + y = y
suc x + y = suc (x + y)

_*_ : ℕ → ℕ → ℕ
zero  * y = 
suc x * y = x * y + y

infixr  _+_
infixr  _*_

sample-list₀ : List ℕ
sample-list₀ =  ::  ::  :: []

sample-list₁ : List Bool
sample-list₁ = true || false && true :: false :: true :: true :: []

length : {A : Type} → List A → ℕ
length []        = 
length (x :: xs) =  + length xs

_++_ : {A : Type} → List A → List A → List A
[]        ++ ys = ys
(x :: xs) ++ ys = x :: (xs ++ ys)

infixr  _++_

More sophisticated examples of types in Agda

Sometimes we may wish to consider lists over a type A of a given length n : ℕ. The elements of this type, written Vector A n, are called vectors, and the type can be defined as follows:

data Vector (A : Type) : ℕ → Type where
 []   : Vector A 
 _::_ : {n : ℕ} → A → Vector A n → Vector A (suc n)

This is called a dependent type because it is a type that depends on elements n of another type, namely ℕ.

In Agda, we can’t define the head and tail functions on lists, because they are undefined for the empty list, and functions must be total in Agda. Vectors solve this problem:

head : {A : Type} {n : ℕ} → Vector A (suc n) → A
head (x :: xs) = x

tail : {A : Type} {n : ℕ} → Vector A (suc n) → Vector A n
tail (x :: xs) = xs

Agda accepts the above definitions because it knows that the input vector has at least one element, and hence does have a head and a tail. Here is another example.

Dependent types are pervasive in Agda.

The empty type and the unit type

data 𝟘 : Type where

data 𝟙 : Type where
 ⋆ : 𝟙

_≣_ : ℕ → ℕ → Type
     ≣      = 𝟙
     ≣ suc y = 𝟘
suc x ≣      = 𝟘
suc x ≣ suc y = x ≣ y

infix  _≣_

ℕ-refl : (x : ℕ) → x ≣ x
ℕ-refl        = ⋆
ℕ-refl (suc x) = ℕ-refl x

The identity type former _≡_

data _≡_ {A : Type} : A → A → Type where
 refl : (x : A) → x ≡ x

infix  _≡_

trans : {A : Type} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans (refl x) (refl x) = refl x

sym : {A : Type} {x y : A} → x ≡ y → y ≡ x
sym (refl x) = refl x

ap : {A B : Type} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y
ap f (refl x) = refl (f x)

The identity type is a little bit subtle and there is a lot to say about it. For the moment, let’s convince ourselves that we can convert back and forth between the types x ≡ y and x ≣ y, in the case that A is the type of natural numbers, as follows:

back : (x y : ℕ) → x ≡ y → x ≣ y
back x x (refl x) = ℕ-refl x

forth : (x y : ℕ) → x ≣ y → x ≡ y
forth               ⋆ = refl 
forth (suc x) (suc y) p = I
 where
  IH : x ≡ y
  IH = forth x y p

  I : suc x ≡ suc y
  I = ap suc IH

Propositions as types

The CurryHoward interpretation of logic, after Haskell Curry and William Howard, interprets logical statements, also known as propositions, as types. Per Martin-Löf extended this interpretation of propositions as types with equality, by introducing the identity type discussed above.

An incomplete table of the CurryHoward–Martin-Löf interpretation of logical propositions is the following:

This was enough for our examples above.

For more complex examples of reasoning about programs, we need to complete the following table:

This will be the subject of future handouts.

Agda manual

Please study the Agda manual as a complement to these lecture notes.

Go back to the table of contents