一句话：提出首个融入邮箱类型的编程语言 Pat，并用算法化类型系统静态防范 actor 通信协议错误与死锁。
Actor 语言通过邮箱实现异步单向通信，适合可靠可扩展的分布式系统，但 actor 仍可能违反通信协议或发生死锁。邮箱类型由 de’Liguoro 与 Padovani 提出，以交换正则表达式刻画邮箱内容，此前仅用于进程演算。由于别名和嵌套求值上下文，将其迁移到编程语言颇具挑战。本文提出 Pat，首个融入邮箱类型的编程语言，并给出算法化类型系统；借助准线性类型控制别名复杂性，并通过新颖的后向双向类型推导实现共上下文类型检查，且证明其相对声明式类型系统既可靠又完备。作者实现原型类型检查器，并用工厂自动化案例和 Savina actor 基准示例展示 Pat 的表达能力。
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.
@article{paperbot1919,
title = {Special Delivery: Programming with Mailbox Types},
author = {Simon Fowler and Duncan Paul Attard and Franciszek Sowul and Simon J. Gay and Phil Trinder},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {ICFP},
year = {2023},
doi = {10.1145/3607832}
}