Types-safe Distributed Haskell
This page collects thinking about mechanisms that support type-safe distribution of Haskell programs, particularly focusing on the issues of serialisation. The corresponding Trac ticket to track progress is #7015 (closed).
Several distinct layers are involved; they constitute the main payload of this design:
Typeable: built-in support for generating and using run-time type representations. The
Typeableclass has been part of (GHC) Haskell for many years, but it needs to evolve further.
StaticPointers: built-in support for so-called static pointers. These were introduced in the original Cloud Haskell paper (link below), but the design was not fleshed out there.
DistributedClosures: library support for serialisable closures. These closures can be implemented in a library,
distributed-closurebuilding on the two layers below, but the design of that library is far from trivial.
StaticPointers/ImplementationPlan: a phased approach to implementing the extension in GHC.
StaticPointers/TypesafeDecoding: options for encoding and decoding static pointers.
Our goal is to identify the smallest possible built-in extension to GHC, with
the smallest possible trusted code base, that would enable
distributed-closure to be written in an entirely type-safe way.
See also this ticket about rationalising the runtime reflection naming structures: #10068.
Much of what is suggested here is implemented, in some form, in two existing projects
HdpH libraries hdph and hdph-closure. Background in the paper Implementing a high-level distributed-memory parallel Haskell in Haskell
Simon PJ's long blog post is also relevant, but mainly as background. It should eventually be fully subsumed by the above pages.
The rest of ths page gives background, to set the scene for the main pages above.
In distributed programming, processes on different nodes exchange data by asynchronously sending messages to each other. It is useful to go beyond this model, and allow processes to send other processes to other nodes, not just first-order data. For instance, an extremely useful feature of distributed frameworks in Hasell (e.g. distributed-process, HdpH) and other languages (Erlang, Scala), is the ability for a process on one node to spawn a process on another node.
For example, consider a simple calculator-as-a-service. It is
a process living on some node B, accepting requests of some type
ArithRequest, allowing to express simple arithmetic expressions.
Given a request, the calculator-as-a-service must decode it, interpret
the arithmetic expression, and return the result. But ideally, one
would like a more direct way of performing computations remotely. As
a client, a process on some node A, we would like to be able to do
something like the following instead:
client = do spawn nodeB $ plus 10 2 spawn nodeB $ mult (2^10) (3^10) spawn nodeB $ neg 1
This avoids the need for effectively defining a new DSL, and avoids
the need for an interpreter for this DSL on the other end. Expressing
computations as straight Haskell expressions allows us to reuse GHC's
syntax and type checking at little cost. The above code is similar to
what one would write in a concurrent but single-node setting, using
forkIO instead of spawn. Except that the above snippet implies that
spawn is able to serialize arbitrary Haskell values (or closures).
This is undesirable, because in general closures might capture all
manner of system and local resources (e.g. sockets, locks, file
descriptors) that it makes no sense to send on the wire. We instead
want to limit what can be spawned in this manner to so-called static
closures: values expressed using only top-level identifiers,
literals, and serializable locally-bound variables.
With this extension, one can write:
client = do spawn nodeB $ closure $ static (plus 10 2) spawn nodeB $ closure $ static (mult (2^10) (3^10)) spawn nodeB $ closure $ static (neg 1)
I'm going to assume a a type class
Serialisable, something like this:
class (Typeable a, Binary a) => Serialisable a class Binary a where encode :: a -> ByteString decode :: ByteString -> Maybe (a, ByteString)
(The real class
Binary uses a
Get monad (with methods
get), but I'll use the simpler form above because it introduces all issues that we need here without the clutter of the Real Thing.)
I'll use "encode" and "decode" as synonyms for "serialise" and "deserialise", because the former are easier to pronounce.
Here's an interesting question: are instances of
Binary part of the TCB? No, they are not.
Here is a tricky case:
decode (encode [True,False]) :: Maybe (Int, ByteString)
Here I have encode a
[Bool] into a
ByteString, and then decoded an
Int from that
ByteString. This may
be naughty or undesirable, but it cannot seg-fault: it is type-safe in the sense above. You can
think of it like this: a decoder is simply a parser for the bits in the
ByteString, so a decoder
Int can fail to parse a full
Nothing), but it can't return a non-
For the naughtiness, one could imagine that a Cloud Haskell library
might send fingerprints or
TypeReps or whatnot to eliminate
potential naughtiness. But even then it is very valuable if the
type-safety of the system does not rely on the CH library. Type
safety depends only on the correctness of the (small) TCB;
naughtiness-safety might additionally depend on the correctness of the
-XStaticPointers language extension
StaticPointers language extension adds a new syntactic
construct to Haskell expressions:
E ::= ... | static E
E is any Haskell expression, but restricted as follows: it must
contain no free variables (module-level identifiers are ok). For
technical reasons, the body
E of a static form is further restricted
to be of unqualified type. In other words,
E is allowed to be of
polymorphic type, but no unresolved type class or equality constraints
of any kind are allowed.
An expression of the form
static E has type
StaticPtr T if
T. Any value of type
StaticPtr T can be "resolved" to a value
T by the following new primitive, which can be brought into
scope by importing
GHC.StaticPtr (so-named by symmetry with
unstatic :: StaticPtr a -> a
This is the full extent of the impact on GHC. The above isn't a standalone solution for remoting arbitrary computations across a set of nodes, but the remaining support can be implemented in userland libraries.
The trusted code base
Typeable class, and its associated functions, in
GHC offers a type-safe abstraction, in the classic sense that
"well typed programs won't go wrong". For example, we in
Data.Typeable we have
cast :: forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast to be type-safe: if
cast returns a value
Just x then we really do know
x :: b. Let's remind ourselves of class
class Typeable a where typeRep :: proxy a -> TypeRep
(It's not quite this, but close.) The
proxy a argument is
just a proxy for type argument; its value is never inspected
and you can always pass bottom.
Under the hood,
typeRep to get the runtime
b, and compares them, thus:
cast :: forall a b. (Typeable a, Typeable b) => a -> Maybe b cast x = if typeRep (Proxy :: Proxy a) == typeRep (Proxy :: Proxy b) then Just (unsafeCoerce x) else Nothing
cast is written in Haskell, it uses
unsafeCoerce. For it
to truly be type-safe, it must trust the
Typeable instances. If the
user could write a
Typeable instance, they could write a bogus one, and
defeat type safety. So only GHC is allowed write
cast and the
Typeable instances are part of the trusted code base, or TCB:
- The TCB should be as small as possible
- The TCB should have a small, well-defined, statically-typed API used by client code
- Client code is un-trusted; if the client code is well-typed, and the TCB is implemented correctly, nothing can go wrong
The "Dict trick"
We refer occasionally to the "Dict Trick", well known in Haskell folk lore:
data Dict (c :: Constraint) where Dict :: forall c. c => Dict c
Now a value of, say, type
Dict (Typeable a) is an ordinary value that embodies a
Typeable a dictionary. For example:
f :: Dict (Typeable a) -> Dict (Typeable b) -> a -> Maybe b f Dict Dict val = cast val
The pattern-matches against the
Dict constructor brings the
into scope, so they can be used to discharge the constraint arising from the call to