First-class Named Effect Handlers

See the HOPE’21 presentation (opens in new tab).

Algebraic effect handlers are a novel technique for adding composable computational effects to functional languages. While programming with distinct effects is concise, using multiple instances of the same effect is difficult to express. This work studies _named effect handlers_, such that an operation can explicitly yield to a specific handler by name. We propose a novel design of named handlers, where names are first-class values bound by regular lambdas, and are guaranteed not to escape through the standard rank-2 polymorphism. We also formalize dynamically instantiated named handlers, which can express first-class isolated heaps with dynamic mutable references. Finally, we provide an implementation of named handlers in the Koka programming language, showing that the proposed ideas enable supporting named handlers with moderate effort.