Continuation passing style for effect handlers

Daniel Hillerström, Sam Lindley, Robert Atkey, KC Sivaramakrishnan

Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 2 Citations

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.
LanguageEnglish
Title of host publication2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
EditorsDale Miller
Place of PublicationGermany
Pages18:1-18:19
Number of pages19
DOIs
StatePublished - 3 Sep 2017

Publication series

NameLeibniz International Proceedings in Informatics (LIPIcs)
Volume84

Fingerprint

Computer programming languages
Semantics

Keywords

  • effect handlers
  • delimited control
  • continuation passing system
  • CPS
  • algebraic effects

Cite this

Hillerström, D., Lindley, S., Atkey, R., & Sivaramakrishnan, KC. (2017). Continuation passing style for effect handlers. In D. Miller (Ed.), 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017) (pp. 18:1-18:19). [18] (Leibniz International Proceedings in Informatics (LIPIcs); Vol. 84). Germany. DOI: 10.4230/LIPIcs.FSCD.2017.18
Hillerström, Daniel ; Lindley, Sam ; Atkey, Robert ; Sivaramakrishnan, KC. / Continuation passing style for effect handlers. 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). editor / Dale Miller. Germany, 2017. pp. 18:1-18:19 (Leibniz International Proceedings in Informatics (LIPIcs)).
@inproceedings{e6cb0c3222794e48bf38cf44e46fe4aa,
title = "Continuation passing style for effect handlers",
abstract = "We present Continuation Passing Style (CPS) translations for Plotkin and Pretnar's effect handlers with Hillerstr{\"o}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.",
keywords = "effect handlers, delimited control, continuation passing system, CPS, algebraic effects",
author = "Daniel Hillerstr{\"o}m and Sam Lindley and Robert Atkey and KC Sivaramakrishnan",
year = "2017",
month = "9",
day = "3",
doi = "10.4230/LIPIcs.FSCD.2017.18",
language = "English",
series = "Leibniz International Proceedings in Informatics (LIPIcs)",
pages = "18:1--18:19",
editor = "Dale Miller",
booktitle = "2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)",

}

Hillerström, D, Lindley, S, Atkey, R & Sivaramakrishnan, KC 2017, Continuation passing style for effect handlers. in D Miller (ed.), 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)., 18, Leibniz International Proceedings in Informatics (LIPIcs), vol. 84, Germany, pp. 18:1-18:19. DOI: 10.4230/LIPIcs.FSCD.2017.18

Continuation passing style for effect handlers. / Hillerström, Daniel; Lindley, Sam; Atkey, Robert; Sivaramakrishnan, KC.

2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). ed. / Dale Miller. Germany, 2017. p. 18:1-18:19 18 (Leibniz International Proceedings in Informatics (LIPIcs); Vol. 84).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

T1 - Continuation passing style for effect handlers

AU - Hillerström,Daniel

AU - Lindley,Sam

AU - Atkey,Robert

AU - Sivaramakrishnan,KC

PY - 2017/9/3

Y1 - 2017/9/3

N2 - 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.

AB - 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.

KW - effect handlers

KW - delimited control

KW - continuation passing system

KW - CPS

KW - algebraic effects

U2 - 10.4230/LIPIcs.FSCD.2017.18

DO - 10.4230/LIPIcs.FSCD.2017.18

M3 - Conference contribution

T3 - Leibniz International Proceedings in Informatics (LIPIcs)

SP - 18:1-18:19

BT - 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)

CY - Germany

ER -

Hillerström D, Lindley S, Atkey R, Sivaramakrishnan KC. Continuation passing style for effect handlers. In Miller D, editor, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Germany. 2017. p. 18:1-18:19. 18. (Leibniz International Proceedings in Informatics (LIPIcs)). Available from, DOI: 10.4230/LIPIcs.FSCD.2017.18