Free Monad

This file defines several canonical instances on the free monad.

Main definitions

• FreeState, FreeWriter, FreeCont: Specific effect monads

Implementation

To execute or interpret these computations, we provide two approaches:

1. Hand-written interpreters (FreeState.run, FreeWriter.run, FreeCont.run) that directly pattern-match on the tree structure
2. Canonical interpreters (FreeState.toStateM, FreeWriter.toWriterT, FreeCont.toContT) derived from the universal property via liftM

We prove that these approaches are equivalent, demonstrating that the implementation aligns with the theory. We also provide uniqueness theorems for the canonical interpreters, which follow from the universal property.

Tags

Free monad, state monad, writer monad, continuation monad

State Monad via FreeM

inductive Cslib.FreeM.StateF (σ : Type u) : Type u → Type u

Type constructor for state operations.

• get {σ : Type u} : StateF σ σ

  Get the current state.

• set {σ : Type u} : σ → StateF σ PUnit.{u + 1}

  Set the state.

@[reducible, inline]

abbrev Cslib.FreeM.FreeState (σ : Type u) (α : Type u_1) : Type (max (u + 1) u_1)

State monad via the FreeM monad.

Equations

• Cslib.FreeM.FreeState σ = Cslib.FreeM (Cslib.FreeM.StateF σ)

instance Cslib.FreeM.FreeState.instMonad {σ : Type u} : Monad (FreeState σ)

Equations

• Cslib.FreeM.FreeState.instMonad = inferInstance

instance Cslib.FreeM.FreeState.instLawfulMonad {σ : Type u} : LawfulMonad (FreeState σ)

instance Cslib.FreeM.FreeState.instMonadStateOf {σ : Type u} : MonadStateOf σ (FreeState σ)

Equations

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

@[simp]

theorem Cslib.FreeM.FreeState.get_def {σ : Type u} : get = lift StateF.get

@[simp]

theorem Cslib.FreeM.FreeState.set_def {σ : Type u} (s : σ) : set s = lift (StateF.set s)

instance Cslib.FreeM.FreeState.instMonadState {σ : Type u} : MonadState σ (FreeState σ)

Equations

• Cslib.FreeM.FreeState.instMonadState = inferInstance

def Cslib.FreeM.FreeState.stateInterp {σ α : Type u} : StateF σ α → StateM σ α

Interpret StateF operations into StateM.

Equations

• Cslib.FreeM.FreeState.stateInterp Cslib.FreeM.StateF.get = MonadStateOf.get
• Cslib.FreeM.FreeState.stateInterp (Cslib.FreeM.StateF.set s) = set s

def Cslib.FreeM.FreeState.toStateM {σ α : Type u} (comp : FreeState σ α) : StateM σ α

Convert a FreeState computation into a StateM computation. This is the canonical interpreter derived from liftM.

Equations

• comp.toStateM = Cslib.FreeM.liftM (fun {ι : Type ?u.18} => Cslib.FreeM.FreeState.stateInterp) comp

theorem Cslib.FreeM.FreeState.toStateM_unique {σ α : Type u} (g : FreeState σ α → StateM σ α) (h : Interprets (fun {ι : Type u} => stateInterp) g) : g = toStateM

toStateM is the unique interpreter extending stateInterp.

def Cslib.FreeM.FreeState.run {σ : Type u} {α : Type v} (comp : FreeState σ α) (s₀ : σ) : α × σ

Run a state computation, returning both the result and final state.

Equations

