A blog post about protocol pipelining in session type framework used by IOHK. Accompanied with an alternative agda implementation.
2 Likes
Could linear types be useful here to give a safer and more precise API?
With initial encoding one does not need linear types; In session-types literature another encoding is used, focused on channels and their type evolution. Channels require linear types to make sure that one does not reuse an old channel again when writing a protocol application. With initial encoding this is not the case. One could write a bogus interpretation of the Peer type, but this is less likely as this is part is general and shared between all protocols.
The api is already as precise as possible: a constructed application is deadlock free and if it terminates then both side will terminate at a terminal state. It possibly could be improved to not require to prove exclusion lemmas for each protocol separately but be proven by the framework once for all protocols that can be encoded in this way (which is not true for all protocols) as the agda implementation suggest.
However, with linear types and channel centric approach there are formulations of mulitparty session types, improving expressiveness. Pipelining in this approach should be possible as well.
2 Likes