[GHC] #7015: Add support for 'static'

[GHC]

#7015: Add support for 'static'
-------------------------------------+-------------------------------------
              Reporter:  edsko       |            Owner:
                  Type:  feature     |           Status:  patch
  request                            |        Milestone:  7.10.1
              Priority:  normal      |          Version:  7.4.2
             Component:  Compiler    |         Keywords:
            Resolution:              |     Architecture:  Unknown/Multiple
      Operating System:              |       Difficulty:  Unknown
  Unknown/Multiple                   |       Blocked By:
       Type of failure:              |  Related Tickets:
  None/Unknown                       |
             Test Case:              |
              Blocking:              |
Differential Revisions:  Phab:D119   |
-------------------------------------+-------------------------------------

Comment (by mboes):

 >  * It would be tremendously helpful to partition the wiki page into
 three layers:[[BR]][[BR]]

 Thank you for this suggestion regarding structure. We will update the wiki
 page shortly.

 >  * I see the need for `Ref` vs `Static`; the latter allows comosition;
 the former is just a code pointer.  But I don't understand what
 `GlobalName` is doing, nor why `Static` needs two type parameters.   All
 very mysterious.

 This should become clearer once we expand the scope of the wiki page. A
 quick primer: `GlobalName` is to `Ref` what `Addr#` is to `Ptr`. That is,
 just like `Ptr` is a wrapper around `Addr#` adding a phantom type
 parameter, so is `Ref` a wrapper around `GlobalName` adding a phantom type
 parameter.

 In our current scheme, `Static` is not a datatype defined in base. Only
 `Ref` is. `Static` is provided by an add-on package which already exists
 and that we are largely reusing: `distributed-static`. The only thing we
 have changed here is to make `distributed-static` parametric in the label
 type. Wherease `distributed-static` used to only support user strings as
 the label type, it is now parametric so that those users that are using
 Cloud Haskell on a current compiler (not supporting the `static` keyword
 extension), can still use the `distributed-static` package. That's where
 the `l` parameter in `Static l a` comes from: `l` is the label type. When
 using `static`, the label type is a `GlobalName`. When not using it, one
 typically uses a free form string. Or some custom datatype with one
 constructor per possible remotable function, if one prefers to in effect
 manually defunctionalize.

 > The major open issue, but one that it not treated head-on in the wiki
 page, is that of '''polymorphism'''.  Polymorphism simply isn't discussed
 by the Cloud Haskell paper.
 > [...]
 > So unless we do something we'll probably end up with `y2`, and that is
 problematic because if we write it out in System F we'll see
 > {{{
 > y2 :: forall a. Static ([a] -> [a])
 > y2 = /\a. static (reverse a)
 > }}}
 > so the argument to `static` hsa a free variable, namely `a`, that is not
 bound at top level.  I ''believe'' (see #9429), that some CH users are
 somehow doing this: instantiate the polymorphic function at `Any`, and
 send that:
 > {{{
 > y2 :: Static ([Any] -> [Any])
 > y2 = static (reverse Any)
 > }}}
 > Now at the other end, you use `unstatic` to get `[Any] -> [Any]`, and in
 some way I do not understand, convert it to `forall a. [a] -> [a])`.

 Yes, in this respect, we haven't changed anything to how `distributed-
 process` is already doing things today. Currently, `distributed-process`
 already uses the `Any` "hack" for a number of internal remotable
 functions. In fact Well-Typed developed an entire package to support this,
 called `rank1dynamic`. It has an implementation of first-order
 unification, so that on the remote end where say `[Any] -> [Any]` is
 expected, it is perfectly fine to send a function of type `[Int] ->
 [Int]`, because `isInstanceOf (typeOf x) (typeOf y) == True` if `x ::
 [Int] -> [Int]` and `y :: [Any] -> [Any]`.

 So while there was an effort to not upheave the status quo too much,
 that's not to say that we shouldn't.

 The crux of the issue is: a) no first class representations of polymorphic
 types, b) avoiding impredicative types, because the support for that in
 GHC is patchy at the moment AFAIU.

 > But all this `y2` stuf is clearly a Gross Hack, and one that becomes
 even clearer when we have overloaded functions like `sum :: forall a. Num
 a => [a] -> a`.  Now the `y2` equivalent really isn't going to work.  With
 explicit System F notation:
 > {{{
 > z2 :: forall a. Num a => Static ([a] -> a)
 > z2 = /\a \(d:Num a). static (sum a d)
 > }}}
 > Now the `(sum a d)` has a free ''value'' variable `d`, which is lambda
 bound, so now `static` really cannot work.  Again what we really want is
 > {{{
 > z1 :: Static (forall a. Num a => [a] -> a)
 > z1 = static sum
 > }}}
 > I'll stop here for now.

 Yes. FWIW, in the current implementation, we don't allow unresolved
 constraints in the type of the body of a static form. We have discussed
 this issue at length, both internally and with Edsko and Duncan. At this
 point, we simply don't know how to deal with constraints well, though
 Edsko did share with us some ideas that from an earlier discussion with
 you. I'll try to dig out that email from somewhere.

 It's worth noting that all overloaded functions can be handled with some
 help from the user, as discussed on the wiki page (conceivably the
 compiler could do this automatically):
 {{{
 data Dict c = c => Dict

 showD :: Dict (Show a) -> String
 showD Dict = show

 t1 = static showD      -- this works.
 }}}

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