Programming Languages

Efficient Compilation

Our goal is to compile effect handlers to efficient code. There are two aspects to performance: enabling compile-time optimizations and having efficient run-time constructs. Here we focus on the former.

As a first step, we embed a small functional language into Idris. It does not feature effect handlers, but only delimited control. Using dependent types, effectful statements are indexed by the “shape” of the stack. The language serves as case study and shows how to efficiently compile languages with control effects when the shape of the stack is known at compile time.

As a second step, we add effect handlers. We show that the translation to iterated continuation-passing style and the formulation of effect handlers in capability-passing style together make it possible to eliminate, at compile time, all overhead from using effect handlers. This is only possible under certain conditions, which we make explicit.

Currently, we are working on an intermediate language which allows for both, the compile-time optimizations that we have investigated and at the same time the generation of efficient low-level code.

Related Publications

Compiling Effect Handlers in Capability-Passing Style

by Philipp Schuster, Jonathan Immanuel Brachthäuser, and Klaus Ostermann

In Proc. Int’l Conf. Functional Programming (ICFP). ACM Press, 2020.

Learn More

Zero-cost Effect Handlers by Staging (Technical Report)

by Philipp Schuster, Jonathan Immanuel Brachthäuser, and Klaus Ostermann

Technical report. University of Tübingen, Germany, 2019.

Learn More

Typing, Representing, and Abstracting Control: Functional Pearl

by Philipp Schuster and Jonathan Brachthäuser

In Proceedings of the International Workshop on Type-Driven Development. ACM Press, 2018.

Learn More