Different definitions of monad

280 Views Asked by At

A monad is usually defined (for example http://www.cs.cornell.edu/courses/cs6110/2011sp/lectures/lecture37.pdf) as a triple $(F, η, µ)$ where

• $F : C → C$ is an endofunctor on a category $C$;

• $η \hspace{0.1cm}$ ('unit') is a collection of morphisms $η_{A} : A → F A$, one for each object $A$; and

• $µ \hspace{0.1cm}$ ('join') is a collection of morphisms $µ_A : F(F(A)) → F A$, one for each object $A$

I've noticed that bind is sometimes defined differently. For example, in the following two references:

'join' is not employed in the definition of a monad. Rather, we have$FA \rightarrow (A \rightarrow FB) \rightarrow F(B)$, for categories $A, B$, instead of 'join' above, in addition to $η$ and $F$ in the above.

Are these just alternative ways of defining a monad? Am I confusing different types of monad?

1

There are 1 best solutions below

2
On BEST ANSWER

This is largely just a different presentation of monads, but there are some subtleties.

Eugenio Moggi's Notions of Computation and Monads, which is the wellspring from which Wadler's work in this area is derived, does a good job of describing this presentation. Following Manes' Algebraic Theories, he starts with the following presentation (Definition 1.2) called a Kleisli triple:

Let $\mathcal{C}$ be a category, $T : \mathsf{Obj}(\mathcal{C})\to\mathsf{Obj}(\mathcal{C})$ a (class) function, $\eta_A : A \to TA$ for each $A\in\mathsf{Obj}(\mathcal{C})$, and $(-)^* : \mathsf{Hom}(A,TB)\to\mathsf{Hom}(TA,TB)$ for each $A, B\in\mathsf{Obj}(\mathcal{C})$ satisfying $\eta_A^* = id_{TA}$, $f^*\circ\eta_A = f$, and $f^* \circ g^* = (f^* \circ g)^*$. With this we can defined the Kleisli category.

Proposition 1.6 proves that there is a one-to-one correspondence between monads and Kleisli triples. Going from a monad $(T,\eta,\mu)$ to a Kleisli triple just requires us to define $(-)^*$ which we can do as follows, $f^* = \mu\circ Tf$. It's easy to check that the laws above follow from the monad laws and naturality. Going the other way, we need to define the action of $T$ on arrows and $\mu$ and show that $\eta$ is natural. We have $Tf = (\eta\circ f)^*$ and $\mu = id^*$. The monad laws hold: $$\mu\circ\eta = id^*\circ\eta = id \qquad \mu\circ T\eta = id^*\circ(\eta\circ\eta)^* = (id^* \circ \eta \circ \eta)^* = id \\ \mu\circ T\mu = id^*\circ(\eta\circ id^*)^* = (id^*\circ\eta\circ id^*)^* = id^{**} = (id^*\circ id)^* = id^*\circ id^* = \mu\circ\mu$$ the functor laws hold: $$T id = (\eta\circ id)^* = \eta^* = id \\ Tf\circ Tg = (\eta \circ f)^*\circ(\eta \circ g)^* = ((\eta\circ f)^*\circ\eta\circ g)^* = (\eta\circ f\circ g)^* = T(f\circ g)$$ and naturality holds: $$Tf \circ \eta = (\eta\circ f)^*\circ \eta = \eta \circ f \\ \mu\circ T^2 f = id^*\circ(\eta\circ(\eta\circ f)^*)^* = id^*\circ\eta\circ(\eta\circ f)^{**} = ((\eta\circ f)^*\circ id)^* = Tf\circ\mu$$

That's how they are the same, however, the $(-)^*$ operation, called extend or extension is not bind. In fact, the type of bind doesn't even make sense; it combines homsets and objects. This leads to Definition 3.2, a strong monad. A strong monad is a monad that has a strength which is a natural transformation: $\sigma : A\times TB \to T(A\times B)$ (where we're assuming $\mathcal{C}$ has finite products now) satisfying several laws which I won't repeat here but which say that $\sigma$ is a tensorial strength and that $\eta$ and $\mu$ are (self-)enriched natural transformations. The upshot of the strength is that the action of $T$ is internalized and from there we get that $(-)^*$ internalizes to $(-)^* : TB^A\to TB^{TA}$ assuming these exponentials exist. We then get bind by transposition, $\mathsf{bind} : TA\times TB^A\to TB$. In a category with these exponentials and $\mathsf{bind}$, $\sigma=\mathsf{bind}\circ\langle\pi_2,\mathsf{curry}(\eta)\circ\pi_1\rangle$ where $\mathsf{curry} : \mathsf{Hom}(A\times B,TC)\to\mathsf{Hom}(A,TC^B)$ natural in $A$, $B$, and $C$. So the presentation in terms of $\mathsf{bind}$ means we have a strong monad. This is why most theoretical work uses the extend operation instead, since it needs fewer assumptions.

The point of the strength, even without the exponentials, is that it lets us formulate multi-parameter monadic actions, i.e. it allows us to have a multi-parameter extension which maps e.g. $\mathsf{Hom}(A\times B,TC)$ into $\mathsf{Hom}(TA\times TB,TC)$ via $f \mapsto f^*\circ\mu\circ T(T\mathsf{swap}\circ\sigma\circ\mathsf{swap})\circ \sigma$ where $\mathsf{swap} : A\times B \to B \times A$ natural in $A$ and $B$.