[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:
----------------------------------------------+----------------------------

Comment (by ross):

 Replying to [comment:20 jstolarek]:
 > Can I once again ask for help in reading the comments?
 >
 > {{{
 > -- D; xs1 |-a c : () --> t
 > -- D; xs' |-a do { ss } : t'   xs2 = xs' - defs(p)
 > -- -----------------------------------
 > -- D; xs  |-a do { p <- c; ss } : t'
 > --
 > --        ---> premap (\ (xs) -> (((xs1),()),(xs2)))
 > --            (first c >>> arr (\ (p, (xs2)) -> (xs'))) >>> ss
 > }}}
 > I'm totally confused by `(\ (xs) -> (((xs1),()),(xs2)))`. Where do `xs1`
 and `xs2` come from, if we only bind `xs` as the input to `do { p <- c; ss
 }`?

 They are subsets of `xs`: `xs1` is the variables used by `c`, while `xs2`
 is the variables used by `ss` but not bound in `p`.  So the command 'c'
 gets local environment `xs1` and stack `()`.  The translations of
 statements are arrows that take an environment (here `xs2`) as input.

 > Also, do I understand correctly that bind expression generated in
 desugaring of arrow do-notation does not have a source-level equivalent?
 If so is it even correct to represent it using the !BindStmt constructor?
 >
 > In my prototype I'm ignoring Ross' proposal of the new desugaring.

 I don't understand that question - I don't see a bind expression in the
 generated code.  Do you mean the `BindStmt` emitted by the type checker?
 No, that wouldn't correspond to something one could write in the command
 sublanguage.  Part of the motivation for my proposal is that the
 desugaring of do notation would have a source-level equivalent, albeit
 still in the command sublanguage, but it could be checked using the
 existing rules for commands.

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