It's difficult to design a language that has implicit arguments *and* allows you to explicitly instantiate them. Agda has done very admirably.
But I do not like bound names, which are often single letters, getting undeservedly elevated to names that play a descriptive role.
My maxim is:
If you see {A = A} in an argument list, they blew it.
There is something very honest about the way this is dealt with in Rocq, oversimplified below:
1. Implicitness of arguments is a "calling convention" that is configured for each defined function.
2. If you want to deviate from the implicit calling convention of a named function, you use an `@` sigil before the function, and then all arguments become explicit.
I like this a bit more because it discourages you from making things implicit that you frequently have to supply explicitly. Very quickly you learn whether your API is realistic in light of the unifier.
Discouraging users from overusing implicit arguments sounds reasonable (I am very guilty of this). I'm not convinced, however, in the edge cases where users do want to give some implicit arguments, that specifying them by position is any better than specifying them by name. Both are kinda arbitrary (especially in the presence of features like generalised variables, where the order in which variables are bound is really an implementation detail, though maybe this is a flaw in the design of generalised variables).
One idea I have wondered about is, inspired by bidirectional typechecking, allowing users to provide two implicitness-signatures for each definition: a synthesisable one and a checkable one. E.g. it would be nice to easily toggle between
Jon Sterling
Nathaniel Burkerefl : {A : Type} (x : A) -> x = x
and
refl : {A : Type} {x : A} -> x = x
but making A explicit is almost never desirable.
Of course in the presence of dependent types, metavariables and fancy unification, whether a particular argument is inferable is not a very local property, so this is probably overly simplistic, but I still think some approximation of it might be better than toggling all implicitness?
@NathanielB There are indeed some interesting points here that deserve some careful design.
Your example of two modes for 'refl' is very realistic, and I've had this come up in practice too. I think there is a chance to do this in a reasonable way…
Now, coming back to how to name things, I think that all this may be some evidence in favour of the idea of some form of keyword arguments. The idea would be to distinguish the *name* of the argument from the variable it binds. Then, one must use the *name* when explicitly instantiating an implicit argument.
(I'm an old Objective-C programmer, so I do keep reaching for Smalltalk-style method selectors.)