Free monad and free operation

Question

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

By virtue of its primacy, any mapping from endofunctor t to the monoid m in End(Hask) induces a mapping from Free t to m .

In any case, any natural conversion from Functor t to Monad m induces a natural conversion from Free t to m

I expected to be able to write a function

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

but this cannot be unified, whereas the following works

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

or its generalization with a signature

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

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

I would be interested to know about some kind of wisdom here.

PS: code with enabled

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

Answer 1

Haskell's translation seems incorrect. A big hint that your free implementation does not use monadic binding (or join) anywhere. You can find free as foldFree with the following definition:

 free :: Monad m => (forall x. tx -> mx) -> (forall a. Free ta -> ma) free f (Pure a) = return a free f (Free fs) = f fs >>= free f 

The key point is that f specializes in t (Free ta) -> m (Free ta) , thereby 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.

Considering

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

when you map the pattern by Free tfta , you get

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

And thus,

 free f :: forall a. Free ta -> ma 

leading to

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

So, to collapse this t (ma) into the desired ma , you need to apply f to it (to "turn t into m "), and then use the fact that m is a monad:

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

which means that you can correct your original definition by changing the second free branch:

 {-# LANGUAGE RankNTypes, UnicodeSyntax #-} import Control.Monad.Free import Control.Monad free :: (Functor t, Monad m) => (∀ a. ta → ma) → (∀ a. Free ta → ma) free f (Pure a) = return a free f (Free tfta) = join . f . fmap (free f) $ tfta 

These are typechecks, and probably maybe this is what you want :)