Session Types Megathread — All Discussion Here 📌 PINNED 🔥 HOT

Okay, bumping this with a proper summary post since we're on page 43 and new folks keep asking the same questions. Let me do a quick recap of where the discussion has landed.

What are session types?
Session types are, at the highest level, a way to describe communication protocols as types. Session types can be thought of as "types for protocols", essentially extending the notion of the data type that we know and love to communicating systems. So instead of just saying "this channel carries ints", you say "this channel first sends an int, then receives a bool, then closes." The type enforces the protocol.

Why do we need linearity?
In order for session typing in programming languages to make sense, we need linearity, wherein each session endpoint must be used exactly once. This is, I would say, the largest barrier to implementation. If you could duplicate channel endpoints, all your protocol guarantees fall apart immediately.

The three implementation strategies:
Static: Conformance to session types is fully checked at compile time. Any error (be it sending the wrong message, not completing a session, or duplicating an endpoint) will be reported before a program compiles.
Dynamic: Conformance to session types is checked at runtime. Session types are compiled into communicating finite-state machines, and messages are verified against these CFSMs. These approaches are very flexible, extending session types to dynamically-checked languages, and allowing things like assertions on data.
Hybrid: Sending messages in the right order is checked statically. Linearity is checked dynamically. This is a promising approach, with drop-in libraries available to be used in general-purpose languages today!

See also: static vs. dynamic session typing thread | CFSMs and their relation to session types

Great summary. I want to add the logical foundations angle since people always ask about it.

Session type systems have been given strong logical foundations via Curry-Howard correspondences with linear logic, a resource-aware logic that naturally captures structured interactions. This isn't just aesthetic — it has real consequences for what properties you get "for free". Deadlock freedom, for instance, is provable from the logical interpretation.

There are two presentations of linear logic, classical and intuitionistic, and session type systems derived from linear logic have inherited this dichotomy. This is the source of a lot of confusion when comparing papers. Caires-Pfenning use intuitionistic, Wadler's CP uses classical. They're closely related but have different shapes in the typing rules.

For the intuitionist crowd: Caires and Pfenning's correspondence uses an intuitionistic linear logic where judgments for process are two-sided, with zero or many channels on the left and exactly one channel on the right. Such judgments have a convenient rely-guarantee reading: the process relies on the behaviors described by the channels on the left to guarantee the behavior of the one channel on the right.

See: Curry-Howard for session types deep dive | Linear Logic Primer

Also adding the wiki reference page to the sidebar. Thanks to lambdacatgirl and DualityNyan for keeping this thread high-quality. 🐾

Okay I've been following this thread for months and finally got a working session-types impl in Rust. Here's what I learned:

There is an implementation of binary session types in Mozilla's Rust language, making use of Rust's affine typing system. The key insight is that implementing session types requires a way to model that certain actions in the protocol have taken place. This is a complicated thing to do statically in most programming languages, but in Rust it is easy because of move semantics. Using move semantics, we ensure that "taking a step" in the protocol (sending, receiving, etc) cannot be repeated.

Here's a minimal example using the session-types crate. The basic channel type is Chan<E, P> where E is an environment and P is the protocol:

// A server that receives a String, sends back its length, loops
type Server = Rec<
    Offer<
        Eps,
        Recv<String, Send<usize, Var<Z>>>
    >
>;

fn server(c: Chan<(), Server>) {
    let mut c = c.enter();
    loop {
        c = match c.offer() {
            Branch::Left(c)  => { c.close(); break; }
            Branch::Right(c) => {
                let (c, s) = c.recv();
                c.send(s.len()).zero()
            }
        };
    }
}

The caveat: a value of affine type can be used no more than once, but it may not be used at all. Thus, the Rust encoding guarantees that if a protocol proceeds then it will comply with its session type, but does not prevent a program from simply discarding a channel half way through a protocol. True linear types would catch the "drop it halfway" case at compile time, affine types don't.

More on the Rust specifics: dedicated Rust session types thread

This is exactly why the Haskell side is interesting. There have been several approaches:

There is an implementation of session types in Concurrent Haskell, through the observation that session types can be encoded using an effect system (and vice versa). That's the Orchard & Yoshida (POPL'16) approach.

Then there's the Linear Haskell approach (priority-sesh): priority-sesh is an implementation of deadlock-free session types in Linear Haskell. Using Linear Haskell allows us to check linearity—or more accurately, have linearity guaranteed for us—without relying on complex type-level machinery.

Here's what a session type for a multiplication service looks like in Linear Haskell:

type MulServer = Recv Int (Recv Int (Send Int End))
type MulClient = Send Int (Send Int (Recv Int End))

