文章基本信息

标题：Typed Equivalence of Effect Handlers and Delimited Control
本地全文：下载
作者：Maciej Pir{'o}g ; Piotr Polesiuk ; Filip Sieczkowski 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2019
卷号：131
页码：1-16
DOI：10.4230/LIPIcs.FSCD.2019.30
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：It is folklore that effect handlers and delimited control operators are closely related: recently, this relationship has been proved in an untyped setting for deep handlers and the shift_0 delimited control operator. We positively resolve the conjecture that in an appropriately polymorphic type system this relationship can be extended to the level of types, by identifying the necessary forms of polymorphism, thus extending the definability result to the typed context. In the process, we identify a novel and potentially interesting type system feature for delimited control operators. Moreover, we extend these results to substantiate the folklore connection between shallow handlers and control_0 flavour of delimited control, both in an untyped and typed settings.
关键词：type-and-effect systems; algebraic effects; delimited control; macro expressibility