• Cslib.FreeM.FreeState.run (Cslib.FreeM.pure a) s₀ = (a, s₀)
• Cslib.FreeM.FreeState.run (Cslib.FreeM.liftBind Cslib.FreeM.StateF.get k) s₀ = Cslib.FreeM.FreeState.run (k s₀) s₀
• Cslib.FreeM.FreeState.run (Cslib.FreeM.liftBind (Cslib.FreeM.StateF.set s') k) s₀ = Cslib.FreeM.FreeState.run (k PUnit.unit) s'

@[simp]

theorem Cslib.FreeM.FreeState.run_toStateM {σ α : Type u} (comp : FreeState σ α) : StateT.run comp.toStateM = comp.run

The canonical interpreter toStateM derived from liftM agrees with the hand-written recursive interpreter run for FreeState.

@[simp]

theorem Cslib.FreeM.FreeState.run_pure {σ : Type u} {α : Type v} (a : α) (s₀ : σ) : run (FreeM.pure a) s₀ = (a, s₀)

@[simp]

theorem Cslib.FreeM.FreeState.run_get {σ : Type u} {α : Type v} (k : σ → FreeState σ α) (s₀ : σ) : run (liftBind StateF.get k) s₀ = (k s₀).run s₀

@[simp]

theorem Cslib.FreeM.FreeState.run_set {σ : Type u} {α : Type v} (s' : σ) (k : PUnit.{u + 1} → FreeState σ α) (s₀ : σ) : run (liftBind (StateF.set s') k) s₀ = (k PUnit.unit).run s'

def Cslib.FreeM.FreeState.run' {σ : Type u} {α : Type v} (c : FreeState σ α) (s₀ : σ) : α

Run a state computation, returning only the result.

Equations

• c.run' s₀ = (c.run s₀).fst

@[simp]

theorem Cslib.FreeM.FreeState.run'_toStateM {σ α : Type u} (comp : FreeState σ α) : StateT.run' comp.toStateM = comp.run'

@[simp]

theorem Cslib.FreeM.FreeState.run'_pure {σ : Type u} {α : Type v} (a : α) (s₀ : σ) : run' (FreeM.pure a) s₀ = a

@[simp]

theorem Cslib.FreeM.FreeState.run'_get {σ : Type u} {α : Type v} (k : σ → FreeState σ α) (s₀ : σ) : run' (liftBind StateF.get k) s₀ = (k s₀).run' s₀

@[simp]

theorem Cslib.FreeM.FreeState.run'_set {σ : Type u} {α : Type v} (s' : σ) (k : PUnit.{u + 1} → FreeState σ α) (s₀ : σ) : run' (liftBind (StateF.set s') k) s₀ = (k PUnit.unit).run' s'

Writer Monad via FreeM

inductive Cslib.FreeM.WriterF (ω : Type u) : Type v → Type u

Type constructor for writer operations. Writer has a single effect, so the definition has just one constructor.

• tell {ω : Type u} : ω → WriterF ω PUnit.{v + 1}

  Write a value to the log.

@[reducible, inline]

abbrev Cslib.FreeM.FreeWriter (ω : Type u) (α : Type u_1) : Type (max (max (u_2 + 1) u) u_1)

Writer monad implemented via the FreeM monad construction. This provides a more efficient implementation than the traditional WriterT transformer, as it avoids buffering the log.

Equations

• Cslib.FreeM.FreeWriter ω = Cslib.FreeM (Cslib.FreeM.WriterF ω)

instance Cslib.FreeM.FreeWriter.instMonad {ω : Type u} : Monad (FreeWriter ω)

Equations

• Cslib.FreeM.FreeWriter.instMonad = inferInstance

instance Cslib.FreeM.FreeWriter.instLawfulMonad {ω : Type u} : LawfulMonad (FreeWriter ω)

def Cslib.FreeM.FreeWriter.writerInterp {ω α : Type u} : WriterF ω α → WriterT ω Id α

Interpret WriterF operations into WriterT.

Equations

• Cslib.FreeM.FreeWriter.writerInterp (Cslib.FreeM.WriterF.tell w) = tell w

def Cslib.FreeM.FreeWriter.toWriterT {ω α : Type u} [Monoid ω] (comp : FreeWriter ω α) : WriterT ω Id α

Convert a FreeWriter computation into a WriterT computation. This is the canonical interpreter derived from liftM.

Equations

• comp.toWriterT = Cslib.FreeM.liftM (fun {ι : Type ?u.8} => Cslib.FreeM.FreeWriter.writerInterp) comp

theorem Cslib.FreeM.FreeWriter.toWriterT_unique {ω α : Type u} [Monoid ω] (g : FreeWriter ω α → WriterT ω Id α) (h : Interprets (fun {ι : Type u} => writerInterp) g) : g = toWriterT

toWriterT is the unique interpreter extending writerInterp.

@[reducible, inline]

abbrev Cslib.FreeM.FreeWriter.tell {ω : Type u} (w : ω) : FreeWriter ω PUnit.{u_1 + 1}

Writes a log entry. This creates an effectful node in the computation tree.

Equations

• Cslib.FreeM.FreeWriter.tell w = Cslib.FreeM.lift (Cslib.FreeM.WriterF.tell w)

@[simp]

