Hi
Mea culpa, I suspect. I haven't checked, but it looks like
you've run into one of the known bugs. It's annoying, but
there's a workaround.
The trouble is the dog that doesn't bark...
On 29 Feb 2008, at 14:16, Serguey Zefirov wrote:
I decided to write transpose with implicit parameters. And get
stuck, as usual.
This is partial code:
( n : Nat ; m : Nat ; xys : Vec n (Vec m X) !
let !-!
!transpose _n _m xys : Vec m (Vec n X))
...where does X go? Inconsistently with the notation,
Epigram is actually adding X as an implicit argument
as far left as possible. I know it looks like you're
signalling that n and m should come first and second,
but actually what happens just now is that code which
manages rules puts X first.
So, here,
transpose _ n _ m xys = rec xys
{ transpose _ n _ m xys = case xys
{ transpose _ n _ zero vnil [= case _n]
transpose _ n _ (suc m) (vcons xy xys) []
}
}
n and m refer to the first and second arguments,
and if you look in the Horace buffer (an often
neglected source of information!) you'll probably
see an unexpected n : * which may confirm my
suspicions.
The workaround is to declare the order of arguments
explicitly. I'd write
( n ; m ; X ; xys : Vec n (Vec m X) !
let !-!
! transpose _n _m xys : Vec m (Vec n X) )
Epigram will figure out the types of n, m and X
without difficulty, and it will use the order of
arguments n m X xys, with n, m and X hidden by
default at usage sites, and n and m visible
during the definition.
I'm sorry the poor thing isn't as good at guessing
as it should be, but it's not so hard just to tell
it what you want.
Hope this helps
Conor
