License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2019.30
URN: urn:nbn:de:0030-drops-105376
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/10537/
Go to the corresponding LIPIcs Volume Portal

Piróg, Maciej ; Polesiuk, Piotr ; Sieczkowski, Filip

Typed Equivalence of Effect Handlers and Delimited Control

pdf-format:
LIPIcs-FSCD-2019-30.pdf (0.5 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{pirg_et_al:LIPIcs:2019:10537,
  author =	{Maciej Pir{\'o}g and Piotr Polesiuk and Filip Sieczkowski},
  title =	{{Typed Equivalence of Effect Handlers and Delimited Control}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{30:1--30:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Herman Geuvers},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/10537},
  URN =		{urn:nbn:de:0030-drops-105376},
  doi =		{10.4230/LIPIcs.FSCD.2019.30},
  annote =	{Keywords: type-and-effect systems, algebraic effects, delimited control, macro expressibility}
}

Keywords: type-and-effect systems, algebraic effects, delimited control, macro expressibility
Collection: 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)
Issue Date: 2019
Date of publication: 18.06.2019
Supplementary Material: The formalisation of results presented in this paper, performed in the Coq proof assistant, can be found at https://pl-uwr.bitbucket.io/efftrans.zip.

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI