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
- data Nat (n :: N ) where
- 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
Functor m => Functor ( PeerPipelined ps pr st m) Source # | |
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 ::
records the number of outstanding pipelined responses. Note that when this isOutstanding
)Z
then we have no such outstanding responses, and we are in an equivalent situation to a normal non-pipelinedPeer
-
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 | |
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 |
A normal non-pipelined
Note that we cannot mix pipelined and normal synchronous syle, so this can only be used when there are no outstanding pipelined responses.
The
|
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
Note that we cannot mix pipelined and normal synchronous syle, so this can only be used when there are no outstanding pipelined responses.
The
|
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
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:
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
Functor m => Functor ( PeerSender ps pr st n c m) Source # | |
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 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.
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.