Network.TypedProtocol · typed-protocols-1.2.2.0

SingI 'ClientAgencyDefined in typed-protocols-1.2.2.0 · Network.TypedProtocol.Core
SingI 'NobodyAgencyDefined in typed-protocols-1.2.2.0 · Network.TypedProtocol.Core
SingI 'ServerAgencyDefined in typed-protocols-1.2.2.0 · Network.TypedProtocol.Core
type Sing = SingAgencyDefined in typed-protocols-1.2.2.0 · Network.TypedProtocol.Core

familytype family FlipAgency (pr :: PeerRole) :: PeerRole where

#

Equations

FlipAgency 'AsClient = 'AsServer
FlipAgency 'AsServer = 'AsClient

classclass IsActiveState (st :: ps) (agency :: Agency) where

#

Methods

activeAgency :: ActiveAgency' st agency

Instances2IsActiveState

'ClientAgency ~ StateAgency st => IsActiveState st 'ClientAgencyDefined in typed-protocols-1.2.2.0 · Network.TypedProtocol.Core
'ServerAgency ~ StateAgency st => IsActiveState st 'ServerAgencyDefined in typed-protocols-1.2.2.0 · Network.TypedProtocol.Core

datadata IsPipelined ps where

#

Constructors

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

familydata family Message ps (st :: ps) (st' :: 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

#

type

type NobodyHasAgencyProof (pr :: PeerRole) (st :: ps) = ReflRelativeAgency (StateAgency st) 'NobodyHasAgency (Relative pr (StateAgency st))

#

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 PeerRole

#

AsClient AsServer

Instances3SingI, Sing

SingI 'AsClientDefined in typed-protocols-1.2.2.0 · Network.TypedProtocol.Core
SingI 'AsServerDefined in typed-protocols-1.2.2.0 · Network.TypedProtocol.Core
type Sing = SingPeerRoleDefined in typed-protocols-1.2.2.0 · Network.TypedProtocol.Core

classclass Protocol ps where

#

Associated types

data family Message ps (st :: ps) (st' :: ps)
type family StateAgency (st :: ps) :: Agency
type family StateToken :: ps -> Type

datadata ReflRelativeAgency (a :: Agency) (r :: RelativeAgency) (r' :: RelativeAgency) where

#

Constructors

ReflClientAgency :: ReflRelativeAgency 'ClientAgency r r
ReflServerAgency :: ReflRelativeAgency 'ServerAgency r r
ReflNobodyAgency :: ReflRelativeAgency 'NobodyAgency r r

familytype family Relative (pr :: PeerRole) (a :: Agency) :: RelativeAgency where

#

Equations

Relative 'AsClient 'ClientAgency = 'WeHaveAgency
Relative 'AsClient 'ServerAgency = 'TheyHaveAgency
Relative 'AsClient 'NobodyAgency = 'NobodyHasAgency
Relative 'AsServer 'ClientAgency = 'TheyHaveAgency
Relative 'AsServer 'ServerAgency = 'WeHaveAgency
Relative 'AsServer 'NobodyAgency = 'NobodyHasAgency

datadata RelativeAgency where

#

Constructors

datadata SenderVariability ps where

#

Constructors

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

datadata SingAgency (a :: Agency) where

#

Constructors

SingClientAgency :: SingAgency 'ClientAgency
SingServerAgency :: SingAgency 'ServerAgency
SingNobodyAgency :: SingAgency 'NobodyAgency

Instances1Show

Show (SingAgency a)Defined in typed-protocols-1.2.2.0 · Network.TypedProtocol.Core

datadata SingPeerRole (pr :: PeerRole) where

#

Constructors

SingAsClient :: SingPeerRole 'AsClient
SingAsServer :: SingPeerRole 'AsServer

Instances1Show

Show (SingPeerRole pr)Defined in typed-protocols-1.2.2.0 · Network.TypedProtocol.Core

familytype family StateAgency (st :: ps) :: Agency

#

familytype family StateToken :: ps -> Type

#

classclass StateTokenI (st :: ps) where

#

Methods

stateToken :: StateToken st

type

type TheyHaveAgencyProof (pr :: PeerRole) (st :: ps) = ReflRelativeAgency (StateAgency st) 'TheyHaveAgency (Relative pr (StateAgency st))

#

type

type WeHaveAgencyProof (pr :: PeerRole) (st :: ps) = ReflRelativeAgency (StateAgency st) 'WeHaveAgency (Relative pr (StateAgency st))

#

datadata Driver ps (pr :: PeerRole) dstate (m :: Type -> Type)

#

Constructors

Driver
- sendMessage :: forall (st :: ps) (st' :: ps). (StateTokenI st, StateTokenI st', ActiveState st) => WeHaveAgencyProof pr st -> Message ps st st' -> m ()
- recvMessage :: forall (st :: ps). (StateTokenI st, ActiveState st) => TheyHaveAgencyProof pr st -> dstate -> m (SomeMessage st, dstate)
- initialDState :: dstate

datadata SomeMessage (st :: ps) where

#

Constructors

SomeMessage :: (StateTokenI st, StateTokenI st', ActiveState st) => Message ps st st' -> SomeMessage st

datadata Queue (n :: N) a where

#

Constructors

EmptyQ :: Queue 'Z a
ConsQ :: a -> Queue n1 a -> Queue ('S n1) a

datadata TerminalStates ps where

#

Constructors

TerminalStates :: StateAgency st ~ 'NobodyAgency => StateToken st -> StateToken st -> TerminalStates ps