Introduction to typed-session

#1

Introduction to typed-session

Typed session are used to ensure desirable properties in concurrent and distributed systems, i.e. absence of communication errors or deadlocks, and protocol conformance.

It was previously called typed-communication-protocol, and is now renamed typed-session.

Origin of typed-protocols

typed-Sesstion was inspired by typed-protocols.

typed-protocols describes itself as: A robust session type framework which supports protocol pipelining.

Duncan Coutts and Marcin Szamotulski have introduced it in many public speeches.

typed-protocols-public-content
typed-protocols-public-content1123×658 38.4 KB

I have introduced it before, but it was called Mini Protocols at that time.

typed-protocols is used extensively in their project.

proj
proj1444×838 65.5 KB

files-protocols
files-protocols1558×874 64.6 KB

Each folder here represents a protocol.

Detailed introduction to typed-protocols

The core idea of ​​typed-protocols is to regard the communication process as a state machine, and each communication will change the state of the state machine.

Here is a simple PingPong communication as an example:

Here is a client and a server. At the beginning, the client is ready to send a message and the server is ready to receive a message. If the client sends MsgPing, the server will reply MsgPong after receiving the message, and then continue to wait for the client to send a message, and the client should continue to send messages. If the client sends MsgDone, the server will end directly after receiving the message. The client should also end directly after sending MsgDone, and should not send any more messages to the server.

This is a schematic diagram:

1.
client   --- MsgPing ---> server
client   <-- MsgPong ---- server

2.
client   --> MsgDone ---> server

So how to solve this problem with the typed-protocols framework?

We must first know what the goal of typed-protocols is. Its goal is: static checking. For the client and the server, communication only requires two behaviors: sending messages and receiving messages. However, the receiving and sending of messages are semantically related. Take PingPong as an example. If the client sends a MsgPing message at the beginning, the next behavior of the client must be to wait for the MsgPong message returned by the server. The client cannot send MsgPing, and then send MsgPing again without receiving MsgPong. This is a logical error in the programming.
For example, the client continues to send MsgPing after sending MsgDone, which is also a logical error.
The purpose of the typed-protocols framework is to statically check whether such logical errors have occurred and reject such programs at compile time. In this way, the type system ensures the correctness of the communication logic of the code you write.

So how does typed-protocols do this?

  1. Encode the communication protocol into the type
  2. Track the changes in the state type in the communication behavior of the client and server

The change of state here is the state machine idea mentioned above.

Take PingPong as an example, after adding the state to the communication, the following is shown:


1.

StIdle                    StIdle

client   --- MsgPing ---> server

StBusy                    StBusy

client   <-- MsgPong ---- server

StIdle                    StIdle


2.
StIdle                    StIdle

client   --- MsgDone ---> server

StDone                    StDone

Three states StIdle, StBusy, StDone are added here. They have no real meaning. They are just used to indicate the change of state. Every message will cause the state to change, which is the meaning of the state machine.

The actual code is as follows:


-- Define the required state
data PingPong where
  StIdle :: PingPong
  StBusy :: PingPong
  StDone :: PingPong

instance Protocol PingPong where

-- Define messages. Note that each message will cause a state change, implemented through GADT
  data Message PingPong from to where
    MsgPing :: Message PingPong StIdle StBusy
    MsgPong :: Message PingPong StBusy StIdle
    MsgDone :: Message PingPong StIdle StDone

  -- Defines that the client can send messages when it is in the StIdle state
  data ClientHasAgency st where
    TokIdle :: ClientHasAgency StIdle

  -- The defined server can send messages when it is in the StBusy state
  data ServerHasAgency st where
    TokBusy :: ServerHasAgency StBusy

  -- Define client, server stops when it is in StDone state
  data NobodyHasAgency st where
    TokDone :: NobodyHasAgency StDone

The above code encodes the PingPong communication protocol described above into the type.

Step 1, encode the communication protocol into the type.

Before starting step 2, I would like to talk about a way of thinking about solving problems in Haskell: problem → build AST → explain AST.

This idea of ​​solving problems is:

  1. Simplify the core of the problem into the corresponding AST data structure

  2. Convert the problem into building AST

  3. Explain AST to solve the problem

