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