Opened 3 years ago

Closed 9 months ago

#7015 closed feature request (fixed)

Add support for 'static'

Reported by: edsko Owned by:
Priority: normal Milestone: 7.12.1
Component: Compiler Version: 7.4.2
Keywords: Cc: 0xbadcode@…, facundominguez@…, watson.timothy@…, simonmar
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Revisions: Phab:D119, Phab:D550, Phab:D568

Description (last modified by simonpj)

.. as described in "Towards Haskell in the Cloud".

See also #9429 (Alternative to type family Any), which is closely related.

Change History (44)

comment:1 Changed 3 years ago by igloo

  • difficulty set to Unknown
  • Milestone set to 7.8.1

comment:3 Changed 19 months ago by mboes

  • Cc 0xbadcode@… added

comment:4 Changed 19 months ago by facundo.dominguez

  • Cc facundominguez@… added
Last edited 19 months ago by facundo.dominguez (previous) (diff)

comment:5 Changed 19 months ago by hyperthunk

  • Cc watson.timothy@… added

comment:6 Changed 19 months ago by carter

Edsko seems to have a good proof of concept that the notion of Static needed for Cloud Haskell is implementable in user land here https://github.com/haskell-distributed/distributed-static/commit/d2bd2ebca5a96ea5df621770e98bfb7a3b745bc7 https://github.com/haskell-distributed/distributed-static/tree/static-with-hsplugins

on the static-with-hsplugins branch of distributed-static.

it seems like that TH + GHC API / hs-plugin approach edsko has shared gets most of the way there! Is there anything that this solution lacks?

comment:7 Changed 19 months ago by simonmar

  • Cc simonmar added

comment:8 Changed 19 months ago by facundo.dominguez

Discussion is also happening here. Threads went disjoint.

Last edited 19 months ago by facundo.dominguez (previous) (diff)

comment:9 Changed 19 months ago by hyperthunk

Indeed - we've not reached a conclusion yet!

comment:10 Changed 16 months ago by thoughtpolice

  • Milestone changed from 7.8.3 to 7.10.1

Moving to 7.10.1.

comment:11 Changed 13 months ago by facundo.dominguez

  • Differential Revisions set to Phab:D119
  • Status changed from new to patch

comment:12 follow-up: Changed 13 months ago by simonpj

Great work. I'm going to add some top level comments here

  • I'd love a wiki page summarising the programmer's-eye-view of the design; and sketching the implementation. You may say that the programmer's eye view is in the paper, but (a) that's less accessible, and (b) details change, such as the type, which you have called Ref.
  • Bikeshed: I don't that is at all a good name... sounds mutable to me. I don't think Static t so bad. StaticName is ok, as is StaticPtr.
  • The type checker is not supposed to do program transformations like floating bindings to top level. It should be possible to display the output of the type checker in an IDE, exactly as the programmer wrote it, fully decorated with type information.

So I think it'd be better if the desugarer did the floating, not the type checker. That should not be a hard change to make.

  • I don't understand checkStaticValues. The typing rule for static in the paper is quite simple, so what is going on here?
  • What is addrToAny# and where is it documented?
  • I'm pretty convinced that static values (Refs) should come with a TypeRep -- or at least the fingerprint of a TypeRep so that we can reject bogus values. That wouldn't be hard, would it? The merit of having a TypeRep tree rather than just a fingerprint is that the error message might be more informative.

Simon

comment:13 in reply to: ↑ 12 Changed 13 months ago by facundo.dominguez

Replying to simonpj:

  • I'd love a wiki page summarising the programmer's-eye-view of the design; ...

Good suggestion.

  • What is addrToAny# and where is it documented?

Found here: http://www.haskell.org/ghc/docs/latest/html/libraries/ghc-prim-0.3.1.0/GHC-Prim.html#v:addrToAny-35-

  • ... So I think it'd be better if the desugarer did the floating, not the type checker. That should not be a hard change to make.

Sure, we can try it.

  • I don't understand checkStaticValues. The typing rule for static in the paper is quite simple, so what is going on here?

One of the major design choices we had to make is how to handle qualified types. Say we have the expression static return, we had to choose between giving it types like:

static return :: Ref (Monad m => a -> m a)
static return :: Monad m => Ref (a -> m a)

or disallow them completely.

The last option looked the simplest while still useful, so we disallowed static forms whose bodies have qualified types. Now, say we want to type-check an expression like

