Monad morphisms under private state

A monad morphism transforms a stateful computation by transforming its complete result/state pair. It preserves sequencing without dropping or reinitializing the private state.

Main results

• Cslib.IsMonadHom.stateT: lift a monad morphism pointwise under StateT.
• StateT.foldlM_run: running a list foldlM in StateT σ m folds the stateful step over pairs.
• StateT.foldlM_run_except: running a list foldlM in StateT σ (Except ε) is a pure List.foldl with Except.bind.

References

Uses the upstream Cslib.IsMonadHom interface and Lean's StateT.

theorem Cslib.IsMonadHom.stateT {m : Type u → Type v} {n : Type u → Type w} [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n] {f : {α : Type u} → m α → n α} (hf : IsMonadHom m n fun {α : Type u} => f) (State : Type u) : IsMonadHom (StateT State m) (StateT State n) fun {α : Type u} (program : StateT State m α) (state : State) => f (program state)

Transforming the underlying effect while retaining state is a monad morphism.

theorem StateT.foldlM_run {m : Type u → Type v} [Monad m] {σ β γ : Type u} (g : β → γ → StateT σ m β) (l : List γ) (b : β) (s : σ) : (List.foldlM g b l).run s = List.foldlM (fun (p : β × σ) (c : γ) => (g p.fst c).run p.snd) (b, s) l

Running a monadic left fold in StateT σ m folds the stateful step over value-state pairs.

theorem StateT.foldlM_run_except {σ ε β γ : Type u} (g : β → γ → StateT σ (Except ε) β) (l : List γ) (b : β) (s : σ) : (List.foldlM g b l).run s = List.foldl (fun (acc : Except ε (β × σ)) (c : γ) => acc.bind fun (p : β × σ) => (g p.fst c).run p.snd) (Except.ok (b, s)) l

Running a fold in the state-and-exception monad StateT σ (Except ε) is a pure List.foldl chaining results with Except.bind.