[Feature] Overrideable parameters blocks

[jjl]

• [x ] I have read CONTRIBUTING.md.
• [x ] I have checked that there is no existing PR/issue about my proposal.

Summary

Parameters blocks could be much more useful with this one weird trick.

Motivation

Outside of a parameters block, anything defined within one looks like a function taking extra parameters. This is good and simple and expected. Inside parameters blocks, however, those are fixed. There is no means to call a second function within the same parameters block while varying one of the parameters - it is fixed to what it was given the first time something outside the block called it.

This is inconvenient in many cases. A classic example that comes to mind is writing an interpreter for the lambda calculus. We end up taking a lot of arguments not abstracted away by the parameters block so that we can vary them. Well no, probably we end up with some ghastly hodgepodge squeezed into the monad format, instead. Much better!

Instead, wouldn't it be nice if i could simply override the parts that need changing when calling another function? This would greatly increase the number of situations in which i could use parameters blocks to tidy up quite a lot of code and vastly reduce the number of cases in which i might turn to nested parameters blocks and pray that i don't trip myself up with the related bugs.

The proposal

Initially I'm suggesting we implement this only for named implicits. We already have a syntax for explicitly providing a named implicit. In this situation, it should override the value rather than throwing an error as it does now. Not that I wouldn't like more, but the other cases seem less obvious.

Examples

okay, this is a bit contrived, but i don't really want to write an interpreter here...

parameters {foo : Nat}
  fac : Nat
  fac = case foo of
    Z => 1
    S bar => foo + fac {foo=bar}

Technical implementation

As I understand it, parameters blocks don't really exist and are basically elaborator hacks. I could be wrong about this. We would have to implement more elaborator hacks?

Alternatives considered

I ran this past @andrevidela who suggested a prefix keyword before the name binding and a prefix keyword at the override site. I don't think this is necessary since we can't break any existing code. On the other hand andre's example wasn't with an implicit, so perhaps the first (here mutable, but i don't like the name) isn't so bad?

parameter (mutable s : State)
    fn : …
    fn = fn {s = update s}

Conclusion

You will surely not regret 64 parameters <64amps.jpg>. But only if we make parameters blocks more useful first.