A finite universe in Agda

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

2 Responses to “A finite universe in Agda”

  1. Russell O'Connor Says:

    Why no Unicode character for => ?

  2. Samuel Bronson Says:

    @roconnor: Perhaps because => is so much easier to type than \RightArrow? I usually have to try several times before getting it right…

Leave a Reply