An updated tutorial for Session Types, Part 3
This is the third part of this multi-part tutorial in which I hope to explain quite how my Session Types implementation can be used.
Contents
- Part 1: Making Session Types
- Part 2: Using Session Types
- Part 3: Advanced Functionality; you are here!
Pids, forking, creating channels and multi-receive
It's pretty limiting if all you can do is create new threads to run implementations of single (or perfectly nested) Session Types. It really won't be very long before you want a single thread that's able to handle a number of channels and interleave actions across them. Furthermore, you really want to be able to communicate Pids or Process IDs and then use a Pid to create a new channel between you and that Pid. Additionally, once you've got a set of open channels, you really want some kind of receive construct that is capable taking a subset of those channels and blocking until one of them has some value ready for you to receive, thus allowing you to respond to the first available channel. Finally, it is also a pretty common requirement to be able to pass channels over channels, being able to delegate a channel to a particular party.
All of these features are catered for and these are the subject of this installment.
Pids
A Pid contains a number of pieces of information about another process. Firstly it contains a unique ID. If you're at all familiar with Erlang, then the IDs will be at least slightly familiar to you. However, the actual ID is of very little use so I'll move on. The main piece of information that a Pid contains is a list of all the Session Types that the process indicated by the Pid is prepared to take part in. Now sadly, this is not a perfect piece of information, as the list can change dynamically (it can shrink), for the following reasons.
If you have the Pid of another process, you don't really know what that process is up to. You may have some information about it, but its true state is dependent on many things, for example, the scheduler. It may actually be that that process has already died, or it may be that it's been created but not yet run at all, you really don't know, and there's no way for that process to change the type of the Pid you hold in order to make you more aware.
Thus the list of Session Types that the Pid contains is the biggest that the list could be. I.e. it's the list of Session Types that the process is aware of at the point at which the process is created. It may well be that if you try to create a channel with that process that it will never answer your call as it's already gone down some path which prevents it from ever agreeing to your request. But if you try to create a channel to a process, then you can only do so if that process knows about the Session Type you're trying to use for the new channel. So you get some guarantees, but certainly further analysis beyond what I can do with GHC is necessary to give stronger guarantees.
Finally, note that every Pid uses the same Session Type - there is simply one large Session Type which is propagated everywhere. What actually varies are the labels to the fragments that a Pid is prepared to start a channel at. We'll come back to Pids in little while.
Interleaving
Before we get as far as throwing Pids about and creating new channels to existing Pids, let me show you how to interleave actions on channels. Put simply, you have an SMonad wrapping around a list of SMonads. Then you choose which inner SMonad (i.e. channel) you want to work on and do so. So how do you build this list?
fork takes four arguments:
- The label of the fragment within the Session Type that you want
the channel to start at. Recall that
runat the end of tutorial 2 took a label to the fragment to start at, well it's all the same idea as that. - To dual or not to dual. Are you going to implement the
fragment as it's defined (and thus the child will implement the dual),
or are you going to implement the dual and the child will implement
the fragment as defined? Use
dualif you're going to implement the dual andnotDualif you're going to implement as written. - The fragment list. The child has a Pid. That Pid must contain some
sort of list of Session Types that the Pid is willing to take part in
(or as is actually the case, a list of labels into the
Session Type). If a given label isn't in this list then the child
cannot create a channel starting at that label. Note that this is
solely for the use of
createSession, covered below, and not for the use offork. Also, the labels are actually tuples containing the fragment anddualornotDualto indicate whether the Pid is willing to deal with the fragment as written, or the dual of the fragment. - The child implementation. This is the function which will be run in a new thread. It receives two arguments: firstly the channel to its parent and secondly the Pid of its parent.
fork returns to you a tuple containing the channel to
the child and the Pid of the child. So, let's see this in action!
test = runInterleaved nil st master
where
(st, (l1, l2))
= makeSessionType $
newLabel ~>>= \l1 ->
newLabel ~>>= \l2 ->
l1 .= send int ~>> send int ~>> recv bool ~>> end ~>>
l2 .= send bool ~>> recv bool ~>> end ~>>
sreturn (l1, l2)
where
int = undefined :: Int
bool = undefined :: Bool
childA parentCh parentPid
= (sliftIO . putStrLn $ "ChildA is alive!") ~>>
withChannel parentCh srecv ~>>= \x ->
withChannel parentCh srecv ~>>= \y ->
withChannel parentCh (ssend (x == y))
childB parentCh parentPid
= (sliftIO . putStrLn $ "ChildB is alive!") ~>>
withChannel parentCh (ssend True ~>>
srecv ~>>=
sliftIO . putStrLn . (++) "ChildB received a Bool: " . show
)
master
= fork l1 notDual nil childA ~>>= \(aCh, aPid) ->
fork l2 dual nil childB ~>>= \(bCh, bPid) ->
withChannel aCh (ssend 5) ~>>
withChannel bCh srecv ~>>= \boolB ->
(if boolB
then withChannel aCh (ssend 6 ~>> srecv)
else withChannel aCh (ssend 5 ~>> srecv)
) ~>>= \boolA ->
withChannel bCh (ssend (boolA && boolB)) ~>>
(sliftIO . putStrLn $ "Master has finished. Bye bye.")
This demonstrates all of the above. Firstly we have the Session
Type itself, st, which uses two labels, l1
and l2 and exposes them both through
sreturn. We have definitions for two children, and we
have the definition of the master, or root process. Finally, we have
test which runs the whole thing. In a very similar way to
fork, runInterleaved takes a list of (index,
dual) tuples which sets the list of fragments in the Pid of the root
process. This explains what the nil is doing there. It
also takes the Session Type for the entire tree of processes and the
function that is the root process.
master starts by creating two children. Note that for
childA, master states that
master will do the fragment labelled by l1
as written which means childA will do the dual. However,
for childB, master states that it will do
the dual of the fragment labelled by l2, thus
childB must do the fragment as written.
master then just continues to use the two channels to
the two children, interleaving actions through the use of
withChannel. Note that both inside and outside
withChannel we're in SMonad instances
(though different ones), so the combinators are the same, and
sliftIO (and the rest) all work as expected.
childA starts up receiving the channel to the parent
(parameterised by the dual of the fragment labelled by
l1) and the Pid of its parent and then does some
work. Note that childA could have been written as:
withChannel parentCh (srecv ~>>= \x -> srecv ~>>=
\y -> ssend (x == y)) - it makes no difference at all.
childB similarly makes use of its channel to the
parent.
So hopefully, it should be clear how interleaving works and you're getting more comfortable with the idea that there is one global Session Type and it's referred to by the labels exposed by the session type and a weird sort of boolean value indicating whether you're working on the fragment as written or its dual. This still has limitations though, in particular, how can you send Pids around and use them to create new channels? Without this, all you can do is create trees of processes where communications can only flow up and down the trees.
Working with Pids
Sadly, Pids are a little bit of a special case. When specifying
sending or receiving a Pid in a Session Type you can't just use
send or recv. If you do (and you manage to
get the type of the Pid right!), you'll get GHC exploding with an
infinite type problem. So, there are a couple of "special" functions
for specifying the communication of Pids: sendPid and
recvPid. Note that this only exists when specifying
Session Types - in the implementation you use ssend and
srecv as normal.
By now you've probably been able to predict that
sendPid and recvPid are going to take lists
of (label, dual) tuples. You're right. So, we could specify a Session
Type as follows:
(st, _) = makeSessionType $
newLabel ~>>= \l1 ->
newLabel ~>>= \l2 ->
l1 .= sendPid (cons (l2, notDual) nil) ~>> end ~>>
l2 .= send int ~>> end
where
int = undefined :: Int
Thus the fragment at label l1 says that a Pid must be
sent, and that the process identified by that Pid may be willing to
take part in a channel parameterised by the fragment at label
l2 as written. Which means that if you receive that Pid,
you may use it to try and create a channel where you are using the
dual of the fragment at l2: i.e. recv int ~>>
end.
You may be wondering why we can't just use normal Haskell lists to
specify the parameters to the Pid. The problem is that we need the
type of the parameters to reflect the value which means we actually
need a heterogeneous list. This then requires that we use our own
constructs for the list - cons and nil
rather than the normal (:) and []
constructors.
So let's implement this session type:
test = runInterleaved (cons (l2, dual) nil) st master
where
(st, (l1, l2))
= makeSessionType $
newLabel ~>>= \l1 ->
newLabel ~>>= \l2 ->
l1 .= sendPid (cons (l2, notDual) nil) ~>> end ~>>
l2 .= send int ~>> end ~>>
sreturn (l1, l2)
where
int = undefined :: Int
master
= fork l1 dual (cons (l2, notDual) nil) child ~>>= \(childCh, childPid) ->
withChannel childCh srecv ~>>= \childPid' ->
createSession l2 dual childPid' ~>>= \chA ->
createSession l2 dual childPid ~>>= \chB ->
withChannel chA (srecv ~>>= sliftIO . putStrLn . (++) "Received on chA: " . show) ~>>
withChannel chB (srecv ~>>= sliftIO . putStrLn . (++) "Received on chB: " . show) ~>>
sreturn ()
child parentCh parentPid
= myPid ~>>= \me ->
withChannel parentCh (ssend me) ~>>
createSession l2 notDual parentPid ~>>= \chA ->
createSession l2 notDual parentPid ~>>= \chB ->
withChannel chA (ssend 10) ~>>
withChannel chB (ssend 20)
So, runInterleaved specifies that the Pid of
master will contain (l2, dual). That's
good news, because it means that master can call
createSession l2 dual somePid provided that
somePid contains (l2, notDual). Now the Pid of
child just happens to be that way inclined as you can see
from the call to fork in master.
So what actually happens here is that master forks off
child. Child then gets its own Pid (myPid is
provided for this purpose) and sends its own Pid to its parent. Note
that the call to fork says that master is
doing the dual of l1 - i.e. it will receive a Pid
parameterised by (l2, notDual) (note that the library is
very careful about making sure these dual booleans always refer to the
original Session Type as written), which is exactly what it gets. Of
course, master already has the Pid of child,
but it gets a second copy anyway. Just to prove they are both the
same, it uses each one in calls to createSession. This is
really the same idea as fork except instead of suppling a
list of fragment labels and an implementation, you just specify the
Pid. Because we know that the child will do the
(l2, notDual) side of things, the master
must do the (l2, dual) side of things which is exactly
what happens. The child mirrors the creation of the two
new channels and sends two numbers to the master which
are received and printed out.
Note that createSession is a synchronous operation. It
will block until the process indicated by the supplied Pid performs
the reciprocal call.
Also note that the ability to specify labels in the Session Type for the communication of Pids is very useful when Pids refer to each other. Consider:
(st, _) = makeSessionType $
newLabel ~>>= \l1 ->
newLabel ~>>= \l2 ->
l1 .= sendPid (cons (l2, notDual) nil) ~>> end ~>>
l2 .= sendPid (cons (l1, notDual) nil) ~>> end
I.e. the Pid that will be sent in l1 will participate
in sessions in which it will send the Pid indicated in
l2. And that Pid is prepared to participate in
sessions in which it will send the Pid indicated in
l1. And that Pid... Yes, stuff like this will
slowly break your head, and you really need to draw out what points to
what. But it is actually pretty useful.
Multi-receive
It is often the case that you have a set of channels open and the
next action on all of them is some sort of recv. You
don't know which one will be ready first, and you know that if you
block waiting on the wrong one then you can get a deadlock. So you
want a multi-receive construct which will block until any of those
channels becomes ready to srecv on.
multiReceive is just like soffer in that
it takes a list of continuations. In this case, each list element is a
tuple, where the left hand side is a channel and the right hand side
is a function. The function will be called if that channel is the
first channel to become ready. Let's see it in action:
test aDelay bDelay = runInterleaved nil st master
where
(st, l) = makeSessionType $
newLabel ~>>= \l ->
l .= send int ~>> end ~>>
sreturn l
where
int = undefined :: Int
master
= fork l dual nil (child aDelay) ~>>= \(aCh, _) ->
fork l dual nil (child bDelay) ~>>= \(bCh, _) ->
multiReceive ( (aCh, receive "A" aCh ~>> receive "B" bCh)
~|||~
(bCh, receive "B" bCh ~>> receive "A" aCh)
~|||~
MultiReceiveNil
)
receive str ch
= withChannel ch (srecv ~>>=
sliftIO . putStrLn .
(++) ("Master received from child " ++ str ++ ": ") . show)
child delay parentCh _
= (sliftIO . threadDelay $ delay) ~>>
withChannel parentCh (ssend delay)
Yes, we now have (~|||~) as well as
(~||~) and (~|~)! So master
creates two children which are both parameterised by different values,
supplied through test. They sleep for that number of
microseconds before replying. master just wants to get
the responses as quickly as possible so it uses
multiReceive. If the aCh becomes ready
first, it receives on aCh first and then on
bCh. Otherwise the other way round. So the values to
aDelay and bDelay will control the order in
which the print expressions get executed:
*Tests> test 1000000 100
Master received from child B: 100
Master received from child A: 1000000
*Tests> test 100 1000000
Master received from child A: 100
Master received from child B: 1000000
Again, every function in the list to multiReceive must
perform the same actions, just they can do it in different orders: the
state of all the channels must be the same at the end of every
function in the multiReceive list.
Higher order channels and session types
Finally, you may wish to send a channel over a channel. This would mean that if you have processes a, b and c then if a and b know about each other, and b and c know about each other then b could make a channel to a, b could make a channel to c, and then b could pass its end of the channel to a to c. Thus a and c would then be able to talk to each other even though they don't know each other's Pid.
Just like with communicating Pids, specifying higher-order session
types is a special case, and in this case, it's also a special case in
the implementation: you can't just use ssend and
srecv. To specify a higher-order session type, use
sendSession and recvSession. These take
fragments directly:
(st, _) = makeSessionType $
newLabel ~>>= \a ->
newLabel ~>>= \b ->
a .= sendSession (recv int ~>> end) ~>> end ~>>
b .= send int ~>> recv int ~>> end
where
int = undefined :: Int
Thus we know that in a, where we send a session, that
session must be the receiving of an int. The implementation is
similarly straight forward, using sendChannel and
recvChannel to implement sendSession and
recvSession respectively:
testHigherOrderSessionTypes = runInterleaved nil st master
where
(st, (a, b))
= makeSessionType $
newLabel ~>>= \a ->
newLabel ~>>= \b ->
a .= sendSession (recv int ~>> end) ~>> end ~>>
b .= send int ~>> recv int ~>> end ~>>
sreturn (a, b)
where
int = undefined :: Int
master = fork b notDual nil childA ~>>= master'
-- master' used to avoid monomorphism restriction on lambdas
master' (chA, _) = fork a notDual nil childB ~>>= \(chB, _) ->
withChannel chA (ssend 41) ~>>
sendChannel chA chB
childA chP _ = withChannel chP (srecv ~>>= ssend . (+) 1)
childB chP _ = recvChannel chP ~>>= \chA ->
withChannel chA (srecv ~>>= sliftIO . print)
Thus master creates a child running
childA and then another child running
childB. master then sends 41 to
childA and then passes that channel to
childB. Thus the two children don't know of each other,
but they're able to communicate with one another over a channel which
was originally created between childA and
master and subseqently sent to childB.
Note that having sent the channel to childB,
master cannot then make use of that channel any further -
to try to do so is a compile-time error.
Some conclusions
Hopefully, these three articles have gone some way to explaining
how to use this library. One of the problems with abusing the Haskell
type system to this extent is that the type signatures become huge:
there's a reason why there are no type signatures in these
articles. The other problem is that when you make a mistake, the error
messages are enormous and often fairly unhelpful: you're normally much
better off thinking for a few seconds about what might be wrong rather
than trying to parse a few thousand lines of error message. Having
said that, the most useful lines of such an error message will be the
first two where it will tend to say something like Expected
"Send Int", Inferred "Recv Int" which will normally make it
quite clear what is wrong.
Also, I would recommend that you always turn off the monomorphism
restriction when working with session types. It's quite common for the
library to reject code because, for example, a channel bound with a
lambda needs a polymorphic type which is forbidden by default. Thus
adding {-# LANGUAGE NoMonomorphismRestriction #-} to the
top of your code is normally required, unless you're not going to use
lambdas.
I am very keen to receive feedback. You probably already know my
email address, given this domain, and my name's Matthew, you should
hopefully be able to put the two together and contact me. Otherwise, I
tend to sit on #haskell on freenode.net. If
you have problems, thoughts, comments etc, I'd be very happy to
receive them. Many thanks.