Part 1: Defining the Free Monad in Lean

1. Introduction

Free monads provide a way to represent effectful sequential programs as pure syntactic data, separate from their interpretation. You describe what should happen as an abstract tree of effects, leaving open how you want it to happen. By decoupling syntax from semantics like this you gain full control over how programs are evaluated and interpreted - for example we could interpret a syntax tree in multiple ways:

• Run it directly
• Pretty print it
• Analyze it statically

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 four-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 functional language like Haskell.

In part 2 we will further explore some theory and study initial algebras and catamorphisms, and how they give rise to interpreters for effectful computation trees. In part 3 we will study the universal property of free monads and what it provides for us as programmers. Finally in part 4, 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. You can find most of the code used here at this Mathlib PR

Table of Contents

1. Introduction
2. Free Objects
3. Free Monads
   • In Haskell
   • In Lean
4. Conclusion

2. Free Objects

Before getting into free monads, we will first consider what it means for some structure to be “free”. This section is pretty mathematical but if you’re like me it may help understand things down the line when we start coding, otherwise you can skim this section.

As a familiar example, consider a vector space $V$ over a field $F$ with basis $B$. $V$ is said to be “free” on $B$: it is the smallest vector space containing $B$, and is generated by taking all finite linear combinations of elements in $B$ with coefficients in $F$. A similar construction is done for other algebraic structures, for example the free group $G_S$ on a set $S$ consists of all the reduced words of elements of $S$.

The free object which is most familiar to the programmer is the free monoid on a datatype α, aka the type List α. This is of course the type of all finite sequences of elements of α, which forms the monoid (List α, ++, []), where ++ is list concatenation.

How can we generalize this? In general categories, free constructions are defined as left adjoints to forgetful functors. If a forgetful functor $U : C \to D$ has a left adjoint $F : D \to C$, then for any $x \in D$, $Fx$ is the free $C$-object on $x$.

Consider the functor $U : \texttt{Grp} \to \texttt{Set}$ which forgets the group structure and returns the underlying set. If $F : \texttt{Set} \to \texttt{Grp}$ is left adjoint to $U$, then $FX$ is the free group on $X$ for any set $X$.

This can also be stated in terms of a universal property. Slightly informally, an object $X’$ is the free $C$-object on $X$ if there is an embedding $\iota : X \to X’$ such that for any $C$-object $G$ with a map $h : X \to G$, there is a unique $C$-morphism $\hat{h} : X’ \to G$ such that the following diagram commutes:

(Exercise: Let $U : \texttt{Grp} \to \texttt{Set}$ be the forgetful functor and $F$ a left adjoint. Prove $FX$ satisfies the above universal property for any set $X$.)

The moral of the story here is that a free construction is the canonical way to generate the desired structure from some underlying data, adding only what is necessary to satisfy the rules of the desired structure. Our free monad is thus the canonical monad generated from an endofunctor, satisfying nothing other than the monad laws.

3. Free Monads

“A monad is just a monoid in the category of endofunctors, what’s the problem?”

You’ve probably heard someone jokingly say monads are just monoids in the category of endofunctors. It’s technically a correct definition, but it tells you nothing if you don’t speak category theory. However, understanding monads as monoids may actually help us construct the free monad by analogy to the free monoid, aka the List type. I know I promised this was an article on Lean but we will start with some Haskell first.

3.1. In Haskell

The List type is defined as follows:

data List a = Nil | Cons a (List a) 

Categorically this looks like:

i.e., the List type is a fixed point of the functor:

Part 2 goes into more detail about inductive types as fixed points of functors. This part is just briefly explaining the analogy between lists and free monads, and the mathematical detail is not centrally important yet

The List functor maps a type to its free monoid, and we want our free monad functor to map an endofunctor to its free monad. The heart of the analogy is that lists are to types as free monads are to functors. So, we “lift” what we have done on lists in the category of types to free monads in the category of endofunctors. In programmer terms, we are defining a higher-order functor that is analogous to List, but acts on functors rather than types.

Our monoidal product in the endofunctor category is functor composition, the terminal object is the identity functor, and coproduct is defined component-wise. Thus the analogous functor is:

Note how this corresponds to the above definition of List. Our free monad is the (least) fixed point:

Finally we are all done with the category theory for this part. Let’s now write our free monad in code:

data Free f a = Pure a | Free (f (Free f a))

To be more explicit with the types, we have the constructors:

Pure :: a -> Free f a
Free :: f (Free f a) -> Free f a

Convince yourself that this definition corresponds to the categorical one we gave above.

This already kind of looks like a monad by definition! Now, given that f is a functor, we can define a straightforward monad instance on Free f as follows:

instance Functor f => Monad (Free f) where
  return = Pure
  Pure x >>= f = f x
  Free g >>= f = Free ((>>= f) <$> g)

3.2. In Lean

Now, as promised, we will do the rest of our work in Lean. Let’s write the same definition in Lean:

inductive Free (f : Type → Type) (a : Type) where
  | pure : a → Free f a
  | free : f (Free f a) → Free f a

Weird. We get this opaque error message:

-- error: (kernel) arg #3 of `Free.free' contains a non valid occurrence of the
datatypes being declared

