On the expressive power of user-defined effects: effect handlers, monadic reflection, delimited control
On the expressive power of user-defined effects: effect handlers, monadic reflection, delimited control
复制标题
关于用户定义效果的表现力：效果处理程序、单子反射、分隔控制
DOI：
10.1145/3110257
复制
发表时间：
2017
影响因子：
--
通讯作者：
Forster Y
中科院分区：
文献类型：
--
作者：
Forster Y
我们比较了用户定义的计算效果的三个编程抽象的表达能力：Plotkin和Pretnar的效果处理程序，Filinski的一元反射，和分隔控制没有答案类型修改。这种比较允许对每种编程抽象的相对表达性进行精确的讨论。它还演示了敏感性的相对表现力的用户定义的效果，看似正交的语言features.We提出了三个演算，每个抽象，扩展利维的调用推值。对于每一个演算，我们提出的语法，操作语义，一个自然的类型和效果系统，并为效果处理程序和一元反射，一套理论的指称语义。我们建立其基本的元理论属性：安全性，终止，并在适用的情况下，健全性和充分性。使用Felleisen的宏观翻译的概念，我们表明，这些抽象可以宏观表达对方，并显示哪些翻译保持可输入性。我们使用足够的有限集理论的指称语义的一元演算，效果处理程序不能宏表示，同时保留类型由一元反射或分隔控制。我们的论证在对类型系统（如多态和归纳类型）进行简单更改时失败。我们补充我们的发展与机械化阿贝拉正规化。
We compare the expressive power of three programming abstractions for user-defined computational effects: Plotkin and Pretnar's effect handlers, Filinski's monadic reflection, and delimited control without answer-type-modification. This comparison allows a precise discussion about the relative expressiveness of each programming abstraction. It also demonstrates the sensitivity of the relative expressiveness of user-defined effects to seemingly orthogonal language features.We present three calculi, one per abstraction, extending Levy's call-by-push-value. For each calculus, we present syntax, operational semantics, a natural type-and-effect system, and, for effect handlers and monadic reflection, a set-theoretic denotational semantics. We establish their basic metatheoretic properties: safety, termination, and, where applicable, soundness and adequacy. Using Felleisen's notion of a macro translation, we show that these abstractions can macro-express each other, and show which translations preserve typeability. We use the adequate finitary set-theoretic denotational semantics for the monadic calculus to show that effect handlers cannot be macro-expressed while preserving typeability either by monadic reflection or by delimited control. Our argument fails with simple changes to the type system such as polymorphism and inductive types. We supplement our development with a mechanised Abella formalisation.
登录
查看更多内容
Haskell 中的 Monadic 解析
影响因子：
1.1
作者：
Graham Hutton;Erik Meijer
通讯作者：
Erik Meijer
DOI：
10.1016/0167-6423(90)90056-j
发表时间：
1990
期刊：
Sci. Comput. Program.
影响因子：
--
作者：
M. Spivey
通讯作者：
M. Spivey
第二届计算和演绎形式结构国际会议 (FSCD 2017)
DOI：
--
发表时间：
2017
期刊：
影响因子：
--
作者：
D. Miller
通讯作者：
D. Miller
用于定界延续的子结构类型系统
DOI：
--
发表时间：
2007
期刊：
International Conference on Typed Lambda Calculus and Applications
影响因子：
--
作者：
O. Kiselyov;Chung
通讯作者：
Chung
结合控制效果及其模型：静态、动态和分隔控制效果层次结构的游戏语义
影响因子：
0.8
作者：
J. Laird
通讯作者：
J. Laird