I don't know what your definition of retract
is, but given
retract :: Monad m => Free m a -> m a
retract (Pure a) = return a
retract (Impure fx) = fx >>= retract
and
liftF :: Functor f => f a -> Free f a
liftF fx = Impure (fmap Pure fx)
note that (proofs might be wrong, did them by hand and haven't checked them)
retract $ liftF x
= retract (Impure (fmap Pure x))
= (fmap Pure x) >>= retract
= (x >>= return . Pure) >>= retract
= x >>= \y -> (return $ Pure y) >>= retract
= x >>= \y -> (retract (Pure y))
= x >>= \y -> return y
= x >>= return
= x
so you have
retract (liftF x >>= liftF . f)
= retract ((Impure (fmap Pure x)) >>= liftF . f)
= retract $ Impure $ fmap (>>= liftF . f) $ fmap Pure x
= (fmap (>>= liftF . f) $ fmap Pure x) >>= retract
= (fmap (\y -> Pure y >>= liftF . f) x) >>= retract
= (fmap (liftF . f) x) >>= retract
= (liftM (liftF . f) x) >>= retract
= (x >>= return . liftF . f) >>= retract
= x >>= (\y -> (return $ liftF $ f y >>= retract)
= x >>= (\y -> retract $ liftF $ f y)
= x >>= (\y -> retract . liftF $ f y)
= x >>= (\y -> f y)
= x >>= f
this does not mean that Free m a
is isomorphic to m a
, just that retract
is really witness to a retraction. Note that liftF
is not a monad morphism (return
does not go to return
). Free is functor in the category of functors, but it is not a monad in the category of monads (despite retract
looking a lot like join
and liftF
looking a lot like return
).
EDIT: Note that the retraction implies a sort of equivalence. Define
~ : Free m a -> Free m a -> Prop
a ~ b = (retract a) ==_(m a) (retract b)
Then consider the quotient type Free m a/~
. I assert that this type is isomorphic to m a
. Since (liftF (retract x)) ~ x
because (retract . liftF . retract $ x) ==_(m a) retract x
. Thus, the free monad over a monad is exactly that monad plus some extra data. This is exactly the same as the claim that [m]
is "essentially the same" as m
when m
is m
is a monoid.