Well Quite!


The Rants, Raves, and Rituals of Matthew Sackman
Tuesday, March 25th, 2008

A Tutorial for Session Types, Part 1

This is the first part of this 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.

Contents

Some Notes

  • You will need at least GHC 6.8
  • This tutorial assumes Session Types version 2008.3.25. It's possible that the API will change in the future.
  • You can download Session Types version 2008.3.25.
  • 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:


 a = cons (SendInt ~> RecvBool ~> end) nil

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.

Now, immediately, you're wondering two questions:

Why is Int and Bool attacted to Send and Recv?

Fear not, you can send any type. The problem is that you're specifying a type through a value, and so you would have to use values of the type Int and Bool. So you can write, if you wish:


 a = cons (Send (0::Int) ~> Recv True ~> end) nil
except that doesn't really look very nice. You could also write: 

 a = cons (Send (undefined::Int) ~> Recv (undefined::Bool) ~> end) nil
which is better in that you don't have arbitrary values floating around. If you want to be super clear then you could write: 

 a = cons (Send int ~> Recv bool ~> end) nil
     where
       int = undefined::Int
       bool = undefined::Bool
but in order to save you unnecessary pain, I created a few special constructors which you may wish to use for the most common cases: 

data Send :: * -> * where
             Send       :: t -> Send t
             SendInt    :: Send Int
             SendBool   :: Send Bool
             SendChar   :: Send Char
             SendStr    :: Send String
             SendDouble :: Send Double

data Recv :: * -> * where
             Recv       :: t -> Recv t
             RecvInt    :: Recv Int
             RecvBool   :: Recv Bool
             RecvChar   :: Recv Char
             RecvStr    :: Recv String
             RecvDouble :: Recv Double

The other question you're asking is:

What's with the cons and nil thing?

Well, it turns out that GHC doesn't like infinite types. As a result, there is a small cost to pay when doing recursion and that is that a Session Type is actually a list of small fragments and each fragment can refer to other fragments by their index. So effectively you have the ability to point to other fragments within the same Session Type. Don't worry, this is perfectly safe: I check that you're not pointing at "illegal" addresses and so forth. But it does mean that you have to construct this list of fragments and in the simplest case, the list is one element long, hence the cons and nil.

All of which probably means you're now wondering why you can't just use the standard Haskell list type. To which the answer is that the standard Haskell list only allows values of the same type and we actually need a heterogeneous list that reflects at the type level the contents of the list.

Adding a loop


 a = cons (SendInt ~> RecvBool ~> jump (D0 E)) nil

This specifies that after sending an Int and receiving a Bool we then jump to the 0th index of this Session Type, which, as it happens is the very same fragment - i.e. we've only build a one-element list, so we can only jump to the first element of this list, aka the 0th index. We've in fact specified an infinite loop.

The type-level numbers that I've implemented are all base 10, not peano, and every constructor starts with a D and you use E to indicate the end of the number. So D5 E is 5, D1 (D5 (D2 E)) is 152. There are no D constructors greater than D9, hence the nesting.

The above Session Type is equivalent to:


 a = cons (SendInt ~> jump (D1 E)) $
     cons (RecvBool ~> jump (D0 E))
     nil

Hopefully, the list structure is a bit clearer now.

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.


 a = cons (SendInt ~> end) $
     cons (offer ( (D0 E)
                   ~|~
                   (D2 E)
                   ~|~
                   nil
                 )
          ) $
     cons (RecvBool ~> end)
     nil

So at the first index (D1 E), we have an offer construct. This basically takes a list of indexes, just use (~|~) to construct the list as it does some other things too. These indexes specify, in order, what the available branches are. So we see there are two branches, the first (or D0 Eth label) is to jump to the first fragment in our Session Type, send an Int and then stop; the second (or D1 Est label) is to jump to the third fragment (or D2 End index) in our Session Type and receive a Bool.

So the order in which the indexes appear specify the labels of the branches. Also, note that the dual of an offer is a select construct which looks exactly the same: it takes a list of indexes. 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 = cons (offer ((D1 E) ~|~      -- add
                               (D2 E) ~|~      -- subtract
                               (D3 E) ~|~      -- multiply
                               (D4 E) ~|~      -- negate
                               (D5 E) ~|~ nil) -- quit
                       ) $
                  cons (RecvInt ~> RecvInt ~> SendInt ~> jump (D0 E)) $
                  cons (RecvInt ~> RecvInt ~> SendInt ~> jump (D0 E)) $
                  cons (RecvInt ~> RecvInt ~> SendInt ~> jump (D0 E)) $
                  cons (RecvInt ~> SendInt ~> jump (D0 E)) $
                  cons end nil

Of course, you're probably wondering why is the same line repeated three different times? Well, you actually don't have to: the important thing is the number of labels and the fact that we will (in the implementation) attach different behaviours to each label. The following is actually exactly equivalent to the above Session Type:

 calculatorSpec = cons (offer ((D1 E) ~|~      -- add
                               (D1 E) ~|~      -- subtract
                               (D1 E) ~|~      -- multiply
                               (D2 E) ~|~      -- negate
                               (D3 E) ~|~ nil) -- quit
                       ) $
                  cons (RecvInt ~> RecvInt ~> SendInt ~> jump (D0 E)) $
                  cons (RecvInt ~> SendInt ~> jump (D0 E)) $
                  cons end nil

So we still have different labels for the add, subtract and multiply branch, it's just that now they all point to the same fragment, where as before they pointed to different fragments, it's just that those fragments turned out to be the same.

To Part 2