Morphisms Between Monads

class IsMonadHom (m : Type u → Type v) [Pure m] [Bind m] (n : Type u → Type w) [Pure n] [Bind n] (f : {α : Type u} → m α → n α) : Prop

• map_pure {α : Type u} (x : α) : f (pure x) = pure x
• map_bind {α β : Type u} (x : m α) (y : α → m β) : f (x >>= y) = f x >>= f ∘ y

structure MonadHom (m : Type u → Type v) [Pure m] [Bind m] (n : Type u → Type w) [Pure n] [Bind n] : Type (max (max (u + 1) v) w)

Structure to represent a well-behaved mapping between computations in two monads m and n. This is similar to MonadLift but isn't a type-class but rather an actual object. This is useful for non-canonical mappings that shouldn't be applied automatically in general. We also enforce similar laws to LawfulMonadLift.

• toFun {α : Type u} : m α → n α
• toFun_pure' {α : Type u} (x : α) : self.toFun (pure x) = pure x
• toFun_bind' {α β : Type u} (x : m α) (y : α → m β) : self.toFun (x >>= y) = do let a ← self.toFun x self.toFun (y a)

def «term_→ᵐ_» : Lean.TrailingParserDescr

instance instIsMonadHomToFun (m : Type u → Type v) [Pure m] [Bind m] (n : Type u → Type w) [Pure n] [Bind n] (F : m →ᵐ n) : IsMonadHom m n fun {α : Type u} => F.toFun

instance instCoeFunMonadHomForallForall (m : Type u → Type v) [Pure m] [Bind m] (n : Type u → Type w) [Pure n] [Bind n] : CoeFun (m →ᵐ n) fun (x : m →ᵐ n) => {α : Type u} → m α → n α

View a monad map as a function between computations. Note we can't have a full FunLike instance because the type parameter α isn't constrained by the types.

@[simp]

theorem MonadHom.mmap_pure {m : Type u → Type v} [Monad m] {n : Type u → Type w} [Monad n] {α : Type u} (F : m →ᵐ n) (x : α) : (fun {x : Type u} (x_1 : m x) => F.toFun x_1) (pure x) = pure x

@[simp]

theorem MonadHom.mmap_bind {m : Type u → Type v} [Monad m] {n : Type u → Type w} [Monad n] {α β : Type u} (F : m →ᵐ n) (x : m α) (y : α → m β) : (fun {x : Type u} (x_1 : m x) => F.toFun x_1) (x >>= y) = do let x ← (fun {x : Type u} (x_1 : m x) => F.toFun x_1) x (fun {x : Type u} (x_1 : m x) => F.toFun x_1) (y x)

@[simp]

theorem MonadHom.mmap_map {m : Type u → Type v} [Monad m] {n : Type u → Type w} [Monad n] {α β : Type u} [LawfulMonad m] [LawfulMonad n] (F : m →ᵐ n) (x : m α) (g : α → β) : (fun {x : Type u} (x_1 : m x) => F.toFun x_1) (g <$> x) = g <$> (fun {x : Type u} (x_1 : m x) => F.toFun x_1) x

@[simp]

theorem MonadHom.mmap_seq {m : Type u → Type v} [Monad m] {n : Type u → Type w} [Monad n] {α β : Type u} [LawfulMonad m] [LawfulMonad n] (F : m →ᵐ n) (x : m (α → β)) (y : m α) : (fun {x : Type u} (x_1 : m x) => F.toFun x_1) (x <*> y) = (fun {x : Type u} (x_1 : m x) => F.toFun x_1) x <*> (fun {x : Type u} (x_1 : m x) => F.toFun x_1) y

@[simp]

theorem MonadHom.mmap_seqLeft {m : Type u → Type v} [Monad m] {n : Type u → Type w} [Monad n] {α β : Type u} [LawfulMonad m] [LawfulMonad n] (F : m →ᵐ n) (x : m α) (y : m β) : (fun {x : Type u} (x_1 : m x) => F.toFun x_1) (x <* y) = (fun {x : Type u} (x_1 : m x) => F.toFun x_1) x <* (fun {x : Type u} (x_1 : m x) => F.toFun x_1) y

@[simp]

theorem MonadHom.mmap_seqRight {m : Type u → Type v} [Monad m] {n : Type u → Type w} [Monad n] {α β : Type u} [LawfulMonad m] [LawfulMonad n] (F : m →ᵐ n) (x : m α) (y : m β) : (fun {x : Type u} (x_1 : m x) => F.toFun x_1) (x *> y) = (fun {x : Type u} (x_1 : m x) => F.toFun x_1) x *> (fun {x : Type u} (x_1 : m x) => F.toFun x_1) y

def MonadHom.ofLift (m n : Type u → Type v) [Monad m] [Monad n] [MonadLift m n] [LawfulMonadLift m n] : m →ᵐ n

Construct a MonadHom from a lawful monad lift.

@[simp]

theorem MonadHom.mmap_ofLift (m n : Type u → Type v) [Monad m] [Monad n] [MonadLift m n] [LawfulMonadLift m n] {α : Type u} (x : m α) : (fun {x : Type u} (x_1 : m x) => (ofLift m n).toFun x_1) x = liftM x