Marcin Szamotulski - Protocol pipelining in Typed-Protocols
Special thanks to the Haskell Foundation for supporting the production of this video!
Haskell Love 2021 schedule: https://emamo.com/event/haskell-love
Haskell Love twitter: / _haskellove
Pipelining is a latency hiding technique commonly used in various systems including network applications or processor architecture. I will present a new approach to protocol pipelining in our typed-protocols package. Typed-protocols is an implementation of binary session types in terms of an initial deep encoding. For performance reasons we provide pipelining, which however depends on concurrency and though an elegant solution it restricts the way some application has to be written. I will present how to design pipelining in a typed correct way without these limitations, at an expense of advanced type level programming. The talk will be illustrated by two simple ping-pong protocols. I will also present a proof that client and server applications, whether using pipelining or not, build with the framework are always dual to each other (hence communicate without deadlocks), and if they terminate they terminate at a common terminal state.
