bound
bound copied to clipboard
Docfix: Bound instances are right monad modules
(>>>= id)
gives a natural transformation t m . m ⇒ t m,
i.e. m acts on the right.
I see, so https://www.sciencedirect.com/science/article/pii/S0890540109002405 has a mistake, what they call left is actually right. (compare to e.g. https://en.wikipedia.org/wiki/Module_(mathematics))
- André Hirschowitz, Marco Maggesi: Definition 8 (Left modules). A left R-module is given by a functor M : C → D equipped with a natural transformation μ: M · R → M, called the action, which is compatible with the monad composition, more precisely, we require that the following diagrams commute...
- Algebra: A left R-module M consists of an abelian group (M, +) and an operation ⋅ : R × M → M such that for all r, s in R and x, y in M, we have: ...
So this fix is correct, @RyanGlScott, @ekmett, do you agree?
Wait. Isn't it that m
is the right module of t m
. We have t m (m a) -> t m a
.
As I said, it's confusing.
The monad is m
and the module is t m
. Let me write f = t m
. Referring to the definition in nLab, the 1-cell is the functor f: Hask -> Hask
and the 2-cell is the natural transformation f . m ⇒ f
(i.e. a coherent family of functions f (m a) -> f a
). In other words, m
acts on f
on the right, making t m
a right m
-module. (The fact that f = t m
is parameterized by m
is irrelevant and possibly added to the confusion.)
By contrast, a left m
-module is a functor f
with a natural transformation m . f ⇒ f
with some laws, giving a coherent family of m
-algebras m (f a) -> f a
.
R = m
, M = t m
. Who is wrong, Maggesi or nLab ?
I think nLab (and @arkeet's fix) is right. Corroborated in https://research-information.bris.ac.uk/ws/portalfiles/portal/70069065/20.pdf and https://hal.archives-ouvertes.fr/hal-02338144v3/document (the latter being from Maggesi's coauthor on the paper you linked above).