Why does the definition work in Haskell but not Lean?

Strict Positivity

Recall that, in languages like Lean (or Coq, or Agda), in order for the proof system to be consistent, all functions must terminate. Proofs correspond to programs, and if we had programs that could loop forever, we could prove anything, and our logic would be useless.

To enforce this, defining inductive types has a restriction, called strict positivity. Basically, an inductive type can not refer to itself on the left side of an arrow in its constructors. If Lean allowed this definition, we could inhabit the empty type (i.e. prove False) using a contravariant functor.

Since the free monad doesn’t work due to type-theoretic restrictions, we need a little bit more freedom. Enter the freer monad. The below definition is strictly positive:

inductive FreeM.{u, v, w} (f : Type u → Type v) (α : Type w) where
  | pure : α → FreeM f α
  | liftBind {ι : Type u} (op : f ι) (cont : ι → FreeM f α) : FreeM f α

In fact, this is freer in the sense that we no longer even require f to be a functor. Let’s define the Functor and Monad instances for this type, given any type constructor.

Monad Instance of FreeM f

We begin by providing a Functor instance, which is just defining a map function, lifting a function $f : \alpha \to \beta$ to a function $Ff : \text{FreeM } F \ \alpha \to \text{FreeM } F \ \beta$:

universe u v w w' w''
namespace FreeM
variable {F : Type u → Type v} {ι : Type u} {α : Type w} {β : Type w'} {γ : Type w''}

def map (f : α → β) : FreeM F α → FreeM F β
  | .pure a => .pure (f a)
  | .liftBind op cont => .liftBind op (fun z => FreeM.map f (cont z))

instance : Functor (FreeM F) where
  map := .map

Now we can provide a monad instance by defining pure and bind as follows:

protected def bind (x : FreeM F α) (f : α → FreeM F β) : FreeM F β :=
  match x with
  | .pure a => f a
  | .liftBind op cont => .liftBind op (fun z => FreeM.bind (cont z) f)

instance : Monad (FreeM F) where
  pure := .pure
  bind := .bind

Of course we all love Lean because you can actually prove things about the code you write. Lean provides not just a Monad typeclass, but a LawfulMonad typeclass, which additionally requires explicit proofs that the monad laws are satisfied. Let’s do this for fun. Throughout these posts I will be using some lemmas that you can find in the source code whose statements/proofs I won’t expliclty be showing here.

We first prove it is a lawful functor, i.e. it is functorial in the categorical sense:

• Identity law: $\text{map}\ id = id$
• Composition law: $\text{map}\ (g \circ f) = \text{map}\ g \circ \text{map}\ f$

instance : LawfulFunctor (FreeM F) where
  map_const := rfl
  id_map x := by
    induction x with
    | pure a => rfl
    | liftBind op cont ih =>
      simp_all [map_eq_map, lift_def, map, ih]
  comp_map g h x := by
    induction x with
    | pure a => rfl
    | liftBind op cont ih =>
      simp_all [map_eq_map, lift_def, map, ih]

Now we prove that our structure is a lawful monad, meaning it satisfies the following monad laws:

• bind_pure_comp : x >>= (λ a → pure (f a)) = f <$> x
  A bind followed by pure composed with a function is equivalent to a functorial map.

• id_map : id <$> x = x
  Mapping the identity function over a value leaves it unchanged.

• pure_bind : pure x >>= f = f x
  Pure followed by bind is equivalent to function application.

• bind_assoc : (x >>= f) >>= g = x >>= (λ a → f a >>= g)
  Bind is associative.

The proof is as follows:

-- Lemma that bind is associative
protected theorem bind_assoc (x : FreeM F α) (f : α → FreeM F β) (g : β → FreeM F γ) :
    (x.bind f).bind g = x.bind (fun x => (f x).bind g) := by
  induction x with
  | pure a => rfl
  | liftBind op cont ih =>
    simp [FreeM.bind,  ← pure_eq_pure] at *
    simp [ih]

-- Complete proof that FreeM F is a lawful monad
instance : LawfulMonad (FreeM F) := LawfulMonad.mk'
  (bind_pure_comp := fun f x => by
    induction x with
    | pure a => rfl
    | liftBind op cont ih =>
      simp only [FreeM.bind, bind_eq_bind, map_eq_map, pure_eq_purePure, map] at *
      simp only [ih]
  )
  (id_map := id_map)
  (pure_bind := fun x f => rfl)
  (bind_assoc := FreeM.bind_assoc)

I won’t write out the informal details of the proof, but it is mostly straightforward, we unfold all the definitions using simp, and in some cases when we have a value of type FreeM F a we perform induction on it and simplify further using our lemmas.

4. Conclusion

In this first part of our series, we explored the concept of free objects and introduced the idea of a free monad from a categorical perspective. Starting from familiar examples like free vector spaces and monoids, we generalized the construction to free monads, and implemented the free monad in Lean from the ground up.

We discussed the idea of strict positivity, leading us to the freer monad construction as both a workaround and a generalization. We were able to define a monad instance on FreeM F for any F : Type -> Type, and proved that it satisfies the monad laws.

The story continues in Part 2 with catamorphisms, interpreters, and universal properties.