The asynchronous and unidirectional communication model supported by mailboxes is a key reason for the success of actor languages like Erlang and Elixir for implementing reliable and scalable distributed systems. While many actors may send messages to some actor, only the actor may (selectively) receive from its mailbox. Although actors eliminate many of the issues stemming from shared memory concurrency, they remain vulnerable to communication errors such as protocol violations and deadlocks. Mailbox types are a novel behavioural type system for mailboxes first introduced for a process calculus by de'Liguoro and Padovani in 2018, which capture the contents of a mailbox as a commutative regular expression. Due to aliasing and nested evaluation contexts, moving from a process calculus to a programming language is challenging. This paper presents Pat, the first programming language design incorporating mailbox types, and describes an algorithmic type system. We make essential use of quasi-linear typing to tame some of the complexity introduced by aliasing. Our algorithmic type system is necessarily co-contextual, achieved through a novel use of backwards bidirectional typing, and we prove it sound and complete with respect to our declarative type system. We implement a prototype type checker, and use it to demonstrate the expressiveness of Pat on a factory automation case study and a series of examples from the Savina actor benchmark suite.

翻译：邮箱所支持的异步单向通信模型是Erlang和Elixir等actor语言成功实现可靠且可扩展分布式系统的关键原因。尽管多个actor可以向某个actor发送消息，但只有该actor能够（选择性地）从其邮箱接收消息。虽然actor消除了共享内存并发带来的许多问题，但它们仍然容易受到协议违规和死锁等通信错误的影响。邮箱类型是一种新颖的行为类型系统，最初由de'Liguoro和Padovani在2018年为进程演算引入，它将邮箱内容表示为可交换正则表达式。由于别名和嵌套求值上下文的存在，从进程演算过渡到编程语言具有挑战性。本文提出了Pat——首个融入邮箱类型的编程语言设计，并描述了一种算法化类型系统。我们关键性地使用了准线性类型来抑制别名引入的部分复杂性。我们的算法化类型系统必然是上下文无关的，这是通过反向双向类型化的创新应用实现的，并且我们证明了它相对于声明式类型系统的完备性与可靠性。我们实现了一个原型类型检查器，并通过工厂自动化案例研究和来自Savina actor基准测试套件的一系列示例，展示了Pat的表达能力。