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.

We will use as a running example a simple "ping/pong" protocol. (You can see the example in full in Network.TypedProtocol.PingPong.Type.) In this example protocol the client sends a ping message and the serve must respond with a pong message. The client can also terminate the protocol. So modelled as a state machine this protocol has three states, the one in which the client can send a ping or terminate message, the one in which the server must send a pong, and the terminal state where neither can send anything. We somewhat arbitrarily choose label these protocol states as "idle" "busy" and "done".

For this ping pong example the protocol tag and the protocol state types would be defined (via promoted data kinds) as:

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

We use DataKinds promotion here so StIdle, StBusy and StDone are types (of kind PingPong) representing the three states in this protocol's state machine. PingPong itself is both the kind of these types and is also the tag for protocol. We only ever use these as types, via the DataKinds promotion, never as value level data constructors.

Having defined our protocol tag and states we can instantiate the Protocol type class and fill out the other details.

The protocol must define what its messages are. These form the state transitions in the protocol state machine. Each transition specifies a "from" and "to" state as type parameters. This of course determines in which protocol states each message can appear.

In the "ping/pong" protocol example, the messages are of course ping and pong, which transition between the two main states. There is also a done message that moves the system into a terminal state.

instance Protocol PingPong where
  data Message PingPong from to where
    MsgPing :: Message PingPong StIdle StBusy
    MsgPong :: Message PingPong StBusy StIdle
    MsgDone :: Message PingPong StIdle StDone

This says that in the idle state a ping message takes us to the busy state, while a pong message takes us back to idle. Also in the idle state a done message takes us to the done state.

It is not required that protocols have any terminal states or corresponding transitions, as in this example, but it is often useful and it aids testing to have protocols that terminate cleanly as it allows them to return a result.

As described above, this style of protocol gives agency to only one peer at once. That is, in each protocol state, one peer has agency (the ability to send) and the other does not (it must only receive).

In the "ping/pong" protocol example, the idle state is the one in which the client can send a message, and the busy state is the one in which the server must respond. Finally in the done state, neither peer can send any further messages. This arrangement is defined as so:

   -- still within the instance Protocol PingPong
   type StateAgency StIdle = ClientAgency
   type StateAgency StBusy = ServerAgency
   type StateAgency StDone = NobodyAgency

In this simple protocol there is exactly one state in each category, but in general for non-trivial protocols there may be several protocol states in each category.

Finally we need to point which singletons to use for the protocol states

   -- still within the instance Protocol PingPong, 'SPingPong' type is what we define next.
   type StateToken = SPingPong

Furthermore we use singletons to provide term level reflection of type level states. One is required to provide singletons for all types of kind PingPong. These definitions are provided outside of the Protocol type class. This is as simple as providing a GADT:

data SingPingPong (st :: PingPong) where
  SingIdle :: SingPingPong StIdle
  SingBusy :: SingPingPong StBusy
  SingDone :: SingPingPong StDone

together with StateTokenI instance (similar to SingI from the "singletons" package):

instance StateTokenI StIdle where stateToken = SingIdle
instance StateTokenI StBusy where stateToken = SingBusy
instance StateTokenI StDone where stateToken = SingDone

This and other example protocols are provided in "typed-protocols-examples" package.

The connect proof 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. This property is true by construction, since we use a type family StateAgency which maps states to agencies, however we still need an evince that cases where both peer have the agency or neither of them has it can be eliminated.

The packages defines lemmas (in a hidden module) which 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 ⊥.

The framework defines protocol-agnostic proofs (in the hidden module Lemmas) which excludes that the client and server have agency at the same time.

• exclusionLemma_ClientAndServerHaveAgency,
• terminationLemma_1,
• terminationLemma_2.

The protocols we consider either give agency to one side (one side can send a message) or the protocol terminated. Agency is a (type-level) function of the protocol state, and thus uniquely determined by it.

The following types define the necessary type-level machinery and its term-level evidence to provide type-safe API for `typed-protocols`. Required proofs are hidden in an (unexposed) module Network.TypedProtocol.Lemmas.