Safe Haskell	None
Language	GHC2021

Network.TypedProtocol.Driver

Contents

Introduction
Normal peers
Pipelined peers

Description

Actions for running Peers with a Driver

Synopsis

data Driver ps (pr :: PeerRole) dstate (m :: Type -> Type) = Driver {
- sendMessage :: forall (st :: ps) (st' :: ps). (StateTokenI st, StateTokenI st', ActiveState st) => WeHaveAgencyProof pr st -> Message ps st st' -> m ()
- recvMessage :: forall (st :: ps). (StateTokenI st, ActiveState st) => TheyHaveAgencyProof pr st -> dstate -> m (SomeMessage st, dstate)
- initialDState :: dstate
}
data SomeMessage (st :: ps) where
- SomeMessage :: forall ps (st :: ps) (st' :: ps). (StateTokenI st, StateTokenI st', ActiveState st) => Message ps st st' -> SomeMessage st
runPeerWithDriver :: forall ps (st :: ps) (pr :: PeerRole) dstate m a. Monad m => Driver ps pr dstate m -> Peer ps pr 'NonPipelined st m a -> m (a, dstate)
runPipelinedPeerWithDriver :: forall ps (st :: ps) (pr :: PeerRole) dstate m a. MonadAsync m => Driver ps pr dstate m -> PeerPipelined ps pr st m a -> m (a, dstate)

Introduction

A Peer is a particular implementation of an agent that engages in a typed protocol. To actually run one we need an untyped channel representing one end of an untyped duplex message transport, which allows to send and receive bytes. One will also need a Codec which handles conversion between the typed protocol messages and the untyped channel.

Given the Peer, a compatible Codec and an untyped channel we can run the peer in some appropriate monad (e.g. IO, or a simulation monad for testing purposes). The peer and codec have to agree on the same protocol. The codec and channel have to agree on the same untyped medium, e.g. text or bytes. All three have to agree on the same monad in which they will run.

This module provides drivers for normal and pipelined peers. There is very little policy involved here so typically it should be possible to use these drivers, and customise things by adjusting the peer, or codec or channel (together with an implementation of a Driver based on it).

For implementing a Driver based on some untyped channel, the runDecoder function may be a helpful utility.

For a possible definition of an untyped channel and how to construct a Driver from it see typed-protocols-examples package. For production grade examples see https://github.com/IntersectMBO/ouroboros-network repository.

data Driver ps (pr :: PeerRole) dstate (m :: Type -> Type) Source #

Constructors

Driver

Fields

sendMessage :: forall (st :: ps) (st' :: ps). (StateTokenI st, StateTokenI st', ActiveState st) => WeHaveAgencyProof pr st -> Message ps st st' -> m ()
Send a message; the message must transition from an active state. One needs to supply agency evidence.
recvMessage :: forall (st :: ps). (StateTokenI st, ActiveState st) => TheyHaveAgencyProof pr st -> dstate -> m (SomeMessage st, dstate)
Receive some message, since we don't know the final state of the protocol it is wrapped in SomeMessage type; the message must transition from an active state. One needs to supply agency evidence.
initialDState :: dstate
Initial state of the driver

data SomeMessage (st :: ps) where Source #

When decoding a Message we only know the expected "from" state. We cannot know the "to" state as this depends on the message we decode. To resolve this we use the SomeMessage wrapper which uses an existential type to hide the "to" state.

Constructors

SomeMessage :: forall ps (st :: ps) (st' :: ps). (StateTokenI st, StateTokenI st', ActiveState st) => Message ps st st' -> SomeMessage st

Normal peers

runPeerWithDriver :: forall ps (st :: ps) (pr :: PeerRole) dstate m a. Monad m => Driver ps pr dstate m -> Peer ps pr 'NonPipelined st m a -> m (a, dstate) Source #

Run a peer with the given driver.

This runs the peer to completion (if the protocol allows for termination).

Pipelined peers

runPipelinedPeerWithDriver :: forall ps (st :: ps) (pr :: PeerRole) dstate m a. MonadAsync m => Driver ps pr dstate m -> PeerPipelined ps pr st m a -> m (a, dstate) Source #

Run a pipelined peer with the given driver.

This runs the peer to completion (if the protocol allows for termination).

Unlike normal peers, running pipelined peers rely on concurrency, hence the MonadAsync constraint.