paperbot · PL 论文追踪

全部论文 待读 收藏

P2 The Relative Monadic Metalanguage

相对单子元语言
POPL 10(POPL)2026匹配度 2/10 · 论文属于纯 PL 形式语义与语言设计,研究相对单子、graded monads 与 arrows,未涉及静态分析、浮点程序分析、贝叶斯程序分析或 LLM/Agent 与 PL 的交叉。仅与 PL 理论基础有较弱关联,与用户研究画像的核心问题基本无关。引用 1 inbox
Jack Liell-Cock, Zev Shirazi, Sam Staton
crossref: 2026-09-10

AI 速览

一句话:将单子元语言推广到相对单子设置,给出完备语义,并据此重新刻画 graded monads 与 arrows 并设计保守扩展语言。

相对单子为计算提供更受控的视角。论文将单子元语言推广到相对设置,提出相对单子元语言,并用强相对单子给出完备语义。基于此,作者重新审视文献中两个程序演算:其一为 graded monads 设计线性-非线性语言 LNL-RMM,并通过语义证明它是 graded monadic metalanguage 的保守扩展;其二为 arrow calculus 提供完备语义,说明它可视为受限的相对单子元语言,进而引入 ARMM——一种 computational lambda calculus 风格的 arrows 语言,并证明它保守扩展 arrow calculus。该工作统一了 graded monads 与 arrows 的语义解释,并为相应语言设计提供范畴论基础。

问题
如何将单子元语言及其语义从普通单子推广到相对单子,以统一刻画 graded monads 和 arrows 等受控计算演算。
方法
定义相对单子元语言,使用强相对单子给出完备语义;据此构造 LNL-RMM 和 ARMM,并证明保守扩展。
评估
通过语义证明表明 LNL-RMM 是 graded monadic metalanguage 的保守扩展,ARMM 保守扩展 arrow calculus;并证明 arrow calculus 的完备语义。
原文摘要(Abstract)

Relative monads provide a controlled view of computation. We generalise the monadic metalanguage to a relative setting and give a complete semantics with strong relative monads. Adopting this perspective, we generalise two existing program calculi from the literature. We provide a linear-non-linear language for graded monads, LNL-RMM, along with a semantic proof that it is a conservative extension of the graded monadic metalanguage. Additionally, we provide a complete semantics for the arrow calculus, showing it is a restricted relative monadic metalanguage. This motivates the introduction of ARMM, a computational lambda calculus-style language for arrows that conservatively extends the arrow calculus.

链接与引用

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

BibTeX
@article{LiellCockSS26,
  title = {The Relative Monadic Metalanguage},
  author = {Jack Liell-Cock and Zev Shirazi and Sam Staton},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {10},
  number = {POPL},
  year = {2026},
  doi = {10.1145/3776702}
}