agenticraft_foundation.mpst.local_types

Local type projection — per-role views derived from global types.

Local session types and projection algorithm.

Local types describe the communication behavior from a single participant's perspective. They are derived from global types via projection.

Local Type Syntax: - !q(M).L (Send: send M to q, then continue with L) - ?p(M).L (Receive: receive M from p, then continue with L) - ⊕q{lᵢ: Lᵢ} (Select: send choice lᵢ to q) - &p{lᵢ: Lᵢ} (Branch: receive choice from p) - μX.L (Recursion) - X (Variable) - end (End)

Projection Rules: - (p → q : M.G) ↓ p = !q(M).(G ↓ p) (sender projects to send) - (p → q : M.G) ↓ q = ?p(M).(G ↓ q) (receiver projects to receive) - (p → q : M.G) ↓ r = G ↓ r (other participants skip)

Key Theorem: If G ↓ p is defined for all p ∈ participants(G), then the local types are consistent and the session is deadlock-free.

References: - Honda, Yoshida, Carbone (2008) - Multiparty Session Types

LocalEndType dataclass

Bases: SessionType

Local end type: Session termination from local perspective.

SendType dataclass

Bases: SessionType

Send type: !q(M).L

Send message M to participant q, then continue with L.

ATTRIBUTE	DESCRIPTION
receiver	Target participant q TYPE: ParticipantId
payload	Message payload M TYPE: MessagePayload
continuation	Continuation type L TYPE: SessionType

ReceiveType dataclass

Bases: SessionType

Receive type: ?p(M).L

Receive message M from participant p, then continue with L.

ATTRIBUTE	DESCRIPTION
sender	Source participant p TYPE: ParticipantId
payload	Message payload M TYPE: MessagePayload
continuation	Continuation type L TYPE: SessionType

SelectType dataclass

Bases: SessionType

Select type: ⊕q{lᵢ: Lᵢ}

Send choice to participant q, selecting one of the labels.

ATTRIBUTE	DESCRIPTION
receiver	Target participant q TYPE: ParticipantId
branches	Available choices with continuations TYPE: dict[MessageLabel, SessionType]

BranchType dataclass

Bases: SessionType

Branch type: &p{lᵢ: Lᵢ}

Receive choice from participant p, branching on the label.

ATTRIBUTE	DESCRIPTION
sender	Source participant p TYPE: ParticipantId
branches	Possible branches with continuations TYPE: dict[MessageLabel, SessionType]

LocalRecursionType dataclass

Bases: SessionType

Local recursion type: μX.L

ATTRIBUTE	DESCRIPTION
variable	Recursion variable name TYPE: str
body	Body of the recursion TYPE: SessionType

LocalVariableType dataclass

Bases: SessionType

Local variable type: X

ATTRIBUTE	DESCRIPTION
name	Variable name TYPE: str

Projector

Projects global session types to local types for each participant.

The projection algorithm derives the local view of a session from the global choreography.

Key Property: If projection is defined for all participants, the session is well-formed and deadlock-free.

__init__(strict=True)

Initialize projector.

PARAMETER	DESCRIPTION
strict	If True, raise errors on projection failure. If False, return None on failure. TYPE: bool DEFAULT: True

project(global_type, participant)

Project global type to local type for participant.

G ↓ p = local type for participant p

PARAMETER	DESCRIPTION
global_type	Global session type G TYPE: SessionType
participant	Participant to project to p TYPE: ParticipantId

RETURNS	DESCRIPTION
SessionType | None	Local session type (G ↓ p), or None if undefined

RAISES	DESCRIPTION
ProjectionError	If projection fails and strict=True

project_all(global_type, participants=None)

Project global type to local types for all (or specified) participants.

PARAMETER	DESCRIPTION
global_type	Global session type TYPE: SessionType
participants	Optional subset of participants to project. If None, auto-discovers all participants from the global type. TYPE: set[ParticipantId] | list[str] | None DEFAULT: None

RETURNS	DESCRIPTION
dict[ParticipantId, SessionType]	Dictionary mapping each participant to their local type

RAISES	DESCRIPTION
ProjectionError	If projection fails for any participant

project(global_type, participant, strict=True)

Project global type to local type for a participant.

PARAMETER	DESCRIPTION
global_type	Global session type TYPE: SessionType
participant	Participant ID TYPE: ParticipantId | str
strict	If True, raise on failure TYPE: bool DEFAULT: True

RETURNS	DESCRIPTION
SessionType | None	Local type or None if undefined

project_all(global_type, participants=None)

Project global type to local types for all (or specified) participants.

PARAMETER	DESCRIPTION
global_type	Global session type TYPE: SessionType
participants	Optional subset of participants to project. If None, auto-discovers all participants from the global type. TYPE: set[ParticipantId] | list[str] | None DEFAULT: None

RETURNS	DESCRIPTION
dict[ParticipantId, SessionType]	Dictionary of local types per participant