paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Rows and Capabilities as Modal Effects

行与能力作为模态效应
POPL 10(POPL)2026匹配度 2/10 · 该论文属于纯 PL 类型系统与形式语义研究,讨论行多态与能力效应系统的模态编码,不涉及 LLM/Agent、静态分析在机器学习系统中的应用、浮点程序分析或贝叶斯程序分析。虽与程序语言理论相关,但不在用户当前研究画像的核心交叉方向上。引用 3 inbox
Wenhao Tang, Sam Lindley
crossref: 2026-09-10

AI 速览

一句话:提出统一框架,用模态效应类型编码并比较基于行多态与基于能力的效应系统,证明编码保持类型与语义。

效应处理器支持模块化地建模与组合计算效应,效应系统静态保证效应均被处理。近期实用效应系统多基于行多态或能力,但二者基础迥异,其精确关系尚不清晰;难点在于效应追踪通常与函数等特性纠缠。本文提出统一框架,用于编码、分析和比较效应系统。该框架推广模态效应类型,用模态将效应追踪与函数解耦,可精细控制追踪时机与方式,表达不同追踪策略。作者给出从基于行和基于能力的系统到该框架的宏翻译编码,证明编码保持类型与语义。编码揭示不同效应追踪机制的本质,支持直接分析差异,并为语言设计提供洞见。

问题
基于行多态与基于能力的效应系统基础不同,二者之间的精确关系尚不清晰,且效应追踪常与函数等特性纠缠,难以直接比较。
方法
推广模态效应类型,将效应追踪与函数解耦,并把基于行和基于能力的效应系统通过宏翻译编码进统一框架。
评估
证明这些编码保持类型与语义,并据此分析不同效应系统追踪机制的差异,得出语言设计启示。
原文摘要(Abstract)

Effect handlers allow programmers to model and compose computational effects modularly. Effect systems statically guarantee that all effects are handled. Several recent practical effect systems are based on either row polymorphism or capabilities. However, there remains a gap in understanding the precise relationship between effect systems with such disparate foundations. The main difficulty is that in both row-based and capability-based systems, effect tracking is typically entangled with other features such as functions. We propose a uniform framework for encoding, analysing, and comparing effect systems. Our framework exploits and generalises modal effect types, a recent novel effect system which decouples effect tracking from functions via modalities. Modalities offer fine-grained control over when and how effects are tracked, enabling us to express different strategies for effect tracking. We give encodings as macro translations from existing row-based and capability-based effect systems into our framework and show that these encodings preserve types and semantics. Our encodings reveal the essence of effect tracking mechanisms in different effect systems, enable a direct analysis on their differences, and provide practical insights on language design.

链接与引用

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

BibTeX
@article{abs-2507-10301,
  title = {Rows and Capabilities as Modal Effects},
  author = {Wenhao Tang and Sam Lindley},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {10},
  number = {POPL},
  year = {2026},
  doi = {10.1145/3776674}
}