Operator sections and rebindable syntax
As part of fixing #19154 (closed) and #19167 (closed) I developed !4981 (merged), fleshing out out plan to implement RebindableSyntax in the renamer rather than the typechecker.
As part of that it felt natural to give the same treatment to operator sections. This ticket is to discuss the details.
I ended up with this translation
(`op` e) ==> rightSection op e
(e `op`) ==> leftSection (op e)
where those two new function are defined like this
leftSection :: (a->b) -> a -> b
rightSection :: (a->b->c) -> b -> a -> c
Benefits:
- This expansion is pretty easy, and can be done in the renamer. Special code paths in the typechecker and desugarer can disappear.
- When RebindableSyntax is on, we can just use whatever
leftSection
andrightSection
are in scope, extending the range ofRebindableSyntax
.
Benefit (1) is purely internal. Benefit (2) is user-visible.
Some observations and questions.
-
Do we want infix application to be rebindable too?
-
leftSection
looks like an identity function. Why don't we do this(e `op`) ==> op e
Answer: we want to enforce that
op e
has a function type; that's allleftSection
does. -
What about higher rank types? Suppose
op :: (forall a. a->a) -> (forall b. [b] -> [b]) -> blah
We might hope that
(id `op`) (`op` reverse)
would both work. And the will, under the above translation, through the magic of Quick Look
-
What about nested quantification? Suppose
op :: forall a. Eq a => a -> forall b. Ord b => b -> blah
That will work for left sections (under the scheme above) but not for right sections (because we don't do deep instantiation any more).
If we changed the expansion thus:
(`op` e) ==> rightSection (\x y -> op x y) e
then we'd get nested quantification, but would lose higher rank functions, because the lambda-bound
x
andy
would get monotypes. -
leftSection
andrightSection
as not treated uniformly. Why not make itleftSection :: (a->b) -> a -> b rightSection :: (a->b->c) -> b -> a -> c
We could do that, but then nested quantification would not work for left sections either. On the other hand it would give more wiggle room for what you can do with RebindableSyntax, because the operator and argument are passed separately.
No one is begging for rebindable syntax for operator sections or infix operators so, since there are some tricky corners, perhaps we should park rebindable syntax for now.
That leaves benefit (1). And there we still have the questions about
- Whether higher-rank operators should work. I think they should
- Whether operators with nested quantification should work. I'm happy if they don't, because it's hard to give a typing rule.
The unifying idea is that we explain the typing rule for sections (and indeed infix) by saying "It typechecks iff this translation typechecks", which is much easier for users and implementors than some fancy new rule that has to account for higher rank, nested quantification, and impredicative instantiation.