[GHC] #7828: RebindableSyntax and Arrow

[GHC]

#7828: RebindableSyntax and Arrow
----------------------------------------------+----------------------------
        Reporter:  AlessandroVermeulen        |            Owner:
            Type:  bug                        |  jstolarek
        Priority:  normal                     |           Status:  new
       Component:  Compiler (Type checker)    |        Milestone:  7.10.1
      Resolution:                             |          Version:  7.6.2
Operating System:  Unknown/Multiple           |         Keywords:
 Type of failure:  GHC rejects valid program  |     Architecture:
       Test Case:                             |  Unknown/Multiple
        Blocking:                             |       Difficulty:  Unknown
                                              |       Blocked By:
                                              |  Related Tickets:  #1537,
                                              |  #3613
----------------------------------------------+----------------------------

Comment (by ross):

 Replying to [comment:30 jstolarek]:
 > A few more questions to make sure that I understand:
 >
 > 1. If your solution was implemented then `bind`, `bind_` and
 `ifThenElseA` would be rebindable and `arr` & friends would not?

 Yes.

 > 2. `bind`, `bind_` and `ifThenElseA` currently don't exist in the
 libraries. Implementing yor proposal would require adding their
 definitions to Control.Arrow. Desugared arrow notation would call these
 default definitions, unless `RebindableSyntax` is enabled, in which case
 we use the definitions of `bind` etc. that are currently in scope.
 Correct?

 It would probably be helpful to add them, but it wouldn't be necessary,
 just as the libraries don't currently have a definition of `ifThenElse`.
 The point is that the existing translation is equivalent to translating
 via these operators, so with `RebindableSyntax` turned on one could
 translate to those names instead.  Then again, always translating via
 those names would mean less desugaring code, which Simon would approve of.

 (I've edited comment:17 to add the translation of `rec`, which I forgot
 before.)

 > 3. In comment:17 you wrote:
 >
 > {{{
 > do { p <- cmd; stmts } = cmd `bind` \ p -> do { stmts }
 > }}}
 >   Is `\ p -> do { stmts }` a shorthand for "put `p` on the stack and
 desugar `do { stmts }`"? If not, then what does it mean (code as written
 does not typecheck because `bind` needs an arrow, not a lambda).

 Remember that we're still in the command world here, so the infix operator
 `bind` is applied to two commands.  A command can have the form `\ p ->
 cmd`, and that's what we have here.  The meaning follows from the above
 implementation of `bind` and the existing translation rules for commands.
 The `bind`operator will leave the output of the first command on the
 stack, and the second command will take it off and match it against `p` to
 extend its local environment.

 > 4. I assume that this desugaring still requires the stack to store bound
 parameters (`p` in this example)?

 The rules for commands other than `do` and `if` would be as before.  The
 lambda would take the argument off the stack, match it against `p`, and
 add to the local environment an entry for each variable in `p`.

 > Replying to [comment:28 ross]:
 > > I don't see how the former can work, as each language construct is
 translated to several of those combinators.
 >
 > This seems technically simple to me: just store in a constructor as many
 copies of the required combinators as necessary for desugaring. Although
 simple it leads to a design I'm not happy with. For example `RecStmt`
 requires 11 (sic!) combinators to desugar: 5x `>>>`, 4x `arr`, `first` and
 `loop`.
 >
 > > you have less control of the types of these things, because the
 translation re-arranges and trims the environment it passes through the
 arrow.
 >
 > Yes, if I need to write down the exact types for typechecking this
 becomes a problem. Which brings me to another question related to Simon's
 answer:
 >
 > Replying to [comment:29 simonpj]:
 > > The last sentence is terribly important!
 >
 > That's what I suspected. So in the typechecker we type check `pat <-
 rhs; stmt` as if it was `rhs >>= \pat -> stmt` and later in the desugarer
 we actually convert it to such form, right? So if I want to typecheck the
 arrow desugaring I need to typecheck *exactly* the form to which it will
 later be desugared, including all the explicit stacks, etc?

 Yes you do, and that will be harder in the arrow case, because the local
 environment is an explicit input to the resulting arrow, and the desugarer
 feels free to trim unused variables from that environment, which will
 change its type.  It would probably be necessary to force the replacements
 for the arrow combinators to be polymorphic in the environment.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/7828#comment:31>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler