Safe Haskell	None
Language	Haskell2010

Network.TypedProtocol.Pipelined

Synopsis

data PeerPipelined ps (pr :: PeerRole ) (st :: ps) m a where
- PeerPipelined :: PeerSender ps pr st Z c m a -> PeerPipelined ps pr st m a
data PeerSender ps (pr :: PeerRole ) (st :: ps) (n :: Outstanding ) c m a where
- SenderEffect :: m ( PeerSender ps pr st n c m a) -> PeerSender ps pr st n c m a
- SenderDone :: !( NobodyHasAgency st) -> a -> PeerSender ps pr st Z c m a
- SenderYield :: !( WeHaveAgency pr st) -> Message ps st st' -> PeerSender ps pr st' Z c m a -> PeerSender ps pr st Z c m a
- SenderAwait :: !( TheyHaveAgency pr st) -> ( forall st'. Message ps st st' -> PeerSender ps pr st' Z c m a) -> PeerSender ps pr st Z c m a
- 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
- SenderCollect :: Maybe ( 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
data PeerReceiver ps (pr :: PeerRole ) (st :: ps) (stdone :: ps) m c where
- 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) -> ( forall st'. Message ps st st' -> PeerReceiver ps pr st' stdone m c) -> PeerReceiver ps pr st stdone m c
type Outstanding = N
data N
- = Z
- | S N
data Nat (n :: N ) where
- pattern Zero :: () => Z ~ n => Nat n
- pattern Succ :: () => m ~ S n => Nat n -> Nat m
natToInt :: Nat n -> Int
unsafeIntToNat :: Int -> Nat n
fmapPeerPipelined :: ( forall 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

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

PeerPipelined :: PeerSender 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 Source # (<$) :: a -> PeerPipelined ps pr st m b -> PeerPipelined ps pr st m a Source #

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) -> ( forall 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.
SenderCollect :: Maybe ( 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 Source # (<$) :: a -> PeerSender ps pr st n c m b -> PeerSender ps pr st n c m a Source #

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) -> ( forall 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 showsPrec :: Int -> Nat n -> ShowS Source # show :: Nat n -> String Source # showList :: [ Nat n] -> ShowS Source #

natToInt :: Nat n -> Int Source #

unsafeIntToNat :: Int -> Nat n Source #

fmapPeerPipelined :: ( forall 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.