Elaine: Elaborations of Higher-Order Effects as First-Class Language Feature

Abstract

Algebraic effects and handlers have become a popular abstraction for effectful computation, with implementations even in mainstream programming languages, such as OCaml. The operations of an algebraic effect define the syntax of the effect, while handlers define the semantics. This provides modularity, because we can choose which handler to apply to a computation. However, we cannot write handlers for many higher-order operations; operations that take effectful computations as parameters. Such higher-order operations can therefore not enjoy this modularity. Hefty algebras provide an additional layer of abstraction in the form of elaborations to make implementations of higher-order operations modular as well. Several languages, such as Koka, natively support algebraic effects and handlers. However, until now, no languages have been created with native support for higher-order effects. In this thesis, we introduce Elaine, a language featuring both handlers for algebraic effects and elaborations for higher-order effects. Additionally, we introduce implicit elaboration resolution; a type-directed procedure which infers the appropriate elaborations from context. We conjecture that hefty algebras are the semantics for Elaine. We provide a specification for Elaine, including its syntax definition, typing judgments and reduction semantics. This specification is implemented in a publicly available prototype which can type check and evaluate the set of example programs included with this thesis.