Instance definitions for the free monad are monad laws

Free.hs

import Control.Monad
import Data.Functor

data Free f a = Unit a | Join (f (Free f a))

runMonad :: Functor f => (a -> f a) -> (f (f a) -> f a) -> Free f a -> f a
runMonad unit join (Unit x) = unit x
runMonad unit join (Join x) = join (runMonad unit join <$> x)

runMonad' :: (Functor m, Monad m) => Free m a -> m a
runMonad' = runMonad return join

instance Functor f => Functor (Free f) where
    fmap f (Unit x) = Unit (f x) -- eta-comm
    fmap f (Join x) = Join (fmap (fmap f) x) -- mu-comm

-- ident: (x : F A) → fmap id x ≡ x
--  x = Unit x' => fmap id x          | def
--              =  fmap id (Unit x')  | eta-comm
--              =  Unit (id x')       | def
--              =  Unit x'            | def
--              =  x
--  x = Join x' => fmap id x                 | def
--              =  fmap id (Join x')         | mu-comm
--              =  Join (fmap (fmap id) x')  | ident (induction)
--              =  Join (fmap id x')         | ident
--              =  Join x'                   | def
--              =  x

-- homo: (p : B → C) (q : A → B) (x : F A) → fmap (p ∘ q) x ≡ fmap p (fmap q x)
--  x = Unit x' => fmap (p . q) x             | def
--              =  fmap (p . q) (Unit x')     | eta-comm
--              =  Unit ((p . q) x')          | def
--              =  Unit (p (q x'))            | eta-comm
--              =  fmap p (Unit (q x'))       | eta-comm
--              =  fmap p (fmap q (Unit x'))  | def
--              =  fmap p (fmap q x)
--  x = Join x' => fmap (p . q) x                           | def
--              =  fmap (p . q) (Join x')                   | mu-comm
--              =  Join (fmap (fmap (p . q)) x')            | homo (induction)
--              =  Join (fmap (fmap p . fmap q)) x')        | homo
--              =  Join (fmap (fmap p) (fmap (fmap q) x'))  | mu-comm
--              =  fmap p (Join (fmap (fmap q) x'))         | mu-comm
--              =  fmap p (fmap q (Join x'))                | def
--              =  fmap p (fmap q x)

freeUnit :: Functor f => a -> Free f a
freeUnit = Unit

freeJoin :: Functor f => Free f (Free f a) -> Free f a
freeJoin (Unit x) = x -- left identity
freeJoin (Join x) = Join (freeJoin <$> x) -- assoc

-- right identity: (x : M A) → join (fmap unit x) ≡ x
--  x = Unit x' => join (fmap unit x)          | def
--              =  join (fmap unit (Unit x'))  | eta-comm
--              =  join (Unit (Unit x'))       | left-id
--              =  Unit x'                     | def
--              =  x
--  x = Join x' => join (fmap unit x)                      | def
--              =  join (fmap unit (Join x'))              | mu-comm
--              =  join (Join (fmap (fmap unit) x'))       | assoc
--              =  Join (fmap join (fmap (fmap unit) x'))  | homo
--              =  Join (fmap (join . fmap unit) x')       | right-id (induction)
--              =  Join (fmap id x')                       | ident
--              =  Join x'                                 | def
--              =  x

instance Functor f => Monad (Free f) where
    return = freeUnit
    x >>= f = freeJoin (f <$> x)