typed-protocols-0.1.0.0: A framework for strongly typed protocols
Safe HaskellNone
LanguageHaskell2010

Network.TypedProtocol.Codec

Synopsis

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 text-based 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.

Constructors

Codec 

Fields

hoistCodecFunctor n ⇒ (∀ x. m x → n x) → Codec ps failure m bytes → Codec ps failure n bytes Source #

isoCodecFunctor m ⇒ (bytes → bytes') → (bytes' → bytes) → Codec ps failure m bytes → Codec ps failure m bytes' Source #

mapFailureCodecFunctor m ⇒ (failure → failure') → Codec ps failure m bytes → Codec ps failure' m bytes Source #

Related types

data PeerRole Source #

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.

Constructors

AsClient 
AsServer 

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 Yielding or Awaiting, and when writing message encoders/decoders.

Instances

Instances details
(∀ (st' ∷ ps). Show (ClientHasAgency st'), ∀ (st' ∷ ps). Show (ServerHasAgency st')) ⇒ Show (PeerHasAgency pr st) Source # 
Instance details

Defined in Network.TypedProtocol.Core

Methods

showsPrecIntPeerHasAgency pr st → ShowS Source #

showPeerHasAgency pr st → String Source #

showList ∷ [PeerHasAgency pr st] → ShowS Source #

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.

Constructors

SomeMessageMessage 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.

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.

Constructors

DecodePartial (Maybe bytes → m (DecodeStep bytes failure m a))

The decoder has consumed the available input and needs more to continue. Provide Just if more input is available and Nothing otherwise, and you will get a new DecodeStep.

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 fail or was not provided enough input.

runDecoderMonad 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

runDecoderPureMonad m ⇒ (∀ 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)` .

Constructors

AnyMessageMessage ps st st' → AnyMessage ps 

Instances

Instances details
(∀ (st ∷ ps) (st' ∷ ps). Show (Message ps st st')) ⇒ Show (AnyMessage ps) Source # 
Instance details

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.

Constructors

AnyMessageAndAgencyPeerHasAgency pr (st ∷ ps) → Message ps (st ∷ ps) (st' ∷ ps) → AnyMessageAndAgency ps 

Instances

Instances details
(∀ (st ∷ ps). Show (ClientHasAgency st), ∀ (st ∷ ps). Show (ServerHasAgency st), ∀ (st ∷ ps) (st' ∷ ps). Show (Message ps st st')) ⇒ Show (AnyMessageAndAgency ps) Source # 
Instance details

Defined in Network.TypedProtocol.Codec

prop_codecM ∷ ∀ ps failure m bytes. (Monad m, Eq (AnyMessage ps)) ⇒ Codec ps failure m bytes → AnyMessageAndAgency ps → m Bool Source #

The Codec round-trip property: decode after encode gives the same message. Every codec must satisfy this property.

prop_codec ∷ ∀ ps failure m bytes. (Monad m, Eq (AnyMessage ps)) ⇒ (∀ a. m a → a) → Codec ps failure m bytes → AnyMessageAndAgency ps → Bool Source #

The Codec round-trip property in a pure monad.

prop_codec_splitsM Source #

Arguments

∷ ∀ ps failure m bytes. (Monad m, Eq (AnyMessage ps)) 
⇒ (bytes → [[bytes]])

alternative re-chunkings of serialised form

Codec ps failure m bytes 
AnyMessageAndAgency ps 
→ m Bool 

A variant on the codec round-trip 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 ∷ ∀ ps failure m bytes. (Monad m, Eq (AnyMessage ps)) ⇒ (bytes → [[bytes]]) → (∀ a. m a → a) → Codec ps failure m bytes → AnyMessageAndAgency ps → Bool Source #

Like prop_codec_splitsM but run in a pure monad m, e.g. Identity.

prop_codec_binary_compatM Source #

Arguments

∷ ∀ psA psB failure m bytes. (Monad m, Eq (AnyMessage psA)) 
Codec psA failure m bytes 
Codec psB failure m bytes 
→ (∀ 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:

  1. Using codec A, we encode a message of protocol psA to bytes.
  2. When we decode those bytes using codec B, we get a message of protocol psB.
  3. When we encode that message again using codec B, we get bytes.
  4. When we decode those bytes using codec A, we get the original message again.

prop_codec_binary_compat ∷ ∀ psA psB failure m bytes. (Monad m, Eq (AnyMessage psA)) ⇒ (∀ a. m a → a) → Codec psA failure m bytes → Codec psB failure m bytes → (∀ pr (stA ∷ psA). PeerHasAgency pr stA → SamePeerHasAgency pr psB) → AnyMessageAndAgency psA → Bool Source #

Like prop_codec_splitsM but run in a pure monad m, e.g. Identity.

prop_codecs_compatM ∷ ∀ ps failure m bytes. (Monad m, Eq (AnyMessage ps), ∀ 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 ∷ ∀ ps failure m bytes. (Monad m, Eq (AnyMessage ps), ∀ a. Monoid a ⇒ Monoid (m a)) ⇒ (∀ a. m a → a) → Codec ps failure m bytes → Codec ps failure m bytes → AnyMessageAndAgency ps → Bool Source #

Like prop_codecs_compatM but run in a pure monad 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.

Constructors

SamePeerHasAgency ∷ ∀ (pr ∷ PeerRole) ps (st ∷ ps). PeerHasAgency pr st → SamePeerHasAgency pr ps