paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Algebraic effects and handlers for arrows

面向 Arrow 的代数效应与处理器
JFP vol.342024匹配度 2/10 · 该论文属于纯 PL 形式语义与函数式编程理论,研究 Arrow 演算的代数效应/处理器及操作-指称语义,不涉及静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析,与用户核心研究方向仅有很间接的 PL 理论基础关联。引用 1 inbox
TAKAHIRO SANADA
crossref: 2026-09-10

AI 速览

一句话:为 Arrow 演算引入代数效应与处理器,给出操作/指称语义,并证明可靠性与充分性。

论文研究如何在 Arrow 演算中支持代数效应及其处理器。作者在 Lindley、Wadler 与 Yallop 的 Arrow 演算基础上,扩展出带操作和 handler 的 arrow calculus,并同时给出操作语义与指称语义。指称语义使用范畴与 profunctor 双范畴中的强 (pro)monad A 来建模;由于大小问题,强 monad A 的构造并不平凡。为此,作者分析 A-代数,将 handler 解释为 A-代数之间的 A-同态,并由此反向指导语法与操作语义的设计。最后证明操作语义相对于指称语义的可靠性与充分性。

问题
如何为 Arrow 演算扩展代数效应与处理器,并为其提供统一的操作语义与指称语义?
方法
在 Lindley-Wadler-Yallop Arrow 演算上定义带 operations/handlers 的 calculus;用 categories and profunctors 双范畴中的强 (pro)monad A 构造指称模型,并通过 A-代数与 A-同态解释 handler,据此导出语法和操作语义。
评估
证明操作语义对指称语义的 soundness 与 adequacy 定理。
原文摘要(Abstract)

Abstract We present an arrow calculus with operations and handlers and its operational and denotational semantics. The calculus is an extension of Lindley, Wadler and Yallop’s arrow calculus. The denotational semantics is given using a strong (pro)monad $\mathcal{A}$ in the bicategory of categories and profunctors. The construction of this strong monad $\mathcal{A}$ is not trivial because of a size problem. To build denotational semantics, we investigate what $\mathcal{A}$ -algebras are, and a handler is interpreted as an $\mathcal{A}$ -homomorphisms between $\mathcal{A}$ -algebras. The syntax and operational semantics are derived from the observations on $\mathcal{A}$ -algebras. We prove the soundness and adequacy theorem of the operational semantics for the denotational semantics.

链接与引用

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

BibTeX
@article{paperbot2686,
  title = {Algebraic effects and handlers for arrows},
  author = {TAKAHIRO SANADA},
  journal = {Journal of Functional Programming},
  volume = {34},
  year = {2024},
  doi = {10.1017/s0956796824000066}
}