Functor Laws, applicative laws, and monad Laws

def StateT.mk {σ : Type u} {m : Type u → Type v} {α : Type u} (f : σ → m (α × σ)) : StateT σ m α

StateT doesn't require a constructor, but it appears confusing to declare the following theorem as a simp theorem.

@[simp]
theorem run_fun (f : σ → m (α × σ)) (st : σ) : StateT.run (fun s => f s) st = f st :=
  rfl

If we declare this theorem as a simp theorem, StateT.run f st is simplified to f st by eta reduction. This breaks the structure of StateT. So, we declare a constructor-like definition StateT.mk and a simp theorem for it.

Equations

• StateT.mk f = f

@[simp]

theorem StateT.run_mk {σ : Type u} {m : Type u → Type v} {α : Type u} (f : σ → m (α × σ)) (st : σ) : (StateT.mk f).run st = f st

theorem StateT.map_const {σ : Type u} {m : Type u → Type v} {α β : Type u} [Monad m] : Functor.mapConst = Functor.map ∘ Function.const β

A copy of LawfulFunctor.map_const for StateT that holds even if m is not lawful.

@[simp]

theorem StateT.run_mapConst {σ : Type u} {m : Type u → Type v} {α β : Type u} [Monad m] [LawfulMonad m] (x : StateT σ m α) (y : β) (st : σ) : (Functor.mapConst y x).run st = Prod.map (Function.const α y) id <$> x.run st

@[simp]

theorem ExceptT.run_monadLift {α ε : Type u} {m : Type u → Type v} {n : Type u → Type u_1} [Monad m] [MonadLiftT n m] (x : n α) : (monadLift x).run = Except.ok <$> monadLift x

@[simp]

theorem ExceptT.run_monadMap {α ε : Type u} {m : Type u → Type v} (x : ExceptT ε m α) {n : Type u → Type u_1} [MonadFunctorT n m] (f : {α : Type u} → n α → n α) : (monadMap f x).run = monadMap f x.run

def ReaderT.mk {m : Type u → Type v} {α σ : Type u} (f : σ → m α) : ReaderT σ m α

ReaderT doesn't require a constructor, but it appears confusing to declare the following theorem as a simp theorem.

@[simp]
theorem run_fun (f : σ → m α) (r : σ) : ReaderT.run (fun r' => f r') r = f r :=
  rfl

If we declare this theorem as a simp theorem, ReaderT.run f st is simplified to f st by eta reduction. This breaks the structure of ReaderT. So, we declare a constructor-like definition ReaderT.mk and a simp theorem for it.

Equations

• ReaderT.mk f = f

@[simp]

theorem ReaderT.run_mk {m : Type u → Type v} {α σ : Type u} (f : σ → m α) (r : σ) : (ReaderT.mk f).run r = f r