Modular Semantics for Algebraic Effects

Abstract

An important part of writing programs is to ensure that these programs behave as expected. Oftentimes, unit tests are written to show that parts of a program behave correctly in specific cases. Rather than resort to testing only some cases, we can use formal verification to prove that our program behaves correctly in all possible cases. Purely functional programming languages allow us to reason about programs as mathematical functions, but they do not contain side effects (impure operations). Using free monads, we can introduce the syntax of impure operations into a pure programming language, allowing one to syntactically define programs containing side effects. To execute and reason about such programs, we define semantics for the free monad by interpreting their impure operations within a target monad. By defining semantics in terms of monad transformers, combining them comes down to building up a monad transformer stack, and the choice of base monad gives rise to different kinds of semantics. This lets us write and reason about programs containing a variety of side effects in a modular way.