Constructs a TestTree checking that the writer monad laws hold for m with writer type w and value types a and b, using a given equality test for values of type forall u. m u. The equality context type t is for constructors m from which we can only extract a value within a context, such as reader-like constructors.

We use a slightly different set of primitives for the writer laws; rather than tell, listen, and pass, we use tell and draft :: (Monoid w) => m a -> m (a,w), which is similar to listen but resets the writer value to mempty.

draft (tell w) === return ((),w)

tell mempty === return ()

tell w1 >> tell w2 === tell (mappend w1 w2)

draft (return a) === return a

draft (x >>= f) === draft x >>= (draft' f) where draft' f (a,w) = mapsnd (mappend w) $ draft (f a)

As far as I can tell there isn't an agreed upon set of axioms for the standard writer monad primitives, so the best we can do is show that tell+draft is equivalent in power to tell+listen+pass for the only concrete writer monad we do have: the tuple monad.

Along with the property tests (for arbitrary writer monads) we'll demonstrate these equivalences (for the tuple monad) with some equational proofs, and for this purpose we need some concrete definitions.

data Writer w a = Writer { runWriter :: (a,w) }

Note that Writer and runWriter are mutual inverses.

instance (Monoid w) => Monad (Writer w) where
  return a = Writer (a, mempty)

  (Writer (a,w)) >>= f =
    let (b,w2) = runWriter (f a)
    in Writer (b, mappend w w2)

tell :: w -> Writer w ()
tell w = Writer ((),w)

draft :: (Monoid w) => Writer w a -> Writer w (a,w)
draft (Writer (a,w)) = Writer ((a,w),mempty)

listen :: Writer w a -> Writer w (a,w)
listen (Writer (a,w)) = Writer ((a,w),w)

pass :: Writer w (a, w -> w) -> Writer w a
pass u =
  let ((a,f),w) = runWriter u
  in Writer (a, f w)

listen x === do (a,w) <- draft x; tell w; return (a,w)

Suppose x === Writer (a,w). Then we have:

    do (a,w) <- draft x; tell w; return (a,w)
===   (desugar do-notation)
    draft x >>= \(a',w') -> tell w' >> return (a',w')
===   (substitute x)
    draft (Writer (a,w)) >>= \(a',w') -> tell w' >> return (a',w')
===   (definition of draft)
    Writer ((a,w), mempty) >>= \(a',w') -> tell w' >> return (a',w')
===   (definition of >>=)
    let (b,w2) = runWriter (tell w >> return (a,w))
    in Writer (b, mappend mempty w2)
===   (monoid identity law)
    let (b,w2) = runWriter (tell w >> return (a,w))
    in Writer (b, w2)
===   (let substitution)
    Writer $ runWriter (tell w >> return (a,w))
===   (constructor/destructor)
    tell w >> return (a,w)
===   (definition of tell and >>)
    Writer ((),w) >>= \_ -> return (a,w)
===   (definition of >>=)
    let (b,w2) = runWriter (return (a,w))
    in Writer (b, mappend w w2)
===   (definition of return)
    let (b,w2) = runWriter (Writer ((a,w),mempty))
    in Writer (b, mappend w w2)
===   (constructor/destructor)
    let (b,w2) = ((a,w),mempty)
    in Writer (b, mappend w w2)
===   (let substitution)
    Writer ((a,w), mappend w mempty)
===   (monoid identity law)
    Writer ((a,w), w)
===   (definition of listen)
    listen (Writer (a,w))
===   (substitute x)
    listen x

pass u === do ((a,f),w) <- draft u; tell (f w); return a

Suppose u = Writer ((a,f),w). Then we have:

    do ((a,f),w) <- draft u; tell (f w); return a
===   (desugar do notation)
    draft u >>= \((a',f'),w') -> tell (f' w') >> return a'
===   (substitute u)
    Writer (((a,f),w),mempty) >>= \((a',f'),w') -> tell (f' w') >> return a'
===   (definition of >>=)
    let (b,w2) = runWriter (tell (f w) >> return a)
    in Writer (b, mappend mempty w2)
===   (monoid identity law)
    let (b,w2) = runWriter (tell (f w) >> return a)
    in Writer (b,w2)
===   (let substitution)
    Writer $ runWriter (tell (f w) >> return a)
===   (constructor/destructor)
    tell (f w) >> return a
===   (definition of tell, >>, and return)
    Writer ((), f w) >>= \_ -> Writer (a, mempty)
===   (definition of >>=)
    let (b,w2) = runWriter (Writer (a,mempty))
    in Writer (b, mappend (f w) w2)
===   (constructor/destructor)
    let (b,w2) = (a,mempty)
    in Writer (b, mappend (f w) w2)
===   (let substitution)
    Writer (a, mappend (f w) mempty)
===   (monoid identity law)
    Writer (a, f w)
===   (definition of pass)
    pass (Writer (a,f) w)
===   (substitute u)
    pass u

draft x === pass $ do (a,w) <- listen x; return ((a,w), const mempty)

Suppose x = Writer (a,w). Then we have:

    pass $ do (a,w) <- listen x; return ((a,w), const mempty)
===   (desugar do notation)
    pass $ listen x >>= \(a',w') -> return ((a',w'), const mempty)
===   (substitute x)
    pass $ listen (Writer (a,w)) >>= \(a',w') -> return ((a',w'), const mempty)
===   (definition of listen)
    pass $ Writer ((a,w),w) >>= \(a',w') -> return ((a',w'), const mempty)
===   (definition of >>=)
    pass $ let (b,w2) = runWriter (return ((a,w), const mempty))
           in Writer (b, mappend w w2)
===   (definition of return)
    pass $ let (b,w2) = runWriter (Writer (((a,w), const mempty), mempty))
           in Writer (b, mappend w w2)
===   (constructor/destructor)
    pass $ let (b,w2) = (((a,w), const mempty), mempty)
           in Writer (b, mappend w w2)
===   (let substitution)
    pass $ Writer (((a,w), const mempty), mappend w mempty)
===   (monoid identity law)
    pass $ Writer (((a,w), const mempty), w)
===   (definition of pass)
    Writer ((a,w), const mempty w)
===   (definition of const)
    Writer ((a,w), mempty)
===   (definition of draft)
    draft (Writer (a,w))
===   (substitute x)
    draft x