Free Monad

This file defines a general FreeM monad construction for representing effectful programs as pure syntax trees, separate from their interpretation.

The FreeM monad generates a free monad from any type constructor f : Type → Type, without requiring f to be a Functor. This implementation uses the "freer monad" approach as the traditional free monad is not safely definable in Lean due to termination checking.

In this construction, effectful programs are represented as trees of effects. Each node (FreeM.liftBind) represents a request to perform an effect, accompanied by a continuation specifying how the computation proceeds after the effect. The leaves (FreeM.pure) represent completed computations with final results.

This separation of syntax from semantics enables multiple interpretations of the same program: execution, static analysis, optimization, pretty-printing, verification, and more.

A key insight is that FreeM F satisfies the universal property of free monads: for any monad M and effect handler f : F → M, there exists a unique way to interpret FreeM F computations in M that respects the effect semantics given by f. This unique interpreter is FreeM.liftM f

Main Definitions

• FreeM: The free monad construction
• FreeM.liftM: The canonical interpreter satisfying the universal property
• FreeM.liftM_unique: Proof of the universal property

For elimination and interpretation theory, see Free/Fold.lean.

See the Haskell freer-simple library for the Haskell implementation that inspired this approach.

Implementation Notes

The FreeM monad is defined using an inductive type with constructors .pure and .liftBind. We implement Functor and Monad instances, and prove the corresponding LawfulFunctor and LawfulMonad instances.

For now we choose to make the constructors the simp-normal form, as opposed to the standard monad notation.

The file Free/Effects.lean demonstrates practical applications by implementing State, Writer, and Continuations monads using FreeM with appropriate effect signatures.

The file Free/Fold.lean provides the theory of the fold operation for free monads.

References

• Oleg Kiselyov, Hiromi Ishii. Freer Monads, More Extensible Effects
• Bartosz Milewski. The Dao of Functional Programming

Tags

Free monad, state monad

inductive FreeM (F : Type u → Type v) (α : Type w) : Type (max (max (u + 1) v) w)

The Free monad over a type constructor F.

A FreeM F a is a tree of operations from the type constructor F, with leaves of type a. It has two constructors: pure for wrapping a value of type a, and liftBind for representing an operation from F followed by a continuation.

This construction provides a free monad for any type constructor F, allowing for composable effect descriptions that can be interpreted later. Unlike the traditional free monad, this does not require F to be a functor.

• pure {F : Type u → Type v} {α : Type w} (a : α) : FreeM F α

  The action that does nothing and returns a.

• liftBind {F : Type u → Type v} {α : Type w} {ι : Type u} (op : F ι) (cont : ι → FreeM F α) : FreeM F α

  Invoke the operation op with contuation cont.

  Note that Lean's inductive types prevent us splitting this into separate bind and lift constructors.

instance FreeM.instPure {F : Type u → Type v} : Pure (FreeM F)

Equations

• FreeM.instPure = { pure := fun {α : Type ?u.9} => FreeM.pure }

@[simp]

theorem FreeM.pure_eq_pure {F : Type u → Type v} {α : Type w} : pure = FreeM.pure

