TY - GEN
T1 - Session Types Without Sophistry
T2 - 15th International Symposium on Functional and Logic Programming, FLOPS 2020
AU - Kiselyov, Oleg
AU - Imai, Keigo
N1 - Funding Information:
Acknowledgments. We thank anonymous reviewers for many, helpful comments and suggestions. This work was partially supported by JSPS KAKENHI Grant Number 18H03218 and 17K12662.
Publisher Copyright:
© 2020, Springer Nature Switzerland AG.
PY - 2020
Y1 - 2020
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85091339439&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85091339439&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-59025-3_5
DO - 10.1007/978-3-030-59025-3_5
M3 - Conference contribution
AN - SCOPUS:85091339439
SN - 9783030590246
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 66
EP - 87
BT - Functional and Logic Programming - 15th International Symposium, FLOPS 2020, Proceedings
A2 - Nakano, Keisuke
A2 - Sagonas, Konstantinos
PB - Springer Science and Business Media Deutschland GmbH
Y2 - 14 September 2020 through 16 September 2020
ER -