Question

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?

Was it helpful?

Solution

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.

OTHER TIPS

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?

Example of different monad instances

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 (*)
Licensed under: CC-BY-SA with attribution
Not affiliated with StackOverflow
scroll top