agenticraft_foundation.mpst.global_types

Global type specification — bird's-eye view of multi-party protocols.

Global session types for multi-party choreographies.

Global types describe the overall communication structure from a bird's-eye view, specifying message exchanges between all participants.

Syntax: - p → q : M.G (Message: p sends M to q, then continue with G) - p → q : {lᵢ: Gᵢ} (Choice: p sends choice lᵢ to q, continue with Gᵢ) - μX.G (Recursion: recursive type bound to X) - X (Variable: recursion variable reference) - end (End: successful termination)

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

EndType dataclass

Bases: SessionType

End type: Successful session termination.

Represents the end of a session with no further communication. Written as 'end' in session type notation.

MessageType dataclass

Bases: SessionType

Message type: p → q : M.G

Represents a single message from sender to receiver, followed by a continuation.

ATTRIBUTE	DESCRIPTION
sender	Sending participant p TYPE: ParticipantId
receiver	Receiving participant q TYPE: ParticipantId
payload	Message payload M TYPE: MessagePayload
continuation	Continuation type G TYPE: SessionType

ChoiceType dataclass

Bases: SessionType

Choice type: p → q : {lᵢ: Gᵢ}

Represents a branching choice where sender selects a label and both parties continue with the corresponding branch.

ATTRIBUTE	DESCRIPTION
sender	Participant making the choice p TYPE: ParticipantId
receiver	Participant receiving the choice q TYPE: ParticipantId
branches	Mapping from labels to continuation types TYPE: dict[MessageLabel, SessionType]

RecursionType dataclass

Bases: SessionType

Recursion type: μX.G

Represents a recursive session type where variable X is bound in the body G.

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

unfold_once()

Unfold one level of recursion.

Returns the body with the variable replaced by self.

VariableType dataclass

Bases: SessionType

Variable type: X

Represents a recursion variable reference.

ATTRIBUTE	DESCRIPTION
name	Variable name TYPE: str

ParallelType dataclass

Bases: SessionType

Parallel composition: G₁ | G₂

Represents parallel execution of two independent sessions. Participants of G₁ and G₂ should be disjoint.

ATTRIBUTE	DESCRIPTION
left	Left session type G₁ TYPE: SessionType
right	Right session type G₂ TYPE: SessionType

msg(sender, receiver, label, continuation=None, payload_type='any')

Convenience constructor for MessageType.

PARAMETER	DESCRIPTION
sender	Sending participant TYPE: str | ParticipantId
receiver	Receiving participant TYPE: str | ParticipantId
label	Message label TYPE: str | MessageLabel
continuation	Continuation type (default: EndType) TYPE: SessionType | None DEFAULT: None
payload_type	Type of payload TYPE: str DEFAULT: 'any'

RETURNS	DESCRIPTION
MessageType	MessageType instance

Example

Client → Server : Request. Server → Client : Response. end

msg("client", "server", "request", msg("server", "client", "response"))

choice(sender, receiver, branches)

Convenience constructor for ChoiceType.

PARAMETER	DESCRIPTION
sender	Participant making the choice TYPE: str | ParticipantId
receiver	Participant receiving the choice TYPE: str | ParticipantId
branches	Mapping from label strings to continuation types TYPE: dict[str, SessionType]

RETURNS	DESCRIPTION
ChoiceType	ChoiceType instance

Example

choice("client", "server", { "buy": msg("server", "client", "confirm"), "cancel": msg("server", "client", "cancelled"), })

rec(variable, body)

Convenience constructor for RecursionType.

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

RETURNS	DESCRIPTION
RecursionType	RecursionType instance

Example

μX. Client → Server : Request. Server → Client : Response. X

rec("X", msg("client", "server", "request", msg("server", "client", "response", var("X"))))

var(name)

Convenience constructor for VariableType.

PARAMETER	DESCRIPTION
name	Variable name TYPE: str

RETURNS	DESCRIPTION
VariableType	VariableType instance

end()

Convenience constructor for EndType.

RETURNS	DESCRIPTION
EndType	EndType instance

parallel(left, right)

Convenience constructor for ParallelType.

PARAMETER	DESCRIPTION
left	Left session type TYPE: SessionType
right	Right session type TYPE: SessionType

RETURNS	DESCRIPTION
ParallelType	ParallelType instance