Motivation: boundary bugs are protocol bugs
Many integration failures are not data-type errors; they are interaction errors. A service calls an endpoint “at the wrong time”, retries in a way the other side cannot handle, or assumes a response that is not guaranteed. A protocol description makes these expectations explicit.
Session types provide a disciplined way to write those protocols. The key move is that the type describes a structured conversation. If a conversation is typed, it becomes possible to ask compatibility questions (do the endpoints agree on the protocol?) and refinement questions (does an implementation adhere to a specification?).
What a protocol type describes
A protocol type typically captures:
- SequencingWhat message comes next?
- BranchingWho chooses between alternatives, and what are the alternatives?
- RecursionWhat loops are allowed (e.g., repeated requests)?
- ConcurrencyWhich messages can be interleaved or happen independently?
- TerminationHow does the conversation end (normal completion or error paths)?
Thinking this way immediately improves documentation: you can read the protocol as a story about interaction rather than a pile of endpoints.
Diagram: a tiny request/response protocol
How session types help in practice
The strongest benefit is preventing “protocol drift”: when one side evolves its behaviour and the other side silently assumes the old behaviour. A protocol type makes drift visible by making interaction changes explicit.
Session types also sharpen design questions. For example: who is responsible for choosing a branch (client or server)? Where do error paths live? Is retry behaviour part of the protocol or an external assumption? These questions exist anyway; session types force them into an explicit artefact.
Finally, protocol structure supports modular reasoning. If an endpoint is typed, you can reason about an implementation by checking adherence to the protocol rather than reading the entire codebase.
Key definitions
- ProtocolA specification of allowed sequences of interaction steps.
- DualityA compatibility relation between endpoints (one sends where the other receives, choices match, etc.).
- LinearityA discipline ensuring each channel/session is used according to a single conversation.
- Branching / selectionStructured choice: one side selects, the other offers alternatives.
- RefinementAn implementation provides fewer behaviours (or more guarantees) than its specification.
Common pitfalls
- Confusing data types with behavioural typesData typing alone does not prevent “wrong order” mistakes.
- Leaving error paths unspecifiedMany systems fail in the error-handling branches; model them explicitly.
- Assuming implicit retriesRetry behaviour can change semantics; if it matters, it belongs in the protocol.
- Ignoring concurrencyIf messages can be interleaved, the protocol must say so; otherwise implementations diverge.
Internal links
- Projects: protocolsA project-style view and reading path.
- Behavioural contractsAssumptions and guarantees as interfaces.
- Research: behavioural typesHow protocols connect to other themes.