Control.Protocol.Example

Example command and protocol definition.

Documentation

type MyProtocol = Protocol MyCommand '[Recipient, Broker, Sender]

Example protocol type.

data MyCommand :: Command Party ChannelState where

Example command data type of kind Command Party ChannelState.

Constructors

Create :: MyCommand '(Recipient, None, Ready) '(Broker, None, Ready) ()

Notify :: MyCommand '(Recipient, Ready, Ready) '(Sender, None, Ready) ()

Send :: String -> MyCommand '(Sender, Ready, Ready) '(Broker, Ready, Busy) ()

Forward :: MyCommand '(Broker, Busy, Ready) '(Recipient, Ready, Ready) String

scenario :: String -> MyProtocol '[None, None, None] '[Ready, Ready, Ready] String

Example protocol scenario.

If you modify this scenario to Send before channel is Created or to Send two messages in a row without forwarding them, the scenario will not compile.

data Party

Constructors

Recipient

Broker

Sender

Instances

Eq Party

Defined in Control.Protocol.Example

Methods

(==) :: Party -> Party -> Bool

(/=) :: Party -> Party -> Bool

Show Party

Defined in Control.Protocol.Example

Methods

showsPrec :: Int -> Party -> ShowS

show :: Party -> String

showList :: [Party] -> ShowS

PShow Party

Defined in Control.Protocol.Example

Associated Types

type ShowsPrec arg arg1 arg2 :: Symbol

type Show_ arg :: Symbol

type ShowList arg arg1 :: Symbol

SShow Party

Defined in Control.Protocol.Example

Methods

sShowsPrec :: Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply ShowsPrecSym0 t1) t2) t3)

sShow_ :: Sing t -> Sing (Apply Show_Sym0 t)

sShowList :: Sing t1 -> Sing t2 -> Sing (Apply (Apply ShowListSym0 t1) t2)

SEq Party

Defined in Control.Protocol.Example

Methods

(%==) :: Sing a -> Sing b -> Sing (a == b)

(%/=) :: Sing a -> Sing b -> Sing (a /= b)

PEq Party

Defined in Control.Protocol.Example

Associated Types

type x == y :: Bool

type x /= y :: Bool

SDecide Party

Defined in Control.Protocol.Example

Methods

(%~) :: Sing a -> Sing b -> Decision (a :~: b)

SingKind Party

Defined in Control.Protocol.Example

Associated Types

type Demote Party = (r :: Type)

Methods

fromSing :: Sing a -> Demote Party

toSing :: Demote Party -> SomeSing Party

SingI Recipient

Defined in Control.Protocol.Example

Methods

sing :: Sing Recipient

SingI Broker

Defined in Control.Protocol.Example

Methods

sing :: Sing Broker

SingI Sender

Defined in Control.Protocol.Example

Methods

sing :: Sing Sender

Show (Sing z)

Defined in Control.Protocol.Example

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

data Sing (a :: Party)

Defined in Control.Protocol.Example

data Sing (a :: Party) where

• SRecipient :: forall (a :: Party). Sing Recipient
• SBroker :: forall (a :: Party). Sing Broker
• SSender :: forall (a :: Party). Sing Sender

type Demote Party

Defined in Control.Protocol.Example

type Demote Party = Party

type Show_ (arg :: Party)

Defined in Control.Protocol.Example

type Show_ (arg :: Party) = Apply (Show__6989586621680262835Sym0 :: TyFun Party Symbol -> Type) arg

type ShowList (arg :: [Party]) arg1

Defined in Control.Protocol.Example

type ShowList (arg :: [Party]) arg1 = Apply (Apply (ShowList_6989586621680262846Sym0 :: TyFun [Party] (Symbol ~> Symbol) -> Type) arg) arg1

type (x :: Party) /= (y :: Party)

Defined in Control.Protocol.Example

type (x :: Party) /= (y :: Party) = Not (x == y)

type (a :: Party) == (b :: Party)

Defined in Control.Protocol.Example

type (a :: Party) == (b :: Party)

type ShowsPrec a1 (a2 :: Party) a3

Defined in Control.Protocol.Example

type ShowsPrec a1 (a2 :: Party) a3

data ChannelState

Example type defining the possible resource states, in this case some communication channel.

Constructors

None

Ready

Busy

Instances

Eq ChannelState

Defined in Control.Protocol.Example

Methods

(==) :: ChannelState -> ChannelState -> Bool

(/=) :: ChannelState -> ChannelState -> Bool

Show ChannelState

Defined in Control.Protocol.Example

Methods

showsPrec :: Int -> ChannelState -> ShowS

show :: ChannelState -> String

showList :: [ChannelState] -> ShowS