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.

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.