| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Network.TypedProtocol.Stateful.Peer
Synopsis
- data Peer ps (pr :: PeerRole) (st :: ps) (f :: ps -> Type) (m :: Type -> Type) a where
- Effect :: forall ps (pr :: PeerRole) (st :: ps) (f :: ps -> Type) (m :: Type -> Type) a. m (Peer ps pr st f m a) -> Peer ps pr st f m a
- Yield :: forall ps (pr :: PeerRole) (st :: ps) (st' :: ps) (f :: ps -> Type) (m :: Type -> Type) a. (StateTokenI st, StateTokenI st', ActiveState st) => WeHaveAgencyProof pr st -> f st' -> Message ps st st' -> Peer ps pr st' f m a -> Peer ps pr st f m a
- Await :: forall ps (pr :: PeerRole) (st :: ps) (f :: ps -> Type) (m :: Type -> Type) a. (StateTokenI st, ActiveState st) => TheyHaveAgencyProof pr st -> (forall (st' :: ps). f st -> Message ps st st' -> (Peer ps pr st' f m a, f st')) -> Peer ps pr st f m a
- Done :: forall ps (pr :: PeerRole) (st :: ps) (f :: ps -> Type) (m :: Type -> Type) a. (StateTokenI st, StateAgency st ~ 'NobodyAgency) => NobodyHasAgencyProof pr st -> a -> Peer ps pr st f m a
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 monad in which the peer operates; and
- the type of any final result once the peer terminates.
For example:
pingPongClientExample :: Peer PingPong AsClient StIdle m () pingPongServerExample :: Peer PingPong AsServer StIdle m Int
The actions that a peer can take are:
- to perform local monadic effects
- to terminate with a result (but only in a terminal protocol state)
- to send a message (but only in a protocol state in which we have agency)
- to 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 |
| Yield | Send a message to the other peer and then continue. This 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 MsgPing $ ... |
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 Example: Await ReflClientAgency $ \msg -> case msg of MsgDone -> ... MsgPing -> ... |
Fields
| |
| Done | Terminate with a result. A state token must be provided from the
Example: Yield ReflClientAgency
MsgDone
(Done ReflNobodyAgency TokDone result) |
Fields
| |