I try to write small familiar programs to understand dependent types
programming better (more precisely, understand it at all). All usual
maps and folds are done and I processed to more dependent ones.
That's what I managed to write:
------------------------------------------------------------------------------
( n : Nat !
data (---------! where (------------! ; !--------------!
! Nat : * ) ! zero : Nat ) ! succ n : Nat )
------------------------------------------------------------------------------
( A : * ! ( a : A !
data !-------------! where (-------------------! ; !------------------!
! Maybe A : * ) ! Nothing : Maybe A ) ! Just a : Maybe A )
------------------------------------------------------------------------------
( A : * ; B : * ! ( a : A ; b : B !
data !----------------! where !----------------------!
! Pair A B : * ) ! Tuple a b : Pair A B )
------------------------------------------------------------------------------
( n : Nat ; X : * ! ( x : X ; xs : Vec n X !
data !------------------! where (--------------! ; !-----------------------!
! Vec n X : * ) ! vnil : ! ! vcons x xs : !
! Vec zero X ) ! Vec (succ n) X )
------------------------------------------------------------------------------
let (-------------!
! width : Nat )
width => succ (succ zero)
------------------------------------------------------------------------------
And here I got stuck:
------------------------------------------------------------------------------
( X : * ; xs : Vec (succ n) X !
let !------------------------------!
! vecInit xs : Vec n X )
vecInit xs <= case xs
{ vecInit (vcons n' ns) => vcons n' (vecInit ns)
}
------------------------------------------------------------------------------
This is a version of init function from Haskell Prelude:
init [x] = []
init (x:xs) = x:init xs
I do not get second case from Epigram when elaborating. And, actually,
Epigram does not like "=> vcons n' (vecInit ns)" part. But I can
understand that, albeit not formally.
Where should I look for hints on to get a clue on how to do it right?