theorem Cslib.FreeM.FreeWriter.tell_def {ω : Type u} (w : ω) : tell w = lift (WriterF.tell w)

def Cslib.FreeM.FreeWriter.run {ω : Type u} {α : Type v} [Monoid ω] : FreeWriter ω α → α × ω

Interprets a FreeWriter computation by recursively traversing the tree, accumulating log entries with the monoid operation, and returns the final value paired with the accumulated log.

Equations

• Cslib.FreeM.FreeWriter.run (Cslib.FreeM.pure a) = (a, 1)
• Cslib.FreeM.FreeWriter.run (Cslib.FreeM.liftBind (Cslib.FreeM.WriterF.tell w) k) = match Cslib.FreeM.FreeWriter.run (k PUnit.unit) with | (a, w') => (a, w * w')

@[simp]

theorem Cslib.FreeM.FreeWriter.run_pure {ω : Type u} {α : Type v} [Monoid ω] (a : α) : run (FreeM.pure a) = (a, 1)

@[simp]

theorem Cslib.FreeM.FreeWriter.run_liftBind_tell {ω : Type u} {α : Type v} [Monoid ω] (w : ω) (k : PUnit.{u_1 + 1} → FreeWriter ω α) : run (liftBind (WriterF.tell w) k) = match (k PUnit.unit).run with | (a, w') => (a, w * w')

@[simp]

theorem Cslib.FreeM.FreeWriter.run_toWriterT {ω α : Type u} [Monoid ω] (comp : FreeWriter ω α) : comp.toWriterT.run = comp.run

The canonical interpreter toWriterT derived from liftM agrees with the hand-written recursive interpreter run for FreeWriter.

def Cslib.FreeM.FreeWriter.listen {ω : Type u} {α : Type v} [Monoid ω] : FreeWriter ω α → FreeWriter ω (α × ω)

listen captures the log produced by a subcomputation incrementally. It traverses the computation, emitting log entries as encountered, and returns the accumulated log as a result.

Equations

• One or more equations did not get rendered due to their size.
• Cslib.FreeM.FreeWriter.listen (Cslib.FreeM.pure a) = Cslib.FreeM.pure (a, 1)

@[simp]

theorem Cslib.FreeM.FreeWriter.listen_pure {ω : Type u} {α : Type v} [Monoid ω] (a : α) : listen (FreeM.pure a) = FreeM.pure (a, 1)

@[simp]

theorem Cslib.FreeM.FreeWriter.listen_liftBind_tell {ω : Type u} {α : Type v} [Monoid ω] (w : ω) (k : PUnit.{u_1 + 1} → FreeWriter ω α) : listen (liftBind (WriterF.tell w) k) = liftBind (WriterF.tell w) fun (x : PUnit.{u_2 + 1}) => do let x ← (k PUnit.unit).listen match x with | (a, w') => pure (a, w * w')

def Cslib.FreeM.FreeWriter.pass {ω : Type u} {α : Type v} [Monoid ω] (m : FreeWriter ω (α × (ω → ω))) : FreeWriter ω α

pass allows a subcomputation to modify its own log. After traversing the computation and accumulating its log, the resulting function is applied to rewrite the accumulated log before re-emission.

Equations

• m.pass = match m.run with | ((a, f), w) => Cslib.FreeM.liftBind (Cslib.FreeM.WriterF.tell (f w)) fun (x : PUnit.{?u.29 + 1}) => Cslib.FreeM.pure a

@[simp]

theorem Cslib.FreeM.FreeWriter.pass_def {ω : Type u} {α : Type v} [Monoid ω] (m : FreeWriter ω (α × (ω → ω))) : m.pass = match m.run with | ((a, f), w) => liftBind (WriterF.tell (f w)) fun (x : PUnit.{u_2 + 1}) => FreeM.pure a

instance Cslib.FreeM.FreeWriter.instMonadWriterOfMonoid {ω : Type u} [Monoid ω] : MonadWriter ω (FreeWriter ω)

Equations

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

Continuation Monad via FreeM

inductive Cslib.FreeM.ContF (r : Type u) (α : Type v) : Type (max u v)

Type constructor for continuation operations.

• callCC {r : Type u} {α : Type v} : ((α → r) → r) → ContF r α

  Call with current continuation: provides access to the current continuation.

instance Cslib.FreeM.instFunctorContF {r : Type u} : Functor (ContF r)

