Session Types

Core Idea

Session types are a type discipline for communication-centric programs that assigns types to communication channels, specifying the sequence, direction, and payload types of messages exchanged between processes. A session type like !Int.?Bool.end describes a channel that first sends an integer, then receives a Boolean, then closes. The type system statically guarantees that communicating processes follow their protocols: messages are sent and received in the correct order with the correct types, and every session is properly completed. Violations — sending when the protocol expects receiving, sending the wrong type, or abandoning a session — are caught at compile time.

Explainer

Concurrent and distributed programs communicate by sending messages over channels. A pervasive source of bugs is protocol violations: a process sends a message when the other side expects silence, sends data of the wrong type, or closes a connection before the protocol is complete. Testing catches some of these, but the combinatorial space of interleavings makes thorough testing nearly impossible. Session types bring the power of static type checking to communication protocols, catching protocol violations at compile time.

A session type describes the communication behavior of a channel endpoint as a sequence of operations. !T means "send a value of type T." ?T means "receive a value of type T." The dot . sequences operations: `!Int.?Bool.end` means "send an Int, then receive a Bool, then close." Branching (&{label1: S1, label2: S2}) offers a choice to the other process, and selection (choose{label1: S1, label2: S2}) makes a choice. Recursion (rec X. !Int.X) models repeating protocols. The key invariant is duality: if one endpoint has type S, the other must have the dual type, obtained by swapping every ! with ? and every & with choose. This ensures that whenever one process sends, the other receives, and vice versa.

Linearity is the enforcement mechanism. Each channel endpoint must be used exactly once — you cannot duplicate an endpoint (which would create two processes trying to follow the same protocol step) or discard one (which would abandon the session mid-protocol). Linear type systems track this ownership: when a process sends on an endpoint of type !Int.S, the endpoint's type advances to S (the remaining protocol), and the old type !Int.S is consumed. This progression through the session type mirrors the progression through the communication protocol, and the type system verifies that every step is followed correctly.

Session types were introduced by Honda (1993) and extended by Honda, Vasconcelos, and Kubo. The theory has matured significantly: multiparty session types (Yoshida, Honda, and others) extend the framework from two-party to n-party protocols, specifying each participant's role in a global protocol description. Advanced systems guarantee not just type safety but deadlock freedom and progress — well-typed programs always advance and never reach a state where all processes are stuck waiting. These properties are checked statically through structural constraints on how sessions are composed.

Practical adoption is growing. Languages like Links and frameworks for Scala, Go, Rust, and TypeScript incorporate session types or session-type-inspired discipline. In microservice architectures, where services communicate via structured protocols, session types offer a way to verify at compile time that all services conform to the agreed-upon API contract. The connection to process calculi is deep: session types were originally formulated for the pi-calculus, and the duality/linearity discipline directly reflects the resource-sensitive nature of communication channels in concurrent computation.