Well Quite!

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

• Part 1: Making Session Types
• Part 2: Using Session Types; you are here!
• Part 3: Advanced Functionality

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 instance 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 higher context 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 send int ~>> send bool 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 recv int ~>> recv int ~>> send bool then you could implement that with srecv ~>>= \x -> srecv ~>>= \y -> ssend (x == y)

sjump

Follow a jump. Whereever you have a jump label 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:

 (s, _) = makeSessionType $
          newLabel ~>>= \l1 ->
          newLabel ~>>= \l2 ->
          l1 .= send int ~>> jump l2 ~>>
          l2 .= recv bool ~>>
        where
          int = undefined :: Int
          bool = undefined :: Bool

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:

 (s, _) = makeSessionType $
          newLabel ~>>= \l ->
          l .= offer ( (send int ~>> jump l)
                       ~|~
                       (recv bool ~>> end)
                       ~|~ BLNil
                     )

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 BLNil. 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. Remember that the labels are always numbered from 0 upwards, and correspond to the order in which branches are specified in the offer or select session type constructs.

In order to ensure that the label specified is valid (i.e. greater than or equal to zero and less than the number of branches specified), "normal" numbers are not used. Instead, type-level numbers are used that allow the static verification of the selection of a branch.

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. These numbers are used to select which branch is taken: the D0 Eth branch is the first branch specified in the list and so on.

The example in the following section demonstrates the use of sselect

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:

testCalculator = run calculatorSpec l calculatorServer calculatorClient
    where
      (calculatorSpec, l)
          = makeSessionType $
            newLabel ~>>= \l ->
            l .= offer ( bin l ~|~
                         bin l ~|~
                         bin l ~|~
                         uni l ~|~
                         end ~|~
                         BLNil
                       ) ~>>
            sreturn l
                where
                  int = undefined :: Int
                  bin t = recv int ~>> recv int ~>> send int ~>> jump t
                  uni t = recv int ~>> send int ~>> jump t

      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 = sjoin (sliftIO doMenu)
          where
            doMenu
                = do { putStrLn "Menu:\n 1. Add\n 2. Subtract\n 3. Multiply\n 4. Negate\n 5. Quit\n Enter your choice:"
                     ; line <- hGetLine stdin
                     ; case read line 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"
                     ; line <- hGetLine stdin
                     ; return . read $ line
                     }
            two = sliftIO fetchInt ~>>=
                  ssend ~>> one
            one = sliftIO fetchInt ~>>=
                  ssend ~>>
                  srecv ~>>= sliftIO . print ~>>
                  sjump ~>> sjoin (sliftIO doMenu)

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 label of the fragment of 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.

This then should explain why makeSessionType returns a tuple: the left hand side is the session type itself. The right hand side is available for you to use through sreturn within the session type itself - the obvious use is to allow you to expose labels which are used within the session type and associated with fragments which you then wish to use as an argument to run or, as we shall see later, other functions.

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