Part 1: Defining the Free Monad in Lean
1. Introduction
In this part we define the free monad in Lean from first principles. We begin thinking about what free means in mathematics, with familiar examples like vector spaces and the free monoid (the List type). The free monad is the analogous construction one level up, the canonical monad generated from an endofunctor.
Then we consider its implementation, first in Haskell, where the standard Free f definition works naturally. Then in Lean, where Lean’s type theory poses an obstacle for the initial definition, which we sidestep with a nice generalization. We close by giving FreeM F a Monad instance and proving it’s lawful.
All the code is packaged into CSlib.
Table of Contents
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 $k$ with basis $B$. $V$ is said to be “free” on $B$: it is generated by taking all finite linear combinations of elements in $B$ with coefficients in $k$. 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$.
The correspondence of morphisms given by this adjunction leads to 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 structure we want. 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 the joke that monads are just monoids in the category of endofunctors. It’s true, and 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:
\[L_a \cong \mathbf{1} + (a \times L_a)\]i.e., the List type is a fixed point of the functor:
\[F_a x = \mathbf{1} + (a \times x)\]The heart of the analogy is that lists are to types as free monads are to functors. So we lift what we did with List in the category of types up to the category of endofunctors, defining a higher-order functor analogous to List but acting 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:
\[\Phi_F G = \text{Id} + F \circ G\]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 and proofs I won’t explicitly 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 => ...
| liftBind op cont ih => ...
comp_map g h x := by
induction x with
| pure a => ...
| liftBind op cont 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 => ...
| liftBind op cont 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 => ...
| liftBind op cont ih => ...
)
(id_map := id_map)
(pure_bind := fun x f => rfl)
(bind_assoc := FreeM.bind_assoc)
The proof is mostly mechanical. Unfold definitions with simp, and where we have a FreeM F a value, induct on it and simplify further with 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.