typed-protocols-0.1.0.0: A framework for strongly typed protocols

Network.TypedProtocol.Core

Description

This module defines the core of the typed protocol framework.

Synopsis

# Introduction

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.

# Defining protocols

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.

class Protocol ps where Source #

The protocol type class bundles up all the requirements for a typed protocol.

Each protocol consists of three things:

• The protocol itself, which is also expected to be the kind of the types of the protocol states. The class is indexed on the protocol itself.
• The protocol messages.
• The partition of the protocol states into those in which the client has agency, or the server has agency, or neither have agency.

The labelling of each protocol state with the peer that has agency in that state is done by giving a definition to the data families ClientHasAgency, ServerHasAgency and NobodyHasAgency. These definitions are expected to be singleton-style GADTs with one constructor per protocol state.

Each protocol state must be assigned to only one label. See Network.TypedProtocol.Proofs for more details on this point.

Associated Types

data Message ps (st ∷ ps) (st' ∷ ps) Source #

The messages for this protocol. It is expected to be a GADT that is indexed by the from and to protocol states. That is the protocol state the message transitions from, and the protocol state it transitions into. These are the edges of the protocol state transition system.

data ClientHasAgency (st ∷ ps) Source #

Tokens for those protocol states in which the client has agency.

data ServerHasAgency (st ∷ ps) Source #

Tokens for those protocol states in which the server has agency.

data NobodyHasAgency (st ∷ ps) Source #

Tokens for terminal protocol states in which neither the client nor server has agency.

Methods

exclusionLemma_ClientAndServerHaveAgency ∷ ∀ (st ∷ ps). ClientHasAgency st → ServerHasAgency st → Void Source #

Lemma that if the client has agency for a state, there are no cases in which the server has agency for the same state.

exclusionLemma_NobodyAndClientHaveAgency ∷ ∀ (st ∷ ps). NobodyHasAgency st → ClientHasAgency st → Void Source #

Lemma that if the nobody has agency for a state, there are no cases in which the client has agency for the same state.

exclusionLemma_NobodyAndServerHaveAgency ∷ ∀ (st ∷ ps). NobodyHasAgency st → ServerHasAgency st → Void Source #

Lemma that if the nobody has agency for a state, there are no cases in which the server has agency for the same state.

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.

# Engaging in protocols

data PeerRole Source #

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.

Constructors

 AsClient AsServer

type family FlipAgency (pr ∷ PeerRole) where ... Source #

A type function to flip the client and server roles.

Equations

 FlipAgency AsClient = AsServer FlipAgency AsServer = AsClient

data PeerHasAgency (pr ∷ PeerRole) (st ∷ ps) where Source #

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.

Constructors

 ClientAgency ∷ !(ClientHasAgency st) → PeerHasAgency AsClient st ServerAgency ∷ !(ServerHasAgency st) → PeerHasAgency AsServer st

#### Instances

Instances details
 (∀ (st' ∷ ps). Show (ClientHasAgency st'), ∀ (st' ∷ ps). Show (ServerHasAgency st')) ⇒ Show (PeerHasAgency pr st) Source # Instance detailsDefined in Network.TypedProtocol.Core MethodsshowsPrec ∷ Int → PeerHasAgency pr st → ShowS #show ∷ PeerHasAgency pr st → String #showList ∷ [PeerHasAgency pr st] → ShowS #

type WeHaveAgency (pr ∷ PeerRole) st = PeerHasAgency pr st Source #

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.

type TheyHaveAgency (pr ∷ PeerRole) st = PeerHasAgency (FlipAgency pr) st Source #

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.

data Peer ps (pr ∷ PeerRole) (st ∷ ps) m a where Source #

A description of a peer that engages in a protocol.

The protocol describes what messages peers may send or must accept. A particular peer implementation decides what to actually do within the constraints of the protocol.

Peers engage in a protocol in either the client or server role. Of course the client role can only interact with the serve role for the same protocol and vice versa.

Peer has several type arguments:

• the protocol itself;
• the client/server role;
• .the current protocol state;
• the monad in which the peer operates; and
• the type of any final result once the peer terminates.

For example:

pingPongClientExample :: Int -> Peer PingPong AsClient StIdle m ()
pingPongServerExample ::        Peer PingPong AsServer StIdle m Int

The actions that a peer can take are:

• to perform local monadic effects
• to terminate with a result (but only in a terminal protocol state)
• to send a message (but only in a protocol state in which we have agency)
• to wait to receive a message (but only in a protocol state in which the other peer has agency)

In the Done, Yield and Await cases we must provide evidence of both the protocol state we are in and that the appropriate peer has agency. This takes the form of ClientAgency or ServerAgency applied to a protocol-specific state token: either a ClientHasAgency or a ServerHasAgency token for the protocol. The Done state does not need the extra agency information.

While this evidence must be provided, the types guarantee that it is not possible to supply incorrect evidence.

Constructors

 Effect ∷ m (Peer ps pr st m a) → Peer ps pr st m a Perform a local monadic effect and then continue.Example:Effect $do ... -- actions in the monad return$ ... -- another Peer value Done ∷ !(NobodyHasAgency st) → a → Peer ps pr st m a Terminate with a result. A state token must be provided from the NobodyHasAgency states, so show that this is a state in which we can terminate.Example:Yield (ClientAgency TokIdle) MsgDone (Done TokDone result) Yield ∷ !(WeHaveAgency pr st) → Message ps st st' → Peer ps pr st' m a → Peer ps pr st m a Send a message to the other peer and then continue. This takes the message and the continuation. It also requires evidence that we have agency for this protocol state and thus are allowed to send messages.Example:Yield (ClientAgency TokIdle) MsgPing $... Await ∷ !(TheyHaveAgency pr st) → (∀ st'. Message ps st st' → Peer ps pr st' m a) → Peer ps pr st m a Waits to receive a message from the other peer and then continues. This takes the the continuation that is supplied with the received message. It also requires evidence that the other peer has agency for this protocol state and thus we are expected to wait to receive messages.Note that the continuation that gets supplied with the message must be prepared to deal with any message that is allowed in this protocol state. This is why the continuation must be polymorphic in the target state of the message (the third type argument of Message).Example:Await (ClientAgency TokIdle)$ \msg -> case msg of MsgDone -> ... MsgPing -> ...

#### Instances

Instances details
 Functor m ⇒ Functor (Peer ps pr st m) Source # Instance detailsDefined in Network.TypedProtocol.Core Methodsfmap ∷ (a → b) → Peer ps pr st m a → Peer ps pr st m b #(<\$) ∷ a → Peer ps pr st m b → Peer ps pr st m a #

# Protocol proofs and tests

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.