Theory

Session types as algebraic reticulates — the formal foundations.

Session Types

A session type describes a communication protocol on an object — the legal sequences of method calls, branches, and selections that a client may perform. Instead of a flat interface, an object's type evolves as methods are called, enforcing protocol compliance at compile time.

Example: File Object

open . rec X . &{read: +{data: X, eof: close . end}}

Open the file, then repeatedly read: on data, loop back; on eof, close and terminate. The type ensures close is always called exactly once.

Grammar

Session types are defined by the following grammar:

S  ::=  &{ m₁ : S₁ , … , mₙ : Sₙ }    — branch (external choice)
     |  +{ l₁ : S₁ , … , lₙ : Sₙ }    — selection (internal choice)
     |  ( S₁ || S₂ )                    — parallel
     |  rec X . S                        — recursion
     |  X                                — variable
     |  end                              — terminated
     |  S₁ . S₂                          — sequencing

Constructors

&{…} — Branch

External choice. The environment (client) chooses which method to call. Each branch leads to a different continuation type. This is the most common constructor — it models an object offering a menu of operations.

+{…} — Selection

Internal choice. The object (server) decides the outcome. The client must handle all possibilities. Models return values, error codes, and non-deterministic outcomes.

( S₁ || S₂ ) — Parallel

Concurrent access. Two execution paths run simultaneously on a shared object. The combined state space is the product lattice of the individual spaces. This is the key novelty of this work.

rec X . S — Recursion

Looping protocols. The variable X marks the loop point. Well-formed recursive types must have an exit path (termination condition) to avoid infinite protocols.

S₁ . S₂ — Sequencing

Sequential composition. Syntactic sugar for a single-method branch: m . S is equivalent to &{m: S}. Chains the end of S₁ to the start of S₂.

end — Terminated

Protocol end. No further operations are allowed. Every well-formed session type must eventually reach end along all execution paths.

State Spaces

Given a session type S, we construct its state space L(S) — a directed graph where:

The reachability ordering defines a partial order on states: s₁ ≥ s₂ iff there is a path from s₁ to s₂. This ordering gives the state space the structure of a poset (partially ordered set).

Lattice Properties

A state space is a lattice (a reticulate) if and only if:

  1. There is a top element (initial state reachable from all states or reaching all states)
  2. There is a bottom element (terminal state reachable from all states)
  3. Every pair of states has a meet (greatest lower bound)
  4. Every pair of states has a join (least upper bound)

For cyclic state spaces (from recursion), we first quotient by SCCs (strongly connected components) to obtain an acyclic DAG, then check lattice properties on the quotient.

The Parallel Constructor

The ∥ constructor is the key novelty of this work. When two branches execute in parallel on a shared object:

L(S₁ ∥ S₂) = L(S₁) × L(S₂)

The product construction orders states componentwise: (s₁, s₂) ≥ (t₁, t₂) iff s₁ ≥ t₁ and s₂ ≥ t₂.

Crucially, the product of two lattices is always a lattice. This means that any well-formed session type using ∥ necessarily has a lattice state space — making lattice structure a natural consequence of concurrency rather than an imposed requirement.

Example: Two-Buyer Protocol

lookup . getPrice . (proposeA . end || proposeB . +{ACCEPT: pay . end, REJECT: end})

After lookup and pricing, two buyers propose concurrently. The parallel region creates a 2×3 = 6 state product lattice for the concurrent part, embedded in the larger 10-state protocol.

Morphism Hierarchy

Between session-type state spaces, we define a hierarchy of structure-preserving maps:

  1. Isomorphism — bijective, order-preserving and reflecting. The state spaces are identical up to renaming.
  2. Embedding — injective, order-preserving and reflecting. One state space faithfully sits inside another.
  3. Projection — surjective, order-preserving. One state space maps onto another, possibly collapsing states.
  4. Galois connection — an adjunction α(x) ≤ y ⇔ x ≤ γ(y). Connects abstract interpretation to session type refinement.

This hierarchy provides the formal foundation for subtyping, protocol refinement, and compatibility checking between session types.

Try the Interactive Analyzer →