Compiler proposal: add implicit parameters

Change Proposals
#1

Pros:

  1. edwardkmett sid that they are much better than ReaderT

  2. they are used everywhere in ihp

  3. idris2 too has implicit parameters / arguments Miscellany — Idris2 0.0 documentation

Cons:

  1. What's wrong with ImplicitParams
1 Like
#2

I don’t really like the sound of this personally.

PureScript already decided coherence was an important thing, and correspondingly disallowed orphan instances entirely. It would be a little odd to then go ahead and introduce implicit parameters which are incoherent by design.

I guess you could argue they’re meant to solve different problems, so the same logic might not apply to both, but I’d need to see some good arguments to show that the convenience is really that much better than the alternatives.

8 Likes