Enum GlobalType 

pub enum GlobalType {
    End,
    Message {
        from: Role,
        to: Role,
        payload: Payload,
        cont: Box<GlobalType>,
    },
    Choice {
        from: Role,
        to: Role,
        arms: BTreeMap<String, GlobalType>,
    },
    Rec(String, Box<GlobalType>),
    Var(String),
}

A global session type — the protocol viewed from above. Each constructor names every participant explicitly so projection has no ambiguity.

Serialisable so a global type can travel between deployment stages (declaration in source → IR → an enterprise registry that drives the §41.f WS surface). Hashable so a deployment can fingerprint the declared protocol before issuing snapshots that bind to it.

Variants

End

end — the protocol terminates.

Message

p → q : T . G — role from sends a value of type payload to role to, then the protocol continues as cont. from ≠ to is enforced by the projection gate (a self-message has no operational meaning at the global layer).

Fields

from: Role

to: Role

payload: Payload

cont: Box<GlobalType>

Choice

p → q : { ℓᵢ : Gᵢ } — role from selects label ℓᵢ, sends it to to, the protocol continues as Gᵢ. The label set is canonical (BTreeMap); arms must be non-empty.

Fields

from: Role

to: Role

arms: BTreeMap<String, GlobalType>

Rec(String, Box<GlobalType>)

μX. G — recursive protocol. Bind var in body.

Var(String)

X — recursion variable. Free vars on the gate’s input are an error (ProjectionError::UnboundVariable).

Implementations

impl GlobalType

pub fn message( from: impl Into<String>, to: impl Into<String>, payload: impl Into<String>, cont: GlobalType, ) -> GlobalType

from → to : payload . cont.

pub fn choice( from: impl Into<String>, to: impl Into<String>, arms: impl IntoIterator<Item = (String, GlobalType)>, ) -> GlobalType

from → to : { ℓ : G, … }.

pub fn rec(var: impl Into<String>, body: GlobalType) -> GlobalType

μX. G.

pub fn var(name: impl Into<String>) -> GlobalType

X.

pub fn roles(&self) -> BTreeSet<Role>

Every participant named anywhere in self. Used by Self::project_all to drive the per-role projection loop.

pub fn project(&self, r: &Role) -> Result<SessionType, ProjectionError>

Project self to the local session type role r is expected to run. Returns the binary SessionType the §41.a algebra + §41.d runtime consume.

Total over closed, contractive global types; rejects only if the gate fires:

• ProjectionError::SelfMessage — from == to somewhere;
• ProjectionError::MergeFailed — a non-participating role couldn’t observe the choice (arms diverge);
• ProjectionError::EmptyChoice — Choice { arms: {} };
• ProjectionError::UnboundVariable — Var(x) without an enclosing Rec(x, _) on the path.

pub fn project_all( &self, ) -> Result<BTreeMap<Role, SessionType>, ProjectionError>

Project for every role this global type mentions. A Result::Ok is the safe-realizability certificate: every endpoint has a well-defined local protocol, and any compliant per-role runtime composes into a faithful realisation of self.

pub fn is_safely_realizable(&self) -> bool

Is self safely realisable? Convenience wrapper around Self::project_all for callers that only care about the gate verdict (the type-checker’s safety predicate).

Trait Implementations

impl Clone for GlobalType

fn clone(&self) -> GlobalType

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for GlobalType

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for GlobalType

fn deserialize<__D>( __deserializer: __D, ) -> Result<GlobalType, <__D as Deserializer<'de>>::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Eq for GlobalType

impl Hash for GlobalType

fn hash<__H>(&self, state: &mut __H)

where __H: Hasher,

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl PartialEq for GlobalType

fn eq(&self, other: &GlobalType) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Serialize for GlobalType

fn serialize<__S>( &self, __serializer: __S, ) -> Result<<__S as Serializer>::Ok, <__S as Serializer>::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl StructuralPartialEq for GlobalType