## A finite universe in Agda

May 9th, 2008 by ThorstenIn 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