paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Speak Now: Safe Actor Programming with Multiparty Session Types

Speak Now:基于多方会话类型的安全 Actor 编程
OOPSLA 10(OOPSLA1)2026匹配度 1/10 · 论文属于并发编程语言、类型系统与多方会话类型(MPST)方向,未涉及 LLM、Agentic 程序、ML 系统、浮点程序分析或贝叶斯程序分析,与用户研究画像的核心交叉方向基本无关;Actor 模型仅可能作为背景,不构成直接匹配。引用 0 inbox
Simon Fowler, Raymond Hu
crossref: 2026-09-10

AI 速览

一句话:提出 Maty,首个支持静态多方会话类型且允许 Actor 参与多个会话的 Actor 语言设计。

Erlang/Elixir 等 Actor 语言适合构建可扩展、可靠的分布式应用,但其通信模式缺乏形式规约,容易出现消息不匹配和死锁;而多方会话类型(MPST)此前难以适配 Actor 的多发送者、单接收者通信。本文提出 Maty,首个同时支持静态多方会话类型和 Actor 参与多个会话的 Actor 语言设计。其核心是通过流敏感效果系统、事件驱动编程风格和一等消息处理器来实施会话类型,从而保证通信安全:进程不会发送或接收意外消息,也不会因等待永不到来的消息而卡住。Maty 还扩展支持 Erlang 式监督与级联失败,并保持强元理论。作者用 Scala 的 API 生成方式实现 Maty,并通过 Savina 基准、工厂场景和聊天服务器展示表达能力。

问题
Actor 语言通信模式缺乏形式规约,易导致消息不匹配与死锁;MPST 因 Actor 的多发送者、单接收者特点难以直接适用。
方法
提出 Maty,用流敏感效果系统、事件驱动风格与一等消息处理器支持静态多方会话类型及 Actor 参与多个会话,保证通信安全,并扩展 Erlang 式监督/级联失败。
评估
以 Scala API 生成方式实现,在 Savina Actor 基准、工业工厂场景和聊天服务器上展示表达力与元理论保持。
原文摘要(Abstract)

Actor languages such as Erlang and Elixir are widely used for implementing scalable and reliable distributed applications, but the informally-specified nature of actor communication patterns leaves systems vulnerable to costly errors such as communication mismatches and deadlocks. Multiparty session types (MPSTs) rule out communication errors early in the development process, but until now, the many-sender, single-receiver nature of actor communication has made it difficult for actor languages to benefit from session types. This paper introduces Maty, the first actor language design supporting both static multiparty session typing and the full power of actors taking part in multiple sessions . Maty therefore combines the error prevention mechanism of session types with the scalability and fault tolerance of actor languages. Our main insight is to enforce session typing through a flow-sensitive effect system, combined with an event-driven programming style and first-class message handlers. Using MPSTs allows us to guarantee communication safety: a process will never send or receive an unexpected message, nor will a session get stuck because an actor is waiting for a message that will never be sent. We extend Maty to support Erlang-style supervision and cascading failure, and show that this preserves Maty’s strong metatheory. We implement Maty in Scala using an API generation approach, and demonstrate the expressiveness of our model by implementing a representative sample of the widely-used Savina actor benchmark suite; an industry-supplied factory scenario; and a chat server.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot3792,
  title = {Speak Now: Safe Actor Programming with Multiparty Session Types},
  author = {Simon Fowler and Raymond Hu},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {10},
  number = {OOPSLA1},
  year = {2026},
  doi = {10.1145/3798267}
}