mulServer :: Chan MulServer ⊸ IO ()
mulServer c = do
  (x, c) <- recv c
  (y, c) <- recv c
  c      <- send c (x * y)
  close c

The drawback: there are some drawbacks to using Linear Haskell. Most importantly, Linear Haskell is not very mature at this stage. For instance, anonymous functions default to unrestricted. But it's still the most idiomatic approach available today.

See the dedicated: Haskell session types thread | Linear Haskell / GHC LinearTypes extension

Nobody's mentioned Links yet this page, let me rectify that.

Links is a programming language designed at the University of Edinburgh for developing "tierless" web applications. A recent extension of Links adds support for binary session types as language primitives. Session types are checked fully statically, using an extension of the type system to support linear types.

What makes Links notable is that it's one of the few cases where session types are native language constructs rather than a library encoding. The linearity constraints are enforced by the type system directly, not via tricks with phantom types or parameterized monads.

This comes from the Lindley & Morris "Lightweight Functional Session Types" work. The paper proves session type safety as a theorem of the language, not as a property of a specific library. Big difference in terms of guarantees.

Links examples: Links language session type code examples

Question from a relative newcomer: what's the actual difference between session types and just encoding a state machine in the type system with phantom types? I see people do the latter in Rust all the time.

Like:

struct Connection<State> { ... }
impl Connection<Unauthenticated> {
    fn authenticate(self, ...) -> Connection<Authenticated> { ... }
}
impl Connection<Authenticated> {
    fn query(self, ...) -> (Connection<Authenticated>, Results) { ... }
}

Is this session types? Is it equivalent?

Great question, and the answer is "sort of, but not quite." What you're describing is called the typestate pattern. It has a lot of overlap with session types, and in practice for single-threaded, single-party protocol you can absolutely use typestate encoding for the same effect.

Session types are a variant of linear types geared explicitly towards expressing a protocol to be enacted by two or more parties over a shared communication channel, and are distinct from linear types in that they make the precise ordering of messages to be sent explicit in the type.

The critical difference: session types are dual. The type describes both sides of the communication channel simultaneously — if one side sends an Int, the other side's type says it receives an Int. The duality is structural and enforced. Your phantom-type state machine only describes one side, and says nothing about what the other end is doing.

Also, session types compose: you can take a session type and plug it into a larger protocol. The typestate pattern tends to be ad-hoc per struct.

That said, for real Rust code with no concurrency, typestate encoding is usually more ergonomic. See the related thread: typestate vs. session types comparison

Jumping in on the subtyping angle, since it's glossed over constantly. Subtyping for session types is surprisingly non-obvious.

The classic reference is Gay & Hole's "Subtyping for session types in the pi calculus" (Acta Informatica 2005). The key intuition: a session type S is a subtype of T if any program that works with T also works with S. But because session types have both input and output positions, the variance rules get interesting.

For sends (output), subtyping is covariant: if you promised to send an Animal, sending a Cat is fine.

For receives (input), subtyping is contravariant: if the receiver expects to receive a Cat, it's unsafe to have the sender only guarantee sending some Animal.

But there's also the structural dimension: you can also have a subtype that does more than required — e.g., a session that can offer more branches than the type requires. See the discussion thread: session type subtyping — deep dive.

Can we talk about multiparty session types? We've been mostly in binary-session land this page.

Multiparty Session Types extend the theory of binary session types to encompass interactions containing more than two participants. The main idea behind multiparty session types is to describe the interactions between participants in a top-down manner as a global type. These global types can then be "projected" into local types, which describe the interaction from the point of view of a particular participant.

So with MPST you write a global protocol:

-- A three-party auth protocol (pseudocode)
global protocol Auth(role Client, role Server, role Logger) {
  Client -> Server: Credentials;
  choice at Server {
    Server -> Client: Accept;
    Server -> Logger: LogSuccess;
  } or {
    Server -> Client: Reject;
    Server -> Logger: LogFailure;
  }
}

And then the tool projects this down to each participant's local type. The global type guarantees protocol consistency — everyone agrees on who sends what when. No need to manually check that each pair of roles is compatible.

Full MPST thread here | Scribble protocol language

Want to bring up the capability security angle since nullKitty linked the capability thread. How do session types relate to capability-based security?

Linear types correspond to linear logic and ensure that objects are used exactly once. This allows the system to safely deallocate an object after its use, or to design software interfaces that guarantee a resource cannot be used once it has been closed or transitioned to a different state.

