Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
  • GHC GHC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 4,863
    • Issues 4,863
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 455
    • Merge requests 455
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #19354
Closed
Open
Created Feb 12, 2021 by Simon Peyton Jones@simonpjDeveloper

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:

  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.

Edited Feb 15, 2021 by Simon Peyton Jones
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking