typed-protocols- A framework for strongly typed protocols
Safe HaskellNone



Proofs about the typed protocol framework.

It also provides helpful testing utilities.


About these proofs

Typed languages such as Haskell can embed proofs. In total languages this is straightforward: a value inhabiting a type is a proof of the property corresponding to the type.

In languages like Haskell that have ⊥ as a value of every type, things are slightly more complicated. We have to demonstrate that the value that inhabits the type of interest is not ⊥ which we can do by evaluation.

This idea crops up frequently in advanced type level programming in Haskell. For example Refl proofs that two types are equal have to have a runtime representation that is evaluated to demonstrate it is not ⊥ before it can be relied upon.

The proofs here are about the nature of typed protocols in this framework. The connect and connectPipelined proofs rely on a few lemmas about the individual protocol. See AgencyProofs.

Connect proof

connect ∷ ∀ ps (pr ∷ PeerRole) (st ∷ ps) m a b. (Monad m, Protocol ps) ⇒ Peer ps pr st m a → Peer ps (FlipAgency pr) st m b → m (a, b, TerminalStates ps) Source #

The connect function takes two peers that agree on a protocol and runs them in lock step, until (and if) they complete.

The connect function serves a few purposes.

  • The fact we can define this function at at all proves some minimal sanity property of the typed protocol framework.
  • It demonstrates that all protocols defined in the framework can be run with synchronous communication rather than requiring buffered communication.
  • It is useful for testing peer implementations against each other in a minimalistic setting.

data TerminalStates ps where Source #

The terminal states for the protocol. Used in connect and connectPipelined to return the states in which the peers terminated.


TerminalStates ∷ ∀ ps (st ∷ ps). NobodyHasAgency st → NobodyHasAgency st → TerminalStates ps 

Pipelining proofs

Additional proofs specific to the pipelining features

connectPipelined Source #


∷ ∀ ps (pr ∷ PeerRole) (st ∷ ps) m a b. (Monad m, Protocol ps) 
⇒ [Bool]

Interleaving choices. [] gives no pipelining.

PeerPipelined ps pr st m a 
Peer ps (FlipAgency pr) st m b 
→ m (a, b, TerminalStates ps) 

Analogous to connect but for pipelined peers.

Since pipelining allows multiple possible interleavings, we provide a [Bool] parameter to control the choices. Each True will trigger picking the first choice in the SenderCollect construct (if possible), leading to more results outstanding. This can also be interpreted as a greater pipeline depth, or more messages in-flight.

This can be exercised using a QuickCheck style generator.

forgetPipelined ∷ ∀ ps (pr ∷ PeerRole) (st ∷ ps) m a. Functor m ⇒ PeerPipelined ps pr st m a → Peer ps pr st m a Source #

Prove that we have a total conversion from pipelined peers to regular peers. This is a sanity property that shows that pipelining did not give us extra expressiveness or to break the protocol state machine.

Pipeline proof helpers

data Queue (n ∷ N) a where Source #

A size indexed queue. This is useful for proofs, including connectPipelined but also as so-called direct functions for running a client and server wrapper directly against each other.


EmptyQQueue Z a 
ConsQ ∷ a → Queue n a → Queue (S n) a 

enqueue ∷ a → Queue n a → Queue (S n) a Source #

At an element to the end of a Queue. This is not intended to be efficient. It is only for proofs and tests.

Auxilary functions

pipelineInterleaving Source #



Bound on outstanding responses

→ [Bool]

Pipelining choices

→ [req] 
→ [resp] 
→ [Either req resp] 

A reference specification for interleaving of requests and responses with pipelining, where the environment can choose whether a response is available yet.

This also supports bounded choice where the maximum number of outstanding in-flight responses is limted.