Special Delivery: Programming with Mailbox Types
Special Delivery: Programming with Mailbox Types
复制标题
特快专递：使用邮箱类型进行编程
DOI：
10.1145/3607832
复制
发表时间：
2023
影响因子：
--
通讯作者：
Fowler S
中科院分区：
文献类型：
--
作者：
Fowler S
邮箱支持的异步和单向通信模型是 Erlang 和 Elixir 等 Actor 语言成功实现可靠且可扩展的分布式系统的关键原因。虽然许多参与者可以向某个参与者发送消息，但只有该参与者可以（选择性地）从其邮箱接收消息。尽管参与者消除了共享内存并发带来的许多问题，但它们仍然容易受到协议违规和死锁等通信错误的影响。邮箱类型是一种新颖的邮箱行为类型系统，由 de’Liguoro 和 Padovani 于 2018 年首次为流程演算引入，它将邮箱的内容捕获为可交换正则表达式。由于别名和嵌套评估上下文，从过程演算转向编程语言具有挑战性。本文介绍了 Pat，第一个包含邮箱类型的编程语言设计，并描述了一个算法类型系统。我们充分利用准线性类型来抑制混叠带来的一些复杂性。我们的算法类型系统必然是共上下文的，通过向后双向类型的新颖使用来实现，并且我们证明它相对于我们的声明类型系统是健全和完整的。我们实现了一个原型类型检查器，并用它来演示 Pat 在工厂自动化案例研究和 Savina actor 基准套件中的一系列示例中的表现力。
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.
登录
查看更多内容
类型规则的上下文表述及其在增量类型检查中的应用
DOI：
10.1145/2814270.2814277
发表时间：
2015
期刊：
Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications
影响因子：
--
作者：
Sebastian Erdweg;Oliver Bračevac;Edlira Kuci;Matthias Krebs;M. Mezini
通讯作者：
M. Mezini
可靠地扩展
DOI：
10.1145/3107937
发表时间：
2017
期刊：
ACM Transactions on Programming Languages and Systems (TOPLAS)
影响因子：
--
作者：
P. Trinder;Natalia Chechina;N. Papaspyrou;Konstantinos Sagonas;S. Thompson;Stephen Adams;Stavros Aronis;Robert Baker;Eva Bihari;Olivier Boudeville;Francesco Cesarini;M. D. Stefano;Sverker Eriksson;Viktória Fördős;A. Ghaffari;Aggelos Giantsios;Rickard Green;Csaba Hoch;David Klaftenegger;Huiqing Li;Kenneth Lundin;K. Mackenzie;Katerina Roukounaki;Yiannis Tsiouris;Kjell Winblad
通讯作者：
Kjell Winblad
会话类型的基础知识
影响因子：
1
作者：
V. Vasconcelos
通讯作者：
V. Vasconcelos
多方会话参与者的 Erlang 实现
影响因子：
--
作者：
S. Fowler
通讯作者：
S. Fowler
影响因子：
0.4
作者：
Ancona, Davide;Bono, Viviana;Yoshida, Nobuko
通讯作者：
Yoshida, Nobuko