Opened 7 years ago

Last modified 4 years ago

#7015 closed feature request

Add support for 'static' — at Version 17

Reported by: edsko Owned by:
Priority: normal Milestone: 8.0.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 Rev(s): Phab:D119
Wiki Page:

Description (last modified by simonpj)

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

See also #9429, which is closely related.

Change History (17)

comment:1 Changed 7 years ago by igloo

difficulty: Unknown
Milestone: 7.8.1

comment:2 Changed 6 years ago by mboes

comment:3 Changed 6 years ago by mboes

Cc: 0xbadcode@… added

comment:4 Changed 6 years ago by facundo.dominguez

Cc: facundominguez@… added
Last edited 6 years ago by facundo.dominguez (previous) (diff)

comment:5 Changed 6 years ago by hyperthunk

Cc: watson.timothy@… added

comment:6 Changed 6 years 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 6 years ago by simonmar

Cc: simonmar added

comment:8 Changed 6 years ago by facundo.dominguez

Discussion is also happening here. Threads went disjoint.

Last edited 6 years ago by facundo.dominguez (previous) (diff)

comment:9 Changed 6 years ago by hyperthunk

Indeed - we've not reached a conclusion yet!

comment:10 Changed 5 years ago by thoughtpolice

Milestone: 7.8.37.10.1

Moving to 7.10.1.

comment:11 Changed 5 years ago by facundo.dominguez

Differential Rev(s): Phab:D119
Status: newpatch

comment:12 Changed 5 years 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 5 years 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 5 years ago by facundo.dominguez (previous) (diff)

comment:14 Changed 5 years ago by facundo.dominguez

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

comment:15 Changed 5 years 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 5 years ago by facundo.dominguez (previous) (diff)

comment:16 Changed 5 years 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 5 years ago by simonpj

Description: modified (diff)
Note: See TracTickets for help on using tickets.