Uses of first-class implicit function types

Question

Many proof assistants have a way to make certain arguments of a function as "implicit", so that the user doesn't have to supply them but they will be solved by unification. Sometimes, such as in Coq, this information is attached to the name of a function rather than its type, and can even be changed by a command such as Arguments after a function is defined. Other times, as in Agda, there is a first-class notion of "function type whose argument is implicit", distinct from an ordinary function type (but isomorphic to it).

I am interested in reasons why one might make the second choice. My intuition is currently more in line with the first choice: whether a certain argument is implicit seems like a property of the elaborator, rather than an intrinsic aspect of the function that would be described by its type. (In particular, denotational/categorical semantics certainly has no separate notion of "implicit function".) In a sense, declaring f to have one implicit argument is really just declaring f to be a notation for what would otherwise be written f _. And I can also imagine wanting to change the implicitness of certain arguments after a function is defined, which is (as far as I know) impossible with first-class implicit function types. Plus, it seems that the first choice must be easier to implement.

Obviously an advantage of first-class implicit function types is that you can hypothesize implicit functions, take them as arguments to another function, and pass them around as data. But I don't know of any real applications where this is advantageous. Can anyone point to some real code where it is valuable to have first-class implicit function types?

(Note that Coq does allow the fields of a record to be functions with implicit arguments. If the only record types available were generic $\Sigma$-types, then first-class implicit functions would be the only way to bundle implicit functions up with other data, which would certainly be essential. But in the presence of general record types whose fields can be implicit functions, it's harder for me to come up with examples.)

Answer 1

Here is a small and concrete example that I think looks better thanks to Agda's strategy. First, let me show what's wrong in Coq. Consider this type of natural transformations of functors Type -> Type:

Record Nat (f g : Type -> Type) : Type :=
  { apply : forall {a}, f a -> g a }.

The {a} annotation makes that argument implicit for the projection apply, but you still have to name it in construction:

Definition idNat : forall {f}, Nat f f := fun f =>
  {| apply := fun a x => x |}.

In that definition, the variables f and a are unused, and one might say, therefore useless. And indeed, Agda lets you not name implicit arguments also when constructing functions:

record Nat (f g : Set → Set) : Set₁ where
  field
    apply : ∀ {a} → f a → g a

example : ∀ {f} → Nat f f
example = record { apply = λ x → x }

To be fair, this could be argued either way. It may be useful to annotate all binders with their types, in which case no binder should be implicit. But the point is there's room for either opinion, and Coq's second-class implicit system only gives you a shallow level of control.

This may be another mathematician vs programmer divide. The opposite view is that you can tell from a function type that some arguments should be implicit because they can be inferred from the context, so specifying implicitness for individual functions is not quite the right level of abstraction, and you might not even have an opportunity to do that in parameters of higher-order functions.

Not mentioning those inferrable arguments leaves more room for the truly essential parts of a program. And if you really need to, you can always ask the elaborator. You also get the property that it's no harder to write Haskell code (a non-dependently typed language where type parameters are implicit, precisely because they are usually inferrable) in Agda than in Haskell.

Moreover, Coq has some strategies to infer implicit arguments, but when they don't work you're back to manually specifying them. No automatic solution will be completely satisfactory, as in fact, the above example of ∀ {a} → f a → g a is inherently ambiguous. It's fine to make a implicit if f and g are always abstract variables or type constructors, while the situation becomes murkier once you expect to instantiate them with lambdas. In that sense, Agda's system of making implicitness type-based but still ultimately an explicit decision by the user hits a sweet spot of automation vs control in this design space.

Answer 2

Coq's strategy is a little confusing with fixed points over indexed data.

Definition map {A B} (f: A -> B): list A -> list B :=
fix loop x :=
   match x with
   | cons h t => cons (f h) (loop t)
   | nil => nil
   end
.

Works fine

Definition map {A B} (f: A -> B): forall {n}, Vector.t A n -> Vector.t B n :=
fix loop {_} x :=
   match x with
   | Vector.cons h t => Vector.cons (f h) (loop t)
   | Vector.nil => Vector.nil
   end
.

Gets awkward.

The problems get muckier in stuff like recursing over ASTs because what if you need to pass in loop to another mapping function.

(forall {n}, Vector.t A n -> Vector.t B n) is very awkward as an argument to a function.