Effects with Variable Binding

Abstract

Algebraic effects are a simple and modular approach to modelling effectful computations. They are commonly embedded in functional programming languages, where they provide a lightweight and powerful way of programming with effects. Such embeddings typically use host language functions to represent continuations of effectful operations. While host language functions allow for easy programming with effects, they also hinder programmers wishing to define custom optimizations for effectful programs. Specifically, we cannot, in general, know what precisely a host language function does from within the language. This paper presents a solution to this problem by embedding algebraic effects as intrinsically typed, De Bruijn-indexed syntax. Working in Agda, we demonstrate how this provides a safe-by-construction model of effectful computations, with support for optimizations that inspect and transform variable binding. We intend this to be the basis of a verified compiler that uses our notion of effects with variable binding as an intermediate representation.