## Agda Demo 2

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
where open Monad M
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
```