From Capabilities to Regions: Enabling Efficient Compilation of Lexical Effect Handlers
Effect handlers are a high-level abstraction that enables programmers to use effects in a structured
way. They have gained a lot of popularity within academia and subsequently also in industry. However,
the abstraction often comes with a significant runtime cost and there has been intensive research
recently on how to reduce this price.
A promising approach in this regard is to implement effect handlers using a CPS translation and
to provide sufficient information about the nesting of handlers. With this information the
CPS translation can decide how effects have to be lifted through handlers, i.e., which handlers
need to be skipped, in order to handle the effect at the correct place. A structured way to make
this information available is to use a calculus with a region system and explicit subregion
evidence. Such calculi, however, are quite verbose, which makes them impractical to use as a
source-level language.
We present a method to infer the lifting information for a calculus underlying a source-level language.
This calculus uses second-class capabilities for the safe use of effects. To do so, we define a typed translation
to a calculus with regions and evidence and we show that this lift-inference translation is typability-
and semantics-preserving. On the one hand, this exposes the precise relation between the second-class
property and the structure given by regions. On the other hand, it closes a gap in a compiler pipeline
enabling efficient compilation of the source-level language. We have implemented lift inference in this
compiler pipeline and conducted benchmarks which indicate that the approach is indeed working.