Two papers of the effects research team have been conditionally accepted at the International Conference of Functional Programming 2020.

Capability-Passing Style for Zero-Cost Effect Handlers

by Philipp Schuster
AlumniPhilipp Schuster, Jonathan Brachthäuser
AlumniJonathan Immanuel Brachthäuser, and Klaus Ostermann
HeadKlaus Ostermann.

Abstract

Effect handlers encourage programmers to abstract over repeated patterns of complex control flow. As of today, this abstraction comes at a significant price in performance. In this paper, we aim to achieve abstraction without regret for effect handlers. We present a language for effect handlers in capability-passing style (lambda-cap) and an implementation of this language as a translation to simply-typed lambda calculus in iterated continuation-passing style. A suite of benchmarks indicates that the novel combination of capability-passing style and iterated CPS enables significant speedups over existing languages with effect handlers or control operators. Our implementation technique is very general and allows us to generate code in any language that supports first-class functions. We then identify a subset of programs for which we can further improve the performance and guarantee full elimination of the effect handler abstraction. To formally capture this subset, we refine lambda-cap; to llambda-cap; with a more restrictive type system. We present a type-directed translation for llambda-cap; that inserts staging annotations and prove that no abstractions or applications related to effect handlers occur in the translated program. Using this second translation we observe additional speedups in some of the benchmarks.

More about this publication

Effect Handlers, Evidently

by Ningning Xie, Jonathan Brachthäuser
AlumniJonathan Immanuel Brachthäuser, Daniel Hillerström, Philipp Schuster
AlumniPhilipp Schuster, and Daan Leijen.

Abstract

Algebraic effect handlers are a powerful way to incorporate effects in a programming language. Sometimes perhaps even too powerful. In this article we define a restriction of general effect handlers with scoped resumptions. We argue one can still express all important effects, while improving local reasoning about effect handlers. Using the newly gained guarantees, we define a sound and coherent evidence translation for effect handlers which directly passes the handlers as evidence to each operation. We prove full soundness and coherence of the translation into plain lambda calculus. The evidence in turn enables efficient implementations of effect operations; in particular, we show we can execute tail-resumptive operations in place (without needing to capture the evaluation context), and how we can replace the runtime search for a handler by indexing with a constant offset.

More about this publication

Publications