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](http://math.stackexchange.com/questions/927832/adjoint-functors-for-the-power-set-monad) is then about)? — Joachim Breitner, Jan 02 '16 at 13:15
@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. m. could be an AI, Jan 02 '16 at 15:49
There's a [detailed discussion of these matters](http://www.paolocapriotti.com/blog/2013/12/04/free-monads-part-2/) on Paolo Capriotti's blog. Most of it goes way over my head. — dfeuer, Jan 03 '16 at 01:21
Categories in Haskell only form small categories (or is it locally small?). [This](http://math.stackexchange.com/questions/211560/do-free-monads-on-seti-functor-category-always-exist) 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](https://ncatlab.org/nlab/show/free+monad) 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, Jan 04 '16 at 04:03
Disclaimer: I am by no means an expert an may have misinterpreted all of the sources I've cited. — user2407038, Jan 04 '16 at 04:04

score 4 · Answer 1 · edited Jan 07 '16 at 00:08

4

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.

edited Jan 07 '16 at 00:08

Benjamin Hodgson

42,952
15
108
157

answered Jan 02 '16 at 18:18

dfeuer

48,079
5
63
167

That would be my conjecture too, but what are these troublesome functors? Can we characterise them? – n. m. could be an AI Jan 02 '16 at 18:41
5

The covariant power set functor cannot be expressed in Haskell, but the equally troublesome "double power set functor" `(a -> Bool) -> Bool` can be. So, this is not relevant. – Reid Barton Jan 02 '16 at 18:42
@ReidBarton, good point. Power sets of infinite types are rather smaller in Hask than in Set. Perhaps that's the real difference. – dfeuer Jan 02 '16 at 19:27
@ReidBarton How do you write a Functor instance for it? – n. m. could be an AI Jan 02 '16 at 19:51
@n.m., I think `fmap f (DP g) = DP (contramap (contramap f) g)`, or `fmap f (DP g) = DP (g . (. f))`. – dfeuer Jan 02 '16 at 20:43
@n.m., sorry, the first expression was wrong; it should've been `fmap f (DP g) = DP (lmap (lmap f) g)`. – dfeuer Jan 02 '16 at 20:53
@dfeuer hmm, lmap of what? – n. m. could be an AI Jan 02 '16 at 20:58
@n.m., `newtype DP a = DP ((a -> Bool) -> Bool)`, so `lmap` for `->`. More generally, you could do `newtype D p q b c a = D (p (q a b) c)` and `instance (Profunctor p, Profunctor q) => Functor (D p q b c) where fmap f (D x) = D (lmap (lmap f) x)` – dfeuer Jan 02 '16 at 21:12
This is just like doubled contravariant functors, but with different kinds. – dfeuer Jan 02 '16 at 21:14
4

Just remember that `(->)` means *computable* function in Haskell, so `a -> Bool` isn't the powerset of `a`, but the computable powerset of `a`, which is smaller. This allows us to form set-theoretically impossible types such as `newtype S = S (S -> Bool)` – luqui Jan 03 '16 at 05:26
@luqui I am a simple man. I do not possess an engineering degree, nor am I mechanically inclined. Sorry to have taken up so much of your time, but how can we use this wonderful type? It looks like S is its own computable powerset, but how do we proceed from here? – n. m. could be an AI Jan 03 '16 at 06:43
2

@n.m. Two easy elements: `empty = S (const False)` and `full = S (const True)`. A more sophisticated one `containingEmpty = S (\(S f) -> f empty)`. Etc. As far as how you use it to answer your question, I am not sure, I just felt it to be related. – luqui Jan 03 '16 at 09:42

score 1 · Answer 2 · answered Jan 03 '16 at 17:47

1

I (rather) have a suspicion that this is not exactly a definition. Say, this recursive formula specifies a fixpoint; now, how do we know this fixpoint exists? How do we know there's only one fixpoint? And more, how does Free m >>= define anything, except maybe in the case where we assume that we only have finite sequences of applications of Free?

answered Jan 03 '16 at 17:47

Vlad Patryshev

1,379
1
10
16

1

I think we do assume finite number of applications. The fixpoint need not be unique, as we always take the least fixpoint, because inductive. Whether it always exists in Haskell (look at the title ;) is the gist of the question. – n. m. could be an AI Jan 03 '16 at 18:02
I'm afraid using "we" invalidates all the arguments. The (not exactly proven) fact that in some categories it does exist (e.g. in Hask, which, I wonder, is it even defined properly?) does not prove the statement. – Vlad Patryshev Jun 30 '16 at 00:03

Does the free monad always exist?

2 Answers2