I started to look at what let-polymorphism should look like and I have a bit of a problem. Hopefully someone here can give me some ideas or at least opinions.

*** Case 1 (easy): we want to be able to write

map f xs = case xs | nil => [] | cons x xs => cons (f x) (map f xs);

and that should work fairly easily: after inference we get 2 uninstantiated metavars so we add the corresponding 2 lambdas around the whole definition and we're done.

*** Case 2 (easy):

map : (?a -> ?b) -> List ?a -> List ?b;

Here, similarly, the ?a and ?b metavars are left uninstantiated, so we can add the corresponding 2 pis around the type and we're done.

*** Case 3: We could also allow

map : (a -> b) -> List a -> List b;

and automatically treat a reference to an non-existing variable (in a type annotation) as a metavar.

*** Case 4: now comes the tricky part. what about case 1 combined with a type annotation?

map : (a : Type) ≡> (b : Type) ≡> (a -> b) -> List a -> List b; map f xs = case xs | nil => [] | cons x xs => cons (f x) (map f xs);

[ Of course, the type annotation could be shortened as in case 2 and case 3 without making much difference to the situation. ]

Option 1: We could do it by treating the map definition as in case 1 and then checking that the inferred type matches the annotation, but: - in general this will fail because the two types may be "equivalent" yet different (e.g. the order of a and b may be reversed). - it means that we elaborate the definition of `map` without taking much advantage of the type annotation. It would allow polymorphic recursion, but while elaborating map, we wouldn't yet know that there are args `a` and `b` in the environment. In the present case, this probably doesn't matter much, but for type-class arguments this could be more annoying.

Option 2: we could instead automatically wrap the definition of map into 2 erasable lambdas based on the type annotation. This is more natural from a "bidirectional type checking" point of view, takes full advantage of the type annotation, and doesn't suffer from having to later check the type we inferred (with the risk that we didn't infer "quite right").

*** Case 5: sinking deeper.

Now, what about

map : (a : Type) ≡> (b : Type) ≡> (a -> b) -> List a -> List b; map = lambda a ≡> lambda b ≡> lambda f -> lambda xs -> case xs | nil => [] | cons x xs => cons (f x) (map f xs);

This is currently the code we accept, and I think it'd be good to still accept it, but if we go with option 2 in case 4, what should we do here? Before we even look at the "lambda a ≡> lam..." code, we'd end up adding two lambdas around the whole thing, but these would be extraneous here. We could try to arrange so that the "automatic instantiation" (which adds implict args wherever we think they're needed) could save us, by basically auto-rewriting the above as:

map : (a : Type) ≡> (b : Type) ≡> (a -> b) -> List a -> List b; map = (lambda a ≡> lambda b ≡> lambda f -> lambda xs -> case xs | nil => [] | cons x xs => cons (f x) (map f xs)) (a := a) (b := b))

but it feels brittle, and seems wrong: why uselessly add lambdas and then matching applications, when the code came already "written in full"?

[ Side note: notice how in the definition above, we use `a` and `b` which look like free variables but are really bound by the auto-added lambdas. ]

One could think: only auto-add the lambdas if the body doesn't already start with such lambdas, but the thing is that the lambdas need to be added before we elaborate the definition (because the lambdas influence the ctx in which the elaboration takes place), so we can't really look at the definition to make a decision: for all we know, the definition has at its top-level a macro-call which needs to look at the ctx to decide what to do.

I think maybe a good solution is to try and provide two forms of `=` definitions: a basic one that doesn't do any magic, and another one that auto-adds erasable lambdas based on provided type annotations. Hopefully the fancier one can be defined as a declaration-macro.

Still, this "auto-adding lambdas" is pretty intrusive. It means that definitions with a type annotations are handled very differently than those without. And that the type annotation already provides part of the definition.

Another problem is that this only works for "prefix args". If you consider the definition of K:

K : (a : Type) ≡> a -> (b : Type) ≡> b -> a; K = ...

only the `a` argument can be easily auto-added as part of the declaration. To auto-add the `b` argument, we'd need to auto-add lambdas not just around definitions, but around arbitrary expressions: this wouldn't be just let-bound generalization any more but it would require some generic "add implicit lambdas wherever needed". We know from MLF and other type-inference systems that such things can be done in some cases, but - it's tricky - it's usually based on comparing the expression's inferred type with what the context expects, but that means the lambda can only be added after the fact (i.e. this corresponds again to option 1 rather than option 2).

This becomes even more problematic for implicit args (rather than merely erasable args): erasable args typically correspond to System-F style polymorphism and can be usually fully inferred and to a large extent they don't matter, but implicit args are real arguments (think type-class dictionaries) so they have an impact on performance, which means that we don't want to risk adding spurious "lambdas + corresponding calls" since they may not always turn out to be easily optimizable via eta-reduction.

Maybe the best option is to only do the auto-add-lambdas for the case where the definition is of the form "f <args> = <exp>" and in that case we can even auto-add intermediate implicit/erasable args, so we could accept:

K : (a : Type) ≡> a -> (b : Type) ≡> b -> a; K x y = x;

Hmm...

Stefan