typed-protocols-examples
Safe HaskellNone
LanguageHaskell2010

Network.TypedProtocol.PingPong.Client

Synopsis

Normal client

data PingPongClient (m :: Type -> Type) a where Source #

A ping-pong client, on top of some effect m.

At each step the client has a choice: ping or stop.

This type encodes the pattern of state transitions the client can go through. For the ping/pong case this is trivial. We start from one main state, issue a ping and move into a state where we expect a single response, bringing us back to the same main state.

If we had another state in which a different set of options were available then we would need a second type like this. The two would be mutually recursive if we can get in both directions, or perhaps just one way such as a special initialising state or special terminating state.

Constructors

SendMsgPing :: forall (m :: Type -> Type) a. m (PingPongClient m a) -> PingPongClient m a

Choose to go for sending a ping message. The ping has no body so all we have to provide here is a continuation for the single legal reply message.

SendMsgDone :: forall a (m :: Type -> Type). a -> PingPongClient m a

Choose to terminate the protocol. This is an actual but nullary message, we terminate with the local result value. So this ends up being much like return in this case, but in general the termination is a message that can communicate final information.

pingPongClientPeer :: forall (m :: Type -> Type) a. Functor m => PingPongClient m a -> Client PingPong 'NonPipelined 'StIdle m a Source #

Interpret a particular client action sequence into the client side of the PingPong protocol.

Pipelined client

data PingPongClientPipelined c (m :: Type -> Type) a where Source #

A ping-pong client designed for running the PingPong protocol in a pipelined way.

Constructors

PingPongClientPipelined :: forall c (m :: Type -> Type) a. PingPongClientIdle 'Z c m a -> PingPongClientPipelined c m a

A PingPongSender, but starting with zero outstanding pipelined responses, and for any internal collect type c.

data PingPongClientIdle (n :: N) c (m :: Type -> Type) a where Source #

Constructors

SendMsgPingPipelined :: forall (m :: Type -> Type) c (n :: N) a. m c -> PingPongClientIdle ('S n) c m a -> PingPongClientIdle n c m a

Send a Ping message but alike in PingPongClient do not await for the response, instead supply a monadic action which will run on a received Pong message.

CollectPipelined :: forall (n1 :: N) c (m :: Type -> Type) a. Maybe (PingPongClientIdle ('S n1) c m a) -> (c -> PingPongClientIdle n1 c m a) -> PingPongClientIdle ('S n1) c m a

Collect the result of a previous pipelined receive action.

This (optionally) provides two choices:

  • Continue without a pipelined result
  • Continue with a pipelined result, which allows to run a monadic action when MsgPong is received.

Since presenting the first choice is optional, this allows expressing both a blocking collect and a non-blocking collect. This allows implementations to express policies such as sending a short sequence of messages and then waiting for all replies, but also a maximum pipelining policy that keeps a large number of messages in flight but collects results eagerly.

SendMsgDonePipelined :: forall a c (m :: Type -> Type). a -> PingPongClientIdle 'Z c m a

Termination of the ping-pong protocol.

Note that all pipelined results must be collected before terminating.

pingPongClientPeerPipelined :: forall (m :: Type -> Type) c a. Functor m => PingPongClientPipelined c m a -> ClientPipelined PingPong 'StIdle m a Source #

Interpret a pipelined client as a pipelined Peer on the client side of the PingPong protocol.