| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Network.TypedProtocol.Proofs
Description
Proofs about the typed protocol framework.
It also provides helpful testing utilities.
Synopsis
- connect :: forall 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)
-
data
TerminalStates
ps
where
- TerminalStates :: forall ps (st :: ps). NobodyHasAgency st -> NobodyHasAgency st -> TerminalStates ps
- connectPipelined :: forall ps (pr :: PeerRole ) (st :: ps) m a b. ( Monad m, Protocol ps) => [ Bool ] -> PeerPipelined ps pr st m a -> Peer ps ( FlipAgency pr) st m b -> m (a, b, TerminalStates ps)
- forgetPipelined :: forall ps (pr :: PeerRole ) (st :: ps) m a. Functor m => PeerPipelined ps pr st m a -> Peer ps pr st m a
- data Queue (n :: N ) a where
- enqueue :: a -> Queue n a -> Queue ( S n) a
- pipelineInterleaving :: Int -> [ Bool ] -> [req] -> [resp] -> [ Either req resp]
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 :: forall 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.
Constructors
| TerminalStates :: forall ps (st :: ps). NobodyHasAgency st -> NobodyHasAgency st -> TerminalStates ps |
Pipelining proofs
Additional proofs specific to the pipelining features
Arguments
| :: forall 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 :: forall 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.
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
Arguments
| :: Int |
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.