The free monad over an endofunctor on $\mathcal{Set}$

Question

Let $F$ be an endofunctor on the category $\mathbf{Set}$. How can I construct the free monad over $F$? Can this construction be generalized to other categories than $\mathbf{Set}$?

Answer 1

Let's investigate the specific case of free monads over $\newcommand\catname\mathbf\newcommand\Set{\catname{Set}}\Set\newcommand\Mnd{\catname{Mnd}}\newcommand\into\hookrightarrow\newcommand\id{\mathrm{id}}$, and the relationship to the Haskell free monad.

Free Monads in General:

First the general case of what a free monad is. (There are more general notions, but this corresponds to the Haskell notion.) Note that I am not writing the forgetful functor from monads in $C$, $\Mnd_C$, to the endofunctor category, $[C,C]$, explicitly.

Let $F: C\to C$ be an endofunctor. A monad $(T,\mu_T,\iota_T)$ is a free monad for $F$ if for monads $(S,\mu_S,\iota_S)$ we have a natural isomorphism $$[C,C](F,S) \simeq \Mnd_C(T,S).$$ The functor on the right is corepresentable, so a natural transformation $$\Mnd_C(T,S)\to [C,C](F,S)$$ is determined by an element $\alpha$ of $[C,C](F,T)$ by Yoneda's lemma. The free monad is usually considered to be the pair $(T,\alpha)$.

The Haskell Free Monad:

Let $\newcommand{\Hask}{\catname{Hask}}\Hask$ be the "category" of Haskell types (not quite a category, but it's close enough for our discussion).

Then the definition of the Free monad type in Haskell looks like this

data Free f a
  = Pure a
  | Free (f (Free f a))

instance Functor f => Functor (Free f) where
  fmap g (Pure x) = Pure (g x)
  fmap g (Free y) = Free (fmap (fmap g) y)

instance Functor f => Monad (Free f) where
  return = Pure
  (Pure x) >>= g = g x
  (Free y) >>= g = Free (fmap (>>= g) y)

For the non-Haskellers, this translates to if $F:\Hask\to\Hask$ is a functor, the free monad functor $T$ is defined by the equation $T-=-\amalg FT-$.

Then the natural inclusion $A\into TA$ is the identity for the monad, and the multiplication $\mu: T^2A\to TA$ is defined by observing $T^2A=TA\amalg FT^2A$ and defining $\mu$ to satisfy $\mu = \id \amalg F\mu$.

You'll notice we had to solve several equations here, which aren't problems in $\Hask$ because types and functions can be defined recursively, so these equations define valid types and functions.

We should also show that this definition of Free f gives a free functor for f. The natural transformation from f to Free f is just Free . fmap return, but I'll leave the verification out for now.

Translating to Set:

Now let's translate this to $\Set$. It seems like a reasonable guess that solving the equations for $T$ and $\mu$ are where we might run into problems. I'll have to return to this later though, so I'll post this partial answer.

Now we are working with $F : \Set\to \Set$. For each ordinal $\alpha$ define functors $F_\alpha$, with $F_0=\newcommand\Id{\mathrm{Id}}\Id$, $F_{\alpha+1}=-\sqcup FF_\alpha -$, and $F_\beta = \newcommand\colim{\operatorname{colim}} \colim_{\alpha \in \beta} F_\alpha$ when $\beta$ is a limit ordinal. When $\alpha \le \beta$, there are natural maps $F_\alpha\to F_\beta$, which are constructed at the same time as $F_\beta$, so that the colimit makes sense for limit ordinals. The only map that needs to be constructed explicitly is the map $\iota_\alpha: F_\alpha\to F_{\alpha+1}$. $\iota_0 : F_0\to F_1$ is clear, this is just the inclusion of $X$ in $X\sqcup FX$ for all $X$. If $\alpha=\gamma+1$, then $F_\alpha - = -\sqcup FF_\gamma -$. Then by induction $F\iota_\gamma : FF_\gamma \to FF_\alpha$, so $$\iota_\alpha = \id \sqcup F\iota_\gamma$$ works. On the other hand, if $\alpha$ is a limit ordinal, for $\gamma \in \alpha$, define $j_\gamma : F_\gamma \to F_{\alpha+1}$ by the following formulas. $j_0$ is the inclusion of $F_0=\Id$ into $F_{\alpha+1}$, $$j_{\delta+1} = \id \sqcup F (F_\delta\to F_\alpha),$$ and for limit ordinals $\delta$, $$j_{\delta} = F_\delta \newcommand\toby\xrightarrow\toby{\iota_{\delta}} F_{\delta+1}\toby{j_{\delta+1}} F_{\alpha+1}.$$ It's not hard to show that these $j$s commute with the $\iota$s, and thus induce the desired map $\iota_{\alpha}: F_\alpha\to F_{\alpha+1}$.

This completes our construction of the functors $F_\alpha$. Note that since we have $F\to F_1$, and $\Id\to F_0$, for all $\alpha \ge 1$, we have maps $F\to F_\alpha$ and $\Id \to F_\alpha$. We can think of these as being approximations to a solution to our equation.

We also need an approximation of our multiplication. Let $i_{\alpha,\beta} : F_\alpha\to F_\beta$ be the maps constructed above. Define $\mu_{\alpha,\beta}: F_\alpha F_\beta \to F_{\alpha+\beta}$ recursively. (Side note, ordinal addition is noncommutative, but I don't remember which order is correct. I think I may want $\beta+\alpha$ here actually, but this can be deduced from the definition of $\mu$ that I give.) We have $$\mu_{0,\beta} = \id,$$ $$\mu_{\alpha+1,\beta} = i_{\beta,\alpha+\beta+1} \sqcup F\mu_{\alpha,\beta},$$ and in the limit ordinal case, $$\mu_{\alpha,\beta} = \colim_{\gamma\in\alpha} i_{\gamma+\beta,\alpha+\beta}\circ \mu_{\gamma,\beta}.$$

Then if the sequence $F_\alpha$ stabilizes eventually, we see that we can solve the equations defining the free monad in $\Set$.

There's quite a bit more to add here, but once again, I'll have to leave it at a partial answer for now.