How to define init for vectors?

[Serguey Zefirov]

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?

[Conor McBride-2]

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.

>
> Where should I look for hints on to get a clue on how to do it right?

The tail of the list!

All the best

Conor


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.

[Serguey Zefirov]

> 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)