论用户定义效应的表达力：效应处理器、单子反射、定界控制
计算机科学中的逻辑
2017-03-01 v2 编程语言
摘要
我们比较了三种用于用户定义计算效应的编程抽象的表达力：Bauer和Pretnar的效应处理器(effect handlers)、Filinski的单子反射(monadic reflection)以及无答案类型修改的定界控制(delimited control)。该比较允许对每种编程抽象的相对表达力进行精确讨论。它还展示了用户定义效应的相对表达力对看似正交的语言特征的敏感性。我们提出了三种演算，每种抽象一个，扩展了Levy的按值调用推送(call-by-push-value)。对于每个演算，我们给出了语法、操作语义、自然类型与效应系统，并且对于效应处理器和单子反射，给出了集合论指称语义。我们确立了它们的基本元理论性质：安全性、终止性，以及在适用情况下的可靠性和充分性。利用Felleisen的宏翻译概念，我们展示了这些抽象可以宏表达彼此，并展示了哪些翻译保持可类型化。我们利用单子演算的适当的有限集合论指称语义来证明，效应处理器不能在保持可类型化的前提下被单子反射或定界控制宏表达。我们以机械化的Abella形式化补充了我们的研究。
引用
@article{arxiv.1610.09161,
title = {On the Expressive Power of User-Defined Effects: Effect Handlers, Monadic Reflection, Delimited Control},
author = {Yannick Forster and Ohad Kammar and Sam Lindley and Matija Pretnar},
journal= {arXiv preprint arXiv:1610.09161},
year = {2017}
}