CODEWITHSUNDEEP
haskellcategory-theoryfree-monad
n. m. could be an AI
n. m. could be an AI

Reputation: 119877

Does the free monad always exist?

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?

Upvotes: 38

Views: 691

Answers (2)

dfeuer
dfeuer

Reputation: 48591

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.

Upvotes: 4

Vlad Patryshev
Vlad Patryshev

Reputation: 1422

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?

Upvotes: 1

Related Questions