[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 simonpj):

 Thank you for writing the [wiki:StaticValues] wiki page.  It is extremely
 helpful.  We should get it settled down before I can comment meaningfully
 about the implementation.

  * It would be tremendously helpful to partition the wiki page into three
 layers:[[BR]][[BR]]
    * '''Library code built on top of the primitives GHC provides'''.
 `Closure` fits here.[[BR]][[BR]]
    * '''Primitives that GHC provides, as seen by the programmer'''.  I
 believe that the `static` language construct and `Static` type (abstract)
 fit here, along with `applyStatic`, and `unstatic`.[[BR]][[BR]]
    * '''How those primitives are implemented in GHC'''.  I believe that
 `GlobalName`, `Ref`, and of course the constructors of `Static`, are part
 of the implementation, not part of the programmer-advertised API of the
 feature.
  Would it be possible to make that decomposition explicit?  Doing so would
 require quite a bit of re-structuring, because at the moment the three
 layers are all mixed up together.

  * 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.

 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.  This, for example, is fine:
 {{{
 x :: Static ([Int] -> [Int])
 x = static (reverse :: [Int] -> [Int])
 }}}
 Everything is monomorphic, and we can send a code pointer of type `[Int]
 -> [Int]`.  But should either of these be OK?
 {{{
 y1 :: Static (forall a. [a] -> [a])
 y1 = static reverse

 y2 :: forall a. Static ([a] -> [a])
 y2 = static reverse
 }}}
 The former is somehow really what we want: we want to encapsulate a code
 pointer to the real, polymorphic, reverse function.  But it's tricky
 becuase GHC (and Haskell) don't usually allow a type constructor applied a
 polytype, thus `Static (forall a. [a] -> [a])`.

 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])`.

 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.

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