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:
Hi Serguey
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
It's not known that the length of ns is a succ, so it isn't
appropriate to
call vecInit here. The Haskell function is exploiting fall-through
in patterns
here, so you should expect the Epigram version to be slightly
noisier. So far,
you haven't quite determined which case you're in.
