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