## Archive for May, 2008

### A finite universe in Agda

Friday, May 9th, 2008 by Thorsten

In exercise 3 of our lecture notes on generic programming we suggest to show that the universe of finite types is closed under coproducts, products and exponentials and implement views allowing to do pattern matching over the derived structure. I though that (re)doing this in Agda may be a good way to explore views in Agda and play with the with-rule (local case). Indeed, I discovered that our remark that it is not possible to implement a view for function types due to lack of extensionality was wrong, since we only have to show that every code is generated by a function.

Exercises: show that the categorical properties of coproducts, products and exponentials hold and implement Pi and Sigma-types.

module funi where

{- Defining a universe of finite types with +, × and =>
and accompanying views -}

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

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

data Fin : ℕ -> Set where
fz : forall {n} -> Fin (succ n)
fs : forall {n} -> Fin n -> Fin (succ n)

{- coproducts -}

finl : forall {m n} -> Fin m -> Fin (m + n)
finl fz     = fz
finl (fs i) = fs (finl i)

finr : forall {m n} -> Fin n -> Fin (m + n)
finr {zero}   {n} i = i
finr {succ m} {n} i = fs (finr {m} i)

data PlusView : forall {m n} -> Fin (m + n) -> Set where
inl : forall {m n} -> (i : Fin m) -> PlusView {m} {n} (finl i)
inr : forall {m n} -> (i : Fin n) -> PlusView {m} {n} (finr {m} i)

plusView : forall {m n} -> (i : Fin (m + n)) -> PlusView {m} {n} i
plusView {zero}   i      = inr i
plusView {succ m} fz     = inl (fz {m})
plusView {succ m} (fs i) with plusView {m} i
plusView {succ m} (fs ._) | (inl j) = inl {succ m} (fs j)
plusView {succ m} (fs ._) | (inr j) = inr j

fcase : forall {m n} -> {A : Set}
-> ((i : Fin m) -> A)
-> ((j : Fin n) -> A)
-> ( k : Fin (m + n) ) -> A
fcase {m} minl minr k with plusView {m} k
fcase {m} minl minr ._ | inl i = minl i
fcase {m} minl minr ._ | inr j = minr j

{- products -}

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

fpair : forall {m n} -> Fin m -> Fin n -> Fin (m × n)
fpair {zero}   {n} ()     _
fpair {succ m} {n} fz     i = finl {n} {m × n} i
fpair {succ m} {n} (fs j) i = finr {n} {m × n} (fpair j i)

data PairView : forall {m n} -> Fin (m × n) -> Set where
pair : forall {m n} -> (i : Fin m)(j : Fin n) -> PairView {m} {n} (fpair i j)

pairView : forall {m n} -> (i : Fin (m × n) ) -> PairView {m} {n} i
pairView {zero}   {n} ()
pairView {succ m} {n} i with plusView {n} {m × n} i
pairView {succ m} {n} ._ | inl j =  pair fz j
pairView {succ m} {n} ._ | inr k  with pairView {m} {n} k
pairView {succ m} {n} ._ | inr ._  |  pair k0 k1 =  pair (fs k0) k1

fst : forall {m n} -> (i : Fin (m × n) ) -> Fin m
fst {m} i with pairView {m} i
fst {m} ._ | pair j k = j

snd : forall {m n} -> (i : Fin (m × n) ) -> Fin n
snd {m} i with pairView {m} i
snd {m} ._ | pair j k = k

{- exponentials -}

_=>_ : ℕ -> ℕ -> ℕ
zero     => n = succ zero
(succ m) => n = n × (m => n)

flam : forall {m n} -> ((Fin m) -> (Fin n)) -> Fin (m => n)
flam {zero}   {n} f = fz
flam {succ m} {n} f = fpair {n} {m => n} (f fz) (flam {m} {n} (\ i -> f (fs i) ) )

data FunView : forall {m n} -> Fin (m => n) -> Set where
lam : forall {m n} -> (f : (Fin m) -> (Fin n)) -> FunView {m} {n} (flam f)

fzero : {A : Set} -> Fin zero -> A
fzero ()

fsucc : forall {m} -> {A : Set} -> A -> ((Fin m) -> A) -> Fin (succ m) -> A
fsucc a f fz     = a
fsucc a f (fs i) = f i

