Mathlib.Control.Monad.Basic

Module docstring

{"# 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

map_eq_bind_pure_comp theorem

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

Full source

@[monad_norm]
theorem map_eq_bind_pure_comp (m : Type u → Type v) [Monad m] [LawfulMonad m]
    (f : α → β) (x : m α) : f <$> x = x >>= pure ∘ f :=
  (bind_pure_comp f x).symm

Map as Bind of Pure Composition: $f <$> x = x \gg= \text{pure} \circ f$

Informal description

For any monad `m` that satisfies the monad laws, a function `f : α → β`, and a monadic value `x : m α`, the map operation `f <$> x` is equivalent to binding `x` with the composition of `pure` and `f`, i.e., `x >>= pure ∘ f`.

StateT.eval definition

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

Full source

/-- run a `StateT` program and discard the final state -/
def StateT.eval {m : Type u → Type v} [Functor m] (cmd : StateT σ m α) (s : σ) : m α :=
  Prod.fstProd.fst <$> cmd.run s

Evaluate state monad computation and discard final state

Informal description

Given a state monad transformer `StateT σ m α` and an initial state `s : σ`, the function `StateT.eval` runs the monadic computation `cmd` and returns the result of type `m α`, discarding the final state. This is equivalent to taking the first component (the result) of the pair returned by `cmd.run s` and applying the functor `m` to it.

StateT.equiv definition

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

Full source

/-- reduce the equivalence between two state monads to the equivalence between
their respective function spaces -/
def StateT.equiv {σ₁ α₁ : Type u₀} {σ₂ α₂ : Type u₁}
    {m₁ : Type u₀ → Type v₀} {m₂ : Type u₁ → Type v₁}
    (F : (σ₁ → m₁ (α₁ × σ₁)) ≃ (σ₂ → m₂ (α₂ × σ₂))) : StateTStateT σ₁ m₁ α₁ ≃ StateT σ₂ m₂ α₂ :=
  F

Equivalence of State Monads via Function Space Equivalence

Informal description

Given an equivalence $F$ between function spaces $\sigma_1 \to m_1 (\alpha_1 \times \sigma_1)$ and $\sigma_2 \to m_2 (\alpha_2 \times \sigma_2)$, where $m_1$ and $m_2$ are monads, the equivalence $F$ induces an equivalence between the state monads $\text{StateT}~\sigma_1~m_1~\alpha_1$ and $\text{StateT}~\sigma_2~m_2~\alpha_2$.

ReaderT.equiv definition

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

Full source

/-- reduce the equivalence between two reader monads to the equivalence between
their respective function spaces -/
def ReaderT.equiv {ρ₁ α₁ : Type u₀} {ρ₂ α₂ : Type u₁}
    {m₁ : Type u₀ → Type v₀} {m₂ : Type u₁ → Type v₁}
    (F : (ρ₁ → m₁ α₁) ≃ (ρ₂ → m₂ α₂)) : ReaderTReaderT ρ₁ m₁ α₁ ≃ ReaderT ρ₂ m₂ α₂ :=
  F

Equivalence of Reader Monads via Function Space Equivalence

Informal description

Given an equivalence $F$ between function spaces $(\rho_1 \to m_1 \alpha_1)$ and $(\rho_2 \to m_2 \alpha_2)$, the function `ReaderT.equiv` constructs an equivalence between the reader monads `ReaderT ρ₁ m₁ α₁` and `ReaderT ρ₂ m₂ α₂`. This reduces the problem of showing equivalence between two reader monads to showing equivalence between their underlying function spaces.