Safe Haskell  None 

Language  Haskell2010 
Synopsis

data
Codec
ps failure m bytes =
Codec
{
 encode :: forall (pr :: PeerRole ) (st :: ps) (st' :: ps). PeerHasAgency pr st > Message ps st st' > bytes
 decode :: forall (pr :: PeerRole ) (st :: ps). PeerHasAgency pr st > m ( DecodeStep bytes failure m ( SomeMessage st))
 hoistCodec :: Functor n => ( forall x. m x > n x) > Codec ps failure m bytes > Codec ps failure n bytes
 isoCodec :: Functor m => (bytes > bytes') > (bytes' > bytes) > Codec ps failure m bytes > Codec ps failure m bytes'
 mapFailureCodec :: Functor m => (failure > failure') > Codec ps failure m bytes > Codec ps failure' m bytes
 data PeerRole

data
PeerHasAgency
(pr ::
PeerRole
) (st :: ps)
where
 ClientAgency :: !( ClientHasAgency st) > PeerHasAgency AsClient st
 ServerAgency :: !( ServerHasAgency st) > PeerHasAgency AsServer st
 type WeHaveAgency (pr :: PeerRole ) st = PeerHasAgency pr st
 type TheyHaveAgency (pr :: PeerRole ) st = PeerHasAgency ( FlipAgency pr) st

data
SomeMessage
(st :: ps)
where
 SomeMessage :: Message ps st st' > SomeMessage st
 data CodecFailure

data
DecodeStep
bytes failure m a
 = DecodePartial ( Maybe bytes > m ( DecodeStep bytes failure m a))
  DecodeDone a ( Maybe bytes)
  DecodeFail failure
 runDecoder :: Monad m => [bytes] > DecodeStep bytes failure m a > m ( Either failure a)
 runDecoderPure :: Monad m => ( forall b. m b > b) > m ( DecodeStep bytes failure m a) > [bytes] > Either failure a

data
AnyMessage
ps
where
 AnyMessage :: Message ps st st' > AnyMessage ps

data
AnyMessageAndAgency
ps
where
 AnyMessageAndAgency :: PeerHasAgency pr (st :: ps) > Message ps (st :: ps) (st' :: ps) > AnyMessageAndAgency ps
 prop_codecM :: forall ps failure m bytes. ( Monad m, Eq ( AnyMessage ps)) => Codec ps failure m bytes > AnyMessageAndAgency ps > m Bool
 prop_codec :: forall ps failure m bytes. ( Monad m, Eq ( AnyMessage ps)) => ( forall a. m a > a) > Codec ps failure m bytes > AnyMessageAndAgency ps > Bool
 prop_codec_splitsM :: forall ps failure m bytes. ( Monad m, Eq ( AnyMessage ps)) => (bytes > [[bytes]]) > Codec ps failure m bytes > AnyMessageAndAgency ps > m Bool
 prop_codec_splits :: forall ps failure m bytes. ( Monad m, Eq ( AnyMessage ps)) => (bytes > [[bytes]]) > ( forall a. m a > a) > Codec ps failure m bytes > AnyMessageAndAgency ps > Bool
 prop_codec_binary_compatM :: forall psA psB failure m bytes. ( Monad m, Eq ( AnyMessage psA)) => Codec psA failure m bytes > Codec psB failure m bytes > ( forall pr (stA :: psA). PeerHasAgency pr stA > SamePeerHasAgency pr psB) > AnyMessageAndAgency psA > m Bool
 prop_codec_binary_compat :: forall psA psB failure m bytes. ( Monad m, Eq ( AnyMessage psA)) => ( forall a. m a > a) > Codec psA failure m bytes > Codec psB failure m bytes > ( forall pr (stA :: psA). PeerHasAgency pr stA > SamePeerHasAgency pr psB) > AnyMessageAndAgency psA > Bool
 prop_codecs_compatM :: forall ps failure m bytes. ( Monad m, Eq ( AnyMessage ps), forall a. Monoid a => Monoid (m a)) => Codec ps failure m bytes > Codec ps failure m bytes > AnyMessageAndAgency ps > m Bool
 prop_codecs_compat :: forall ps failure m bytes. ( Monad m, Eq ( AnyMessage ps), forall a. Monoid a => Monoid (m a)) => ( forall a. m a > a) > Codec ps failure m bytes > Codec ps failure m bytes > AnyMessageAndAgency ps > Bool

data
SamePeerHasAgency
(pr ::
PeerRole
) (ps ::
Type
)
where
 SamePeerHasAgency :: forall (pr :: PeerRole ) ps (st :: ps). PeerHasAgency pr st > SamePeerHasAgency pr ps
Defining and using Codecs
data Codec ps failure m bytes Source #
A codec for a
Protocol
handles the encoding and decoding of typed
protocol messages. This is typically used when sending protocol messages
over untyped channels. The codec chooses the exact encoding, for example
encoding in some textbased syntax, or some choice of binary format.
The codec is parametrised by:
 The protocol
 The peer role (client/server)
 the type of decoding failures
 the monad in which the decoder runs
 the type of the encoded data (typically strings or bytes)
It is expected that typical codec implementations will be polymorphic in the peer role. For example a codec for the ping/pong protocol might have type:
codecPingPong :: forall m. Monad m => Codec PingPong String m String
A codec consists of a message encoder and a decoder.
The encoder is supplied both with the message to encode and the current protocol state (matching the message). The protocol state can be either a client or server state, but for either peer role it is a protocol state in which the peer has agency, since those are the only states where a peer needs to encode a message to be able to send it.
For example a simple text encoder for the ping/pong protocol could be:
encode :: WeHaveAgency pr st > Message PingPong st st' > String encode (ClientAgency TokIdle) MsgPing = "ping\n" encode (ClientAgency TokIdle) MsgDone = "done\n" encode (ServerAgency TokBusy) MsgPong = "pong\n"
The decoder is also given the current protocol state and it is expected to be able to decode any message that is valid in that state, but only messages that are valid in that state. Messages that are unexpected for the current state should be treated like any other decoding format error.
While the current protocol state is known, the state that the message will
have the peer transition to is not known. For this reason the decoded
message is wrapped in the
SomeMessage
constructor which hides the "to"
state.
The decoder uses an incremental decoding interface
DecodeStep
so that
input can be supplied (e.g. from a Channel) bit by bit. This style of
decoder allows but does not require a format with message framing where the
decoder input matches exactly with the message boundaries.
decode :: TheyHaveAgency pr st > m (DecodeStep String String m (SomeMessage st)) decode stok = decodeTerminatedFrame '\n' $ \str trailing > case (stok, str) of (ServerAgency TokBusy, "pong") > DecodeDone (SomeMessage MsgPong) trailing (ClientAgency TokIdle, "ping") > DecodeDone (SomeMessage MsgPing) trailing (ClientAgency TokIdle, "done") > DecodeDone (SomeMessage MsgDone) trailing _ > DecodeFail ("unexpected message: " ++ str)
The main thing to note is the pattern matching on the combination of the message string and the protocol state. This neatly fulfils the requirement that we only return messages that are of the correct type for the given protocol state.
This toy example format uses newlines
n
as a framing format. See
DecodeStep
for suggestions on how to use it for more realistic formats.
Codec  

hoistCodec :: Functor n => ( forall x. m x > n x) > Codec ps failure m bytes > Codec ps failure n bytes Source #
isoCodec :: Functor m => (bytes > bytes') > (bytes' > bytes) > Codec ps failure m bytes > Codec ps failure m bytes' Source #
mapFailureCodec :: Functor m => (failure > failure') > Codec ps failure m bytes > Codec ps failure' m bytes Source #
Related types
Types for client and server peer roles. As protocol can be viewed from either client or server side.
Note that technically "client" and "server" are arbitrary labels. The framework is completely symmetric between the two peers.
This definition is only used as promoted types and kinds, never as values.
data PeerHasAgency (pr :: PeerRole ) (st :: ps) where Source #
This data type is used to hold state tokens for states with either client
or server agency. This GADT shows up when writing protocol peers, when
Yield
ing or
Await
ing, and when writing message encoders/decoders.
ClientAgency :: !( ClientHasAgency st) > PeerHasAgency AsClient st  
ServerAgency :: !( ServerHasAgency st) > PeerHasAgency AsServer st 
Instances
( forall (st' :: ps). Show ( ClientHasAgency st'), forall (st' :: ps). Show ( ServerHasAgency st')) => Show ( PeerHasAgency pr st) Source #  
Defined in Network.TypedProtocol.Core 
type WeHaveAgency (pr :: PeerRole ) st = PeerHasAgency pr st Source #
A synonym for an state token in which "our" peer has agency. This is parametrised over the client or server roles. In either case the peer in question has agency.
This shows up when we are sending messages, or dealing with encoding outgoing messages.
type TheyHaveAgency (pr :: PeerRole ) st = PeerHasAgency ( FlipAgency pr) st Source #
A synonym for an state token in which the other peer has agency. This is parametrised over the client or server roles. In either case the other peer has agency.
This shows up when we are receiving messages, or dealing with decoding incoming messages.
data SomeMessage (st :: ps) where Source #
When decoding a
Message
we only know the expected "from" state. We
cannot know the "to" state as this depends on the message we decode. To
resolve this we use the
SomeMessage
wrapper which uses an existential
type to hide the "to" state.
SomeMessage :: Message ps st st' > SomeMessage st 
data CodecFailure Source #
Each
Codec
can use whatever
failure
type is appropriate. This simple
exception type is provided for use by simple codecs (e.g. "identity") when
nothing more than a
String
is needed. It is an instance of
Exception
.
Instances
Eq CodecFailure Source #  
Defined in Network.TypedProtocol.Codec (==) :: CodecFailure > CodecFailure > Bool Source # (/=) :: CodecFailure > CodecFailure > Bool Source # 

Show CodecFailure Source #  
Defined in Network.TypedProtocol.Codec 

Exception CodecFailure Source #  
Defined in Network.TypedProtocol.Codec 
Incremental decoding
data DecodeStep bytes failure m a Source #
An incremental decoder with return a value of type
a
.
This interface is not designed to be used directly for implementing decoders, only for running them. In real applications it is expected to use libraries for text or binary decoding and to implement appropriate wrappers to match up with this incremental decoder interface.
This style of interface already closely matches that provided by libraries
such as
attoparsec
for text formats, and
binary
,
cereal
and
cborg
for binary formats.
DecodePartial ( Maybe bytes > m ( DecodeStep bytes failure m a)) 
The decoder has consumed the available input and needs more
to continue. Provide

DecodeDone a ( Maybe bytes) 
The decoder has successfully finished. This provides the decoded result value plus any unused input. 
DecodeFail failure 
The decoder ran into an error. The decoder either used

runDecoder :: Monad m => [bytes] > DecodeStep bytes failure m a > m ( Either failure a) Source #
Run a codec incremental decoder
DecodeStep
against a list of input.
It ignores any unused trailing data. This is useful for demos, quick experiments and tests.
See also
runDecoderWithChannel
runDecoderPure :: Monad m => ( forall b. m b > b) > m ( DecodeStep bytes failure m a) > [bytes] > Either failure a Source #
A variant of
runDecoder
that is suitable for "pure" monads that have
a run function. This includes
ST
, using
runST
.
Codec properties
data AnyMessage ps where Source #
Any message for a protocol, without knowing the protocol state.
Used at least for
Eq
instances for messages, but also as a target for an
identity codec `Codec ps failure m (AnyMessage ps)` .
AnyMessage :: Message ps st st' > AnyMessage ps 
Instances
( forall (st :: ps) (st' :: ps). Show ( Message ps st st')) => Show ( AnyMessage ps) Source #  
Defined in Network.TypedProtocol.Codec 
data AnyMessageAndAgency ps where Source #
Used to hold the
PeerHasAgency
state token and a corresponding
Message
.
Used where we don't know statically what the state type is, but need the agency and message to match each other.
AnyMessageAndAgency :: PeerHasAgency pr (st :: ps) > Message ps (st :: ps) (st' :: ps) > AnyMessageAndAgency ps 
Instances
( forall (st :: ps). Show ( ClientHasAgency st), forall (st :: ps). Show ( ServerHasAgency st), forall (st :: ps) (st' :: ps). Show ( Message ps st st')) => Show ( AnyMessageAndAgency ps) Source #  
Defined in Network.TypedProtocol.Codec 
prop_codecM :: forall ps failure m bytes. ( Monad m, Eq ( AnyMessage ps)) => Codec ps failure m bytes > AnyMessageAndAgency ps > m Bool Source #
The
Codec
roundtrip property: decode after encode gives the same
message. Every codec must satisfy this property.
prop_codec :: forall ps failure m bytes. ( Monad m, Eq ( AnyMessage ps)) => ( forall a. m a > a) > Codec ps failure m bytes > AnyMessageAndAgency ps > Bool Source #
The
Codec
roundtrip property in a pure monad.
:: forall ps failure m bytes. ( Monad m, Eq ( AnyMessage ps))  
=> (bytes > [[bytes]]) 
alternative rechunkings of serialised form 
> Codec ps failure m bytes  
> AnyMessageAndAgency ps  
> m Bool 
A variant on the codec roundtrip property: given the encoding of a message, check that decode always gives the same result irrespective of how the chunks of input are fed to the incremental decoder.
This property guards against boundary errors in incremental decoders. It is not necessary to check this for every message type, just for each generic codec construction. For example given some binary serialisation library one would write a generic adaptor to the codec interface. This adaptor has to deal with the incremental decoding and this is what needs to be checked.
prop_codec_splits :: forall ps failure m bytes. ( Monad m, Eq ( AnyMessage ps)) => (bytes > [[bytes]]) > ( forall a. m a > a) > Codec ps failure m bytes > AnyMessageAndAgency ps > Bool Source #
Like
but run in a pure monad
prop_codec_splitsM
m
, e.g.
Identity
.
prop_codec_binary_compatM Source #
:: forall psA psB failure m bytes. ( Monad m, Eq ( AnyMessage psA))  
=> Codec psA failure m bytes  
> Codec psB failure m bytes  
> ( forall pr (stA :: psA). PeerHasAgency pr stA > SamePeerHasAgency pr psB) 
The states of A map directly of states of B. 
> AnyMessageAndAgency psA  
> m Bool 
Binary compatibility of two protocols
We check the following property:

Using codec A, we encode a message of protocol
psA
tobytes
. 
When we decode those
bytes
using codec B, we get a message of protocolps
B. 
When we encode that message again using codec B, we get
bytes
. 
When we decode those
bytes
using codec A, we get the original message again.
prop_codec_binary_compat :: forall psA psB failure m bytes. ( Monad m, Eq ( AnyMessage psA)) => ( forall a. m a > a) > Codec psA failure m bytes > Codec psB failure m bytes > ( forall pr (stA :: psA). PeerHasAgency pr stA > SamePeerHasAgency pr psB) > AnyMessageAndAgency psA > Bool Source #
Like
but run in a pure monad
prop_codec_splitsM
m
, e.g.
Identity
.
prop_codecs_compatM :: forall ps failure m bytes. ( Monad m, Eq ( AnyMessage ps), forall a. Monoid a => Monoid (m a)) => Codec ps failure m bytes > Codec ps failure m bytes > AnyMessageAndAgency ps > m Bool Source #
Compatibility between two codecs of the same protocol. Encode a message with one codec and decode it with the other one, then compare if the result is the same as initial message.
prop_codecs_compat :: forall ps failure m bytes. ( Monad m, Eq ( AnyMessage ps), forall a. Monoid a => Monoid (m a)) => ( forall a. m a > a) > Codec ps failure m bytes > Codec ps failure m bytes > AnyMessageAndAgency ps > Bool Source #
Like
but run in a pure monad
prop_codecs_compatM
m
, e.g.
Identity
.
data SamePeerHasAgency (pr :: PeerRole ) (ps :: Type ) where Source #
Auxiliary definition for
prop_codec_binary_compatM
.
Used for the existential
st :: ps
parameter when expressing that for each
value of
PeerHasAgency
for protocol A, there is a corresponding
PeerHasAgency
for protocol B of some
st :: ps
.
SamePeerHasAgency :: forall (pr :: PeerRole ) ps (st :: ps). PeerHasAgency pr st > SamePeerHasAgency pr ps 