Lift Inference for Lexical Effect Handlers with Second-Class Functions
Algebraic effects and handlers are a popular language feature among programming language researchers and they also start to gain traction in more industrially used languages. This increasingly raises the need for efficient implementation techniques that eliminate the overhead incurred by the powerful abstraction. One promising approach for lexical effect handlers is to use capability-passing style. Translating lexical handlers into iterated continuation-passing style has been shown to open up large potential for optimizations, potentially removing the overhead of the added abstraction altogether. However, to avoid a runtime search for the correct handler, the translation requires knowledge about the nesting structure of handlers. We show how to infer this information for $\mathsf{Effekt}$, a language with a second-class restriction on functions. We present a translation from $\mathsf{System};\Xi$ (the core calculus of $\mathsf{Effekt}$) to $\Lambda_{\mathsf{\textbf{\textsf{cap}}}}$, a language with a region system and explicit subregion evidence, inferring the missing information. This allows us to immediately reuse the existing iterated CPS translation from $\Lambda_{\mathsf{\textbf{\textsf{cap}}}}$ and unlock the optimization potential.
Sun 11 SepDisplayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Prague change
09:00 - 10:30 | |||
09:00 30mTalk | Lift Inference for Lexical Effect Handlers with Second-Class Functions HOPE Marius Müller University of Tübingen, Philipp Schuster University of Tübingen, Jonathan Immanuel Brachthäuser University of Tübingen, Klaus Ostermann University of Tübingen | ||
09:30 30mTalk | Higher order programming with probabilistic effects: A model of stochastic memoization and name generation HOPE | ||
10:00 30mTalk | Effect Handlers in Scope, EvidentlyVirtual HOPE File Attached |