Martin Andrieux

We present a technique for expressing higher-order effects as algebraic ones. Algebraic effects provide a clean and modular account of computational effects, but they exclude higher-order effects such as local or catch. The standard representation of higher-order effects breaks the separation between syntax and interpretation that algebraic effects rely on. Our proposal, effect algebraization, transforms higher-order effects into combinations of algebraic effects. Each higherorder effect is split into a pair of operations-Open and Close-that together capture the same behavior using only algebraic constructs. The approach is illustrated on reader effects, ask and local. We also sketch a proof of semantics preservation: for every interpretation of the original higher-order effects, there exists a corresponding interpretation of the algebraized ones yielding the same result.

We present PySkel, a formalization of the semantics of a fragment of Python in Skel, a simple semantics description language. We describe a subset of the Python programming language including assignments, function calls, object oriented features, and exceptions. This subset is large enough to include challenges in the formalization of Python such as the handling of scopes. This formalization is used to generate an OCaml interpreter that can be used to run Python programs.

Algebraic effects are a long-studied programming language construct allowing the implementation of complex control flow in a structured way. With OCaml 5, such features are finally available in a mainstream programming language, giving us a great opportunity to experiment with varied concurrency constructs implemented as simple libraries. In this article, we explore how to implement concurrency features such as futures and active objects using algebraic effects, both in theory and in practice. On the practical side, we present a library of active objects implemented in OCaml, with futures, cooperative scheduling of active objects, and thread-level parallelism. On the theoretical side, we formalise the compilation of a future calculus that models our library into an effect calculus similar to the primitives available in OCaml; we then prove the correctness of the compilation scheme.