Nottingham FP Lab Blog

Agda Demo

by Nils Anders Danielsson on May 2, 2008.
Tagged as: Lunches.

Today I ran a hands-on Agda demonstration. The code written during the demo:

module LiveDemo where

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

_+_ : ℕ -> ℕ -> ℕ
zero  + n = n
suc m + n = suc (m + n)

infixr 5 _◅_ _++_

data Vec (a : Set) : ℕ -> Set where
  []  : Vec a zero
  _◅_ : {n : ℕ} -> a -> Vec a n -> Vec a (suc n)

_++_ : forall {a m n} -> Vec a m -> Vec a n -> Vec a (m + n)
[]       ++ ys = ys
(x ◅ xs) ++ ys = x ◅ xs ++ ys

data Last {a : Set} : forall {n} -> Vec a n -> Set where
  []  : Last []
  _▻_ : forall {n} (xs : Vec a n) (x : a) -> Last (xs ++ x ◅ [])

last : forall {a n} (xs : Vec a n) -> Last xs
last []       = []
last (x ◅ xs) with last xs
last (x ◅ .[])              | []       = [] ▻ x
last (x ◅ .(ys ++ y ◅ []))  | (ys ▻ y) = (x ◅ ys) ▻ y

Some exercises:

Define an inductive family for natural numbers less than a given natural number.
Use this family to define a safe lookup function for vectors.

If you want more exercises, check out the Agda courses from the Types Summer School 2007 and the LerNET Summer School 2008 (available from the Agda wiki). Conor’s Epigram lecture notes from the AFP Summer School 2004 also contain a bunch of exercises.