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 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 extend Pat with sums, products and higher-order functions, and also interfaces that allow finer-grained reasoning about mailbox contents. 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等参与者语言在实现可靠、可扩展分布式系统方面取得成功的关键原因。虽然多个参与者可能向某个参与者发送消息，但只有该参与者能从其邮箱接收消息。尽管参与者消除了共享内存并发带来的许多问题，它们仍然容易受到协议违规和死锁等通信错误的影响。邮箱类型是de'Liguoro和Padovani于2018年首次为进程演算提出的一种新型邮箱行为类型系统，该系统将邮箱内容捕获为可交换正则表达式。由于别名和嵌套求值上下文的存在，从进程演算过渡到编程语言具有挑战性。本文提出了首个融合邮箱类型的编程语言设计Pat，并描述了一种算法类型系统。我们通过准线性类型的关键运用来应对别名引入的部分复杂性。我们的算法类型系统必然采用共上下文设计，这是通过反向双向类型标注的新颖应用实现的，并证明了其相对于声明式类型系统的可靠性与完备性。我们通过和类型、积类型及高阶函数对Pat进行扩展，同时引入支持对邮箱内容进行更细粒度推理的接口。我们实现了原型类型检查器，并通过工厂自动化案例研究和Savina参与者基准测试套件中的系列示例，展示了Pat的表达能力。