WG211/M18 Kiselyov

Session types without sophistry by Oleg Kiselyov, joint work with Keigo Imai of Gifu University

Whereas ordinary types approximate the results, session types approximate communication among computations. Session types are appealing because they can be inferred/checked statically, and because well--session-typed programs "do not go wrong": the computations do not deadlock, do not send data or commands their party is not prepared to handle, do not try to use closed or delegated away channels.

Session types are a form of typestate: they describe not only what is communicated now but also what should or could be communicated next. Therefore, they are non-trivial to realize in conventional languages. We need not just monads but parameterized monads as well as type functions and linear types. Realizing session types in OCaml requires inordinary cleverness - meaning the implementation and the error messages are very hard to understand. One is constantly reminded of template metaprogramming in C++.

We present the ongoing work exploring a very different approach to session typing: programming the inference and checking in the appropriate language (OCaml) and still obtaining the static assurances about communicating programs. We can emit detailed error messages customized at will, and use the ordinary debugger. The key idea is staging: ordinary run-time checks in the generator are `type-checks' from the point of view of the generated program. Fancy types are replaced with boring generator terms. (In type-checking, like in investing, exciting is ruinous.) Our library of binary session types supports multiple communication channels, internal and external choices, and channel delegation.