Continuation passing style for effect handlers

Hillerström, Daniel and Lindley, Sam and Atkey, Robert and Sivaramakrishnan, KC; Miller, Dale, ed. (2017) Continuation passing style for effect handlers. In: 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs) . Dagstuhl Publishing, Germany, 18:1-18:19. (https://doi.org/10.4230/LIPIcs.FSCD.2017.18)

[thumbnail of Hillerstrom-etal-FSCD-2017-continuation-passing-style-for-effect-handlers]
Preview
 Text. Filename: Hillerstrom_etal_FSCD_2017_continuation_passing_style_for_effect_handlers.pdf
Final Published Version
License: Creative Commons Attribution 4.0 logo
Download (702kB)| Preview

Abstract

We present Continuation Passing Style (CPS) translations for Plotkin and Pretnar's effect handlers with Hillerström and Lindley's row-typed fine-grain call-by-value calculus of effect handlers as the source language. CPS translations of handlers are interesting theoretically, to explain the semantics of handlers, and also offer a practical implementation technique that does not require special support in the target language's runtime. We begin with a first-order CPS translation into untyped lambda calculus which manages a stack of continuations and handlers as a curried sequence of arguments. We then refine the initial CPS translation first by uncurrying it to yield a properly tail-recursive translation and second by making it higher-order in order to contract administrative redexes at translation time. We prove that the higher-order CPS translation simulates effect handler reduction. We have implemented the higher-order CPS translation as a JavaScript backend for the Links programming language.

ORCID iDs

Hillerström, Daniel, Lindley, Sam, Atkey, Robert ORCID logoORCID: https://orcid.org/0000-0002-4414-5047 and Sivaramakrishnan, KC; Miller, Dale
CORE (COnnecting REpositories)