agenticraft_foundation.mpst.types

Session type definitions — base types for global and local session specifications.

Core type definitions for Multiparty Session Types (MPST).

This module provides the foundational types for MPST-based verification of multi-agent choreographies.

References: - Honda, Yoshida, Carbone (2008) - Multiparty Session Types - Scalas, Yoshida (2019) - Less is More: Multiparty Session Types Revisited

Key Theorem: Well-typed sessions are deadlock-free. If all participants conform to their local projections, the global protocol is deadlock-free.

ParticipantId

Bases: str

Unique identifier for a session participant (agent).

MessageLabel

Bases: str

Label for a message type in session communication.

SessionState

Bases: str, Enum

States of a session execution.

TypeKind

Bases: str, Enum

Kinds of session types.

MessagePayload dataclass

Payload type for session messages.

ATTRIBUTE	DESCRIPTION
label	Message label/type identifier TYPE: MessageLabel
payload_type	Type of the payload data TYPE: str
schema	Optional JSON schema for validation TYPE: dict[str, Any] | None

SessionMessage dataclass

A message in a session.

ATTRIBUTE	DESCRIPTION
sender	Sending participant TYPE: ParticipantId
receiver	Receiving participant TYPE: ParticipantId
payload	Message payload TYPE: MessagePayload
session_id	Session this message belongs to TYPE: str
sequence	Sequence number in session TYPE: int
metadata	Additional message metadata TYPE: dict[str, Any]

SessionContext dataclass

Runtime context for session execution.

ATTRIBUTE	DESCRIPTION
session_id	Unique session identifier TYPE: str
participants	Set of participant IDs TYPE: set[ParticipantId]
current_state	Current execution state TYPE: SessionState
message_history	History of messages exchanged TYPE: list[SessionMessage]
local_states	Per-participant local state TYPE: dict[ParticipantId, str]
metadata	Additional context metadata TYPE: dict[str, Any]

add_message(message)

Record a message in the session history.

get_participant_messages(participant)

Get all messages involving a participant.

SessionType

Bases: ABC

Abstract base for session types (both global and local).

Session types describe the structure of multi-party communication.

kind abstractmethod property

The kind of session type.

participants() abstractmethod

Get all participants referenced in this type.

RETURNS	DESCRIPTION
set[ParticipantId]	Set of participant identifiers.

is_terminated() abstractmethod

Check if this type represents termination.

unfold(bindings) abstractmethod

Unfold recursion variables with given bindings.

ProjectionError dataclass

Bases: Exception

Error during type projection.

ATTRIBUTE	DESCRIPTION
message	Error message TYPE: str
participant	Participant being projected TYPE: ParticipantId | None
global_type	Global type being projected TYPE: SessionType | None
cause	Original exception if any TYPE: Exception | None

TypeCheckError dataclass

Bases: Exception

Error during type checking.

ATTRIBUTE	DESCRIPTION
message	Error message TYPE: str
expected	Expected type TYPE: SessionType | None
actual	Actual type encountered TYPE: SessionType | None
location	Location in the session TYPE: str

SessionViolation dataclass

A violation of session type rules.

ATTRIBUTE	DESCRIPTION
violation_type	Type of violation TYPE: str
message	Detailed message TYPE: str
participant	Participant involved TYPE: ParticipantId | None
expected_action	What was expected TYPE: str
actual_action	What actually happened TYPE: str
context	Additional context TYPE: dict[str, Any]