[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:11 jstolarek]:
 > I have a few questions about implementation in `DsArrows` - I think
 these go to Ross.
 >
 >   1. What is the purpose of the stack created in the desugaring process?
 >   2. How do I read the notation describing each case of `dsCmd`? Eg. the
 `HsCmdApp` case has this comment:
 >
 > {{{
 > -- D; ys |-a cmd : (t,stk) --> t'
 > -- D, xs |-  exp :: t
 > -- ------------------------
 > -- D; xs |-a cmd exp : stk --> t'
 > --
 > --        ---> premap (\ ((xs),stk) -> ((ys),(e,stk))) cmd
 > }}}
 > What is `|-a`, `xs` and `ys`? What is the difference between `:` and
 `::`? Could you tell me how to read this particular comment? I should then
 be able to understand all the others. EDIT: Is there a semantic difference
 between `,` and `;` as in `D; ys` vs. `D, xs`?

 Yes, those differences in punctuation are significant.  A type judgement
 for an expression (ignoring constraints) looks like
 {{{
 D |- exp :: t
 }}}
 but one for a command looks like
 {{{
 D; xs |-a cmd : stk --> t
 }}}
 Here
 * a is the type of arrow for this command
 * D is the environment of the surrounding proc expression
 * xs are variables defined within the proc expression, which will be
 inputs to the arrow
 * stk is a list of anonymous inputs to the arrow
 * t is the output type of the arrow
 So the translation of this command should be an expression with type
 {{{
 D |- [[proc (xs) -> cmd]] : a ((xs),stk) t
 }}}
 In this particular rule, exp is typed using an ordinary expression
 judgement.  It can use both external valuables (D) and those local to the
 proc expression (xs), so these are combined in a single environment.
 (Commands, in contrast, need to keep these separate.)  The value of that
 expression is then pushed onto stk, which, together with xs, is input to
 cmd.  (The lambda rule for commands lets you take a value from the stack
 and put it in the local environment, giving it a name.)  The remaining
 wrinkle here is that cmd may not need all the variables in xs, but just
 the subset ys of xs, so the function inside the premap may also trim the
 environment from xs to ys.

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