特别投递：使用邮箱类型进行编程（扩展版本）
摘要：邮箱类型是电子邮箱支持的异步和单向通信模型的一个关键原因，这是实现可靠和可扩展分布式系统的actor语言（如Erlang和Elixir）成功的原因之一。虽然许多actor可以向某个actor发送消息，但只有该actor可以（有选择地）从其邮箱中接收。虽然actor消除了许多与共享内存并发有关的问题，但仍然容易受到通信错误的影响，例如协议违规和死锁。 邮箱类型是一种新颖的邮箱行为类型系统，最初由de'Liguoro和Padovani在2018年用于进程演算，它将邮箱的内容表示为一个可交换的正则表达式。由于别名和嵌套的评估上下文，从进程演算转向编程语言是具有挑战性的。 本文介绍了Pat，这是第一个结合邮箱类型的编程语言设计，并描述了一种算法类型系统。我们采用了准线性类型来缓解别名引入的一些复杂性。我们的算法类型系统是必然的共环境，通过一种新颖的反向双向类型推导来实现，并证明它在我们的声明性类型系统中是完备和有效的。我们实现了一个原型类型检查器，并使用它在一个工厂自动化案例研究和一系列来自Savina actor基准套件的示例中展示Pat的表达能力。
作者：Simon Fowler, Duncan Paul Attard, Franciszek Sowul, Simon J. Gay, Phil Trinder
论文ID：2306.12935
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-06-23