Session types and protocols

In many systems, failures are protocol failures: two parties disagree about what message comes next. One side sends “commit” while the other expects “cancel”; one side retries and duplicates while the other treats duplicates as distinct operations. Traditional type systems can ensure that message payloads have the right shape, but they usually do not capture the allowed sequence of messages.

Session types are a family of ideas that treat a protocol itself as a type: a structured description of the sequence of messages, including choices (branching) and, in richer settings, parallel structure. The point is not academic notation; it is to make the protocol explicit enough that implementations can be checked against it.

Quick takeaways

• Protocols are interfacesThey define what each party may send and when, not just data schemas.
• Ordering bugs are commonMany production issues reduce to “message arrived in a state where it shouldn’t”.
• Types can describe sequencesSession types capture send/receive order and branching decisions.
• Duality mattersClient and server have dual views of the same protocol; mismatches are detectable.
• Protocols interact with failure semanticsTimeouts, retries, and reordering should be part of the protocol story.

Problem framing (why it matters)

Message-based systems are attractive because they scale and isolate components. The cost is that correctness becomes a protocol problem. Without an explicit protocol, “compatibility” is tested indirectly by integration tests and incidents. A small protocol description makes behaviour reviewable and gives you a target for checks.

Session-type thinking also improves design discussions. Instead of arguing about “what happens if the client disconnects”, you can ask: which messages are allowed after disconnect? which state transitions are visible? what must be idempotent?

Key concepts (definitions + mini examples)

A tiny protocol sketch

Consider a simple request/response protocol with an explicit choice:

Client → Server: Request
Server → Client: (Ok(Response) | Error(Code))
Client → Server: Ack

Even this tiny sketch contains ordering: Ack is only valid after Ok or Error. A session-type view turns this into a structured “state machine type”.

Duality (client vs server views)

The client view of a protocol is typically the dual of the server view. If the client must send a message, the server must be ready to receive it. If the server chooses between two replies, the client must be ready for both. This duality is what makes mismatches detectable.

Branching and choices

Many protocols contain choices that matter for correctness: authentication success vs failure, commit vs abort, cache hit vs miss. Session types represent choices explicitly, which prevents an implementation from “forgetting” to handle a branch.

Protocols and failure semantics

Real systems include retries, timeouts, and reordering. A protocol that assumes “messages are delivered exactly once” is rarely compatible with production. In practice, you either (1) include duplication/retry behaviour in the protocol story, or (2) place it below the protocol boundary and rely on a reliable transport abstraction.

Practical checks (steps/checklist)

1) Write the protocol in plain language first

Start with a short table: for each state, list allowed incoming messages and outgoing messages. Most protocol bugs are visible in this table even before any formal tooling is involved.

2) Make states explicit in code

A practical technique is to encode protocol state in types or structures. Even without a full session type system, you can represent “pending request” vs “completed” states and make invalid messages unrepresentable.

3) Validate at boundaries

If an implementation receives a message that is invalid in the current state, that is a protocol error. Decide what the system does: reject, ignore, or treat as idempotent. Making this behaviour explicit is often more important than the particular choice.

4) Test with adversarial traces

Write tests that reorder messages, duplicate messages, and drop messages. Protocols that survive those tests are much less likely to fail in production.

Common pitfalls

• Confusing payload validation with protocol correctnessA message can have the right schema but be invalid in the current state.
• Leaving failure behaviour implicitTimeouts and retries change semantics; if not specified, they cause surprises.
• Handling only the happy pathBranches for errors, cancellations, and disconnects must be part of the protocol.
• State stored in ad-hoc flagsScattered state makes invalid transitions easy to introduce and hard to review.
• Assuming “exactly once” deliveryIf duplicates can happen, the protocol needs an idempotency story.

Related notes

• Specs, invariants, and contractsProtocols are a concrete form of interface contract.
• Model checking primerProtocols can be modelled and checked for safety properties.
• Failure modes, retries, and idempotencyThe protocol needs to define what duplicates mean.
• Time, clocks, and orderingOrdering assumptions shape protocol correctness.