关联函数式和命令式会话类型
摘要：命令式会话类型提供了一种对会话类型通信的命令式接口。在这样的接口中，通道引用是第一类对象，具有可以改变通道类型状态的操作。与功能性会话类型API相比，程序结构在表层上更简单，但是需要使用类型状态来建模通信的当前状态。在早期探索了命令式方法的工作之后，一系列关于会话类型的工作忽视了命令式方法，而选择了使用线性类型来管理通道引用以确保声音。我们证明了功能性方法包含了命令式会话类型的早期工作，通过展示一种保留类型和语义的翻译，将其转化为一种线性功能性会话类型系统。我们进一步展示了从功能性到命令式演算的无类型向后翻译是语义保持的。我们限制了功能性演算的类型系统，使得向后翻译变得类型保持。因此，我们准确地捕捉了这两种演算的表达能力的差异，并得出结论，命令式演算的表达能力不足很大程度上是由其类型系统所施加的限制造成的。
作者：Hannes Saffrich and Peter Thiemann
论文ID：2010.08261
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-06-22