typed protocols

Typed Protocols

Duncan Coutts SkillsMatter Talk

Protocol

• 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

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

More specific types

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

Pipelining for performance optimisation

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!