Control.Protocol

This module provides type Protocol to model distributed multi-party protocols, ensuring the continuity of the associated resource state transitions on the type level for all protocol commands and scenarios.

It accepts used-defined data type for protocol commands (GADT of kind Command) and the list of protocol participants to create protocol type.

Command type serves as a single abstract api between all participants - it is defined to allow decoupling type-level requirements for participants implementations.

Function '(->:)' wraps commands into free parameterized monad (see freer-indexed) so that they can be chained into type-aligned scenarios, optionally written using do notation. These scenarios can be interpreted in any monad using runProtocol function, e.g. to print protocol description or diagram or to execute system-level integration tests.

See protocol definition and scenario examples in Control.Protocol.Example.

Documentation

type Command party state = (party, state, state) -> (party, state, state) -> Type -> Type

Defines the kind of the command data type used by Protocol:

• party - the type (normally enumerable) that defines parties of the protocol (here it is used as a kind). This type should be singletonized.
• state - the kind of the protocol resource state.

The first type-level tuple in command constructors defines the party that sends the command, with the initial and final resource states for that party.

The second tuple defines the party that executes command (e.g., provides some api) with its initial final and states.

See Control.Protocol.Example for command example.

type Protocol cmd parties = XFree (ProtocolCmd cmd parties)

Type synonym to create protocol data type (ProtocolCmd wrapped in XFree - parameterized free monad):

• cmd - user-defined command type constructor that should have the kind Command.
• parties - type-level list of participants - it defines the order of participant states in the combined state of the system described by the protocol.

data ProtocolCmd (cmd :: Command p k) (parties :: [p]) (s :: [k]) (s' :: [k]) (a :: Type)

Protocol data type that wraps a command and explicitly adds command participants.

Its only constructor that is not exported adds command participants and combines participant states in type-level list so that they can be chained in type-aligned sequence of commands:

ProtocolCmd ::
  Sing (from :: p) ->
  Sing (to :: p) ->
  cmd '(from, Prj ps s from, fs') '(to, Prj ps s to, ts') a ->
  ProtocolCmd cmd ps s (Inj ps (Inj ps s from fs') to ts') a

Here:

• from - type of party that sends the command.
• to - type of party that executes command (e.g., provides some API).

Protocol type synonym should be used to construct this type, and function '(->:)' should be used instead of the constructor.

(->:) infix 6

Arguments

:: Sing from

party that sends command

-> Sing to

party that executes command

-> cmd '(from, Prj ps s from, fs') '(to, Prj ps s to, ts') a

command - its initial states for both parties are projected from system state

-> Protocol cmd ps s (Inj ps (Inj ps s from fs') to ts') a

final protocol state injects final states of both participants

Function that wraps command into ProtocolCmd type converted into free parameterized monad.

runProtocol

Arguments

:: Monad m

=> (forall from to b. Sing (P from) -> Sing (P to) -> cmd from to b -> m b)

function to interpret a command

-> Protocol cmd ps s s' a

protocol scenario (see example in Scenario)

-> m a

runProtocol interprets protocol scenario in any monad, using passed runCmd function that interprets individual commands.