Equations

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

@[reducible, inline]

abbrev Cslib.FreeM.FreeCont (r : Type u) (α : Type u_1) : Type (max (max (u_2 + 1) u_2 u) u_1)

Continuation monad via the FreeM monad.

Equations

• Cslib.FreeM.FreeCont r = Cslib.FreeM (Cslib.FreeM.ContF r)

instance Cslib.FreeM.FreeCont.instMonad {r : Type u} : Monad (FreeCont r)

Equations

• Cslib.FreeM.FreeCont.instMonad = inferInstance

instance Cslib.FreeM.FreeCont.instLawfulMonad {r : Type u} : LawfulMonad (FreeCont r)

def Cslib.FreeM.FreeCont.contInterp {r : Type u} {α : Type v} : ContF r α → ContT r Id α

Interpret ContF r operations into ContT r Id.

Equations

• Cslib.FreeM.FreeCont.contInterp (Cslib.FreeM.ContF.callCC g) x✝ = pure (g fun (a : α) => (x✝ a).run)

def Cslib.FreeM.FreeCont.toContT {r α : Type u} (comp : FreeCont r α) : ContT r Id α

Convert a FreeCont computation into a ContT computation. This is the canonical interpreter derived from liftM.

Equations

• comp.toContT = Cslib.FreeM.liftM (fun {ι : Type ?u.7} => Cslib.FreeM.FreeCont.contInterp) comp

theorem Cslib.FreeM.FreeCont.toContT_unique {r α : Type u} (g : FreeCont r α → ContT r Id α) (h : Interprets (fun {ι : Type u} => contInterp) g) : g = toContT

toContT is the unique interpreter extending contInterp.

def Cslib.FreeM.FreeCont.run {r : Type u} {α : Type v} : FreeCont r α → (α → r) → r

Run a continuation computation with the given continuation.

Equations

• Cslib.FreeM.FreeCont.run (Cslib.FreeM.pure a) x✝ = x✝ a
• Cslib.FreeM.FreeCont.run (Cslib.FreeM.liftBind (Cslib.FreeM.ContF.callCC g) cont) x✝ = g fun (a : ι) => Cslib.FreeM.FreeCont.run (cont a) x✝

@[simp]

theorem Cslib.FreeM.FreeCont.run_toContT {r α : Type u} (comp : FreeCont r α) : comp.toContT.run = comp.run

The canonical interpreter toContT derived from liftM agrees with the hand-written recursive interpreter run for FreeCont.

@[simp]

theorem Cslib.FreeM.FreeCont.run_pure {r : Type u} {α : Type v} (a : α) (k : α → r) : run (FreeM.pure a) k = k a

@[simp]

theorem Cslib.FreeM.FreeCont.run_liftBind_callCC {r : Type u} {α : Type v} {β : Type w} (g : (α → r) → r) (cont : α → FreeCont r β) (k : β → r) : run (liftBind (ContF.callCC g) cont) k = g fun (a : α) => (cont a).run k

def Cslib.FreeM.FreeCont.callCC {r : Type u} {α : Type v} {β : Type w} (f : MonadCont.Label α (FreeCont r) β → FreeCont r α) : FreeCont r α

Call with current continuation for the Free continuation monad.

Equations

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

@[simp]

theorem Cslib.FreeM.FreeCont.callCC_def {r : Type u} {α : Type v} {β : Type w} (f : MonadCont.Label α (FreeCont r) β → FreeCont r α) : callCC f = liftBind (ContF.callCC fun (k : α → r) => (f { apply := fun (x : α) => liftBind (ContF.callCC fun (x_1 : β → r) => k x) pure }).run k) pure

instance Cslib.FreeM.FreeCont.instMonadCont {r : Type u} : MonadCont (FreeCont r)

Equations

• Cslib.FreeM.FreeCont.instMonadCont = { callCC := fun {α β : Type ?u.10} => Cslib.FreeM.FreeCont.callCC }

@[simp]

theorem Cslib.FreeM.FreeCont.run_callCC {r : Type u} {α : Type v} {β : Type w} (f : MonadCont.Label α (FreeCont r) β → FreeCont r α) (k : α → r) : (callCC f).run k = (f { apply := fun (x : α) => liftBind (ContF.callCC fun (x_1 : β → r) => k x) pure }).run k

run of a callCC node simplifies to running the handler with the current continuation.