20 Feb 2008 15:01

How to define init for vectors?

```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:
```

20 Feb 2008 17:46

Re: How to define init for vectors?

```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 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.

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. You will need to
look a
bit harder. You'll also need to indicate what you're doing recursion on.
```

20 Feb 2008 23:36

Re: How to define init for vectors?

```> 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. You will need to
>  look a
>  bit harder. You'll also need to indicate what you're doing recursion on.

Yes. I almost used to arriving to the answer the seconds after asking
a question.

( X : * ; xs : Vec (succ n) X !
let !------------------------------!
! vecInit xs : Vec n X )

vecInit xs <= case xs
{ vecInit (vcons n' ns) <= case ns
{ vecInit (vcons n' vnil) => vnil
vecInit (vcons n'' (vcons n' ns)) => vcons n'' (vecInit (vcons n' ns))
}
}

(indentation can be broken, I indented badly pasted version)

I'm looking for more dependent function. Now - with variable length
vector size checking!

(I almost figured out how to do it)
```