Hi
On 22 Feb 2008, at 12:52, Serguey Zefirov wrote:
0xN is an empty list
Nx0, the result of the transposition, is a list of N empty
lists. You
can express this (the value of N...) with vectors/dependent-
types, you
know how long it should be, so you can do this.
does that seem right?
Yes, but I don't know how to find N it through Epigram. I cannot do
case analysis on the length of Vec.
It sometimes happens that an argument which is typically
inferrable when a function is used (hence implicit by default)
is important and needs to be seen when defining the function.
Fortunately, Epigram has a way to deal with this situation.
I'm sure we could do better, but it works.
The standard example is the function vec, which makes a vector
of copies of a given element. Typically, the desired length is
known when you use the function, so you probably want it to
be left implicit, but the vec will be defined by recursion on
the length. Here's how to start
( n ; X ; x : X !
let !--------------------! ; vec _ n x []
! vec _n x : Vec n X )
The underscore character is the "manual override" for implicit
syntax. If you use it to show n in the declaration, you will
also be shown n in the patterns of your program. When you use
this mechanism, it's a good idea to declare the order of
arguments to prevent the machine from making bad choices,
hence the "n ; X ;" premises.
Hope this helps
Conor
