Well Quite!


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

A Tutorial for Session Types, Part 2

This is the second part of this multi-part tutorial in which I hope to explain quite how my Session Types implementation can be used.

Contents

Implementing Session Types

So now that you know how to make Session Types, you probably want to implement them, by which I mean write a function or two which actually behaves and obeys the Session Type.

As you might expect, this is done monadically, but there's a problem in that Haskell's standard Monad class is not as parameterised as I need. So therefore I've my own extended, or Super Monad (SMonad) class which does what I need.

class SMonad (m :: * -> * -> * -> *) where
    (~>>)   :: m x y a ->       m y z b  -> m x z b
    (~>>=)  :: m x y a -> (a -> m y z b) -> m x z b
    sreturn :: a -> m x x a

infixl 1 ~>>
infixl 1 ~>>=

It is in instances of this SMonad class that you will be working all the time. Treat (~>>) like (>>), (~>>=) like (>>=) and sreturn like return and you'll be just fine. Unfortunately, current restrictions in GHC means that I can't redefine things in such a way that I could then use do syntax with this lot, which is a great shame.

Also, you might be interested to know that we are always ultimately in IO and there's a suitable lift which allows general IO to be used:

class (SMonad m) => SMonadIO m where
    sliftIO :: IO a -> m x x a

In general, try sticking an S or s onto the front of things and it may be that I've already defined an equivalent!

The Five Functions

The key to understanding these is that there is a current channel which is held by the SMonad you're in and it's on that channel that you're working. Therefore, none of the following take as a parameter a channel (though we'll see later that in a high abstraction it becomes necessary).

ssend

Send down the current channel the supplied value. The value must be of the correct type: i.e. its type must be the same as the type indicated at this point in the Session Type of the current channel. Also, the current channel must have the next operation as Send. This is an asynchronous operation: the other party need not receive the value before you can continue.

So if the current channel had a Session Type that looked like SendInt ~> SendBool then you could implement that with ssend 5 ~>> ssend False.

srecv

Receive a value from the current channel. The type of the value received is specified by the Session Type of the current channel. Also the Session Type of the current channel must have the next operation as Recv.

So if the current channel had a Session Type that looked like RecvInt ~> RecvInt ~> SendBool then you could implement that with srecv ~>>= \x -> srecv ~>>= \y -> ssend (x == y)

sjump

Follow a jump. This may become implicit in the future, but for the time being this is necessary. Whereever you have a jump num in the Session Type, you implement it just using sjump. Note that the target is taken directly from the Session Type - there's never a choice of where you're jumping to, so sjump does not take any arguments.

So if you have a Session Type like:

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

Then you could implement it with ssend 5 ~>> sjump ~>> srecv ~>>= sliftIO . print

soffer

This implements the offer side of a branching structure, and you should think of this as continuation passing: you pass to soffer a list of implementations, where each implementation in the list corresponds to the Session Type of each branch, in the right order. So, if you have a Session Type of:

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

Then you could implement it with:

 f = soffer ( ( ssend 5 ~>> sjump ~>> f )
              ~||~
              ( srecv ~>>= sliftIO . print )
              ~||~
              OfferImplsNil
            )

Note that (~|~) is for the Session Type and (~||~) is for the implementation. Also note that OfferImplsNil is not the same as nil. Sorry!

Also note that this shows a loop and the implementation of a loop - you just perform the sjump as necessary and then recurse directly. It's really pretty natural, no magic is involved.

Now obviously, you're passing in a list of continuations which will take care of the rest of the Session Type on this channel. That means that they must all agree on certain things, like the result type: all the continuations must return a value of the same type for (~||~) to be happy. This is simply exactly the same as, for example, the two branches on a normal if statement. There's really nothing surprising here.

sselect
This is the dual of soffer. Where soffer took a list of continuations, sselect simply takes the label of the branch that you want to take. Now please remember that the labels are always numbered from D0 E upwards, and are completely disjoint from the indexes specified in a branching structure.

Putting it all together

At the end of the first tutorial, I showed you the Session Type for a calculator. Well now I can show you the implementations of both sides as well:

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

calculatorServer = soffer ( bin (+)
                            ~||~
                            bin (-)
                            ~||~
                            bin (*)
                            ~||~
                            (srecv ~>>=
                             ssend . negate ~>> sjump ~>> calculatorServer)
                            ~||~
                            sreturn ()
                            ~||~
                            OfferImplsNil
                          )
    where
      bin f = (srecv ~>>= \x ->
               srecv ~>>= \y ->
               ssend (f x y) ~>> sjump ~>> calculatorServer)

calculatorClient = sliftIO doMenu ~>>= id
    where
      doMenu = do { putStrLn "Menu:\n1. Add\n2. Subtract\n3. Multiply\n4. Negate\n5. Quit\nEnter your choice:"
                  ; l <- hGetLine stdin
                  ; case read l of
                      1 -> return $ sselect (D0 E) ~>> two
                      2 -> return $ sselect (D1 E) ~>> two
                      3 -> return $ sselect (D2 E) ~>> two
                      4 -> return $ sselect (D3 E) ~>> one
                      5 -> return $ sselect (D4 E)
                      _ -> doMenu
                  }
      fetchInt :: IO Int
      fetchInt = do { putStrLn "Enter an Int"
                    ; l <- hGetLine stdin
                    ; return . read $ l
                    }
      two = sliftIO fetchInt ~>>=
            ssend ~>> one
      one = sliftIO fetchInt ~>>=
            ssend ~>> srecvLog ~>> sjump ~>> sliftIO doMenu ~>>=
            id
                   
testCalculator = run calculatorSpec (D0 E) calculatorServer calculatorClient

Hopefully, the only thing I've not yet explained is run. run is the simplest way of running a pair of implementations. It takes the Session Type of the channel from the point of view of the first implemention (calculatorServer here), the index into the Session Type where we want to start, and the two implementations. It calculates the dual of the Session Type, checks that the implementations implement the Session Type and its dual correctly, and starts a thread for each implementation. It blocks until they both end, finally returning the results of each implementation in a tuple.

Coming Next

Now the limitation with run is that it always creates two new threads, and currently there is no way for a single thread to have more than one channel on the go at the same time. Sure, an implementation could itself call run but it can't interleave actions on different channels. Well all of that can be done, and more. See Part 3 of this tutorial for the details.

To Part 1; To Part 3