There are many benefits to doing this, here are two simple descriptions:

  1. Problem → Build AST In this process, Haskell’s type system can be used to statically check whether the built code meets the semantic requirements, which is what typed-protocotls does. An exception is fir: Write GPU shaders in Haskell and use the Haskell type system to prevent runtime errors.

  2. Build AST → Explain AST In this process, the AST can be optimized or simplified, and more explanations are provided.

The behavior of the do syntax in Haskell is similar to the above idea. The AST is constructed through the do syntax and then interpreted or executed.

So how to solve the problem of client and server communication in typed-protocols?

It defines an AST data structure: data Peer ps (pr :: PeerRole) (st :: ps) m a

data Peer ps (pr :: PeerRole) (st :: ps) m a where

  Effect :: m (Peer ps pr st m a)
         ->    Peer ps pr st m a

  Done   :: !(NobodyHasAgency st)
         -> a
         -> Peer ps pr st m a

  Yield  :: !(WeHaveAgency pr st)
         -> Message ps st st'
         -> Peer ps pr st' m a
         -> Peer ps pr st  m a

  Await  :: !(TheyHaveAgency pr st)
         -> (forall st'. Message ps st st' -> Peer ps pr st' m a)
         -> Peer ps pr st m a

The core behaviors required for communication are defined here: Yield (send message), Await (receive message), Done (end of communication).
Peer tracks state changes in type.

Here is an example of PingPong behavior:

client :: Peer PingPong AsClient StIdle m ()
client =
    Yield (ClientAgency TokIdle) MsgPing $
    Await (ServerAgency TokBusy) $ \MsgPong -> 
        Yield (ClientAgency TokIdle) MsgDone (Done TokDone ())

serverPeer
  :: Peer PingPong AsServer StIdle m ()
serverPeer =
    Await (ClientAgency TokIdle) $ \req ->
    case req of
      MsgDone -> Done TokDone ()
      MsgPing -> Yield (ServerAgency TokBusy) MsgPong serverPeer

This is really building an AST! In actual use, it is very troublesome to write it like this. In reality, they will add another layer outside of this. And then explain this layer to the peer.

data PingPongClient m a where
  SendMsgPing    :: m (PingPongClient m a)
                 -> PingPongClient m a
  SendMsgDone    :: a -> PingPongClient m a

pingPongClientPeer
  :: Monad m
  => PingPongClient m a
  -> Peer PingPong AsClient StIdle m a

pingPongClientPeer (SendMsgDone result) =
    Yield (ClientAgency TokIdle) MsgDone (Done TokDone result)

pingPongClientPeer (SendMsgPing next) =

    Yield (ClientAgency TokIdle) MsgPing $

    Await (ServerAgency TokBusy) $ \MsgPong ->

      Effect $ do
        client <- next
        pure $ pingPongClientPeer client

The example above shows: In actual use, PingPongClient is constructed because it can be more conveniently constructed using do syntax.

My core improvement to typed-protocols comes from this: I found that Await behaves very much like Mcrbide Indexed Monad, so the behavior of Peer is a Mcbride Indexed Monad, which can be described using do syntax. Therefore, the above middle layer is no longer needed. This is my proposed improvement to typed-protocols.

In this way, we can use QualifiedDo syntax to write the above example like this:

client :: Peer PingPong AsClient StIdle m ()
client = I.do
    Yield (ClientAgency TokIdle) MsgPing
    MsgPong <- Await (ServerAgency TokBusy)  
    Yield (ClientAgency TokIdle) MsgDone 
    Done TokDone ()

serverPeer
  :: Peer PingPong AsServer StIdle m ()
serverPeer = I.do
    req <- Await (ClientAgency TokIdle)
    case req of
      MsgDone -> Done TokDone ()
      MsgPing -> I.do 
        Yield (ServerAgency TokBusy) MsgPong 
        serverPeer

Next, let’s explain AST. The runPeerWithDriver function is used to explain Peer, so I won’t explain this function in detail here.
typed-protocols contains a lot of content, such as codec, pipelined, proofs, test, etc. If anyone is interested, I can write more.

After a brief introduction to typed-protocols, we finally get to typed-session.

The core differences between typed-session and typed-protocols are as follows:

  1. typed-session is based on the Mcbride Index Moand and supports do syntax
  2. typed-session allows multi-role communication instead of just client-server communication
  3. typed-session does not support pipelined

In the next article, I will introduce typed-session in detail.

10 Likes