That's basically the capability story: a session endpoint is an unforgeable capability to perform a specific next action in the protocol. Linearity means you can't duplicate or share the capability (no ambient authority), and the session type tells you precisely what the capability authorizes.

There's a nice connection to object capability model (OCap) here. A session type is like a capability with a built-in "usage protocol." The capability security + session types thread goes into this more.

Continuing on the dependent types angle that came up a few pages back. Can session types be combined with dependent types?

Yes, and it's very powerful. The basic idea: index session types by values, so the type of the rest of the protocol can depend on a value sent/received earlier. Classic example — a session that sends a length n, then sends a vector of exactly n elements:

-- Dependent session type (Rast-like pseudocode)
type VecSend[n] =
  if n == 0 then
    ?{done}. end
  else
    !Int. VecSend[n-1]

type Server = ?Int[n]. VecSend[n]. end
-- Receive n, then receive exactly n ints, then close

The Rast language (Das & Pfenning, PPDP'20) implements arithmetically-indexed binary session types over an intuitionistic linear logic base. It's one of the most complete dependent session type systems available today.

See: Dependent session types thread | Rast language discussion

What about using session types in dynamically-typed or mixed-typing environments? Not every codebase is statically typed.

Session types are a rich type discipline, based on linear types, that lift the sort of safety claims that come with type systems to communications. However, web-based applications and micro services are often written in a mix of languages, with type disciplines in a spectrum between static and dynamic typing. Gradual session types address this mixed setting by providing a framework which grants seamless transition between statically typed handling of sessions and any required degree of dynamic typing.

The GradualGV paper (ICFP 2017) proposes GradualGV as an extension of GV with dynamic types and casts. The tricky part: the interplay of linearity and dynamic types requires a novel approach to specifying the dynamics of the language.

Basically you introduce a "?" type (the dynamic type) and casts between static session types and "?". If a cast fails at runtime, you get a blame-tracked error pointing to who violated the protocol.

Gradual session types discussion thread

Surprised nobody's mentioned Ferrite this page. It's a Rust session types library that takes the ILL (intuitionistic linear logic) route rather than the classical approach most other Rust libraries use.

Ferrite's implementation of session types is based on intuitionistic linear logic. This is in contrast with the classical linear logic formulation that is used by some other session types implementations.

The practical consequence: there is no need for dualization in Ferrite. This means that the session type signature remain the same from the perspective of both the provider and the client. While the provider hello_provider sends a string value through a channel with the session type SendValue<String, End>, the client hello_client receives a value from a channel of the same session type.

Compare this to session-types crate where you need to explicitly use the HasDual trait and work with dual types. Ferrite just gives you one type and handles directionality implicitly.

The downside is the API is more complex and the documentation assumes familiarity with ILL. But for research-grade correctness it's hard to beat.

Rust session types thread | Ferrite library dedicated discussion

Coming back to the practical side: what's the actual state of session types in production use? Like, is anyone using this outside of academia?

Session types have emerged as a rigorous formalism for specifying and verifying communication protocols in concurrent systems. They provide a structured approach to ensuring that interactions among independent processes adhere to predefined patterns, thus reducing the likelihood of communication errors. By integrating session types into programming languages, researchers have been able to bridge the gap between theoretical models and practical application, enabling developers to design systems that reliably manage resources, parallelise operations, and prevent deadlocks.

But honestly, production use is still rare. The industry-facing ones are more like: Rust's session-types crate (available on crates.io), Scala's lchannels and Effpi libraries, some Java tools. Most are still library-level, not language-level.

The key problem is ergonomics. Until you can write session-typed code as naturally as you write regular typed code, adoption will stay niche. Linear Haskell and Ferrite are making progress but we're not there yet.

Late night post but I want to leave a reading list for anyone joining this thread for the first time. Compiled from 847 replies of discussion:

Foundational papers:

• Honda (1993) — original session types proposal
• Gay & Hole (2005) — subtyping for session types
• Caires & Pfenning (2010) — session types as intuitionistic linear propositions
• Wadler (2012) — Propositions as Sessions (classical LL)
• Honda, Yoshida & Carbone (2008) — multiparty session types

Implementations to explore:

• Rust: session-types crate, Ferrite
• Haskell: priority-sesh, Linear Haskell / GHC
• Links: native session types in Links
• Scala: lchannels, Effpi
• Rast: arithmetically indexed dependent session types

Related topics on CGPA:

• Linear Types Primer
• π-Calculus Basics
• Typestate vs. Session Types
• Dependent Session Types
• Gradual Session Types
• Capability Security & Session Types
• Static vs. Dynamic Session Checking

-- 🌙 It's 2am and I'm reading session type papers. This is fine.