This package defines the typed protocol framework. This module re-exports the public API.

The typed protocol framework is used to define, test and execute protocols.

It guarantees:

• agreement on which messages can be sent and received;
• the absence of race conditions; and
• the absence of deadlock.

The trade-off to achieve these guarantees is that it places constraints on the kinds of protocol that can be expressed. In particular it requires that protocols be defined as a state transition system. It requires for each protocol state that exactly one of the two peers be able to send and the other must be ready to receive.

This means it is not possible to express protocols such as TCP where there are protocol states where a single peer can both send and receive, however it is suitable for most application-level protocols. In particular many application-level protocols are completely in-order and synchronous. That said, in many (but not all) cases it is possible to pipeline these protocols so that network latency can be hidden and full use made of the available bandwidth. Special support is provided to run protocols in a pipelined way, without having to change the protocol definition.

The protocols in this framework assume an underlying "reliable ordered" connection. A "reliable ordered" connection is a term of art meaning one where the receiving end receives any prefix of the messages sent by the sending end. It is not reliable in the colloquial sense as it does not ensure that anything actually arrives, only that if any message arrives, all the previous messages did too, and that they arrive in the order in which they were sent.

The framework also provides:

• an abstraction for untyped channels;
• a codec abstraction for encoding and decoding protocol messages; and
• drivers for running protocol peers with a channel and a codec.

The Network.TypedProtocol.Core module defines the core of the system.

Start reading here to understand:

• how to define new protocols; or
• to write peers that engage in a protocol.

Typed protocol messages need to be converted to and from untyped serialised forms to send over a transport channel. So part of defining a new protocol is to define the message encoding and the codec for doing the encoding and decoding. This is somewhat (but not significantly) more complex than defining normal data type serialisation because of the need to decode typed protocol messages. The Network.TypedProtocol.Codec module provides the codec abstraction to capture this.

There are a few proofs about the framework that we can state and implement as Haskell functions (using GADTs and evaluation). A couple of these proofs rely on a few lemmas that should be proved for each protocol. The Network.TypedProtocol.Proofs module describes these proof and provides the infrastructure for the simple lemmas that need to be implemented for each protocol.

This module also provides utilities helpful for testing protocols.

Typed protocols need to be able to send messages over untyped transport channels. The Network.TypedProtocol.Channel module provides such an abstraction. You can use existing example implementations of this interface or define your own to run over other transports.

Given a protocol peer, and a channel and a codec we can run the protocol peer so that it engages in the protocol sending and receiving messages over the channel. The Network.TypedProtocol.Driver module provides drivers for normal and pipelined peers.

Protocol pipelining is a technique to make effective use of network resources.

As in the above diagram, instead of sending a request and waiting for the response before sending the next request, pipelining involves sending all three requests back-to-back and waiting for the three replies. The server still simply processes the requests in order and the replies come back in the same order as the requests were made.

Not only does this save network latency, one round trip versus three in the diagram above, but it also makes effective use of the bandwidth by sending requests and replies back-to-back.

In the example in the diagram it stops after three requests, but such a pattern can go on indefinately with messages going in both directions, which can saturate the available bandwidth.

For many (but not all) protocols that can be defined in the typed-protocol framework it is possible to take the protocol, without changing the protocol's state machine, and to engage in the protocol in a pipelined way. Only the pipelined client has to be written specially. The server side can be used unaltered and can be used with either pipelined or non-pipelined clients.