This module defines the core of the typed protocol framework.

A typed protocol between two peers is defined via a state machine: a collection of protocol states and protocol messages which are transitions between those states.

Start from the idea that a protocol is some language of messages sent between two peers. To specify a protocol is to describe what possible sequences of messages are valid. One simple but still relatively expressive way to do this is via a state machine: starting from some initial state, all possible paths through the state machine gives the set of valid protocol traces. This then dictates what a peer participating in a protocol may produce and what it must accept.

In this style we have a fixed number of states and in each state there is some number of valid messages that move us on to the next state. This can be illustrated as a graph, which can be a helpful form of documentation.

We further constrain this idea by saying that the two peers will use the same state machine and change states in lock-step by sending/receiving messages. In this approach, for each protocol state, the description dictates which peer has the agency to choose to send a message, while correspondingly the other must be prepared to receive the message.

The views of the two peers are dual. In each state one peer can send any message that is valid for the current protocol state while the other must be prepared to receive any valid message for current protocol state.

We can also have terminal protocol states in which neither peer has agency.

So part of the protocol description is to label each protocol state with the peer that has the agency in that state, or none for terminal states. We use the labels "client" and "server" for the two peers, but they are in fact symmetric.

The Protocol type class bundles up all the requirements for a typed protocol, which are in fact all type level constructs. Defining a new protocol and making it an instance of the Protocol class requires the following language extensions:

{-# LANGUAGE GADTs, TypeFamilies, DataKinds #-}

The type class itself is indexed on a protocol "tag" type. This type does double duty as the kind of the types of the protocol states.

The connect and connectPipelined proofs rely on lemmas about the protocol. Specifically they rely on the property that each protocol state is labelled with the agency of one peer or the other, or neither, but never both. Or to put it another way, the protocol states should be partitioned into those with agency for one peer, or the other or neither.

The way the labelling is encoded does not automatically enforce this property. It is technically possible to set up the labelling for a protocol so that one state is labelled as having both peers with agency, or declaring simultaneously that one peer has agency and that neither peer has agency in a particular state.

So the overall proofs rely on lemmas that say that the labelling has been done correctly. This type bundles up those three lemmas.

Specifically proofs that it is impossible for a protocol state to have:

• client having agency and server having agency
• client having agency and nobody having agency
• server having agency and nobody having agency

These lemmas are structured as proofs by contradiction, e.g. stating "if the client and the server have agency for this state then it leads to contradiction". Contradiction is represented as the Void type that has no values except ⊥.

For example for the ping/pong protocol, it has three states, and if we set up the labelling correctly we have:

data PingPong where
  StIdle :: PingPong
  StBusy :: PingPong
  StDone :: PingPong

instance Protocol PingPong where

  data ClientHasAgency st where
    TokIdle :: ClientHasAgency StIdle

  data ServerHasAgency st where
    TokBusy :: ServerHasAgency StBusy

  data NobodyHasAgency st where
    TokDone :: NobodyHasAgency StDone

So now we can prove that if the client has agency for a state then there are no cases in which the server has agency.

  exclusionLemma_ClientAndServerHaveAgency TokIdle tok = case tok of {}

For this protocol there is only one state in which the client has agency, the idle state. By pattern matching on the state token for the server agency we can list all the cases in which the server also has agency for the idle state. There are of course none of these so we give the empty set of patterns. GHC can check that we are indeed correct about this. This also requires the EmptyCase language extension.

To get this completeness checking it is important to compile modules containing these lemmas with -Wincomplete-patterns, which is implied by -Wall.

All three lemmas follow the same pattern.

The mechanism for labelling each protocol state with the agency does not automatically prevent mislabelling, ie giving conflicting labels to a single state. It does in fact prevent forgetting to label states in the sense that it would not be possible to write protocol peers that make progress having entered these unlabelled states.

This partition property is however crucial for the framework's guarantees. The Network.TypedProtocol.Proofs module provides a way to guarantee for each protocol that this property is not violated. It also provides utilities helpful for testing protocols.

The connect and connectPipelined proofs rely on lemmas about the protocol. Specifically they rely on the property that each protocol state is labelled with the agency of one peer or the other, or neither, but never both. Or to put it another way, the protocol states should be partitioned into those with agency for one peer, or the other or neither.

The way the labelling is encoded does not automatically enforce this property. It is technically possible to set up the labelling for a protocol so that one state is labelled as having both peers with agency, or declaring simultaneously that one peer has agency and that neither peer has agency in a particular state.

So the overall proofs rely on lemmas that say that the labelling has been done correctly. This type bundles up those three lemmas.

Specifically proofs that it is impossible for a protocol state to have:

• client having agency and server having agency
• client having agency and nobody having agency
• server having agency and nobody having agency

These lemmas are structured as proofs by contradiction, e.g. stating "if the client and the server have agency for this state then it leads to contradiction". Contradiction is represented as the Void type that has no values except ⊥.

For example for the ping/pong protocol, it has three states, and if we set up the labelling correctly we have:

data PingPong where
  StIdle :: PingPong
  StBusy :: PingPong
  StDone :: PingPong

instance Protocol PingPong where

  data ClientHasAgency st where
    TokIdle :: ClientHasAgency StIdle

  data ServerHasAgency st where
    TokBusy :: ServerHasAgency StBusy

  data NobodyHasAgency st where
    TokDone :: NobodyHasAgency StDone

So now we can prove that if the client has agency for a state then there are no cases in which the server has agency.

  exclusionLemma_ClientAndServerHaveAgency TokIdle tok = case tok of {}

For this protocol there is only one state in which the client has agency, the idle state. By pattern matching on the state token for the server agency we can list all the cases in which the server also has agency for the idle state. There are of course none of these so we give the empty set of patterns. GHC can check that we are indeed correct about this. This also requires the EmptyCase language extension.

To get this completeness checking it is important to compile modules containing these lemmas with -Wincomplete-patterns, which is implied by -Wall.

All three lemmas follow the same pattern.