A lawful `MonadFix` instance for writer monads

MonadFix-writer.md

instance Monoid a => MonadFix ((,) a) where
  mfix :: (b -> (a, b)) -> (a, b)
  mfix f = let (a, b) = f b in (a, b)
  -- or
  mfix f = fix (f . snd)

The laws are proved in section 4.5 of Value Recursion in Monadic Computations by Levent Erkök using an embedding into the state monad and are spelt out below.

Purity

h :: a -> a

  mfix (return . h)
= let (a, b) = (mempty, h b) in (a, b)
= let b = h b in (mempty, b)
= (mempty, fix h)
= return (fix h)

Left shrinking

(a, b) :: (a, b)
f :: c -> b -> (a, c)

  mfix (\x -> (a, b) >>= \y -> f x y)
= mfix (\x -> let (a', c) = f x b in (a <> a', c))
= fix (\x -> let (a', c) = f (snd x) b in (a <> a', c))
= let (a', c) = f c b in (a <> a', c)
= let (a', c) = fix (\x -> f (snd x) b) in (a <> a', c)
= let (a', c) = mfix (\x -> f x b) in (a <> a', c)
= (a, b) >>= \y -> mfix (\x -> f x y)

(Strong) sliding

Note the absence of a precondition on h.

f :: a -> (b, c)
h :: c -> a

  mfix (fmap h . f)
= fix (fmap h . f . snd)
= fmap h (fix (f . snd . fmap h)) -- dinaturality of fix
= fmap h (fix (f . h . snd))      -- naturality of snd
= fmap h (mfix (f . h))

Nesting

f :: b -> b -> (a, b)

  mfix (\x -> mfix (\y -> f x y))
= fix (\x -> fix (\y -> f (snd x) (snd y)))
= fix (\x -> f (snd x) (snd x))             -- Bekič's property for f `on` snd
= mfix (\x -> f x x)