Working with type systems and communications can be very difficult. In Haskell, messages between threads are usually conveyed through channels that only accept a single type, and as a result are not very versatile. In networked systems, a stream of bytes is sent that hopefully conforms to one of many protocols including TCP, UDP, and HTTP, and hopefully both parties agree on what is sent and when. Session Types are a way to bridge the gap between these systems, as they can capture complicated protocols, and be properly type checked.

There are many ways that Session Types are notated and implemented. Scribble's notation looks more like an imperative programming language, where others are more functional, using algebraic data types and typeclasses. The notation in this post is inspired by a paper on Gradual Session Types and a paper on Multiparty Session Types.

The most basic units of Session Types are for sending and receiving data; !t represents sending a value of type t, and ?t represents receiving a value of type t. These can be concatenated by a semicolon, so a service that receives a string and responds with its length could be represented by the session type ?String; !Nat, and any client using it would be represented by !String; ?Nat.

To represent more complicated protocols we add the possiblity of branching, though it is useful to include in the notation which party is responsible for choosing the branch. For the party that is deciding on the branch we allocate the session type +{a:x,…,c:z}, where a and c are labels for the Session Types x and z. The party that is not responsible for choosing would have the corresponding session type &{a:x,…,c:z}. With this, we can encode a server that offers the client of receiving a guest page or signing in as a user with the following Session Type:

&{
  guest: !HTML,
  user: ?Username; ?Password; +{
    success: !HTML,
    fail: !Error
  }
}

The last feature of this version of session types is one that allows sessions to loop. For this we use the mu fixed point operator, which is notated as μt.a(t), where a(t) is some session type that contains t, and can be interpreted as the recursive definition t = a(t). If we wanted a user to have unlimited attempts at logging on to a system, our server could have the following Session Type:

μt. (
  ?Username;
  ?Password;
  +{
    success: !HTML,
    fail: t
  }
)

With all of these features, we can attempt to encode a HTTP 1.1 client, which can send as many requests as it wants before receiving responses:

µt. (
  !HTTPRequest;
  +{
    sendMore: t,
    wait: end
  };
  ?HTTPResponse;
  +{
    sendMore: t,
    wait: end
  }
)

Session Types have a notion of duality, where two protocols are compatible when they are duals. We define ?t to be dual to !t, &{a:x,…,c:z} to be dual to +{a:u,…,c:w} when all the choices x and u, z and w etc. are duals, and a series of concatenated session types x;…;z is dual to u;…;w when each pair of session types u and x, w and z etc. are duals. The dual of a fixpoint μt.a(t) is μs.b(s), where assuming t and s are duals implies that a(t) and b(s) are duals.

However, duality on its own does not define compatibility, since our earlier server that offered services to either a guest or a user would be compatible with a client that always chooses to be a guest, with the session type +{ guest: ?HTML }. To formalise this we define what it means for two Session Types a and b to be subtypes, notated a <: b, where the key property we want from subtypes is that if we have a <: b and c <: d and a and c are compatible, then the more general Session Types b and d should be compatible.

With this in mind, &{a:x,…,b:y} is a subtype of &{a:x,…b:y,…,c:z}, since offering extra options does not break compatibility, +{a:x,…b:y,…,c:z} is a subtype of +{a:x,…,b:y}, since choosing a subset of the available options does not break compatibility. Thus offering fewer choices is a subtype of offering more, and choosing between more choices is a subtype of choosing fewer.

To handle fixpoints, if assuming t <: s implies a(t) <: b(s), then μt.a(t) <: μs.b(s). Using this we can come up with a recursive definition of subtypes. Finally, we can define two Session Types to be compatible if one is a subtype of the other's dual.

An alternative syntax for the above operators is to replace ! with send, ? with recv, + with choose, & with offer, ; with significant whitespace, and μ with rec. Therefore the previous HTTP example would be like:

rec t (
  send HTTPRequest
  choose {
    sendMore: t,
    wait: end
  }
  recv HTTPResponse
  choose {
    sendMore: t,
    wait: end
  }
)

Most uses of Session Types are in allowing more complex communication within a strongly typed language, however at Matrix AI we are hoping to apply them to distributed systems. We will use Session Types to describe network protocols, allowing us to check which parts of a distributed system can communicate, to type check the construction of network combinators, and to analyse the behaviour of networked systems.