funView : forall {m n} -> (i : Fin (m => n)) -> FunView {m} {n} i
funView {zero}   {n} fz      = lam fzero
funView {zero}   {n} (fs ())
funView {succ m} {n} i       with pairView {n} {m => n} i
funView {succ m} {n} ._      |    pair f0 ff  with funView {m} ff
funView {succ m} {n} ._      |    pair f0 ._  |    lam g = lam (fsucc f0 g)

fapp : forall {m n} -> Fin (m => n) -> Fin m -> Fin n
fapp {m} {n} f  i with funView {m} {n} f
fapp {m} {n} ._ i  |   lam g  = g i

### Agda Demo 2

Tuesday, May 6th, 2008 by Nils Anders Danielsson

Code from today’s session:

module LiveDemo2 where

open import Data.Bool
open import Data.List

module Sort {a : Set} (_≤_ : a -> a -> Bool) where

insert : a -> [ a ] -> [ a ]
insert x []       = x ∷ []
insert x (y ∷ ys) = if x ≤ y then x ∷ y ∷ ys
else y ∷ insert x ys

sort : [ a ] -> [ a ]
sort = foldr insert []

_≤_ : Bool -> Bool -> Bool
false ≤ _     = true
true  ≤ false = false
true  ≤ true  = true

open Sort _≤_

test = sort (true ∷ false ∷ true ∷ [])

open import Relation.Binary.PropositionalEquality

record Monad (M : Set -> Set) : Set1 where
field
return : forall {a} -> a -> M a
_>>=_  : forall {a b} -> M a -> (a -> M b) -> M b

left-identity : forall {a b} (x : a) (f : a -> M b) ->
(return x >>= f) ≡ f x

-- module Monad {M : Set -> Set} (_ : Monad M) : Set1 where
--   return : forall {a} -> a -> M a
--   _>>=_  : forall {a b} -> M a -> (a -> M b) -> M b

--   left-identity : forall {a b} (x : a) (f : a -> M b) ->
--                   (return x >>= f) ≡ f x

open import Data.Function

join : forall {M} -> Monad M -> forall {a} -> M (M a) -> M a
join M x = x >>= id
join M x = Monad._>>=_ M x id

{ return        = \x -> x ∷ []
; _>>=_         = \xs f -> concat (map f xs)
; left-identity = ?
}

The ? above is left as an exercise.

module SimplyTyped where

infixl 70 _·_
infix  60 λ_

infixr 50 _→_
infixl 40 _▻_
infix  30 _∋_ _⊢_

data Ty : Set where
Nat : Ty
_→_ : Ty -> Ty -> Ty

data Ctxt : Set where
ε   : Ctxt
_▻_ : Ctxt -> Ty -> Ctxt

data _∋_ : Ctxt -> Ty -> Set where
zero : forall {Γ σ}   -> Γ ▻ σ ∋ σ
suc  : forall {Γ σ τ} -> Γ ∋ σ -> Γ ▻ τ ∋ σ

data _⊢_ : Ctxt -> Ty -> Set where
var : forall {Γ σ}   -> Γ ∋ σ -> Γ ⊢ σ
λ_  : forall {Γ σ τ} -> Γ ▻ σ ⊢ τ -> Γ ⊢ σ → τ
_·_ : forall {Γ σ τ} -> Γ ⊢ σ → τ -> Γ ⊢ σ -> Γ ⊢ τ

open import Data.Nat

Dom : Ty -> Set
Dom Nat     = ℕ
Dom (σ → τ) = Dom σ -> Dom τ

data Env : Ctxt -> Set where
ε   : Env ε
_▻_ : forall {Γ σ} -> Env Γ -> Dom σ -> Env (Γ ▻ σ)

lookup : forall {Γ σ} -> Γ ∋ σ -> Env Γ -> Dom σ
lookup zero    (ρ ▻ x) = x
lookup (suc n) (ρ ▻ x) = lookup n ρ

⟦_⟧ : forall {Γ σ} -> Γ ⊢ σ -> Env Γ -> Dom σ
⟦ var x   ⟧ ρ = lookup x ρ
⟦ λ t     ⟧ ρ = \\x -> ⟦ t ⟧ (ρ ▻ x)
⟦ t₁ · t₂ ⟧ ρ = ⟦ t₁ ⟧ ρ (⟦ t₂ ⟧ ρ)

t : ε ⊢ Nat → Nat
t = (λ var zero) · (λ var zero)

example = ⟦ t ⟧ ε 6

-- t₂ : ε ▻ ? ⊢ ?
-- t₂ = var zero · var zero

### Agda Demo

Friday, May 2nd, 2008 by Nils Anders Danielsson

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.