------------------------------------------------------------------------------ [MGS 07 : Dependently typed programming (DTP)! !1st lecture ! ! ! !Thorsten Altenkirch ] ------------------------------------------------------------------------------ [Start with something we know from ordinary functional Programming! !i.e. lists ] ------------------------------------------------------------------------------ ( A : * ! ( a : A ; as : List A ! data !------------! where (--------------! ; !----------------------! ! List A : * ) ! nil : List A ) ! cons a as : List A ) ------------------------------------------------------------------------------ [we implement append: we use <= (by)refining the programming problem by a ! !"tactic" or we return an answer using => (return). ! !The visible Epigram code are just high level scripts which generate code ! !in an underlying core language. ! !Epigram is a total language, all Epigram programs should terminate. ! !Hence we have to mark the use of recursion using rec. ] ------------------------------------------------------------------------------ ( 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) } } ------------------------------------------------------------------------------ [Type parameters are just ordinary parameters, but we have a notion ! !of implicit parameter, introduced by underline. ! !The elaborator inserts declarations of implicit parameters automatically! !and even infers the types of those parameters. ] ------------------------------------------------------------------------------ [ ( A : * ! ( A : * ! ( A : * ; a : A ; as : List A !! !data !--------! where !----------! ; !-------------------------------!! ! ! List A ! ! nil _A : ! ! cons _A a as : List A )! ! ! : * ) ! List A ) ] ------------------------------------------------------------------------------ [Let's import some data...] ------------------------------------------------------------------------------ ( 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)) ------------------------------------------------------------------------------ [and an example function] ------------------------------------------------------------------------------ ( as : List A ! let !-----------------! ! rev as : List A ) rev as <= rec as { rev as <= case as { rev nil => nil rev (cons a as) => append (rev as) (cons a nil) } } ------------------------------------------------------------------------------ [tested interactively] ------------------------------------------------------------------------------ inspect (rev l1) => cons (suc (suc (suc zero))) % (cons (suc (suc zero)) (cons (suc zero) nil)) : List Nat ------------------------------------------------------------------------------ [let's move to another example nth, extracting the nth element of a list! !Can we actually implement this function? ] ------------------------------------------------------------------------------ ( as : List A ; i : Nat ! let !------------------------! ! nth as i : A ) nth as i <= rec as { nth as i <= case as { nth nil i [] nth (cons a as) i <= case i { nth (cons a as) zero => a nth (cons a as) (suc i) => nth as i } } } ------------------------------------------------------------------------------ [Indeed we can not, we cannot complete the shed left. ! !And if A=Empty there is no inhabitant of this type. ! !We could fix this by using Maybe, i.e. dynamic error handling.! !Dependent types off us another solution: more precise types ! !to avoid errors statically. ] ------------------------------------------------------------------------------ ( 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 ) ------------------------------------------------------------------------------ [note that natural number can be implicit parameters too.] ------------------------------------------------------------------------------ [lets implement append for vectors:] ------------------------------------------------------------------------------ ( 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)] } } ------------------------------------------------------------------------------ [Remarks : ! !1. do we actually need the natural numbers at runtime? ! !2. What does the type checker has to do? Symbolic evaluation.! ! What could go wrong? ] ------------------------------------------------------------------------------ ( as : Vec n A ! let !-------------------! ! vrev as : Vec n A ) vrev as <= rec as { vrev as <= case as { vrev vnil => vnil vrev (vcons a as) => [vappend (vrev as) (vcons a vnil)] } } ------------------------------------------------------------------------------ [the type checker can only use definitional equalities directly. ! !We can teach it new tricks by using explicit equational reasoning,! !we will touch upon this later. At least for the time being this is! !quite heavy. ] ------------------------------------------------------------------------------ [At least in this case there is an easier solution: we avoid using ! !vappend and instead implement vsnoc directly. ] ------------------------------------------------------------------------------ ( as : Vec n A ; a : A ! let !----------------------------! ! vsnoc as a : Vec (suc n) A ) vsnoc as a <= rec as { vsnoc as a <= case as { vsnoc vnil a => vcons a vnil vsnoc (vcons a as) a' => vcons a (vsnoc as a') } } ------------------------------------------------------------------------------ ( as : Vec n A ! let !--------------------! ! vrev' as : Vec n A ) vrev' as <= rec as { vrev' as <= case as { vrev' vnil => vnil vrev' (vcons a as) => vsnoc (vrev' as) a } } ------------------------------------------------------------------------------ [Obs: finer types seem to decrease reusability of code.] ------------------------------------------------------------------------------ [We now turn to implementing vnth, first we need an implementation of finite types.] ------------------------------------------------------------------------------ ( n : Nat ! ( i : Fin n ! data !-----------! where (------------------! ; !--------------------! ! Fin n : * ) ! fz : Fin (suc n) ) ! fs i : Fin (suc n) ) ------------------------------------------------------------------------------ [note that there are exactly n inihabitants in Fin 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 } } } ------------------------------------------------------------------------------ [what happens if we analyze the data in a different order?] ------------------------------------------------------------------------------ ( as : Vec n A ; i : Fin n ! let !---------------------------! ! vnth' as i : A ) vnth' as i <= rec as { vnth' as i <= case i { vnth' as fz <= case as { vnth' (vcons a as) fz => a } vnth' as (fs i) <= case as { vnth' (vcons a as) (fs i) => vnth' as i } } } ------------------------------------------------------------------------------ [Exercise] ------------------------------------------------------------------------------ ( n : Nat ! let !-----------------------! ; fmax _ n [] ! fmax _n : Fin (suc n) ) ------------------------------------------------------------------------------ ( i : Fin n ! let !---------------------! ; emb i [] ! emb i : Fin (suc n) ) ------------------------------------------------------------------------------ ( i : Fin n ! let !----------------! ; finv i [] ! finv i : Fin n ) ------------------------------------------------------------------------------