一句话:提出带作用域操作的抽象语法的范畴模型,以分离代数效应与处理器的语法和语义。
本文针对代数效应与 handlers 编程中语法与语义难以分离的问题,提出一种带作用域操作(scoped operations)的抽象语法的范畴模型。与普通树节点不同,带作用域操作能够包含项的一整部分,即作用域;异常处理中的 catch 和非确定性计算中的 once 是典型例子。论文强调这类操作在程序组合即语法替换下的行为,并借助范畴结构给出语法与语义的抽象刻画。该工作为统一描述作用域操作的语法、替换与语义提供了理论基础,并通过实例说明模型能覆盖常见的效应操作。全文为理论建模,未报告实验评估。
Motivated by the problem of separating syntax from semantics in programming with algebraic effects and handlers, we propose a categorical model of abstract syntax with so-called scoped operations. As a building block of a term, a scoped operation is not merely a node in a tree, as it can also encompass a whole part of the term (a scope). Some examples from the area of programming are given by the operation catch for handling exceptions, in which the part in the scope is the code that may raise an exception, or the operation once, which selects a single solution from a nondeterministic computation. A distinctive feature of such operations is their behaviour under program composition, that is, syntactic substitution.