GitLab

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:

1. This expansion is pretty easy, and can be done in the renamer. Special code paths in the typechecker and desugarer can disappear.
2. When RebindableSyntax is on, we can just use whatever leftSection and rightSection are in scope, extending the range of RebindableSyntax.

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 all leftSection 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 and y would get monotypes.

• leftSection and rightSection as not treated uniformly. Why not make it

  leftSection  :: (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.