Towards Efficient Adjustment of Effect Rows

Abstract

Koka is a functional programming language with native support for algebraic effects and handlers. To implement effect handler operations efficiently, Koka employs a semantics where the handlers in scope are passed down to each function as an evidence vector. At runtime, these evidence vectors are adjusted using the open constructs to match the evidence for a particular function. All these adjustments can cause significant runtime overhead. In this paper, we present a novel transformation on the Koka core calculus that we call open floating. This transformation aims to float up open constructs and combine them in order to minimize the adjustments needed at runtime. Open floating improves performance by 2.5 $$\times $$ in an experiment. Furthermore, we formalize an aspect of row-based effect typing, including the closed prefix relation on effect rows, which clarifies the constraint on open floating.