Free monad and the free operation

Question

One way to describe the Free monad is to say it is an initial monoid in the category of endofunctors (of some category C) whose objects are the endofunctors from C to C, arrows are the natural transformations between them. If we take C to be Hask, the endofunctor are what is called Functor in haskell, which are functor from * -> * where * represents the objects of Hask

By initiality, any map from an endofunctor t to a monoid m in End(Hask) induces a map from Free t to m.

Said otherwise, any natural transformation from a Functor t to a Monad m induces a natural transformation from Free t to m

I would have expected to be able to write a function

free :: (Functor t, Monad m) => (∀ a. t a → m a) → (∀ a. Free t a → m a)
free f (Pure  a) = return a
free f (Free (tfta :: t (Free t a))) =
    f (fmap (free f) tfta) 

but this fails to unify, whereas the following works

free :: (Functor t, Monad m) => (t (m a) → m a) → (Free t a → m a)
free f (Pure  a) = return a
free f (Free (tfta :: t (Free t a))) =
    f (fmap (free f) tfta)

or its generalization with signature

free :: (Functor t, Monad m) => (∀ a. t a → a) → (∀ a. Free t a → m a)

Did I make a mistake in the category theory, or in the translation to Haskell ?

I'd be interested to hear about some wisdom here..

PS : code with that enabled

{-# LANGUAGE RankNTypes, UnicodeSyntax #-}
import Control.Monad.Free

Answer 1

The Haskell translation seems wrong. A big hint is that your free implementation doesn't use monadic bind (or join) anywhere. You can find free as foldFree with the following definition:

free :: Monad m => (forall x. t x -> m x) -> (forall a. Free t a -> m a)
free f (Pure a)  = return a
free f (Free fs) = f fs >>= free f

The key point is that f specializes to t (Free t a) -> m (Free t a), thus eliminating one Free layer in one fell swoop.

Answer 2

I don't know about the category theory part, but the Haskell part is definitely not well-typed with your original implementation and original type signature.

Given

free :: (Functor t, Monad m) => (∀ a. t a → m a) → (∀ a. Free t a → m a)

when you pattern match on Free tfta, you get

tfta :: t (Free t a)
f :: forall a. t a -> m a 
free :: (forall a. t a -> m a) -> forall a. Free t a -> m a

And thus

free f :: forall a. Free t a -> m a

leading to

fmap (free f) :: forall a. t (Free t a) -> t (m a) 

So to be able to collapse that t (m a) into your desired m a, you need to apply f on it (to "turn the t into an m") and then exploit the fact that m is a Monad:

f . fmap (free f) :: forall a. t (Free t a) -> m (m a)
join . f . fmap (free f) :: forall a. t (Free t a) -> m a

which means you can fix your original definition by changing the second branch of free:

{-# LANGUAGE RankNTypes, UnicodeSyntax #-}

import Control.Monad.Free
import Control.Monad

free :: (Functor t, Monad m) => (∀ a. t a → m a) → (∀ a. Free t a → m a)
free f (Pure  a) = return a
free f (Free tfta) = join . f . fmap (free f) $ tfta

This typechecks, and is probably maybe could be what you want :)