Session Types Without Sophistry - System Description
Session Types Without Sophistry - System Description
复制标题
DOI：
10.1007/978-3-030-59025-3_5
复制
发表时间：
2020-09
期刊：
影响因子：
--
通讯作者：
O. Kiselyov;Keigo Imai
中科院分区：
文献类型：
--
作者：
O. Kiselyov;Keigo Imai
普通类型近似于结果，而会话类型近似于计算之间的通信。作为类型状态的一种形式，它们不仅描述了现在正在通信的内容，而且还描述了接下来要通信的内容。用普通的编程语言（如OCaml）编写会话类型的程序需要非凡的智慧来模拟类型级计算和线性类型-这意味着实现和错误消息很难理解。一个是不断提醒模板元编程在C++。我们提出了一个系统，探索一个非常不同的方法会话类型：降低类型级诡辩普通编程，同时保持静态保证。错误消息是详细的和可定制的，可以使用普通的调试器来调查会话类型的问题。我们的系统是一个二进制会话类型的DSL面向OCaml的面向服务的编程，支持多个通信通道，内部和外部的选择，递归，也通道delegation.The关键思想是staging：普通的运行时检查在生成器中发挥的作用“类型检查”从生成程序的角度来看。对于后者来说，花哨的类型对于生成器来说是普通的数据。
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.