by Thorsten on May 9, 2008.
Tagged as: Lunches.
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