The Free Monad
In functional programming, monads are how we structure and sequence computations with side effects like state, IO, or failure. Each monad bakes its semantics into its definition. State updates a state, IO talks to the world, Maybe short-circuits on failure. Free monads provide a bit more freedom, in that they let you write effectful programs as pure data, without committing to a particular interpretation of the effects. You can write monadic programs in do notation, describing some sequence of effects, and only decide what they mean later. For example, these are just a few things you can do with a program-as-data:
- Run it directly
- Pretty print it
- Analyze it statically
- Track its resource usage
Each of these corresponds to a different interpreter. This approach also allows effects to be combined without you having to get tangled up in monad transformers.
This three-part series will introduce the free monad in Lean. In this first part we will introduce and implement the free monad from first principles, and discuss some of the finesse involved in implementing it in a proof assistant like Lean, compared to a language like Haskell.
In part 2 we will study the universal property of free monads and what it provides for us as programmers. Finally in part 3, we will use what we’ve learned to build and verify a real interpreter for a small language, making elegant use of freeness to combine effectful computations.
This series assumes you know basic concepts from both category theory and functional programming, including functors, monads, and inductive datatypes. All of the code in this blog post has been packaged into a library, now merged into CSlib.1