Is x >>= f
equivalent to retract (liftF x >>= liftF . f)
?
That is, is the monad instance of a free monad build from a Functor which is also a Monad going to have an equivalent monad instance to the original Monad?
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.
That is, is the monad instance of a free monad build from a Functor which is also a Monad going to have an equivalent monad instance to the original Monad?
No. The free monad over any functor is a monad. Thus, it cannot magically know about the Monad instance when it exists. And it cannot also "guess" it, because the same functor may be made a Monad in different ways (e.g. a writer monad for different monoids).
Another reason is that it doesn't make much sense to ask whether these two monads have equivalent instances because they are not even isomorphic as types. For example, consider the free monad over the writer monad. It will be a list-like structure. What does it mean for these two instances to be equivalent?
In case the above description isn't clear, here's an example of a type with many possible Monad instances.
data M a = M Integer a
bindUsing :: (Integer -> Integer -> Integer) -> M a -> (a -> M b) -> M b
bindUsing f (M n a) k =
let M m b = k a
in M (f m n) b
-- Any of the below instances is a valid Monad instance
instance Monad M where
return x = M 0 x
(>>=) = bindUsing (+)
instance Monad M where
return x = M 1 x
(>>=) = bindUsing (*)