论文标题
本地代数效应理论
Local Algebraic Effect Theories
论文作者
论文摘要
代数效应是计算效应，可以用一组基本操作以及它们之间的方程式描述。由于许多有趣的效果处理程序不尊重这些方程式，因此大多数方法都假设了一个琐碎的理论，既牺牲了推理能力和安全性。 我们提出了一种替代方法，类型系统跟踪程序中观察到的方程式，产生声音和灵活的逻辑，并为实用的优化和推理工具铺平方法。
Algebraic effects are computational effects that can be described with a set of basic operations and equations between them. As many interesting effect handlers do not respect these equations, most approaches assume a trivial theory, sacrificing both reasoning power and safety. We present an alternative approach where the type system tracks equations that are observed in subparts of the program, yielding a sound and flexible logic, and paving a way for practical optimizations and reasoning tools.
