typed-protocols-stateful
Safe HaskellNone
LanguageHaskell2010

Network.TypedProtocol.Stateful.Peer

Description

Protocol stateful EDSL.

Note: Client and Server patterns are easier to use.

Synopsis

Documentation

data Peer ps (pr :: PeerRole) (st :: ps) (f :: ps -> Type) (m :: Type -> Type) a where Source #

A description of a peer that engages in a protocol.

The protocol describes what messages peers may send or must accept. A particular peer implementation decides what to actually do within the constraints of the protocol.

Peers engage in a protocol in either the client or server role. Of course the client role can only interact with the serve role for the same protocol and vice versa.

Peer has several type arguments:

  • the protocol itself;
  • the client/server role;
  • the current protocol state;
  • the local state type;
  • the monad in which the peer operates; and
  • the type of any final result once the peer terminates.

For example:

reqRespClientExample :: Peer (ReqResp FileAPI) AsClient StIdle State m ()
reqRespServerExample :: Peer (ReqResp FileAPI) AsServer StIdle State m Int

The actions that a peer can take are:

  • perform a local monadic effect,
  • terminate with a result (but only in a terminal protocol state),
  • send a message (but only in a protocol state in which we have agency),
  • wait to receive a message (but only in a protocol state in which the other peer has agency).

The Yield, Await and Done constructors require to provide an evidence that the appropriate peer has agency. This information is supplied using one of the constructors of ReflRelativeAgency.

While this evidence must be provided, the types guarantee that it is not possible to supply incorrect evidence. The Client or Server pattern synonyms provide this evidence automatically.

TODO: We are not exposing pipelined version, since it is not possible to write a driver & proofs in a type safe which take into account the state when the peer type only tracks depth of pipelining rather than pipelined transitions.

Constructors

Effect

Perform a local monadic effect and then continue.

Example:

Effect $ do
  ...          -- actions in the monad
  return $ ... -- another Peer value

Fields

  • :: forall ps (pr :: PeerRole) (st :: ps) (f :: ps -> Type) (m :: Type -> Type) a. m (Peer ps pr st f m a)

    monadic continuation

  • -> Peer ps pr st f m a
     
Yield

Send a message to the other peer and then continue. The constructor requires evidence that we have agency for this protocol state and thus are allowed to send messages. It takes local state associated to the source and target protocol state of the message that is sent. This state is only maintained locally, never shared remotely. It also takes the message and the continuation. It also requires evidence that we have agency for this protocol state and thus are allowed to send messages.

Example:

Yield ReflClientAgency (StateBusy (ReadFile /etc/os-release))
                       StateIdle
                     $ MsgResp "..."

Fields

Await

Waits to receive a message from the other peer and then continues. This takes the continuation that is supplied with the received message. It also requires evidence that the other peer has agency for this protocol state and thus we are expected to wait to receive messages.

Note that the continuation that gets supplied with the message must be prepared to deal with any message that is allowed in this protocol state. This is why the continuation must be polymorphic in the target state of the message (the third type argument of Message).

Example:

Await ReflClientAgency $ \f msg ->
case (f, msg) of
  (StateBusy (ReadFile path), MsgResp resp) ->
    ( _continuation
    , StateIdle
    )

Fields

Done

Terminate with a result. A state token must be provided from the NobodyHasAgency states, to show that this is a state in which we can terminate.

Example:

Yield ReflClientAgency
       MsgDone
      (Done ReflNobodyAgency TokDone result)

Fields

Instances

Instances details
Functor m => Functor (Peer ps pr st f m) Source # 
Instance details

Defined in Network.TypedProtocol.Stateful.Peer

Methods

fmap :: (a -> b) -> Peer ps pr st f m a -> Peer ps pr st f m b #

(<$) :: a -> Peer ps pr st f m b -> Peer ps pr st f m a #