MonadFunctor misunderstanding or bug?

Stream: lean4

[Mohith]

The Lean code abstraction for monad functor looks odd to me. It shows the signature of monadMap as:

monadMap {α : Type u} : ({β : Type u} → m β → m β) → n α → n α

The signature appears inconsistent with the Haskell code mentioned in the documentation. The documentation links to an MFunctor Haskell concept, and a broken link to what I believe is a MonadTransFunctor Haskell concept. Both of those sources suggest a different signature for monadMap:

monadMap {α : Type u} : ({β : Type u} → m β → n β) → m α → n α

(note the swapped occurrence of an m and an n)

Is this a bug in the code or a misunderstanding on my end? (I'm still learning the ropes of monadic code with functional programming, so I very well could be misunderstanding something)

[Mohith]

FYI, I wrote some code and proofs of what I think aligns with the original concept.

(It was a great exercise!)

import Mathlib.Control.Lawful -- Enables inferInstance : LawfulMonad (OptionT m)

/--
A function for lifting a computation from an inner `Monad` to an outer `Monad`.
Like Haskell's [`MonadTrans`], this is a functorial version of `MonadLift`.

  [`MonadTrans`]: https://hackage.haskell.org/package/transformers-0.5.5.0/docs/Control-Monad-Trans-Class.html
-/
class MonadTransformer (t : (Type u → Type v) → Type u → Type w) where
  mapMonad (m) [Monad m] : Monad (t m)
  transform (m) [Monad m] : MonadLift m (t m)

instance [MonadTransformer t] [Monad m] : Monad (t m) := MonadTransformer.mapMonad m

@[always_inline, inline, simp]
abbrev MonadTransformer.liftOf [MonadTransformer t] (m) [Monad m] : m α → t m α :=
  (transform m).monadLift

@[always_inline, inline, simp]
abbrev MonadTransformer.lift [MonadTransformer t] {m} [Monad m] : m α → t m α :=
  liftOf m

instance : MonadTransformer (ReaderT ρ) where
  mapMonad _ := inferInstance
  transform := inferInstance

instance : MonadTransformer (ExceptT ε) where
  mapMonad _ := inferInstance
  transform _ := inferInstance

instance : MonadTransformer (StateT σ) where
  mapMonad _ := inferInstance
  transform _ := inferInstance

instance : MonadTransformer OptionT where
  mapMonad _ := inferInstance
  transform _ := inferInstance

/--
The `MonadTransformer` typeclass only contains the operations of a monad transformer.
`LawfulMonadTransformer` further asserts that these operations satisfy the laws of a monad transformer:
```
liftOf m (pure x) = pure x
liftOf m x >>= liftOf m ∘ f = liftOf m (x >>= f)
```
-/
class LawfulMonadTransformer (t) [MonadTransformer t] : Prop where
  monad_functor [Monad m] [LawfulMonad m] : LawfulMonad (t m)
  lift_pure [Monad m] [LawfulMonad m] (x : α) :
    ‹MonadTransformer t›.liftOf m (pure x) = pure x
  lift_bind [Monad m] [LawfulMonad m] (x : m α) (f : α → m β) :
    ‹MonadTransformer t›.lift x >>= MonadTransformer.lift ∘ f = MonadTransformer.lift (x >>= f)

section
attribute [local simp] MonadLift.monadLift Bind.bind

instance : LawfulMonadTransformer (ReaderT ρ) where
  monad_functor := inferInstance
  lift_pure _ := rfl
  lift_bind _ _ := rfl

instance : LawfulMonadTransformer (ExceptT ε) where
  monad_functor := inferInstance
  lift_pure _ := map_pure _ _
  lift_bind _ _ := by
    dsimp [ExceptT.lift]
    rw [map_bind]
    exact bind_map_left _ _ _

instance : LawfulMonadTransformer (StateT σ) where
  monad_functor := inferInstance
  lift_pure _ := funext fun _ => pure_bind _ _
  lift_bind _ _ := by
    funext
    dsimp [StateT.lift, StateT.bind]
    rw [bind_pure_comp, bind_map_left]
    rw [bind_pure_comp, map_bind]
    congr
    funext
    exact bind_pure_comp _ _

instance : LawfulMonadTransformer OptionT where
  monad_functor := inferInstance
  lift_pure _ := pure_bind _ _
  lift_bind _ _ := by
    dsimp [OptionT.lift, OptionT.bind, OptionT.mk]
    rw [bind_pure_comp, bind_map_left]
    rw [bind_pure_comp, map_bind]
    congr
    funext
    exact bind_pure_comp _ _
end

/--
The `MonadLift` typeclass only contains the operations of a monad lift.
`LawfulMonadLift` further asserts that these operations satisfy the laws of a monad lift:
```
monadLift (pure x) = pure x
monadLift x >>= monadLift ∘ f = monadLift (x >>= f)
```
-/
class LawfulMonadLift (m : Type u → Type v) (n : Type u → Type w) [Monad m] [Monad n]
    [MonadLift m n] : Prop where
  lift_pure (x : α) : ‹MonadLift m n›.monadLift (pure x) = pure x
  lift_bind (x : m α) (f : α → m β)
    : ‹MonadLift m n›.monadLift x >>= monadLift ∘ f = monadLift (x >>= f)

namespace MonadTransformer

scoped instance [MonadTransformer t] [Monad m] : MonadLift m (t m) := MonadTransformer.transform m

scoped instance [MonadTransformer t] [Monad m] [LawfulMonad m] [LawfulMonadTransformer t]
    : LawfulMonadLift m (t m) where
  lift_pure := LawfulMonadTransformer.lift_pure
  lift_bind := LawfulMonadTransformer.lift_bind

end MonadTransformer

[Mohith]

I realized a part of my misunderstanding stems from the way the documentation is currently phrased, and also from different conventions used by different authors.

• How it's being used now: A MonadFunctor is a morphism in the category of monads, in the sense of being a compatible functor between two objects of the category of monads. (In the documentation, the preposition "in" was used)
• What I thought earlier: A MonadFunctor is a functor on the category of monads, in the sense of domain and codomain both being the category of Monads

IIUC, the concept of MonadFunctor is slightly different than the concept of MonadTransformer that I wrote above:

• The former is about changing a specific monad, perhaps independently of the data. (In the documentation, this appears to be phrased as "lift monad-transforming functions")
• The latter is about "lifting" pure computations into the effectful world, perhaps independently of the monad

I believe the referenced Haskell code intends for a joint concept called MonadTransFunctor. Such a typeclass would probably extend MonadTransformer, and a lawful such typeclass would probably enforce that each component of the transform is an instance of MonadFunctor (in the sense it's currently being used in the Lean codebase)