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?
A free monad is a construction which allows you to build a monad from any Functor. Like other monads, it is a pure way to represent and manipulate computations. In particular, free monads provide a practical way to: represent stateful computations as data, and run them.
The Maybe sum type is a versatile and useful data structure that forms a monad. This enables you to compose disparate functions that each may err by failing to return a value.
The state monad is a built in monad in Haskell that allows for chaining of a state variable (which may be arbitrarily complex) through a series of function calls, to simulate stateful code.
A monad is an algebraic structure in category theory, and in Haskell it is used to describe computations as sequences of steps, and to handle side effects such as state and IO. Monads are abstract, and they have many useful concrete instances. Monads provide a way to structure a program.
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 (*)
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With