Hi
I hope you don't mind me copying this reply to the mailing list, as it
may be of more general interest.
Jonathan Lee wrote:
I've been trying the tutorial and I'm coming to the part about the
(vec x) function. I'm a bit confused on how the implicit syntax as
when I input:
( n : Nat ; x : X !
let !--------------------!
! vec_n x : Vec n X )
Mea culpa. Since writing the tutorial, I broke this example (and one or
two others) when I made a change to the system's default strategy for
ordering implicit arguments relative to each other and to the explicit
arguments. You can see the symptoms in the Horace buffer
---------------------------------------------------------------
( n : Nat ; x : X !
let !--------------------! ; vec _ n x []
! vec _n x : Vec n X )
---------------------------------------------------------------
{Undo} {Reset} {Quit}
n : * ; n' : Nat ; x : n |- vec _ n x : Vec n' n
{Elaborate}
Epigram has decided, come what may, that the type (which you've called
X) will be the first implicit argument. It has taken your advice to call
the first implicit argument n, even though it's not the argument you
wanted to put there. It's clearly wrong: you're clearly asking for the
number to be implicit and to stand first. It's a case of
fix-one-bug-cause-another, compounded by poor maintenance of the
accompanying collection of examples and documents.
When the tutorial was written, implicit arguments were inserted just
where they were needed. The above declaration would have given you the
order vec_n_X x. If you'd left off the n : Nat in the premises, you'd
have got vec_X x _n, hence the premise for n in the first place.
These days, the system inserts implicit arguments as far left as
possible, relative to the explicitly declared arguments, so you get
vcons_X_n_x, because it *can* put X first. In the absence of any
explicitly underscored arguments, this heuristic is usually cleaner, but
you should still be able to override it with a declaration like the one
you tried.
This sort of issue comes up any time you have these weird functions like
vec which need to *use* an inferrable argument. When you use vec, it's
usually ok to allow the result type to determine the length, but in
vec's definition you need to make reference to the length.
Correspondingly, you need to use the above form, with its broken
implementation. You can play safe by fixing the order of arguments in full.
---------------------------------------------------------------
( n ; X ; x : X !
let !--------------------!
! vec _n x : Vec n X )
vec _ n x <= rec n
{ vec _ n x <= case n
{ vec _ zero x => vnil
vec _ (suc n) x => vcons x (vec x)
}
}
---------------------------------------------------------------
Nasty, but it leaves nothing to chance.
What ought to happen, even in Epigram 1? Implicit arguments should be
quantified as far left as is possible according to dependency and
consistent with the form which the programmer has written. When you
write f_i, you close off the possibility of other implicit arguments
before i. To my mind, the program you have written does indeed determine
the order n, X, x, and the fact that you don't get it is a *bug*.
Meanwhile, if you write
x : X ; xs : Vec n X
------------------------------
vcons x xs : Vec (suc n) X
you should be guaranteed to have n and X implicitly at the front (ie
either vcons_n_X x xs or vcons_X_n x xs) but in no particular order.
(The current implementation gives you vcons_X_n x xs; the old version
gave you vcons_X x _n xs, which is really bad.)
What are the chances that I'll fix this bug? Slim but non-zero. On the
one hand, it causes confusion. On the other hand, there's a reliable
workaround. I certainly know whre the bug is to be found, but I worry
that fiddling with it might have unintended consequences. I'm also don't
know when I'd find the time.
I hope this is a suitably comprehensive and candid, if less than
satisfactory answer to your entirely sensible question.
All the best
Conor
