Sender / receiver roles

Interaction.Role marks which side of a two-party protocol acts at each node. Action and Dual package the active/passive node shapes for the focal side and its environment; interact runs one round.

inductive Interaction.Role : Type

Which side speaks at a protocol node: sender (proposes a move) or receiver (observes).

• sender : Role
• receiver : Role

def Interaction.Role.swap : Role → Role

Exchange sender and receiver (duality on the role type).

def Interaction.Role.Action (role : Role) (m : Type u → Type u) (X : Type u) (Cont : X → Type u) : Type u

Focal party's action type: when acting, the focal party may use effects to choose the next move itself; when observing, it responds to any received move.

def Interaction.Role.Dual (role : Role) (m : Type u → Type u) (X : Type u) (Cont : X → Type u) : Type u

Environment / dual view: sender branch observes the chosen move and may continue effectfully; receiver branch samples the move and continuation.

def Interaction.Role.interact {m : Type u → Type u} [Monad m] {X : Type u} {ACont DCont : X → Type u} {Result : Type u} (role : Role) : role.Action m X ACont → role.Dual m X DCont → ((x : X) → ACont x → DCont x → m Result) → m Result

Run one round: pair an Action with the matching Dual and continue in k.