typed protocols

Typed Protocols

what is a protocol really? Should be more than a bunch of APIs
label state with agency of the peer, ie. who is allowed to send, who must receive
Protocol typeclass instances describe what's allowed in the protocl
- guarantees there's no deadlock -> one peer has agency so not both can wait in receive state
- states are types (datakinds)
- message types is an associated data family of Protocol typeclass
- agency roles are associated data families
- there are lemmas to implement which ensure protocol is correct using GHC

Peer types represent a particular instance of a given protocol:

Peer is indexed by the protocol type, the agency label and initial state, lpus monad and return value
client and server can be composed over some communication medium (a transport channel and codec)
Peer has constructors for each possible action for the peer
The lemmas are required to prove the agency/state relationship is correct:
- NobodyHasAgency is a type to prove we are in initial state,
- Done does the same thing for terminal state,
- WeHaveAgency is a proof we are in the correct role

Await requires other party to have agency, continuation's state is controlled by other party which implies existential variable to represent state

type errors are a bit tricky and hard to mentally map to actual state machine representation

introduce specific datatypes for representing each agency role to provide more guidance
client and serfver are duals: One is sum type and the other product type!
reminds me of free/cofree duality for interpreters and commands: http://abailly.github.io/posts/free.html
Q: could we extract the state diagram from the code?
endup with one datatype per protocol state when it's more complicated than a mere ping-pong
conversion function to Peer type runPeer interprets a Peer using Codec adn Channel

need to avoid latency, pipelining >>> batching

batching = send multiple messages
pipelining = don't wait for replies A pipelined client can be connected to a non-pipelined server by wrapping it in a queue (buffer)
PeerSender encodes the sending side, SenderCollect collect answers depending on a PeerSender

I wish there were more time to go through real examples!