Syntax and Semantics for Operations with Scopes
Syntax and Semantics for Operations with Scopes
复制标题
作用域操作的语法和语义
DOI：
--
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Mauro Jaskelioff
中科院分区：
文献类型：
--
作者：
Maciej Piróg;Tom Schrijvers;Nicolas Wu;Mauro Jaskelioff
出于在使用代数效果和处理程序的编程中将语法与语义分离的问题，我们提出了一个具有所谓作用域操作的抽象语法的分类模型。作为术语的构建块，作用域操作不仅仅是树中的一个节点，因为它还可以包含术语的整个部分（作用域）。编程领域的一些例子是处理异常的操作catch，其中作用域中的部分是可能引发异常的代码，或者是从不确定性计算中选择单个解决方案的操作once。这种操作的一个显著特征是它们在程序组合下的行为，即语法替换。我们的模型是基于什么加尼等人。调用显式替换单子，定义使用的初始代数语义的范畴内的endofunctors。我们还介绍了一种新的多排序代数，称为范围代数，它作为解释的语法范围。在一般情况下，作用域代数的风格的预层形式化的语法与绑定的菲奥雷等人。作为主要的技术成果，我们证明了我们的单子确实产生于自由对象的范畴内的作用域代数。重要的是，我们表明我们的结果是立即适用的。特别是，我们展示了一个Haskell实现，以及实际的，现实生活中的例子。
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. Our model is based on what Ghani et al. call the monad of explicit substitutions, defined using the initial-algebra semantics in the category of endofunctors. We also introduce a new kind of multi-sorted algebras, called scoped algebras, which serve as interpretations of syntax with scopes. In generality, scoped algebras are given in the style of the presheaf formalisation of syntax with binders of Fiore et al. As the main technical result, we show that our monad indeed arises from free objects in the category of scoped algebras. Importantly, we show that our results are immediately applicable. In particular, we show a Haskell implementation together with practical, real-life examples.
离开巢穴：具有交错作用域的变量的名义技术
DOI：
--
发表时间：
2015
期刊：
--
影响因子：
--
作者：
Gabbay MJ
通讯作者：
Gabbay MJ
相对单子形式化
DOI：
10.6092/issn.1972-5787/4389
发表时间：
2014
期刊：
--
影响因子：
--
作者：
Altenkirch T
通讯作者：
Altenkirch T
做是做是做
DOI：
10.1145/3009837.3009897
发表时间：
2017
期刊：
--
影响因子：
--
作者：
Lindley S
通讯作者：
Lindley S