Distributive Interaction of Algebraic Effects

Abstract

While monadic effects are widespread in modern functional programming, the idea of formulating computational effects as algebraic theories seems a less familiar one to programmers. One appealing feature of such algebraic effects is the clear decoupling between specification and implementation (or in more model-theoretic terms, syntax versus semantics). With monads, this distinction is arguably less clear. But perhaps the most compelling reason for considering algebraic effects is the relative ease by which such effects can be combined. This point is clearly of much relevance to the semantics of programming languages since in much of modern software development, one often deals with multiple interacting effects. As a simple example, we may want a program that not only keeps track of some state across the computation (e.g. a parser consuming a string of text), but also account for the possibility of failure. But it is well known that there is more than one way to combine these state and exception effects, each corresponding to a different composition. Neither can be considered canonical, since both have their use cases. It turns out that under the lens of algebraic effects, both interactions can be understood in terms of straightforward amalgamations of the respective equational laws. Both of these constructions arise naturally from the categorical structure of Lawvere theories, a more abstract formulation of equational theories as categories. In this dissertation we seek to further the understanding of combining effects, especially from this more algebraic perspective. Of particular interest is a distributive tensor construction on Lawvere theories that does not seem to be very widely known. The distributive tensor plays a leading role in many examples of computational interest, and two such applications will be considered in some depth. Firstly, from the observation that various combinatorial search strategies are characterised by two equivalent formulations as bunch monadic types and as more structured theories of monoids, we give a number of correspondence results. Furthermore, it is also shown that the list monad transformer is exactly a distributive tensor from the theory of monoids. The second application considers in some detail a derivation of the geometrically convex monad, that is the combination of probabilistic and nondeterministic choice effects, called combined choice. As it is no easy task to capture the equational properties between probabilistic and nondeterministic choice, a technique is explored for reasoning about such equations visually by taking a geometric interpretation of the free models of combined choice, as convex polygons on a plane.