def FreeM.bind {F : Type u → Type v} {α : Type w} {β : Type w'} (x : FreeM F α) (f : α → FreeM F β) : FreeM F β

Bind operation for the FreeM monad.

Equations

• (FreeM.pure a).bind f = f a
• (FreeM.liftBind op cont).bind f = FreeM.liftBind op fun (z : ι) => (cont z).bind f

theorem FreeM.bind_assoc {F : Type u → Type v} {α : Type w} {β : Type w'} {γ : Type w''} (x : FreeM F α) (f : α → FreeM F β) (g : β → FreeM F γ) : (x.bind f).bind g = x.bind fun (x : α) => (f x).bind g

instance FreeM.instBind {F : Type u → Type v} : Bind (FreeM F)

Equations

• FreeM.instBind = { bind := fun {α β : Type ?u.10} => FreeM.bind }

@[simp]

theorem FreeM.bind_eq_bind {F : Type u → Type v} {α β : Type w} : bind = FreeM.bind

def FreeM.map {F : Type u → Type v} {α : Type w} {β : Type w'} (f : α → β) : FreeM F α → FreeM F β

Map a function over a FreeM monad.

Equations

• FreeM.map f (FreeM.pure a) = FreeM.pure (f a)
• FreeM.map f (FreeM.liftBind op cont) = FreeM.liftBind op fun (z : ι) => FreeM.map f (cont z)

@[simp]

theorem FreeM.id_map {F : Type u → Type v} {α : Type w} (x : FreeM F α) : map id x = x

theorem FreeM.comp_map {F : Type u → Type v} {α : Type w} {β : Type w'} {γ : Type w''} (h : β → γ) (g : α → β) (x : FreeM F α) : map (h ∘ g) x = map h (map g x)

instance FreeM.instFunctor {F : Type u → Type v} : Functor (FreeM F)

Equations

• FreeM.instFunctor = { map := fun {α β : Type ?u.14} => FreeM.map }

@[simp]

theorem FreeM.map_eq_map {F : Type u → Type v} {α β : Type w} : Functor.map = map

def FreeM.lift {F : Type u → Type v} {ι : Type u} (op : F ι) : FreeM F ι

Lift an operation from the effect signature F into the FreeM F monad.

Equations

• FreeM.lift op = FreeM.liftBind op FreeM.pure

@[simp]

theorem FreeM.lift_def {F : Type u → Type v} {ι : Type u} (op : F ι) : lift op = liftBind op FreeM.pure

Rewrite lift to the constructor form so that simplification stays in constructor normal form.

@[simp]

theorem FreeM.map_lift {F : Type u → Type v} {ι : Type u} {α : Type w} (f : ι → α) (op : F ι) : map f (lift op) = liftBind op fun (z : ι) => FreeM.pure (f z)

@[simp]

theorem FreeM.pure_bind {F : Type u → Type v} {α : Type w} {β : Type w'} (a : α) (f : α → FreeM F β) : (FreeM.pure a).bind f = f a

.pure a followed by bind collapses immediately.

@[simp]

theorem FreeM.bind_pure {F : Type u → Type v} {α : Type w} (x : FreeM F α) : x.bind FreeM.pure = x

@[simp]

theorem FreeM.bind_pure_comp {F : Type u → Type v} {α : Type w} {β : Type w'} (f : α → β) (x : FreeM F α) : x.bind (FreeM.pure ∘ f) = map f x

@[simp]

theorem FreeM.liftBind_bind {F : Type u → Type v} {ι : Type u} {α : Type w} {β : Type w'} (op : F ι) (cont : ι → FreeM F α) (f : α → FreeM F β) : (liftBind op cont).bind f = liftBind op fun (x : ι) => (cont x).bind f

Collapse a .bind that follows a liftBind into a single liftBind

instance FreeM.instLawfulFunctor {F : Type u → Type v} : LawfulFunctor (FreeM F)

instance FreeM.instMonad {F : Type u → Type v} : Monad (FreeM F)

Equations

• One or more equations did not get rendered due to their size.

instance FreeM.instLawfulMonad {F : Type u → Type v} : LawfulMonad (FreeM F)

def FreeM.liftM {F : Type u → Type v} {m : Type u → Type w} [Monad m] {α : Type u} (interp : {ι : Type u} → F ι → m ι) : FreeM F α → m α

Interpret a FreeM F computation into any monad m by providing an interpretation function for the effect signature F.

This function defines the canonical interpreter from the free monad FreeM F into the target monad m. It is the unique monad morphism that extends the effect handler interp : ∀ {β}, F β → m β via the universal property of FreeM.

Equations

• FreeM.liftM interp (FreeM.pure a) = pure a
• FreeM.liftM interp (FreeM.liftBind op cont) = do let result ← interp op FreeM.liftM (fun {ι : Type ?u.158} => interp) (cont result)

@[simp]

theorem FreeM.liftM_pure {F : Type u → Type v} {m : Type u → Type w} [Monad m] {α : Type u} (interp : {ι : Type u} → F ι → m ι) (a : α) : FreeM.liftM (fun {ι : Type u} => interp) (FreeM.pure a) = pure a

@[simp]

theorem FreeM.liftM_liftBind {F : Type u → Type v} {m : Type u → Type w} [Monad m] {α β : Type u} (interp : {ι : Type u} → F ι → m ι) (op : F β) (cont : β → FreeM F α) : FreeM.liftM (fun {ι : Type u} => interp) (liftBind op cont) = do let b ← interp op FreeM.liftM (fun {ι : Type u} => interp) (cont b)

theorem FreeM.liftM_lift {F : Type u → Type v} {m : Type u → Type w} [Monad m] {β : Type u} [LawfulMonad m] (interp : {ι : Type u} → F ι → m ι) (op : F β) : FreeM.liftM (fun {ι : Type u} => interp) (lift op) = interp op

@[simp]

theorem FreeM.liftM_bind {F : Type u → Type v} {m : Type u → Type w} [Monad m] {α β : Type u} [LawfulMonad m] (interp : {ι : Type u} → F ι → m ι) (x : FreeM F α) (f : α → FreeM F β) : FreeM.liftM (fun {ι : Type u} => interp) (x.bind f) = do let a ← FreeM.liftM (fun {ι : Type u} => interp) x FreeM.liftM (fun {ι : Type u} => interp) (f a)

structure FreeM.Interprets {F : Type u → Type v} {m : Type u → Type w} [Monad m] {α : Type u} (handler : {ι : Type u} → F ι → m ι) (interp : FreeM F α → m α) : Prop

A predicate stating that interp : FreeM F α → m α is an interpreter for the effect handler handler : ∀ {α}, F α → m α.

This means that interp is a monad morphism from the free monad FreeM F to the monad m, and that it extends the interpretation of individual operations given by f.

Formally, interp satisfies the two equations:

• interp (pure a) = pure a
• interp (liftBind op k) = handler op >>= fun x => interp (k x)

• apply_pure (a : α) : interp (FreeM.pure a) = pure a
• apply_liftBind {ι : Type u} (op : F ι) (cont : ι → FreeM F α) : interp (liftBind op cont) = do let x ← handler op interp (cont x)

theorem FreeM.Interprets.eq {F : Type u → Type v} {m : Type u → Type w} [Monad m] {α : Type u} {handler : {ι : Type u} → F ι → m ι} {interp : FreeM F α → m α} (h : Interprets (fun {ι : Type u} => handler) interp) : interp = fun (x : FreeM F α) => FreeM.liftM handler x

theorem FreeM.Interprets.liftM {F : Type u → Type v} {m : Type u → Type w} [Monad m] {α : Type u} (handler : {ι : Type u} → F ι → m ι) : Interprets (fun {ι : Type u} => handler) fun (x : FreeM F α) => FreeM.liftM (fun {ι : Type u} => handler) x

theorem FreeM.Interprets.iff {F : Type u → Type v} {m : Type u → Type w} [Monad m] {α : Type u} (handler : {ι : Type u} → F ι → m ι) (interp : FreeM F α → m α) : Interprets (fun {ι : Type u} => handler) interp ↔ interp = fun (x : FreeM F α) => FreeM.liftM (fun {ι : Type u} => handler) x

The universal property of the free monad FreeM.

That is, liftM handler is the unique interpreter that extends the effect handler handler to interpret FreeM F computations in a monad m.