An updated tutorial for Session Types, Part 1
This is the first part of this updated multi-part tutorial in which
I hope to explain quite how my Session Types implementation can be
used. Note that I'm not trying to explain how it works, just how to
use it. However, if you would like a warm fuzzy feeling inside then
you'll be pleased to know that I don't use unsafeCoerce
or unsafePerformIO anywhere.
This tutorial is an updated version of an old tutorial which covered a previous version of my session types library (and was valid for use up to sessions version 2008.4.2). However, since version 2008.5.2, the way in which session types are described has changed significantly and so this tutorial has been rewritten. Some parts are the same, but there are new parts for new features, such as higher-order channels/session-types.
Contents
- Part 1: Making Session Types; you are here!
- Part 2: Using Session Types
- Part 3: Advanced Functionality
Some Notes
- You will need at least GHC 6.8
- This tutorial assumes Session Types version 2008.5.6. It's possible that the API will change in the future, and it certainly has changed in the past!
- You can download Session Types version 2008.5.6.
- It's also available via Hackage.
- Sometimes the type checking can take a long time. Do not be afraid of this. If GHC seems to be taking ages to type check, go and make a cup of tea, research parallel type checking, over-clock your CPU or just buy a faster computer.
import Control.Concurrent.Session
What is a Session Type?
For the purposes of these tutorials, a Session Type is a specification that dictates how two parties should communicate with each other over a given channel. So we have a notion of a channel which is the medium through which two parties (and only two parties) communicate, and we have the idea that a channel is parameterised by a Session Type.
The Session Type specifies who talks when and the types of the values exchanged. Session Types can contain branching and looping structures. Session Types are completely statically known: they can not be altered dynamically. However, as they support branching and arbitrary recursion, this doesn't reduce their expressivity.
Because two different parties see different ends of the same
channel, they also see different Session Types. To be precise, they
each see the dual of the Session Type that the other party
sees. For example, where party A sees the requirement to
send an Int, party B will see the
requirement to receive an Int. Dual is
a self-inverse relation.
A Very Simple Session Type
These should compile and work:
(s, _) = makeSessionType $
newLabel ~>>= \l ->
l .= send int ~>> recv bool ~>> end
where
int = undefined :: Int
bool = undefined :: Bool
This specifies a Session Type a which requires that a party sends
an Int down a channel, and then receives a
Bool from the same channel before stopping. The
other party, seeing the other end of the same channel, will
have to do the dual: i.e. receive an Int and then send a
Bool. So sends and receives are transposed, as are two
other operactions, select and offer which I shall
cover shortly.
If you're familiar with previous versions of this library then you will probably have noticed a major change in the way session types are defined.
Now, immediately, you're wondering two questions:
- What are these weird
~>>and~>>=functions? The simple answer is that they're just the same as
>>and>>=which we all know and love, except they're a bit different. I actually cover the details of these later, but for now just treat them as if they're normal monadic functions.- What's this
newLabelthing? Well, a session type is actually a collection of fragments and in order to permit recursion, these fragments must be able to refer to each other. So that means that you have to declare the name of a fragment before using it, and that's exactly what the
newLabelfunction does: it produces a new label which we can then attach to a session type fragment, naming the fragment and giving us a means to refer to that fragment.
Adding a loop
(s, _) = makeSessionType $
newLabel ~>>= \l ->
l .= send int ~>> recv bool ~>> jump l
where
int = undefined :: Int
bool = undefined :: Bool
This specifies that after sending an Int and receiving
a Bool we then jump to the fragment identified by the
label l. That label is in fact the only label we're
using, and is attached to the fragment we're within through use of the
(.=) infix function. We've in fact specified an infinite
loop.
The above Session Type is equivalent to:
(s, _) = makeSessionType $
newLabel ~>>= \l1 ->
newLabel ~>>= \l2 ->
l1 .= send int ~>> jump l2 ~>>
l2 .= recv bool ~>> jump l1
where
int = undefined :: Int
bool = undefined :: Bool
Hopefully, you can now see more clearly how and why labels are defined, attached to fragments and used to refer to different fragments.
Branching
Okay, so loops are fun, but it's normally a good idea to be able to exit the loop, and this requires the branching construct. In Session Types, the two sides of the branching construct are called offer and select. The offer side says "Here are your available paths, I've implemented them all, just let me know which path you want me to take and I'll be happy to play along.". The select side says "I'm going to select which branch we're going to take." So it's not a non-deterministic choice. One side (the select side) can dynamically choose which branch to take, but all the branches have to be pre-defined, and the offer side has to be prepared to take any of the specified branches. An example should help.
(s, _) = makeSessionType $
newLabel ~>>= \l ->
l .= offer ( ( send int ~>> end )
~|~
( recv bool ~>> end )
~|~ BLNil
)
where
int = undefined :: Int
bool = undefined :: Bool
So the fragment identified with the label l uses the
offer construct. This basically takes a list of
fragments, just use (~|~) to construct the list as it
does some other things too. These fragments specify the session type
for each of the branches. So we see there are two branches, the first
(or zeroth label) is to send an Int
and then stop; the second (or firstst label) is
to jump to receive a Bool.
Also, note that the dual of an offer is a
select construct which looks exactly the same: it takes a
list of fragments. It's only at runtime, when you're actually
implementing a select that you dynamically pick
which label you wish to take.
Moving On
So that's how you specify Session Types. They don't actually do anything, they are just types which will parameterise channels between different parties. In the second part I shall show you how to actually implement a Session Type so that we can see it working. For the time being I shall leave you with the Session Type for the classic calculator.
(calculatorSpec, a)
= makeSessionType $
newLabel ~>>= \a ->
a .= offer ( bin a ~|~ -- add
bin a ~|~ -- subtract
bin a ~|~ -- multiply
uni a ~|~ -- negate
end ~|~ -- quit
BLNil
) ~>>
sreturn a
where
int = undefined :: Int
bin t = recv int ~>> recv int ~>> send int ~>> jump t
uni t = recv int ~>> send int ~>> jump t