I'm having a bit of a hard time understanding how to prove the Functor
and Monad
laws for free monads. First off, let me put up the definitions I'm using:
data Free f a = Pure a | Free (f (Free f a))
instance Functor f => Functor (Free f) where
fmap f (Pure a) = Pure (f a)
fmap f (Free fa) = Free (fmap (fmap f) fa)
instance Functor f => Monad (Free f) where
return = Pure
Pure a >>= f = f a
Free fa >>= f = Free (fmap (>>=f) fa)
{-
Functor laws:
(1) fmap id x == x
(2) fmap f (fmap g x) = fmap (f . g) x
Monad laws:
(1) return a >>= f == f a
(2) m >>= return == m
(3) (m >>= f) >>= g == m >>= (\x -> f x >>= g)
-}
If I understand things correctly, the equational proofs require appeal to a coinductive hypothesis, and it goes more or less like this example:
Proof: fmap id == id
Case 1: x := Pure a
fmap id (Pure a)
== Pure (id a) -- Functor instance for Free
== Pure a -- id a == a
Case 2: x := Free fa
fmap id (Free fa)
== Free (fmap (fmap id) fa) -- Functor instance for Free f
== Free (fmap id fa) -- By coinductive hypothesis; is this step right?
== Free fa -- Functor f => Functor (Free f), + functor law
I've highlighted the step where I'm not sure if I'm doing things right.
If that proof is right, then the proof for the Free
constructor case of the second law is as follows:
fmap f (fmap g (Free fa))
== fmap f (Free (fmap (fmap g) fa))
== Free (fmap (fmap f) (fmap (fmap g) fa))
== Free (fmap (fmap f . fmap g) fa)
== Free (fmap (fmap (f . g)) fa) -- By coinductive hypothesis
== fmap (f . g) (Free fa)
Yes, this is correct. The 'base case' for the coinduction is the
Pure
constructor, and the induction is over levels of nesting of theFree
constructor.The complete proofs are