I watched Dr. Emily Riehl’s Compose Conf talkA Categorical View of Computational
Effects

last night
and a new intuition emerged. The purpose of the talk was to explicate
the categorical notion of a monad, and while watching it, I was struck
with the realization of how a monad arises from an algebraic data
type.

## Prereqs

In her talk, she first discusses \(T\) as a computation, and defines a \(T\) as a monad: something that can take an \(A\) and lift it to a \(T(A)\), like this:

\[ A \rightarrow T(A) \]

*NB: There is another operation that comes with a monad, bind, but
we’ll skip that for now.*

The canonical example used through the first half of the talk is a
\(\text{List}\): A function from \(A \rightarrow T(A)\) could be a
function from an \(A\) to a \(List\) of \(A\)’s where \(T\) is the
*computation* which constructs a list of \(A\)’s. That is, \(A \rightarrow T(A)\) is simply a more general version of \(A \rightarrow List(A)\).

She goes on to use the notation of \(\leadsto\) to denote a “program” which contains one of these lift operations, but with \(\leadsto\), we elide the \(T\):

\[\ A \rightarrow T(B) = A \leadsto B \]

This notation is meant to denote a “weak” map between \(A\) and \(B\), in
that it’s not a complete \(A \rightarrow B\), due to the fact that it
requires the computation \(T\). This lift from \(A\) to \(T\) of \(B\) is
called a *Kleisli* arrow.

## An ADT Monad

Later in the talk, she defines a function from \(A\) to \(A + \bot\):

\[\ A \rightarrow A + \{\bot\} \]

This should look familiar—it contains a \(+\) after all! It’s an
algebraic data type (ADT)—a sum type to be specfic. It can give us
either an \(A\) or \({\bot}\); \(\bot\) means “bottom” or `false`

in this
context. It would look something like this in Haskell:

```
data Maybe a = Nothing | Just a
f :: a -> Maybe a
```

And as we know, `Maybe`

admits a monad where if we have an `a`

, we
apply our lift to it to get a `Just a`

. In Haskell, this lift is
called `return`

, and made available in the Monad typeclass:

`return :: Monad m => a -> m a`

Which, if we squint, looks an awful lot like `A -> T(A)`

. For
edification purposes, our definition of `return`

for `Maybe`

and the
other requisite pieces of a Monad in Haskell are below.

```
instance Monad Maybe where
return = Just
Just x) >>= f = f x
(Nothing >>= _ = Nothing
```

If you’re still squinting, you can start to see how:

- Our ADT becomes \(T\), the
*computation*which can give us either our`a`

, or`Nothing`

. - Using Dr. Riehl’s notation, we could denote
`f`

mathematically as \(f : A \leadsto A\)