Parametric Effect Monads and Semantics of Effect Systems
Parametric Effect Monads and Semantics of Effect Systems
复制标题
DOI：
10.1145/2535838.2535846
复制
发表时间：
2014-01-01
影响因子：
--
通讯作者：
Katsumata, Shin-ya
中科院分区：
文献类型：
--
作者：
Katsumata, Shin-ya
我们研究的基本属性的单子称为参数效应单子的推广，并将其应用到一般的效果系统的解释，其效果有顺序的组合操作。我们表明，参数效应单子承认类似物的结构和概念，存在的单子，如Kleisli三元组，状态单子和延续单子，Plotkin和电源的代数运算，和范畴TT-提升。我们还展示了一个系统的方法来产生效果和参数效果单子从单子态射。最后，我们引入了两个具有显式和隐式子效应的效应系统，并讨论了它们的指称语义和效应系统的可靠性。
We study fundamental properties of a generalisation of monad called parametric effect monad, and apply it to the interpretation of general effect systems whose effects have sequential composition operators. We show that parametric effect monads admit analogues of the structures and concepts that exist for monads, such as Kleisli triples, the state monad and the continuation monad, Plotkin and Power's algebraic operations, and the categorical TT-lifting. We also show a systematic method to generate both effects and a parametric effect monad from a monad morphism. Finally, we introduce two effect systems with explicit and implicit subeffecting, and discuss their denotational semantics and the soundness of effect systems.