A stateful codec.

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.

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.

A type family for protocol state token, e.g. term level representation of type level state (also known as singleton).

This type family is similar to Sing type class in the "singletons" package, but specific for protocol states.

A type class which hides a state token / singleton inside a class dictionary.

This is similar to the SingI instance, but specific to protocol state singletons.

A constraint which provides an evidence that the protocol isn't in a terminal state.

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.

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.

Any message for a protocol, with a StateTokenI constraint which gives access to protocol state.

Used where we don't know statically what the state type is, but need the agency and message to match each other.

showAnyMessage is can be used to provide Show instance for AnyMessage if showing Message is independent of the state or one accepts showing only partial information included in message constructors or accepts message constructors to carry Show instances for its arguments. Note that the proper solution is to define a custom `Show (AnyMessage ps f)` instance for a protocol ps, which give access to the state functor f in scope of show.

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.

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.