The Epigram Programming Language

Serguey Zefirov | 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:

(Continue reading)

headers

Conor McBride | 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.

(Continue reading)

headers

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

(Continue reading)