Feature request: Allow for overloading function application (the 'whitespace' operator)

[4e554c4c]

Feature request: Allow for overloading function application (the 'whitespace' operator)

[gallais]

*déjà vu*

[plt-amy]

déjà vu

I don't think this reaction is appropriate; it's not April. This issue is a legitimate feature request, with prior art in other proof assistants and, more importantly, our very own (FROMNAT, FROMNEG, FROMSTRING, do notation, idiom brackets).

---

The reason I suspect this would be possible to implement without moving a mountain of code is that we (a) already have handling for deferring the checking of arguments when a function's type is unresolved and (b) already overload function application, in --cubical, to support applying PathPs.

The idea is simple: in checkArgumentsE, if we're checking an application of a visible argument to a type that is definitely not a Pi (or Path), then we instead elaborate (f as # x) es, where as stands for the already-checked arguments, x:es are the arguments-to-check, and _#_ is whatever appropriate builtin --- maybe BUILTIN TOFUNCTION.

However, there are actually a couple implementation challenges regardless.

1. Agda is quite content to assume that any rigid symbol is the "target type" of a Π, even if the type is just a Def, so it's actually pretty difficult to get into a situation where you'd get a ShouldBePi. For example:
   Fixed, see below

2. checkArgumentsE and its callers assume that checking an application can only snoc new Elims onto the end of the head term. The feature proposed here would require some shuffling, so that checkArgumentsE would be allowed to do the "rotation" necessary to build the application of _#_.

   The most sensible thing, IMO, would be to defunctionalise the continuation to checkArguments --- essentially storing the head term ± information about whether or not some parameters should be dropped.

3. inferApplication, checkArguments etc. like to postpone instance constraints. If the user has implemented their _#_ using instance arguments, then it's probably a good idea to at least try solving constraints generated by elaborating f # x immediately.

   Using the 1Lab's _#_ for an example, if we're checking e.g. f x y, for f : T with instance app : Funlike T A (λ _ → B → C) the only viable candidate, then solving the Funlike constraint eagerly would allow us to know that x : A and (f # x) : B → C. This would avoid postponing the checking of x and of the remaining arguments y.

Because this will be a more significant refactoring of checkArgumentsE than I originally thought, I think it's probably a good idea to wait for some actual opinions for/against this feature before I spend my time implementing it. Needless to say, if we do go forward with this, I'm happy to put in the work.

[andreasabel]

@plt-amy

1. This is probably a bug worth fixing regardless of whether or not we go ahead with the feature proposed here.

Indeed! To not side track the discussion here, I singled this out into:

• #7158