Runners in Action
University of Ljubljana
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.