f :: Ref (a -> IO a)
f = static return

We expect the expression return to have type a -> IO a. Yet we don't know if the type of return will be qualified or not until the whole definition of f is type-checked. f could have more equations and no type signature, or we may even have to wait for the whole module to be type-checked because of the monomorphism restriction.

checkStaticValues is the piece of the implementation that considers if the body of the static form has a qualified type. And this, we understand, is only practical to do after the whole module has been type-checked.

  • I'm pretty convinced that static values (Refs) should come with a TypeRep ...

In case you mean Data.Typeable.TypeRep, how could we deal with static forms whose bodies have a polymorphic type?

Bikeshed: ...

I leave this for later.

Thanks for looking at the implementation. It really needs the feedback. And probably, we should document better the design and discuss it.

Last edited 13 months ago by facundo.dominguez (previous) (diff)

comment:14 Changed 13 months ago by facundo.dominguez

Design notes are available here. Please, feel free to comment or ask for refinements.

comment:15 Changed 13 months ago by facundo.dominguez

When trying to do floating in the desugarer I arrived at a point where I need evidence bindings to desugar. For instance, when encountering the expression static return :: Ref (a -> IO a), the desugarer tries to float return as

Main.static:0 :: forall a_azE. a_azE -> GHC.Types.IO a_azE
Main.static:0 =
  \ (@ a_azE) -> GHC.Base.return @ GHC.Types.IO $dMonad_azG @ a_azE

where $dMonad_azG is a variable carrying the Monad IO dictionary. As $dMonad_azG is not in scope the above code is rejected by the Core Lint pass.

When floating is done in the typechecker, the binding of $dMonad_azG is produced by simplifyInfer in checkStaticValues at the place where the floated bindings for static forms are assembled. Further down the processing, desugaring inserts this evidence binding as a core let binding in the rhs of static:0, subsequently inlined to yield something like:

Main.static:0 :: forall a_azE. a_azE -> GHC.Types.IO a_azE
Main.static:0 =
  \ (@ a_azE) -> GHC.Base.return @ GHC.Types.IO GHC.Base.$fMonadIO @ a_azE

Now, to do floating in the desugarer, it looks like evidence bindings need to be communicated to the place in the desugarer (I presume dsExpr) where the floating should be implemented. Would there be a preferred way to do it and is it sensible at all? I couldn't find precedents of similar needs in the ghc code.

Last edited 12 months ago by facundo.dominguez (previous) (diff)

comment:16 Changed 12 months ago by rodlogic

I would just like to document another potential use case for this in addition to the Cloud Haskell one: A Seamless, Client-Centric Programming Model for Type Safe Web Applications.

I am thin on the details here since I just came across the paper, but the idea is to provide an:

... alternative programming model based on Haskell, in which web applications are written as a single program rather than as two independent parts that just so happen to talk to each other.

And:

The remote function takes an arbitrary function, provided that all its arguments as well as its return value are serializable through the Serialize type class, and produces a typed identifier which may be used to refer to the remote function. In this example, the type of greetings is Remote (String → Server ()), indicating that the identifier refers to a remote function with a single String argument and no return value. Remote functions all live in the Server monad. The part of the program contained within the App monad is executed on both the server and the client, albeit with slightly different side effects, as described in section 3.

And here is a simple example:

import Haste.App

helloServer :: String  Server () 
helloServer name = liftIO $ putStrLn (name ++ " says hello!")

main :: App Done 
main = do
  greetings  remote helloServer
  runClient $ do
    name  prompt "Hi there, what is your name?" onServer (greetings <.> name)

I know this is not the core of the design space, but it is another dimension to consider. For example, being able to customize the closure serialization format could be an important requirement.

comment:17 Changed 12 months ago by simonpj

  • Description modified (diff)

comment:18 Changed 12 months ago by simonpj

  • Description modified (diff)

comment:19 follow-up: Changed 12 months ago by simonpj

Thank you for writing the 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:

    • Library code built on top of the primitives GHC provides. Closure fits here.

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

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

comment:20 Changed 12 months ago by carter

on a mildly bikeshedding note, before this work (or applicable subsets) gets merged in, could we update the wiki notes etc to not use the term StaticValues? (this has been discussed elsewhere, but adding it as a note here)

