Defining and using Codecs

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.

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.

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.

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.

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.

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.

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.

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.

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

A variant of runDecoder that is suitable for "pure" monads that have a run function. This includes ST, using runST.

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)` .

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.

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

The Codec round-trip property in a pure monad.

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.

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

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.

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

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.

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

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.