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
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.