Monad

Attributes

• ext
• functor_norm
• monad_norm

Implementation Details

Set of rewrite rules and automation for monads in general and ReaderT, StateT, ExceptT and OptionT in particular.

The rewrite rules for monads are carefully chosen so that simp with functor_norm will not introduce monadic vocabulary in a context where applicatives would do just fine but will handle monadic notation already present in an expression.

In a context where monadic reasoning is desired simp with monad_norm will translate functor and applicative notation into monad notation and use regular functor_norm rules as well.

Tags

functor, applicative, monad, simp

theorem ReaderT.ext_iff {ρ : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_1} {x : ReaderT ρ m α} {y : ReaderT ρ m α} : x = y ↔ ∀ (ctx : ρ), x.run ctx = y.run ctx

theorem ExceptT.ext_iff {ε : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_1} {x : ExceptT ε m α} {y : ExceptT ε m α} : x = y ↔ x.run = y.run

theorem StateT.ext_iff {σ : Type u_1} {m : Type u_1 → Type u_2} {α : Type u_1} {x : StateT σ m α} {y : StateT σ m α} : x = y ↔ ∀ (s : σ), x.run s = y.run s

theorem map_eq_bind_pure_comp {α : Type u} {β : Type u} (m : Type u → Type v) [Monad m] [LawfulMonad m] (f : α → β) (x : m α) : f <$> x = x >>= pure ∘ f

def StateT.eval {α : Type u} {σ : Type u} {m : Type u → Type v} [Functor m] (cmd : StateT σ m α) (s : σ) : m α

run a StateT program and discard the final state

Equations

• cmd.eval s = Prod.fst <$> cmd.run s

def StateT.equiv {σ₁ : Type u₀} {α₁ : Type u₀} {σ₂ : Type u₁} {α₂ : Type u₁} {m₁ : Type u₀ → Type v₀} {m₂ : Type u₁ → Type v₁} (F : (σ₁ → m₁ (α₁ × σ₁)) ≃ (σ₂ → m₂ (α₂ × σ₂))) : StateT σ₁ m₁ α₁ ≃ StateT σ₂ m₂ α₂

reduce the equivalence between two state monads to the equivalence between their respective function spaces

Equations

• StateT.equiv F = F

def ReaderT.equiv {ρ₁ : Type u₀} {α₁ : Type u₀} {ρ₂ : Type u₁} {α₂ : Type u₁} {m₁ : Type u₀ → Type v₀} {m₂ : Type u₁ → Type v₁} (F : (ρ₁ → m₁ α₁) ≃ (ρ₂ → m₂ α₂)) : ReaderT ρ₁ m₁ α₁ ≃ ReaderT ρ₂ m₂ α₂

reduce the equivalence between two reader monads to the equivalence between their respective function spaces

Equations

• ReaderT.equiv F = F