尚未生成 AI 速览(可能缺少 API key 或等待下次运行补跑)。
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 原文 ·
@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}
}