论文标题
将功能和命令性会话类型
Relating Functional and Imperative Session Types
论文作者
论文摘要
命令性会话类型为会话类型的通信提供了当务之急。在这样的接口中，通道引用是具有更改通道打字的操作的一流对象。与功能性会话类型API相比，表面上的程序结构更简单，但是需要打字以建模整个通信的当前状态。在探讨了命令式方法的早期工作之后，会话类型上的重要作品忽略了命令式方法，并选择了使用线性类型来管理频道参考的功能方法。我们证明，功能方法通过展示将翻译保存到线性功能会话类型系统中，将命令性会话类型的早期工作包含在当地会话类型上。我们进一步表明，从功能到命令性演算的非趋势翻译是语义上保存的。我们限制了功能积分的类型系统，以使后翻译变为类型保存。因此，我们精确地捕获了两个微积分的表达性差异，并得出结论，命令式演算中缺乏表现力在很大程度上是由于其类型系统施加的限制。
Imperative session types provide an imperative interface to session-typed communication. In such an interface, channel references are first-class objects with operations that change the typestate of the channel. Compared to functional session type APIs, the program structure is simpler at the surface, but typestate is required to model the current state of communication throughout. Following an early work that explored the imperative approach, a significant body of work on session types has neglected the imperative approach and opts for a functional approach that uses linear types to manage channel references soundly. We demonstrate that the functional approach subsumes the early work on imperative session types by exhibiting a typing and semantics preserving translation into a system of linear functional session types. We further show that the untyped backwards translation from the functional to the imperative calculus is semantics preserving. We restrict the type system of the functional calculus such that the backwards translation becomes type preserving. Thus, we precisely capture the difference in expressiveness of the two calculi and conclude that the lack of expressiveness in the imperative calculus is largely due to restrictions imposed by its type system.