comment:21 in reply to: ↑ 19 Changed 12 months ago by mboes

  • It would be tremendously helpful to partition the wiki page into three layers:

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.

comment:22 follow-up: Changed 12 months ago by simonpj

OK so it sounds as if Static is 100% part of the library layer, and GHC knows nothing about it. That's fine; and will become clear when you re-structure.

Concerning upheaving, my main goal is to have clean, well-designed primitives in GHC. I don't fully understand the Any business (e.g. how can it possible deal with polymorphic functions with more than one type parameter forall a b. a -> b -> b?), but it smells like a hack. And I don't want to enshrine a hack in GHC.

Perhaps we could say, for now, that the argument of static must have no free type variables, just as it has no free term variables (other than top level constants). So,

y1 :: forall a. Static ([a] -> [a])
y1 = static reverse

would be rejected, but

y3 :: Static ([Any] -> [Any])
y3 = static reverse

would be accepted. Now you can continue to do your current hack in the library (pending a better solution for polymorphism), but the GHC part remains simple and clean.

comment:23 in reply to: ↑ 22 Changed 12 months ago by mboes

Replying to simonpj:

Perhaps we could say, for now, that the argument of static must have no free type variables, just as it has no free term variables (other than top level constants). [...] Now you can continue to do your current hack in the library (pending a better solution for polymorphism), but the GHC part remains simple and clean.

Yes. It occurred to me while falling asleep last night that just as we ban qualified types, we could as well ban polymorphic types. In both cases, these features are "emulated" outside of the compiler (using the Any hack and a library implementation of unification in the case of polymorphic functions, passing an explicit Dict in the case of overloaded functions).

Now, for the Any hack to continue working in full generality, we're back to #9429.

I don't fully understand the Any business (e.g. how can it possible deal with polymorphic functions with more than one type parameter forall a b. a -> b -> b?), but it smells like a hack.

