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