Background

This document provides an introduction to the theory behind Rumpsteak-Aura. It covers multiparty session types, choreographic programming, and algebraic effects. Understanding these concepts helps explain how the system achieves type-safe distributed programming.

Session Types

Session types encode communication protocols as types in the type system. They specify the sequence and structure of messages exchanged between processes. A session type acts as a contract that all communication must follow. The compiler verifies that implementations adhere to this contract.

Traditional type systems ensure data safety. They prevent type errors like passing a string where an integer is expected. Session types extend this to communication safety. They prevent protocol errors like sending when you should receive or terminating when more messages are expected.

A session type describes a communication channel from one endpoint’s perspective. The type !String.?Int.end means send a string, then receive an integer, then close the channel. The dual type ?String.!Int.end means receive a string, then send an integer, then close. These types are complementary. They ensure the endpoints coordinate correctly.

Multiparty Session Types (MPST)

Multiparty session types extend binary session types to protocols with three or more participants. While session types handle point-to-point channels, MPST handles protocols where multiple parties interact. Each participant can communicate with multiple others. The type system ensures all interactions remain synchronized.

MPST introduces new challenges beyond binary sessions. Participants must agree on the overall protocol flow. Messages between two participants affect what other participants can do next. The type system must track these dependencies to prevent global deadlocks. Consider a three-party payment protocol where a customer requests a quote from a merchant, the merchant checks with a bank, and the bank approves or denies.

In MPST, each participant has a local view that includes all their partners. The customer’s type shows communication with both merchant and bank. The system ensures all three views are compatible. For a more in-depth discussion of MPST theory, see A Very Gentle Introduction to Multiparty Session Types. Advanced optimizations through asynchronous subtyping are covered in Precise Subtyping for Asynchronous Multiparty Sessions. And Mechanised Subject Reduction for Multiparty Asynchronous Session Types includes a mechanized Coq proof that adds a well-typed condition that fixes the original MPST formulation by Honda et al. The type theory in this crate draws from this revised forumulation.

Global Types and Projection

Global types describe protocols from a neutral, third-party perspective. They specify all interactions between all participants. Local types describe the protocol from one participant’s viewpoint. Projection transforms global types into local types for each participant.

G = Alice -> Bob: Int.
    Bob -> Alice: {Sum: Int, Product: Int}

This global type projects to different local types. Alice gets Bob!Int.Bob&{Sum: Int, Product: Int}. Bob gets Alice?Int.Alice⊕{Sum: Int, Product: Int}. Each participant sees only their part of the protocol.

The projection algorithm ensures the local types are compatible. If projection succeeds, the protocol is guaranteed to be deadlock-free. All participants will complete the protocol without communication errors.

Lean Signatures (Core Types)

Rumpsteak-Aura’s formal core is specified in Lean. The core session types are:

the global protocol type (GlobalType),
the recursive local type (LocalTypeR), and
the coinductive local type used in bisimulation proofs (LocalTypeC).

Below are their exact Lean signatures, with namespaces preserved.

Global types and labels (lean/RumpsteakV2/Protocol/GlobalType.lean):

namespace RumpsteakV2.Protocol.GlobalType

inductive PayloadSort where
  | unit : PayloadSort
  | nat : PayloadSort
  | bool : PayloadSort
  | string : PayloadSort
  | prod : PayloadSort → PayloadSort → PayloadSort
  deriving Repr, DecidableEq, BEq, Inhabited

structure Label where
  name : String
  sort : PayloadSort := PayloadSort.unit
  deriving Repr, DecidableEq, BEq, Inhabited

inductive GlobalType where
  | end : GlobalType
  | comm : String → String → List (Label × GlobalType) → GlobalType
  | mu : String → GlobalType → GlobalType
  | var : String → GlobalType
  deriving Repr, Inhabited

end RumpsteakV2.Protocol.GlobalType

Inductive local types (lean/RumpsteakV2/Protocol/LocalTypeR.lean):

namespace RumpsteakV2.Protocol.LocalTypeR

open RumpsteakV2.Protocol.GlobalType

inductive LocalTypeR where
  | end : LocalTypeR
  | send : String → List (Label × LocalTypeR) → LocalTypeR
  | recv : String → List (Label × LocalTypeR) → LocalTypeR
  | mu : String → LocalTypeR → LocalTypeR
  | var : String → LocalTypeR
  deriving Repr, Inhabited

end RumpsteakV2.Protocol.LocalTypeR

Coinductive local types (M-types) (lean/RumpsteakV2/Coinductive/LocalTypeC.lean):

namespace RumpsteakV2.Coinductive

open RumpsteakV2.Protocol.GlobalType

inductive LocalTypeHead where
  | end  : LocalTypeHead
  | var  : String → LocalTypeHead
  | mu   : String → LocalTypeHead
  | send : String → List Label → LocalTypeHead
  | recv : String → List Label → LocalTypeHead
  deriving Repr, DecidableEq

