Whereas ordinary types approximate the results, session types approximate communication among computations. As a form of typestate, they describe not only what is communicated now but also what is to be communicated next. Writing session-typed programs in an ordinary programming language such an OCaml requires inordinary cleverness to simulate type-level computations and linear typing – meaning the implementation and the error messages are very hard to understand. One is constantly reminded of template metaprogramming in C++. We present a system exploring a very different approach to session typing: lowering type-level sophistry to ordinary programming, while maintaining the static assurances. Error messages are detailed and customizable, and one can use an ordinary debugger to investigate session-type problems. Our system is a binary-session–typed DSL for service-oriented programming in OCaml, supporting multiple communication channels, internal and external choices, recursion, and also channel delegation. The key idea is staging: ordinary run-time checks in the generator play the role of “type-checks” from the point of view of the generated program. What is a fancy type to the latter is ordinary data to the generator.
CITATION STYLE
Kiselyov, O., & Imai, K. (2020). Session Types Without Sophistry: System Description. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 12073 LNCS, pp. 66–87). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-030-59025-3_5
Mendeley helps you to discover research relevant for your work.