Does the free monad always exist?

Question

We know from the category theory that not all endofunctors in Set admit a free monad. The canonical counterexample is the powerset functor.

But Haskell can turn any functor into a free monad.

data Free f a = Pure a | Free (f (Free f a))
instance Functor f => Monad (Free f) where
  return = Pure
  Pure a >>= f = f a
  Free m >>= f = Free ((>>= f) <$> m)

What makes this construction work for any Haskell functor but break down in Set?

Just so that innocent bystanders learn more: If possible with two or three sentence, can you elaborate why the powerset functor does not admit to a monad (and what this is then about)? — Joachim Breitner
@JoachimBreitner The powerset functor is itself a monad (with pure = singleton and join = union), but it does not admit a free monad over it. Why it doesn't is a bit involved question. A free monad is equivalent to the initial algebra for the endofunctor, and Powerset does not have an initial algebra (this follows from the Cantor's theorem: powerset(S) /= S). Note I don't quite understand these notions myself; I guess if I did I wouldn't be asking this question. — n. 1.8e9-where's-my-share m.
There's a detailed discussion of these matters on Paolo Capriotti's blog. Most of it goes way over my head. — dfeuer
Categories in Haskell only form small categories (or is it locally small?). This answer seems to make the argument that the free monad over a endofunctor exists iff it is "locally presentable" (which requries a small cat.) Furthermore, this seems to claim that the free monad as constructed in the OP is only "algebriacally free" but the algebriacally free monad exists only for endofunctors over small classes (which is every class in Haskell). — user2407038

dfeuer dfeuer · Accepted Answer · 2016-01-02T18:18:30

It's become clear that this answer is wrong. I'm leaving it here to preserve valuable discussion in the comments until someone formulates a correct answer.

Consider the power set in Set. If we have a function f : S -> T, we can form f' : PS S -> PS T by f' X = f [X]. Nice covariant functor (I think). We could also form f'' X = f^(-1) [X], a nice contravariant functor (I think).

Let's look at the "power set" in Haskell:

newtype PS t = PS (t -> Bool)

This is not a Functor, but only a Contravariant:

instance Contravariant PS where
  contramap f (PS g) = PS (g . f)

We recognize this because t is in negative position. Unlike Set, we cannot get at the "elements" of the characteristic functions that make up the power set, so the covariant functor isn't available.

I would conjecture, therefore, that the reason Haskell admits a free monad for every covariant functor is that it excludes those covariant functors that cause trouble for Set.

Does the free monad always exist?

2 Answers