------------------------------------------------------------------------------ [MGS 07 : Dependently typed programming (DTP)! !2nd lecture ! ! ! !Thorsten Altenkirch ] ------------------------------------------------------------------------------ [Code from the first lecture] ------------------------------------------------------------------------------ ( A : * ! ( a : A ; as : List A ! data !------------! where (--------------! ; !----------------------! ! List A : * ) ! nil : List A ) ! cons a as : List A ) ------------------------------------------------------------------------------ ( as, bs : List A ! let !-----------------------! ! append as bs : List A ) append as bs <= rec as { append as bs <= case as { append nil bs => bs append (cons a as) bs => cons a (append as bs) } } ------------------------------------------------------------------------------ ( n : Nat ! data (---------! where (------------! ; !-------------! ! Nat : * ) ! zero : Nat ) ! suc n : Nat ) ------------------------------------------------------------------------------ let (-----------! ! one : Nat ) one => suc zero ------------------------------------------------------------------------------ let (-----------! ! two : Nat ) two => suc one ------------------------------------------------------------------------------ let (-------------! ! three : Nat ) three => suc two ------------------------------------------------------------------------------ ( m, n : Nat ! let !---------------! ! add m n : Nat ) add m n <= rec m { add m n <= case m { add zero n => n add (suc m) n => suc (add m n) } } ------------------------------------------------------------------------------ [an example list] ------------------------------------------------------------------------------ let (---------------! ! l1 : List Nat ) l1 => cons one (cons two (cons three nil)) ------------------------------------------------------------------------------ ( n : Nat ; A : * ! ( a : A ; as : Vec n A ! data !------------------! where (--------------! ; !-----------------------! ! Vec n A : * ) ! vnil : ! ! vcons a as : ! ! Vec zero A ) ! Vec (suc n) A ) ------------------------------------------------------------------------------ ( as : Vec n A ; bs : Vec m A ! let !---------------------------------! ! vappend as bs : Vec (add n m) A ) vappend as bs <= rec as { vappend as bs <= case as { vappend vnil bs => bs vappend (vcons a as) bs => [vcons a (vappend as bs)] } } ------------------------------------------------------------------------------ ( n : Nat ! ( i : Fin n ! data !-----------! where (------------------! ; !--------------------! ! Fin n : * ) ! fz : Fin (suc n) ) ! fs i : Fin (suc n) ) ------------------------------------------------------------------------------ ( as : Vec n A ; i : Fin n ! let !---------------------------! ! vnth as i : A ) vnth as i <= rec as { vnth as i <= case as { vnth vnil i <= case i vnth (vcons a as) i <= case i { vnth (vcons a as) fz => a vnth (vcons a as) (fs i) => vnth as i } } } ------------------------------------------------------------------------------ [End of old code] ------------------------------------------------------------------------------ [Solution of old Exercise] ------------------------------------------------------------------------------ ( n : Nat ! let !-----------------------! ! fmax _n : Fin (suc n) ) fmax _ n <= rec n { fmax _ n <= case n { fmax _ zero => fz fmax _ (suc n) => fs fmax } } ------------------------------------------------------------------------------ ( i : Fin n ! let !---------------------! ! emb i : Fin (suc n) ) emb i <= rec i { emb i <= case i { emb fz => fz emb (fs i) => fs (emb i) } } ------------------------------------------------------------------------------ ( i : Fin n ! let !----------------! ! finv i : Fin n ) finv i <= rec i { finv i <= case i { finv fz => fmax finv (fs i) => emb (finv i) } } ------------------------------------------------------------------------------ [Vec n is an applicative functor] ------------------------------------------------------------------------------ ( fs : Vec n (A -> B) ; as : Vec n A ! let !-------------------------------------! ! vapp fs as : Vec n B ) vapp fs' as <= rec fs' { vapp fs' as <= case fs' { vapp vnil as <= case as { vapp vnil vnil => vnil } vapp (vcons f fs') as <= case as { vapp (vcons f fs') (vcons a as) => vcons (f a) (vapp fs' as) } } } ------------------------------------------------------------------------------ ( n : Nat ; A : * ; a : A ! let !---------------------------! ! vreturn _n a : Vec n A ) vreturn _ n a <= rec n { vreturn _ n a <= case n { vreturn _ zero a => vnil vreturn _ (suc n) a => vcons a (vreturn _ n a) } } ------------------------------------------------------------------------------ [Indeed, we can implement vmap just with vreturn and vapp] ------------------------------------------------------------------------------ ( f : A -> B ; as : Vec n A ! let !----------------------------! ! vmap f as : Vec n B ) vmap f as => vapp (vreturn f) as ------------------------------------------------------------------------------ [using vapp we can implement vzip] ------------------------------------------------------------------------------ ( f : A -> B -> C ; as : Vec n A ; bs : Vec n B ! let !-------------------------------------------------! ! vzip f as bs : Vec n C ) vzip f as bs => vapp (vmap f as) bs ------------------------------------------------------------------------------ [and transpose a matrix recursively] ------------------------------------------------------------------------------ ( ass : Vec n (Vec m A) ! let !---------------------------------! ! transpose ass : Vec m (Vec n A) ) transpose ass <= rec ass { transpose ass <= case ass { transpose vnil => vreturn vnil transpose (vcons as ass) => vapp (vmap vcons as) (transpose ass) } } ------------------------------------------------------------------------------ [For people who know about monads: every monad is an applicative functor but! !not vice versa. Indeed (Vec n) is not a monad (Why?) ! !As an example consider the list monad, given by lreturn and bind: ] ------------------------------------------------------------------------------ ( a : A ! let !--------------------! ! lreturn a : List A ) lreturn a => cons a nil ------------------------------------------------------------------------------ ( as : List A ; f : A -> List B ! let !--------------------------------! ! bind as f : List B ) bind as f <= rec as { bind as f <= case as { bind nil f => nil bind (cons a as) f => append (f a) (bind as f) } } ------------------------------------------------------------------------------ [every monad is a functor:] ------------------------------------------------------------------------------ ( f : A -> B ; as : List A ! let !---------------------------! ! map f as : List B ) map f as => bind as (lam a => lreturn (f a)) ------------------------------------------------------------------------------ [Exercise: Show that List is an applicative functor by implementing lapp! !using only bind and lreturn. ] ------------------------------------------------------------------------------ ( fs : List (A -> B) ; as : List A ! let !-----------------------------------! ; lapp fs' as [] ! lapp fs as : List B ) ------------------------------------------------------------------------------ [we can reimplement transpose using lapp and lreturn, but what does it do?] ------------------------------------------------------------------------------ ( ass : List (List A) ! let !--------------------------------! ; ltranspose ass [] ! ltranspose ass : List (List A) ) ------------------------------------------------------------------------------ [In particular do the transposes commute with the forgetful map?] ------------------------------------------------------------------------------ ( as : Vec n A ! let !-----------------! ! fog as : List A ) fog as <= rec as { fog as <= case as { fog vnil => nil fog (vcons a as) => cons a (fog as) } } ------------------------------------------------------------------------------ [using dependent types to represent lambda terms in generalized deBruijn notation] ------------------------------------------------------------------------------ ( n : Nat ! data !-----------! ! Lam n : * ) where (------------------! ! vz : Lam (suc n) ) ( t : Lam n ! ( t, u : Lam n ! ( t : Lam (suc n) ! !--------------------! ; !-----------------! ; !-----------------! ! vs t : Lam (suc n) ) ! app t u : Lam n ) ! abs t : Lam n ) ------------------------------------------------------------------------------ ( i : Fin n ! let !---------------! ! var i : Lam n ) var i <= rec i { var i <= case i { var fz => vz var (fs i) => vs (var i) } } ------------------------------------------------------------------------------ ( t : Lam n ; us : Vec n (Lam m) ! let !---------------------------------! ! subst t us : Lam m ) subst t us <= rec t { subst t us <= case t { subst vz us <= case us { subst vz (vcons u us) => u } subst (vs t) us <= case us { subst (vs t) (vcons u us) => subst t us } subst (app t u) us => app (subst t us) (subst u us) subst (abs t) us => abs (subst t (vcons vz (vmap vs us))) } } ------------------------------------------------------------------------------ [the category of lambda terms] ------------------------------------------------------------------------------ ( n : Nat ! let !-----------------------! ! id _n : Vec n (Lam n) ) id _ n <= rec n { id _ n <= case n { id _ zero => vnil id _ (suc n) => vcons vz (vmap vs id) } } ------------------------------------------------------------------------------ ( ts : Vec n (Lam m) ; us : Vec m (Lam l) ! let !------------------------------------------! ! compose ts us : Vec n (Lam l) ) compose ts us => vmap (lam t => subst t us) ts ------------------------------------------------------------------------------ ( m, n : Nat ! let !---------------! ! Subst m n : * ) Subst m n => Vec n (Lam m) ------------------------------------------------------------------------------ [So far, we have only used Natural numbers as indizes. ! !Let's to simply typed lambda terms as an example where we use other index types] ------------------------------------------------------------------------------ ( a, b : Ty ! data (--------! where (--------! ; !--------------! ! Ty : * ) ! o : Ty ) ! arr a b : Ty ) ------------------------------------------------------------------------------ ( G : List Ty ; a : Ty ! data !-----------------------! ! TLam G a : * ) where (------------------------! ! tz : TLam (cons a G) a ) ( t : TLam G a ! !--------------------------! ! ts t : TLam (cons b G) a ) ( t : TLam G (arr a b) ; u : TLam G a ! ( t : TLam (cons a G) b ! !--------------------------------------! ; !-----------------------! ! tapp t u : TLam G b ) ! tlam t : ! ! TLam G (arr a b) ) ------------------------------------------------------------------------------ ( G, D : List Ty ! data !----------------! ! TSubst G D : * ) ( t : TLam G a ; ts : TSubst G D ! where (---------------------! ; !----------------------------------! ! tnil : TSubst G nil ) ! tcons t ts : TSubst G (cons a D) ) ------------------------------------------------------------------------------ [Exercise; ! !Complete the following definitions following the structure established! !for the untyped lambda calculus. ] ------------------------------------------------------------------------------ ( t : TLam G a ; us : TSubst D G ! let !---------------------------------! ; tsubst t us [] ! tsubst t us : TLam D a ) ------------------------------------------------------------------------------ ( G : List Ty ! let !---------------------! ; tid _ G [] ! tid _G : TSubst G G ) ------------------------------------------------------------------------------ ( f : TSubst X G ; g : TSubst D X ! let !----------------------------------! ; tcomp f g [] ! tcomp f g : TSubst D G ) ------------------------------------------------------------------------------