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

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

Equations

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

@[simp]

theorem Cslib.FreeM.pure_eq_pure {F : Type u → Type v} {α : Type w} : pure = FreeM.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.

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

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

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

Equations

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

@[simp]

theorem Cslib.FreeM.bind_eq_bind {F : Type u → Type v} {α β : Type w} : bind = FreeM.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.

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)

@[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.instFunctor {F : Type u → Type v} : Functor (FreeM F)

Equations

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

@[simp]

theorem Cslib.FreeM.map_eq_map {F : Type u → Type v} {α β : Type w} : Functor.map = 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 Cslib.FreeM.pure

@[simp]

theorem Cslib.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 Cslib.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 Cslib.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 Cslib.FreeM.bind_pure {F : Type u → Type v} {α : Type w} (x : FreeM F α) : x.bind FreeM.pure = x

@[simp]

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

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.170} => 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) (FreeM.pure a) = pure a

@[simp]

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

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_liftBind {ι : Type u} (op : F ι) (cont : ι → FreeM F α) : interp (liftBind 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.