def LocalTypeChild : LocalTypeHead → Type
  | .end       => PEmpty
  | .var _     => PEmpty
  | .mu _      => Unit
  | .send _ ls => Fin ls.length
  | .recv _ ls => Fin ls.length

def LocalTypeF : PFunctor := ⟨LocalTypeHead, LocalTypeChild⟩

abbrev LocalTypeC := PFunctor.M LocalTypeF

end RumpsteakV2.Coinductive

Well-Formedness (Lean)

Well-formedness is explicit in the Lean development.

Global types are well-formed when all of the following hold:

def GlobalType.wellFormed (g : GlobalType) : Bool :=
  g.allVarsBound && g.allCommsNonEmpty && g.noSelfComm && g.isProductive

Intuitively:

allVarsBound: recursion variables are bound
allCommsNonEmpty: communications have at least one branch
noSelfComm: no self-send
isProductive: recursion must pass through a communication

Local types are well-formed when they are closed and contractive:

structure LocalTypeR.WellFormed (t : LocalTypeR) : Prop where
  closed : t.isClosed
  contractive : t.isContractive = true

Coinductive local types are well-formed when they are closed and observable:

def ClosedC (t : LocalTypeC) : Prop :=
  ∀ v, ¬ UnfoldsToVarC t v

structure WellFormedC (t : LocalTypeC) : Prop where
  closed : ClosedC t
  observable : ObservableC t

Progress Conditions (Lean)

Progress is not derived from well-formedness alone. The V2 proofs separate structural well-formedness from a progress predicate that asserts a communication is reachable.

The progress predicate is:

inductive ReachesComm : GlobalType → Prop where
  | comm (sender receiver : String) (branches : List (Label × GlobalType)) :
      branches ≠ [] → ReachesComm (.comm sender receiver branches)
  | mu (t : String) (body : GlobalType) :
      ReachesComm (body.substitute t (.mu t body)) →
      ReachesComm (.mu t body)

The associated progress theorem uses this predicate together with well-formedness and well-typedness:

def CanProgress (c : Configuration) : Prop :=
  ∃ c' act, ConfigStep c c' act

theorem deadlock_free (c : Configuration)
    (htyped : WellTypedConfig c)
    (hwf : c.globalType.wellFormed = true)
    (hcomm : ReachesComm c.globalType) :
    CanProgress c

In other words: well-formedness ensures validity of recursion and structure, while ReachesComm ensures actual progress is possible. Both are required to justify progress.

Choreographic Programming

Choreographic programming takes the global types concept further. Instead of just types, you write actual program logic from a global perspective. The choreography describes computations and data flow between participants. Endpoint projection generates local implementations for each participant.

#![allow(unused)]
fn main() {
choreography!(r#"
protocol Calculator =
  roles Alice, Bob
  Alice -> Bob : Value
  Bob -> Alice : Result
"#);
}

This choreography specifies the communication protocol. The system projects it into separate programs for Alice and Bob. Alice’s program sends a value and receives a result. Bob’s program receives a value and sends back a result.

Choreographic programming eliminates the need to manually coordinate distributed implementations. The global specification ensures all participants agree on the protocol. Type checking at the choreographic level prevents distributed system errors.

A good place to start learning more about choreographic programming is Introduction to Choreographies. For the integration with multiparty session types, see Applied Choreographies.

Algebraic Effects

Algebraic effects separate what a program does from how it does it. The effect algebra defines a set of abstract operations that a program can perform. Handlers provide concrete implementations of these operations. This separation allows the same program to run with different implementations.

In Rumpsteak-Aura, communication operations are effects. Sending and receiving messages are abstract operations. Different handlers implement these operations differently. An in-memory handler passes messages through local channels. A network handler sends messages over TCP or WebSocket connections.

#![allow(unused)]
fn main() {
let program = Program::new()
    .send(Role::Bob, Message::Hello)
    .recv::<Message>(Role::Bob)
    .end();

// Same program, different handlers
interpret(&mut in_memory_handler, &mut endpoint, program).await;
interpret(&mut network_handler, &mut endpoint, program).await;
}

The program specifies what messages to send and receive. The handler determines how this happens. This design enables testing with local handlers and deployment with network handlers. The protocol logic remains unchanged.

Integration in Rumpsteak-Aura

Rumpsteak-Aura combines these concepts into a practical system. Choreographies define distributed protocols globally. The type system ensures protocol safety through MPST. Effect handlers provide flexible execution strategies. The choreography macro parses protocol definitions, generates role and message types automatically, and creates session types for each participant through projection.

The effect system decouples protocol logic from transport mechanisms. Handlers interpret send and receive operations. Middleware can add logging, retry logic, or fault injection. The same choreography works across different deployment scenarios. Content addressing assigns cryptographic identities to all protocol artifacts, enabling memoization and structural sharing.

Topology configuration separates deployment concerns from protocol logic. Resource heaps provide explicit state management with nullifier-based consumption tracking. This integration provides both safety and flexibility through a type system that prevents protocol errors and an effect system that allows diverse implementations.

Rumpsteak Aura