monads

2026-07-19

i don't think any of this post is correct, let alone accurate, and definitely not well-written, but i hope you get something from it anyways.

i was recently speaking to some friends who are much smarter than me about monads, something something endo-burrito in the category of mexican food end post.

in particular, i was curious about the relation between category theoretical monads and monads as you see in functional programming, e.g. haskell, because they didn't seem to map onto each other in any way that makes sense.

what started to elucidate this for me was reading this paper, which revealed the important history to me: monads were initially applied to programming in order to mathematically model side effects in imperative programming, specifically by creating a general algebra with which any kind of side effect can be modelled. the idea that expressions in programming languages can be modelled as mathematical functions from values to values is not ideal, monads let us extend a value with additional structure to represent a computation. then, this idea gained traction and got re-applied to functional programming as a way to keep 'pure' functions whilst still allowing for side effects.

in category theory, a monad is a triple \((T, \eta, \mu)\), where \(T\) is an endofunctor, and \(\eta : X \rightarrow T X\) and \(\mu : T T X \rightarrow T X \) are natural transformations(???). this is all sounding mighty familiar! just like in haskell, it seems like we have some way to raise a value into the monadic context with \(\eta\), and some way to reduce/chain monad operations with \(\mu\).

you should read the example in the paper about stores, i'm going to instead consider the List monad:

$$T X = U(FM(X))$$

that is, the List monad context for a datatype X is the underlying set of the free monoid on X (basically every sequence creatable with elements from X)

$$T (f: X \rightarrow Y) = \lambda l : T X. \texttt{map } f l$$

i don't think i'm cheating here by not defining map. you know what it does.

$$\eta_X(x) = [x]$$

that is, we can raise a value into the List monad context by putting it in a singleton list.

$$\mu_X(l) = \texttt{concat }l$$

that is, we can chain our list of lists into a single list by concatenating them all together!

time to take a look at monads in haskell!

a monad m has functions return :: a -> m a (looks just like \(\eta\)!), and >>= :: m a -> (a -> m b) -> m b

what the fuck. we don't have this >>= anywhere in our definition of monad.

looking at Moggi's original 1991 paper on monads to model programs, we see that there's no mention of any \(\mu\), instead there's all this talk of 'Kleisli triples', which seem to replace \(\mu\) with _*, which turns a function \(f : A \rightarrow TB\) into \(f^* : TA \rightarrow TB\), with some requirements on the behaviour of _*.

from this, we can define >>= simply

$$\texttt{>>=}: T A \rightarrow (A \rightarrow T B) \rightarrow T B = \lambda c : TA. \lambda f: A \rightarrow TB. f^* c$$

and as an inverse, we can define _*:

$$\_ ^* : (A \rightarrow T B) \rightarrow (TA \rightarrow TB) = \lambda f: A \rightarrow TB. \lambda c : TA. c \texttt{ >>= } f$$

so the definitions of >>= and _* are equivalent!

similarly, we can get:

$$\mu : TTA \rightarrow TA = \lambda c:TTA. c \texttt{ >>= } \texttt{id}$$

in this invocation of >>=, the first argument is of type \(TTA\), so passing in a second argument of type \(TA \rightarrow TA\) makes bind return a \(TA\).

and in reverse:

$$\texttt{>>=}: T A \rightarrow (A \rightarrow TB) \rightarrow TB = \lambda c: TA. \lambda f: A \rightarrow TB. \mu(\texttt{fmap } f c)$$

so, all \(\mu, \_ ^* , \texttt{>>=}\) are equivalent. i'm not sure why we see >>= in haskell, and not _* or \(\mu\), perhaps it's because >>= maps more closely to the ergonomics of chaining monadic operations, which is what we want to do in practice most of the time?

for completeness, let's define _* in terms of \(\mu\):

$$\_ ^* : (A \rightarrow TB) \rightarrow (TA \rightarrow TB) = \lambda f: A\rightarrow TB. \lambda c: TA. \mu (\texttt{fmap }f c)$$

writing this one i realised that >>= and _* really are just the same with the parameters swapped around!

doing this interrogation is what finally cleared up the constructions of monads in functional programming vs category theory and how they seem different but are actually the same, from the perspective a very amateur functional programmer and category theorist.