typed-protocols-0.1.0.0: A framework for strongly typed protocols
Safe HaskellNone
LanguageHaskell2010

Network.TypedProtocol.Pipelined

Synopsis

Documentation

data PeerPipelined ps (pr ∷ PeerRole) (st ∷ ps) m a where Source #

A description of a peer that engages in a protocol in a pipelined fashion.

This is very much like Peer, and can work with the same protocol state machine descriptions, but allows the peer to pipeline the execution of the protocol.

This wraps a PeerSender, but works for any internal collect type c, and with the starting condition of zero outstanding pipelined responses.

Constructors

PeerPipelinedPeerSender ps pr st Z c m a → PeerPipelined ps pr st m a 

Instances

Instances details
Functor m ⇒ Functor (PeerPipelined ps pr st m) Source # 
Instance details

Defined in Network.TypedProtocol.Pipelined

Methods

fmap ∷ (a → b) → PeerPipelined ps pr st m a → PeerPipelined ps pr st m b #

(<$) ∷ a → PeerPipelined ps pr st m b → PeerPipelined ps pr st m a #

data PeerSender ps (pr ∷ PeerRole) (st ∷ ps) (n ∷ Outstanding) c m a where Source #

This is the pipelined variant of Peer.

In particular it has two extra type arguments:

  • (n :: Outstanding) records the number of outstanding pipelined responses. Note that when this is Z then we have no such outstanding responses, and we are in an equivalent situation to a normal non-pipelined Peer
  • c records the internal type of the pipelined responses.

Constructors

SenderEffect ∷ m (PeerSender ps pr st n c m a) → PeerSender ps pr st n c m a

Same idea as normal Peer Effect.

SenderDone ∷ !(NobodyHasAgency st) → a → PeerSender ps pr st Z c m a

Same idea as normal Peer Done.

SenderYield ∷ !(WeHaveAgency pr st) → Message ps st st' → PeerSender ps pr st' Z c m a → PeerSender ps pr st Z c m a

A normal non-pipelined Yield.

Note that we cannot mix pipelined and normal synchronous syle, so this can only be used when there are no outstanding pipelined responses.

The n ~ Z constraint provides the type level guarantees that there are no outstanding pipelined responses.

SenderAwait ∷ !(TheyHaveAgency pr st) → (∀ st'. Message ps st st' → PeerSender ps pr st' Z c m a) → PeerSender ps pr st Z c m a

A normal non-pipelined Await. Note that this can only be used .

Note that we cannot mix pipelined and normal synchronous syle, so this can only be used when there are no outstanding pipelined responses.

The n ~ Z constraint provides the type level guarantees that there are no outstanding pipelined responses.

SenderPipeline ∷ !(WeHaveAgency pr st) → Message ps st st' → PeerReceiver ps pr (st' ∷ ps) (st'' ∷ ps) m c → PeerSender ps pr (st'' ∷ ps) (S n) c m a → PeerSender ps pr (st ∷ ps) n c m a

A pipelined equivalent of Yield. The key difference is that instead of moving into the immediate next state st', the sender jumps directly to state st'' and a seperate PeerReceiver has to be supplied which will get from st' to st''. This sets up an outstanding pipelined receive. The queue of outstanding pipelined receive actions PeerReceiver are executed in order, as messages arrive from the remote peer.

The type records the fact that the number of outstanding pipelined responses increases by one.

SenderCollectMaybe (PeerSender ps pr (st ∷ ps) (S n) c m a) → (c → PeerSender ps pr (st ∷ ps) n c m a) → PeerSender ps pr (st ∷ ps) (S n) 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

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.

The type records the fact that when collecting a response, the number of outstanding pipelined responses decreases by one. The type also guarantees that it can only be used when there is at least one outstanding response.

Instances

Instances details
Functor m ⇒ Functor (PeerSender ps pr st n c m) Source # 
Instance details

Defined in Network.TypedProtocol.Pipelined

Methods

fmap ∷ (a → b) → PeerSender ps pr st n c m a → PeerSender ps pr st n c m b #

(<$) ∷ a → PeerSender ps pr st n c m b → PeerSender ps pr st n c m a #

data PeerReceiver ps (pr ∷ PeerRole) (st ∷ ps) (stdone ∷ ps) m c where Source #

Constructors

ReceiverEffect ∷ m (PeerReceiver ps pr st stdone m c) → PeerReceiver ps pr st stdone m c 
ReceiverDone ∷ c → PeerReceiver ps pr stdone stdone m c 
ReceiverAwait ∷ !(TheyHaveAgency pr st) → (∀ st'. Message ps st st' → PeerReceiver ps pr st' stdone m c) → PeerReceiver ps pr st stdone m c 

type Outstanding = N Source #

Type level count of the number of outstanding pipelined yields for which we have not yet collected a receiver result. Used in PeerSender to ensure SenderCollect is only used when there are outstanding results to collect, and to ensure SenderYield, SenderAwait and SenderDone are only used when there are none.

data N Source #

A type level inductive natural number.

Constructors

Z 
S N 

data Nat (n ∷ N) where Source #

A value level inductive natural number, indexed by the corresponding type level natural number N.

This is often needed when writing pipelined peers to be able to count the number of outstanding pipelined yields, and show to the type checker that SenderCollect and SenderDone are being used correctly.

Bundled Patterns

pattern Zero ∷ () ⇒ Z ~ n ⇒ Nat n 
pattern Succ ∷ () ⇒ m ~ S n ⇒ Nat n → Nat m 

Instances

Instances details
Show (Nat n) Source # 
Instance details

Defined in Network.TypedProtocol.Pipelined

Methods

showsPrecIntNat n → ShowS #

showNat n → String #

showList ∷ [Nat n] → ShowS #

natToIntNat n → Int Source #

fmapPeerPipelined ∷ (∀ c. PeerSender ps pr st Z c m a → PeerSender ps' pr st' Z c m b) → PeerPipelined ps pr st m a → PeerPipelined ps' pr st' m b Source #

More general than fmap, as it allows to change the protocol.