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. For polynomial effect signatures with explicit operation shapes and positions, see Cslib.Foundations.Data.PFunctor.Free.

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.

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 Cslib.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.

@[implicit_reducible]

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

Equations

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

@[simp]

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

def Cslib.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.

The builtin >>= notation should be preferred when α and β are in the same universe.

Equations

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

@[implicit_reducible]

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

Equations

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

@[simp]

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

Note that this lemma does not always apply, as it is universe-constrained by Bind.bind.

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

Map a function over a FreeM monad.

The builtin <$> notation should be preferred when α and β are in the same universe.

Equations

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

@[implicit_reducible]

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

Equations

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

@[simp]

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

Note that this lemma does not always apply, as it is universe-constrained by Functor.map.

def Cslib.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

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

@[simp]

theorem Cslib.FreeM.liftBind_eq {F : Type u → Type v} {ι : Type u} {α✝ : Type u_1} {cont : ι → FreeM F α✝} (op : F ι) : liftBind op cont = (lift op).bind cont

theorem Cslib.FreeM.induction {F : Type u → Type v} {α : Type w} {motive : FreeM F α → Prop} (pure : ∀ (a : α), motive (pure a)) (lift_bind : ∀ {ι : Type u} (op : F ι) (cont : ι → FreeM F α), (∀ (i : ι), motive (cont i)) → motive ((lift op).bind cont)) (x : FreeM F α) : motive x

An override for the default induction principle that is in simp-normal form.

Note that when α and ι are in the same universe, this simplifies slightly further.

theorem Cslib.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

@[simp]

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

.pure a followed by bind collapses immediately.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Cslib.FreeM.map_bind {F : Type u → Type v} {α : Type w} {β : Type w'} {γ : Type w''} (f : β → γ) (x : FreeM F α) (c : α → FreeM F β) : map f (x.bind c) = x.bind fun (a : α) => map f (c a)

@[simp]

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

theorem Cslib.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 Cslib.FreeM.instLawfulFunctor {F : Type u → Type v} : LawfulFunctor (FreeM F)

@[implicit_reducible]

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

Equations

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

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

def Cslib.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

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

@[simp]

theorem Cslib.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) (pure a) = pure a

@[simp]

theorem Cslib.FreeM.liftM_lift_bind {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) (lift op >>= cont) = do let b ← interp op FreeM.liftM (fun {ι : Type u} => interp) (cont b)

@[simp]

theorem Cslib.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 Cslib.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 >>= f) = do let a ← FreeM.liftM (fun {ι : Type u} => interp) x FreeM.liftM (fun {ι : Type u} => interp) (f a)

@[simp]

theorem Cslib.FreeM.liftM_map {F : Type u → Type v} {m : Type u → Type w} [Monad m] {α β : Type u} [LawfulMonad m] (interp : {ι : Type u} → F ι → m ι) (f : α → β) (x : FreeM F α) : FreeM.liftM (fun {ι : Type u} => interp) (f <$> x) = f <$> FreeM.liftM (fun {ι : Type u} => interp) x

@[simp]

theorem Cslib.FreeM.liftM_seq {F : Type u → Type v} {m : Type u → Type w} [Monad m] {α β : Type u} [LawfulMonad m] (interp : {ι : Type u} → F ι → m ι) (x : FreeM F (α → β)) (y : FreeM F α) : FreeM.liftM (fun {ι : Type u} => interp) (x <*> y) = FreeM.liftM (fun {ι : Type u} => interp) x <*> FreeM.liftM (fun {ι : Type u} => interp) y

@[simp]

theorem Cslib.FreeM.liftM_seqLeft {F : Type u → Type v} {m : Type u → Type w} [Monad m] {α β : Type u} [LawfulMonad m] (interp : {ι : Type u} → F ι → m ι) (x : FreeM F α) (y : FreeM F β) : FreeM.liftM (fun {ι : Type u} => interp) (x <* y) = FreeM.liftM (fun {ι : Type u} => interp) x <* FreeM.liftM (fun {ι : Type u} => interp) y

@[simp]

theorem Cslib.FreeM.liftM_seqRight {F : Type u → Type v} {m : Type u → Type w} [Monad m] {α β : Type u} [LawfulMonad m] (interp : {ι : Type u} → F ι → m ι) (x : FreeM F α) (y : FreeM F β) : FreeM.liftM (fun {ι : Type u} => interp) (x *> y) = FreeM.liftM (fun {ι : Type u} => interp) x *> FreeM.liftM (fun {ι : Type u} => interp) y

structure Cslib.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_lift_bind {ι : Type u} (op : F ι) (cont : ι → FreeM F α) : interp (lift op >>= cont) = do let x ← handler op interp (cont x)

theorem Cslib.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 Cslib.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 Cslib.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.