Session Types and the Shape of a Channel Protocol

A channel’s type says what it carries. It does not say who sends first, how many messages the exchange comprises, or what the other end is allowed to do next. Those are protocol properties, and they live in documentation, in comments, and in the reader’s memory, which is why a mismatch between two ends of a channel is usually discovered at runtime, as a hang or a parse error, rather than at compile time.

Session types put the protocol in the type. A channel’s type is a sequence of interactions, and the two ends have dual types: whatever one side offers to send, the other side must be prepared to receive, in the same order. Checking a program against this discipline is a type-checking problem, and the guarantee obtained is that a well-typed pair of processes cannot deadlock on protocol mismatch.

The grammar of a protocol

A session type is built from a small set of constructors. The essential ones are: send a value of type T then continue as S; receive a value of type T then continue as S; offer a choice of branches, each labelled and each with its own continuation; and end.

The choice constructor is what makes protocols more than sequences. A server that can respond either with a result or with an error offers two labels; the client must handle both. In the typed presentation, the offer is a single type with a set of labelled continuations, and the client’s type is dual: a selection, where the client chooses one label and continues accordingly. Duality is defined structurally: send dualises to receive, offer dualises to select, end dualises to end.

The resulting types are trees, and the interesting ones are recursive. A protocol for a request-response server is a recursive type whose body is “receive a request, send a response, loop”. A client that sends two requests has the type obtained by unrolling the recursion twice, and the type system’s job is to check that the two ends’ unfoldings match at every step.

-- Pseudo-code for the type syntax above, not Haskell as the compiler accepts
-- it: data type declarations need constructors, and these operations only work
-- in a library that tracks the session in the type.
type Add = Recv Int (Recv Int (Send Int End))

server :: Channel Add -> IO ()
server c = do
  (x, c1) <- recv c          -- each step consumes the handle
  (y, c2) <- recv c1
  send c2 (x + y)            -- the final send ends the session

The essential detail is that the channel is used linearly: each operation consumes the handle it is given and yields a new handle whose type is the continuation. Using the same handle twice, or dropping one without reaching the end of its type, is a type error. This is what makes the protocol enforceable: a channel whose type changes with each interaction cannot be aliased, because two aliases would permit two different continuations.

Linearity is the load-bearing restriction

Session types rest on linear or affine typing of the channel handle. Linear means used exactly once; affine means used at most once. Without either, a program could duplicate a channel and send two conflicting messages, and the protocol would be unenforceable no matter how expressive the type grammar.

Implementations differ in how they reconcile linearity with a language that is not linear. A common approach is to encode the channel state in the type index and require that the old handle be consumed, so the type checker sees a single-use discipline without a general linear type system. Another is to move the session into a monad whose sequencing enforces order. A third, used in object-oriented encodings, represents the channel as an object whose methods return the continuation, so the protocol is a chain of method calls and linearity is approximated by the object’s type changing at each step.

The cost of linearity is that a channel cannot be shared. If two threads need to talk to the same server, they need two channels, and the server’s type must describe how it interleaves them, which is where the theory becomes harder. Multiparty session types address this by giving each participant a projected view of a global protocol, and the projection is what turns one global description into per-endpoint types. The global protocol is written once, and each endpoint’s type is derived from it by projection; a well-formed global protocol yields endpoint types that are guaranteed to be compatible.

What checking buys and what it does not

The guarantee is progress for well-typed processes under certain conditions: a well-typed pair cannot reach a state where one side is waiting to receive and the other is waiting to send something different. This is a real and non-trivial property. It is not the same as deadlock freedom in general: a process that talks over two sessions can send on one while the other end waits to send on the second, and unless the typing rules track the order in which sessions are used, the type system checks each session in isolation and accepts the pair.

Nor does it cover the value level. A session type can say “receive an integer”; it cannot say “receive a positive integer” unless the type system supports refinement. A protocol mismatch in the payload’s meaning, such as a client sending a user ID where the server expects an order ID, is invisible to the session type if both are integers.

The practical benefit is therefore narrower than “correct concurrency” and wider than “documentation”. It eliminates an entire class of bug: the one where two ends disagree about the sequence of interactions. That class includes most protocol deadlocks, most “unexpected message” errors, and most cases of a client that reads a response before sending a request.

Projection from a global protocol

Writing endpoint types by hand does not scale past two participants, because the endpoints are not independent: each one’s type must be the dual of the others’ at every step. Multiparty session types invert the construction. A global protocol is written once, in a notation that names the participants and the messages between them, and each participant’s local type is obtained by projection: keep the interactions that name this participant, drop the rest, and merge the points where the participant is not involved.

Projection is not always defined. If a global protocol lets participant A choose between two branches and the choice is invisible to B, B’s projected type has the same behaviour on both branches, and merging them is sound. If the choice changes what B is asked to do, the projection of B has a choice it did not make, and the protocol is not well-formed for B. The standard restriction is that every choice must be communicated to every participant whose subsequent behaviour depends on it, which is a syntactic condition on the global protocol rather than a proof obligation on the endpoints.

The payoff is that a well-formed global protocol yields endpoint types that are compatible by construction, so the compatibility check is done once on the protocol rather than pairwise on the endpoints. For protocols with more than three participants, that is the difference between a quadratic number of checks and one.

Sessions and the rest of the model

Session types describe a channel’s protocol, so they sit naturally on top of the CSP-style channel, where a send and receive are matched events, with the rendezvous semantics described in Rendezvous and Buffering in CSP-Style Channels. They are less natural on an actor mailbox, because a mailbox is untyped and unordered across senders; encoding a session in an actor system requires a private channel per conversation, which is exactly what most actor libraries provide as a “reply address”.

The interaction with cancellation is where the theory is thinnest. A session type describes a completed protocol; it does not describe what happens if one side is dropped halfway. Extending sessions with cancellation means adding an abort construct at specific points and typing the abort’s effect on the other end, which is the same distinction between safe and unsafe cancellation points that runtime APIs document informally; see Cooperative Cancellation and the Cancel-Safety Contract. Some calculi do this; mainstream languages do not.

The remaining gap is the one that keeps session types out of everyday use: the types are verbose, they change at every step, and they interact badly with the imperative style of most code. A protocol with ten steps produces a type with ten nested constructors, and an error message about a mismatch points at a position in that type rather than at the line of code that got the order wrong. The techniques that make this tolerable, such as inference, abbreviated type names, and editor support that renders the protocol as a sequence diagram, are engineering problems rather than theoretical ones, and they are the reason the idea has spread slowly despite a clear guarantee.