* It would be tremendously helpful to partition the wiki page into

* I see the need for `Ref` vs `Static`; the latter allows comosition;

The major open issue, but one that it not treated head-on in the wiki

[...] So unless we do something we'll probably end up with `y2`, and that is

#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): three layers:[[BR]][[BR]] Thank you for this suggestion regarding structure. We will update the wiki page shortly. 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. page, is that of '''polymorphism'''. Polymorphism simply isn't discussed by the Cloud Haskell paper. 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