Exceptional Asynchronous Session Types: Session Types without Tiers

Simon Fowler

Session types statically guarantee that communication complies with a protocol. However, most accounts of session typing do not account for failure, which means they are of limited use in real applications—especially distributed applications—where failure is pervasive.

We present the first formal integration of asynchronous session types with exception handling in a functional programming language. We define a core calculus which satisfies preservation and progress properties, is deadlock free, confluent, and terminating. We show modular extensions to the calculus which allow more convenient programming idioms, and show the metatheoretic properties which remain with each extension.

We provide the first implementation of session types with exception handling for a fully-fledged functional programming language, by extending the Links web programming language; our implementation draws on existing work on effect handlers. We illustrate our approach through a running example of two-factor authentication, and a larger example of a session-based chat application where communication occurs over session-typed channels and disconnections are handled gracefully. Finally, we touch upon more recent work showing how session types can coexist with the Model-View-Update paradigm, as pioneered by the Elm programming language.

---

Previous: Jens de Waard (TU Delft PL) | Implementing the Decomposition of Soundness Proofs of Abstract Interpreters in Coq
Next: Chiel Bruin | Frame VM: a virtual machine using scopes as frames