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.)
> One idea I have wondered about is [...] allowing users to provide two implicitness-signatures for each definition
Rocq does allow the user to give more than one list of argument implicitness settings, distinguished by the arguments given in each case. As an example, in the Coq-HoTT library, we write `idpath` for the reflexivity path, and have
```
Arguments idpath {A a} , [A] a.
```
which says that `idpath` can be used with both arguments implicit and maximally inserted, or with `A` implicit and non-maximally inserted and `a` explicit. So for a goal of type `a = a`, I can write either `idpath` or `idpath a`, and both are accepted. The latter is useful in a context when Rocq doesn't know the type of paths a priori.
Dan Christensen
Josselin Poiret@, using (A := bubu) just like in Agda. What I dislike though is that the common default for implicit arguments in Rocq is that they're maximally inserted.I think a conservative check would sometimes be too restrictive. Consider
David Berry
Amélia Liao 🍊
Owen Lynchbind : {M : Type -> Type} {A B : Type} -> Monad M -> (A -> M B) -> M A -> M B
In practice, this definition is usually fine because M will be instantiated with some (definitionally) injective type former like List, and problems like List ?B = List Int are solvable, but technically we could instantiate M with a constant family like \_. Nat, and now inferring B is hopeless. Having to make B an explicit arguments to bind, merely to defend against this edge-case, would kinda suck IMO...
@AndrasKovacs Would it make sense/be possible to have a dedicated ‘injective’ function space in the type system for this?
@jonmsterling @AndrasKovacs @olynch @NathanielB i guess it is only introduced by type constructors and has an application rule (and no computation rules). You can wrap it in a normal lambda to recover the usual function space (and probably elaboration can do this automatically).
Though I wonder if it’s possible to do better..
@zyang That suggests you could also have lambdas for this function space as long as the body is injective with respect to the bound variable.
@constantine @jonmsterling @AndrasKovacs @olynch @NathanielB Yes, the syntax for doing this in GHC is like
```
type family MyInjFun (a :: Type) = (result :: Type) | result -> a where
MyInjFun a = Maybe (Maybe a)
```
The syntax looks indeed rather unintuitive...
@jonmsterling I learned that one the hard way a few sessions back, yeah (I'm not spending enough time coding: you'll be getting a fair idea of how often from here).
If I ever really want it for some reason, it's a trivial two-liner to create that mode anyway - but pretty clearly in bad taste in our current environments.
Constantine Theocharis
Zhixuan Yang
Philippa Cowderoy