There are two ways to do this (see #9429): define

type Any1 = Any
type Any2 = Any Any

and then you can encode your type as Any1 -> Any2 -> Any2. Alternatively, Edwardk suggests Any 1 -> Any 2 -> Any 2, using type-level literals. I like that one better. Whatever we do, for the purposes of Cloud Haskell, it must be possible to have a Typeable instance for the resulting type.

If GHC.Exts.Any becomes a type family, then that's no longer a possibility. See proposed solutions in #9429. No matter what we do there, ideally it should be possible to use the Any hack to handle a type like forall a m. Dict (Monad m) => a -> m a, for example. Defining a MyAny :: Nat -> * type for this purposes is an option, but will only work for type variables of kind * and in particular not work for this example. The nice thing about having some datatype with the same properties as GHC 7.8's GHC.Exts.Any (at least for open kinds, not closed kinds, which can't be dealt with), is that the user or libraries don't have to bother defining a proliferation of MyAnys, one for each open kind that gets used in the wild.

comment:24 Changed 12 months ago by edsko

I'm not following the details of the discussion here, but since I wrote rank1dynamic originally, I feel compelled to defend it and say "of course it's a hack, a proper solution wasn't available" :-) One thing to be aware of, though. Giving annotations such

y3 :: Static ([Any] -> [Any])
y3 = static reverse

is okay, but only just: we have to be careful that the compiler doesn't start optimizing the definition for the specific case of the "ANY" type, which is intended as a type variable stand-in, but of course in actually isn't and the compiler might therefore make wrong decisions. In particular, have to be careful with dictionaries here. See "Word of Caution" at the end of http://hackage.haskell.org/package/distributed-static-0.3.0.0/docs/Control-Distributed-Static.html.

comment:25 Changed 12 months ago by mboes

Indeed. In fact a recent issue was reported by Nick Smallbone against the released version of rank1dynamic, whereby using a custom MyAny-like datatype is causing problems, and the proposed fix is again to use GHC.Exts.Any:

https://github.com/haskell-distributed/rank1dynamic/pull/7

comment:26 Changed 12 months ago by simonpj

Edsko my remark about a "hack" was not intended as a criticism. Of course, if GHC is inadequate you must hack around its shortcomings. My intent was solely this: let's not enshrine a temporary hack into the design of the language that GHC implements.

There are two things going on in this ticket:

  • What should be the specification of the feature that GHC implements? I think we are agreeing that: the argument of static should have no free type variables. Let's put that into the spec.

    That leaves open the question of adding an impredicative-like feature, the ability to have terms of type Static (forall a. [a] -> [a]), which make perfect sense, have no free type variables, but which are disallowed at present.
  • Given the above restriction, and the absence of the impredicative support, how can we hack around the restriction to get something like polymorphism. This is the Any discussion on #9429. Even lacking a fix for poly-kinded Any, it's not a disaster because for any particular kind we can always do the job; it's just a bit inelegant.

If we agree about these things, perhaps you can update the wiki page as above and we can go from there.

comment:27 Changed 12 months ago by edsko

One thing I was wondering about: clearly, solving the general problem of impredicativity would take us way off too far here; but if the type checker knows about static, just like, say, it knows about ADTs, then perhaps it wouldn't be too difficult to support things like static (forall a. a -> a), just like it supports universally quantified types as arguments to ADT constructors?

comment:28 Changed 12 months ago by facundo.dominguez

Forbidding free type variables in the static form makes less obvious defining a combinator like the following:

staticCompose :: Static (b -> c) -> Static (a -> b) -> Static (a -> c)
staticCompose sf sg = staticLabel (static (.)) `staticApply` sf `staticApply` sg

This is actually defined in the version of distributed-static in hackage:

composeStatic :: (Typeable a, Typeable b, Typeable c) => Static ((b -> c) -> (a -> b) -> a -> c)
composeStatic = staticLabel "$compose"

staticCompose :: (Typeable a, Typeable b, Typeable c)
              => Static (b -> c) -> Static (a -> b) -> Static (a -> c)
staticCompose g f = composeStatic `staticApply` g `staticApply` f

It doesn't mean that we can't live with the restriction but we will have to evaluate the impact upwards, I guess.

Last edited 12 months ago by facundo.dominguez (previous) (diff)

comment:29 Changed 12 months ago by simonpj

I have spent most of this afternoon writing up some thoughts about StaticPtr and serialisation. Here is the result: simonpj/StaticPointers

I would be very interested in your thoughts. Special thanks to Neil Mitchell who put up with several hours of blather on the way home from ICFP.

I did this by writing something new, rather than by editing StaticPointers, because I didn't want to Utterly Rewrite the latter. For now you can compare the two. Ultimately we should combine them.

Simon

comment:30 Changed 12 months ago by rwbarton

I would just like to echo comment:16: it would be REALLY great not to commit to a particular implementation of unStatic such as dlsym(); in particular the GHCJS backend should be able to have its implementation of the same functionality, with compatible StaticName serializations (if not downright compatible StaticName types). That opens up very interesting possibilities for pure Haskell client/server web applications.

As a more technical point, since GHCJS does dead code elimination, there should be some means by which the GHCJS code generator can know which top-level values are the referents of static expressions, so it can treat them as live, without having to pessimistically assume that everything is live.

comment:31 Changed 12 months ago by simonpj

Agreed. No way should the design mandate any particular implementation for unStatic!

My current proposals are outlined here simonpj/StaticPointers. There is haze around Plan A/B/C near the end, but I'm veering towards some variant of Plan A.

Simon

comment:32 Changed 11 months ago by simonpj

Here's a comment from Phab that should feed into the design: The current implementation does not appear to keep the heap references alive correctly:

{-# LANGUAGE StaticValues #-}
module Main where

import GHC.Ref

import Control.Concurrent
import System.Environment
import System.Mem
import System.Mem.Weak

import Data.Numbers.Primes -- from Numbers

-- Just a Ref to some CAF from another package so that we can deRef it when linked with -dynamic
primes_ref :: Ref [Integer]
primes_ref = static primes

main = do
  as <- getArgs
  let z = primes!!(length as+200)
  print z
  performGC

  -- addFinalizer z (putStrLn "finalizer z")
  print z
  performGC
  threadDelay 1000000
  print . fmap (!!300) =<< deRef primes_ref
  -- uncommenting the next line keeps primes alive and prevents the segfault
  -- print (primes!!300)

and

$ ghc -dynamic -o primes primes.hs
[1 of 1] Compiling Main             ( primes.hs, primes.o )
Linking primes ...
 
$ ./primes
1229
1229
Segmentation fault (core dumped)

comment:33 Changed 11 months ago by luite

I agree with simonpj and rwbarton. My suggestion in the phab discussion (generating foreign exports) was merely something that could be done with the current tools, but now that the patch is going to be rewritten/improved there may be better options.

Other than getting memory management sorted out, I think these are the minimum requirements to make it possible to implement static values properly on different backends:

  • GHC should explicitly keep track of all static metadata (hi files probably)
    • Static names would propagate like typeclass instances
    • It should be possible to build a list (like the Static Pointer Table) at link time for a library or program (and if desired, build a program that can produce this list at runtime)
  • StaticName should be reasonably robust against minor variations between compiles/backends
    • no backend/platform specific internal names
    • a source code location as an identifier for generated names is better than a simple counter
    • at least some simple safeguard against constructing an ill-typed heap object (like a type fingerprint) should be there

As an aside, I think it would be really useful if there was a way to send type details with a more complete serialization of the construction (in terms of Typeable/TypeRep or similar) in the StaticName or at a higher level:

  • It would be possible to generate a more readable type error message if a fingerprint does not match (rather than using show on both sides)
  • Languages like Python and JavaScript could dynamically convert values
  • In conjunction with GHC.Generics or Data.Data one could use this to generate user interfaces that allow typesafe structured construction/editing of arguments (and dictionaries, when supported)

And a final point on my wish list: It would be very useful if the static keyword for toplevel bindings would result in a StaticName that uses the original function name, rather than some generated name:

import qualified Data.Map as M

-- this would guarantee that concat is in the static list
concat :: [[a]] -> [a]
concat = static (foldr (++) [])

-- for functions that do pattern matching we could introduce a pragma
{-# STATIC and #-}
and :: [Bool] -> Bool
and []          =  True
and (x:xs)      =  x && and xs

-- or for exposing functions from other modules
{-# STATIC M.fromList #-}

This would make it easier to have asymmetric CH programs, where one part is merely the callee, but does not include the code where the result from the call is used. I think this could also useful to implement a more flexible foreign exports mechanism for GHCJS, see https://github.com/ghcjs/ghcjs/issues/194 for some discussion.

comment:34 Changed 11 months ago by simonpj

Luite, much of what you say is cast in terms of an underlying implementation, whereas my blog post focuses as exclusively as possible on the specification of what the programmer sees. Can you recast your suggestions in those terms? For example:

  • What does it mean to say that "GHC should explicitly keep track of all static metadata"? How would a programmer be able to tell whether or not GHC did so. That is, what programmer-visible behaviour do you seek?
  • Again "It should be possible to build a list (like the Static Pointer Table) at link time for a library". This is presumably a statement about the implementation but again you must have in mind some user-visible behavior? What is it?
  • Again "Static names would propagate like typeclass instances". I don't really know what this means, but specifically how would a programmer know if this happened? Static names are not visible to the programmer in the design I suggest; I use them only so I can say something about a possible implementation. All the programmer sees is ordinary Haskell values and types (with one new type constructor, StaticPtr.
  • "StaticName should be reasonably robust..." Again, you must have in mind some user-visible behaviour. Here I think I do know what you might mean. If you have a client and server talking to one another, and you recompile one having made only small internal changes, it should still inter-work with the original client. Something like that perhaps? Clearly this isn't yet a precise statement and you might want to make it so.

And so on. Do you see what I mean?

On the question of "I think it would be really useful if there was a way to send type details with a more complete serialization of the construction", I don't understand well enough. I tried (perhaps inadequately) to describe a design in which type security was guaranteed without sending type representations or fingerprints at all. Of course, some higher-level guarantees might be gained by sending type reps, but that would be up to a client library built on top of the facilities GHC provides. Are you asking for any GHC support here, or simply saying something about what a client library might or might not chose to do?

Sorry to be dense. Thanks

Simon

comment:35 Changed 11 months ago by simonpj

Here is the state of play on StaticPtr, as I understand it today, is this:

  • In that blog post, Plan A requires some support from Typable/TypeRep. A new wiki page Typeable describes a design to do exactly that. This will be new to most of you; take a look.
  • The StaticPointers wiki page is out of date; Matthieu and Facundo are planning to update it

None of this amounts to a full Plan; but it does represent progress. I think Matthieu and Facundo are the main driving forces. I'm hoping that you (perhaps with help from others) will

  • work through the proposed design a bit more, to check that it does what you need;
  • develop a plan for how we can more from where we are to the new glorious story with minimum disruption
  • develop an implementation

Simon

comment:36 Changed 11 months ago by simonpj

  • Status changed from patch to new

Taking out of patch status.

comment:37 Changed 9 months ago by facundo.dominguez

  • Differential Revisions changed from Phab:D119 to Phab:D550
  • Status changed from new to patch

comment:38 Changed 9 months ago by Austin Seipp <austin@…>

In fc45f32491313d2a44e72d8d59cdf95b1660189d/ghc:

Implement -XStaticValues

Summary:
As proposed in [1], this extension introduces a new syntactic form
`static e`, where `e :: a` can be any closed expression. The static form
produces a value of type `StaticPtr a`, which works as a reference that
programs can "dereference" to get the value of `e` back. References are
like `Ptr`s, except that they are stable across invocations of a
program.

The relevant wiki pages are [2, 3], which describe the motivation/ideas
and implementation plan respectively.

[1] Jeff Epstein, Andrew P. Black, and Simon Peyton-Jones. Towards
Haskell in the cloud. SIGPLAN Not., 46(12):118–129, September 2011. ISSN
0362-1340.
[2] https://ghc.haskell.org/trac/ghc/wiki/StaticPointers
[3] https://ghc.haskell.org/trac/ghc/wiki/StaticPointers/ImplementationPlan

Authored-by: Facundo Domínguez <[email protected]>
Authored-by: Mathieu Boespflug <[email protected]>
Authored-by: Alexander Vershilov <[email protected]>

Test Plan: `./validate`

Reviewers: hvr, simonmar, simonpj, austin

Reviewed By: simonpj, austin

Subscribers: qnikst, bgamari, mboes, carter, thomie, goldfire

Differential Revision: https://phabricator.haskell.org/D550

GHC Trac Issues: #7015

comment:39 follow-up: Changed 9 months ago by thoughtpolice

  • Differential Revisions changed from Phab:D550 to Phab:D119, Phab:D550
  • Milestone changed from 7.10.1 to 7.12.1
  • Status changed from patch to new

The first draft has landed, awesome! OK, I'm now punting the version on this to 7.12 since there's some future work to do.

Alternatively, we can milestone this to 7.10.1 and close it, and track future improvements through separate tickets. What do you think, Facundo?

(Note, adding the old Phab:D119 to the revision list still, mostly to keep track of historical attempts. Feel free to undo again.)

comment:40 Changed 9 months ago by mboes

Thanks for landing this! As far as I know all features that were requested as part of the GHC 7.10 milestone according to StaticPointers/ImplementationPlan have been implemented and all issues raised by the reviewers addressed. Seeing as this has been merged by now, perhaps it would make sense to go for the latter option, namely track future improvements through separate tickets?

The major future improvement I see is this:

  • Store (higher-order) TypeReps in the SPT and check them upon pointer lookups, in order to reduce the size of trusted base that guarantees type safety.

That improvement is not really possible without switching to a new API for Data.Typeable, as outlined by Simon PJ here, which is a potentially high impact change to base.

I think it means two separate new tickets to track: implement type indexed Data.Typeable, add type representation checking to the SPT.

comment:41 in reply to: ↑ 39 Changed 9 months ago by facundo.dominguez

Alternatively, we can milestone this to 7.10.1 and close it, and track future improvements through separate tickets. What do you think, Facundo?

I think this is best to give its own space to the discussions arising from further work.

(Note, adding the old ​Phab:D119 to the revision list still, mostly to keep track of historical attempts. ...)

Quite appropriate. Thanks.

comment:42 Changed 9 months ago by goldfire

Quick note: there is nothing in the release notes about this significant feature. Please add. Thanks for doing all of this!

comment:43 Changed 9 months ago by Austin Seipp <austin@…>

In bd0f9e1fad6ab69b5967247b32fd8f9305b064a5/ghc:

Write release notes for -XStaticPointers.

Test Plan: ./validate

Reviewers: goldfire, austin

Reviewed By: austin

Subscribers: mboes, carter, thomie

Differential Revision: https://phabricator.haskell.org/D568

GHC Trac Issues: #7015

comment:44 Changed 9 months ago by thoughtpolice

  • Differential Revisions changed from Phab:D119, Phab:D550 to Phab:D119, Phab:D550, Phab:D568
  • Resolution set to fixed
  • Status changed from new to closed

Awesomeness. Merged and closing.

Note: See TracTickets for help on using tickets.