Reasoning about coroutines

In computer science, a side effect modifies some state outside local environment of a program, which means that a side effect has an interaction with the outside world without returning to the original program flow. A very famous example for side effects is exceptions. The main difference between effects and exceptions is that when an effect is raised, the remainder of program is captured and saved in what we call the continuation in order to potentially be resumed later. Effect handlers give semantics to effects raised into the program by defining procedure to deal with effects defined in the program. Effect handlers have access to the continuation variables and can decide to call them (sometimes more than once).

Algebraic effects and algebraic effect handlers are gaining in popularity as an approach of modelling side-effects in a program. Programming using algebraic effects has many advantages as they can be freely composed, and there is a natural separation between their declaration and occurrences within a program and their semantics since the semantics are only given to an effect when it is handled by a handler. This composition adds an extra layer of modularity to using algebraic effects and handlers. We can change the behaviour of the program by applying different handlers to deal with effects differently.

Yet, even though efficient runtime representations have already been studied, most handler-based programs are still much slower than hand-written code. In this thesis, we address the performance issue of handler-based programs while maintaining the modularity they provide. We investigate this issue in two paradigm: Functional Programming and Logic Programming. In the Functional programming part, we use Eff which an ML based language with effects. We show that the performance gap can be drastically narrowed (in some cases even closed) by means of type-and-effect directed optimising compilation. The main aim of these optimisations is to reduce handler related code.

Our approach consists of two stages. Firstly, we combine source-to-source transformations with function specialisation in order to aggressively reduce handler applications. Secondly, we show how to elaborate the source language into a handler-less target language in a way that incurs no overhead for non-effectful computations. Our approach eliminates much of the overhead of handlers and yields competitive performance with hand-written OCaml code. However, implementing these optimisations for Eff is overly error-prone because its core language is implicitly-typed, making code transformations very fragile. To remedy this, we also present in this work an explicitly-typed polymorphic core calculus for algebraic effect handlers with a subtyping-based type-and-effect system to remedy this fragility. The proposed calculus tracks the use of subtyping explicitly by means of cast expressions with coercions as subtyping proofs, quickly exposing typing bugs during program transformations. Our typing-directed elaboration in the new calculus comes with a constraint-based inference algorithm that turns an implicitly-typed Eff-like language into the calculus. Moreover, all coercions and effect information can be erased in a straightforward way, demonstrating that coercions have no computational content.

For the Logic Programming part, we build on delimited control primitives for Prolog to introduce algebraic effects and handlers to the language. Delimited control is used to dynamically manipulate the program control-flow, and to implement a wide range of control-flow and dataflow effects on top of. Unfortunately, delimited control is a rather primitive language feature that is not easy to use. As a remedy, this work introduces algebraic effect handlers as a high-level and structured way of defining new side-effects in a modular fashion. We illustrate the expressive power of the feature and provide an implementation by means of elaboration into the delimited control primitives. The latter add a non-negligible performance overhead when used extensively. To address this issue, we present an optimised compilation approach that combines partial evaluation with dedicated rewrite rules. The rewrite rules are driven by a lightweight effect inference system that analyses what effect operations may be called by a goal. We illustrate the effectiveness of this approach on a range of benchmarks that shows that the overhead of delimited control is diminished after the optimisation process.