Moduletyped-protocols-1.2.2.0

Network.TypedProtocol.Peer.Server

Synopsis

pattern Await
pattern AwaitLookahead
pattern Collect
pattern Done
pattern Effect
pattern FlushSender
pattern ReceiverAwait
pattern ReceiverDone
pattern ReceiverEffect
pattern SenderDone
pattern SenderEffect
pattern SenderYield
pattern ServerLookaheadFixedSender
pattern TheSender
pattern Yield
pattern YieldPipelined
data IsPipelined
data N
newtype Nat
pattern Succ
pattern Zero
family Outstanding
family OutstandingSenders
data SenderVariability
data PeerLookahead
pattern ServerLookahead
value runServerLookahead
data PeerPipelined
pattern ServerPipelined
value runServerPipelined
type Receiver
type Sender
type Server
type ServerLookahead
type ServerLookaheadFixedSender
type ServerPipelined

Packagetyped-protocols-1.2.2.0
Exports36
LicenceApache-2.0

pattern

pattern Await :: () => (StateTokenI st, StateAgency st ~ 'ClientAgency, Outstanding pl ~ 'Z, OutstandingSenders pl ~ 'Z) => (forall (st' :: ps). Message ps st st' -> Server ps pl st' m a) -> Server ps pl st m a

pattern

pattern AwaitLookahead :: () => (StateTokenI st, StateTokenI st', ActiveState st, StateAgency st' ~ 'ClientAgency) => Sender ps sv st st' m -> (forall (st'' :: ps). Message ps st' st'' -> Server ps ('Lookahead ('S n) sv) st'' m a) -> Server ps ('Lookahead n sv) st m a

pattern

pattern Collect :: () => (StateTokenI st, ActiveState st) => Maybe (Server ps ('Pipelined ('S n) c) st m a) -> (c -> Server ps ('Pipelined n c) st m a) -> Server ps ('Pipelined ('S n) c) st m a

pattern

pattern Done :: () => (StateTokenI st, StateAgency st ~ 'NobodyAgency, Outstanding pl ~ 'Z, OutstandingSenders pl ~ 'Z) => a -> Server ps pl st m a

patternpattern Effect :: m (Server ps pl st m a) -> Server ps pl st m a

pattern

pattern FlushSender :: () => StateTokenI st => Maybe (Server ps ('Lookahead ('S n) sv) st m a) -> Server ps ('Lookahead n sv) st m a -> Server ps ('Lookahead ('S n) sv) st m a

pattern

pattern ReceiverAwait :: () => (StateTokenI st, ActiveState st, StateAgency st ~ 'ClientAgency) => (forall (st' :: ps). Message ps st st' -> Receiver ps st' stdone m c) -> Receiver ps st stdone m c

patternpattern ReceiverDone :: c -> Receiver ps stdone stdone m c

patternpattern ReceiverEffect :: m (Receiver ps st stdone m c) -> Receiver ps st stdone m c

patternpattern SenderDone :: Sender ps 'VariableSender stdone stdone m

patternpattern SenderEffect :: m (Sender ps 'VariableSender st stdone m) -> Sender ps 'VariableSender st stdone m

pattern

pattern SenderYield :: () => (StateTokenI st, StateTokenI st', StateAgency st ~ 'ServerAgency) => Message ps st st' -> Sender ps 'VariableSender st' stdone m -> Sender ps 'VariableSender st stdone m

pattern

pattern ServerLookaheadFixedSender :: Sender ps 'VariableSender apst apst' m -> Server ps ('Lookahead 'Z ('FixedSender apst apst')) st m a -> ServerLookaheadFixedSender ps st m a

patternpattern TheSender :: () => sv ~ 'FixedSender st stdone => Sender ps sv st stdone m

pattern

pattern Yield :: () => (StateTokenI st, StateTokenI st', StateAgency st ~ 'ServerAgency, Outstanding pl ~ 'Z, OutstandingSenders pl ~ 'Z) => Message ps st st' -> Server ps pl st' m a -> Server ps pl st m a

pattern

pattern YieldPipelined :: () => (StateTokenI st, StateTokenI st', StateAgency st ~ 'ServerAgency) => Message ps st st' -> Receiver ps st' st'' m c -> Server ps ('Pipelined ('S n) c) st'' m a -> Server ps ('Pipelined n c) st m a

datadata IsPipelined ps where

Constructors

Pipelined :: N -> Type -> IsPipelined ps
NonPipelined :: IsPipelined ps
Lookahead :: N -> SenderVariability ps -> IsPipelined ps

datadata N

Constructors

Z
S N

newtypenewtype Nat (n :: N)

Instances1Show

Show (Nat n)Defined in typed-protocols-1.2.2.0 · Network.TypedProtocol.Core

patternpattern Succ :: () => m ~ 'S n => Nat n -> Nat m

patternpattern Zero :: () => 'Z ~ n => Nat n

familytype family Outstanding (pl :: IsPipelined ps) :: N where

Equations

familytype family OutstandingSenders (pl :: IsPipelined ps) :: N where

Equations

OutstandingSenders 'NonPipelined = 'Z
OutstandingSenders ('Pipelined _1 _2) = 'Z
OutstandingSenders ('Lookahead n _1) = n

datadata SenderVariability ps where

Constructors

VariableSender :: SenderVariability ps
FixedSender :: ps -> ps -> SenderVariability ps

datadata PeerLookahead ps (pr :: PeerRole) (st :: ps) (m :: Type -> Type) a where

Instances1Functor

Functor m => Functor (PeerLookahead ps pr st m)Defined in typed-protocols-1.2.2.0 · Network.TypedProtocol.Peer

patternpattern ServerLookahead :: Server ps ('Lookahead 'Z 'VariableSender) st m a -> ServerLookahead ps st m a

valuerunServerLookahead

:: ServerLookahead ps st m a
-> Server ps ('Lookahead 'Z 'VariableSender) st m a

datadata PeerPipelined ps (pr :: PeerRole) (st :: ps) (m :: Type -> Type) a where

Instances1Functor

Functor m => Functor (PeerPipelined ps pr st m)Defined in typed-protocols-1.2.2.0 · Network.TypedProtocol.Peer

patternpattern ServerPipelined :: Server ps ('Pipelined 'Z c) st m a -> ServerPipelined ps st m a

valuerunServerPipelined :: ()

typetype Receiver ps (st :: ps) (stdone :: ps) (m :: Type -> Type) c = Receiver ps 'AsServer st stdone m c

type

type Sender ps (sv :: SenderVariability ps) (st :: ps) (stdone :: ps) (m :: Type -> Type) = Sender ps 'AsServer sv st stdone m

typetype Server ps (pl :: IsPipelined ps) (st :: ps) (m :: Type -> Type) a = Peer ps 'AsServer pl st m a

typetype ServerLookahead ps (st :: ps) (m :: Type -> Type) a = PeerLookahead ps 'AsServer st m a

typetype ServerLookaheadFixedSender ps (st :: ps) (m :: Type -> Type) a = PeerLookaheadFixedSender ps 'AsServer st m a

typetype ServerPipelined ps (st :: ps) (m :: Type -> Type) a = PeerPipelined ps 'AsServer st m a