Danel Ahman: Runners in action

Abstract: Runners of algebraic effects, also known as comodels, provide a mathematical model of resource management. We show that they also give rise to a programming concept that models top-level external resources, as well as allows programmers to modularly define their own intermediate "virtual machines". We capture the core ideas of programming with runners in an equational calculus λ-coop, which we equip with a sound and coherent denotational semantics that guarantees the linear use of resources and execution of finalisation code.

We demonstrate runners in action through a variety of examples: hiding file handles from user code while guaranteeing their proper finalisation (by closing them); nesting runners to model user code inside a sandbox inside a VM inside an OS etc; nesting runners to instrument user code with cost models; nesting runners to implement (dynamically monitored and enforced) monotonic state on top of a runner that implements ordinary (non-monotonic) ML-style state; and pairing runners to combine different effects (e.g., state and file IO).

We also accompany λ-coop both with a prototype language implementation in OCaml and a library in Haskell. (This is joint work with Andrej Bauer. This talk is a follow-up to our more explorative seminars from earlier this year---you will see some new insights, a formal calculus, a finalisation theorem, and some new examples.)