Nottingham FP Lab Blog

Agda Demo 2

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

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

listMonad : Monad [_]
listMonad = record
  { 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

comments powered by Disqus