Test.Tasty.QuickCheck.Laws.WriterMonad

This module uses an alternative set of primitives for writer monads which are roughly equivalent in power to the standard tell, listen, and pass, but satisfy tidier properties and have a nice intuitive interpretation. We keep tell :: w -> m () and replace listen and pass with draft :: (Monoid w) => m a -> m (a,w), which is similar to listen but resets the writer value to mempty. Intuitively, draft returns what it would have written, but doesn't actually write it. It is also satisfying that draft uses the monoid constraint on w, while tell and pass do not.

Since we are using nonstandard primitives, we also provide an extra tree of tests for checking the equivalence of the two sets.

Documentation

testWriterMonadLaws

Arguments

:: (Monoid w, Monad m, Eq w, Eq a, Eq b, Show t, Show w, Show a, Show (m a), Arbitrary t, Arbitrary w, Arbitrary a, Arbitrary (m a), Arbitrary (m b), CoArbitrary a, Typeable m, Typeable w, Typeable a)

=> Proxy m

Type constructor under test

-> Proxy t

Equality context for m

-> Proxy w

Writer type

-> Proxy a

Value type

-> Proxy b

Value type

-> (forall u. Eq u => t -> m u -> m u -> Bool)

Equality test

-> (w -> m ())

tell

-> (forall u. m u -> m (u, w))

draft

-> TestTree

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.

Writer Monad Laws

testWriterMonadLawDraftTell

Arguments

:: (Monad m, Eq w, Show t, Show w, Arbitrary t, Arbitrary w)

=> Proxy m

Type constructor under test

-> Proxy t

Equality context for m

-> Proxy w

Writer type

-> (forall u. Eq u => t -> m u -> m u -> Bool)

Equality test

-> (w -> m ())

tell

-> (forall u. m u -> m (u, w))

draft

-> TestTree

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

testWriterMonadLawTellMempty

Arguments

:: (Monoid w, Monad m, Show t, Arbitrary t)

=> Proxy m

Type constructor under test

-> Proxy t

Equality context for m

-> Proxy w

Writer type

-> (forall u. Eq u => t -> m u -> m u -> Bool)

Equality test

-> (w -> m ())

tell

-> TestTree

tell mempty === return ()

testWriterMonadLawTellMappend

Arguments

:: (Monoid w, Monad m, Show t, Show w, Arbitrary t, Arbitrary w)

=> Proxy m

Type constructor under test

-> Proxy t

Equality context for m

-> Proxy w

Writer type

-> (forall u. Eq u => t -> m u -> m u -> Bool)

Equality test

-> (w -> m ())

tell

-> TestTree

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

testWriterMonadLawDraftReturn

Arguments

:: (Monoid w, Monad m, Eq w, Eq a, Show t, Show a, Arbitrary t, Arbitrary a)

=> Proxy m

Type constructor under test

-> Proxy t

Equality context for m

-> Proxy w

Writer type

-> Proxy a

Value type

-> (forall u. Eq u => t -> m u -> m u -> Bool)

Equality test

-> (forall u. m u -> m (u, w))

draft

-> TestTree

draft (return a) === return (a, mempty)

testWriterMonadLawDraftBind

Arguments

:: (Monoid w, Monad m, Eq w, Eq b, Show t, Show (m a), Arbitrary t, Arbitrary (m a), Arbitrary (m b), CoArbitrary a)

=> Proxy m

Type constructor under test

-> Proxy t

Equality context for m

-> Proxy w

Writer type

-> Proxy a

Value type

-> Proxy b

Value type

-> (forall u. Eq u => t -> m u -> m u -> Bool)

Equality test

-> (forall u. m u -> m (u, w))

draft

-> TestTree

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

Alternate Primitives

testWriterMonadEquivalences

Arguments

:: (Monoid w, Monad m, Eq w, Eq a, Show t, Show (m a), Show (m (a, w -> w)), Arbitrary t, Arbitrary (m a), Arbitrary (m (a, w -> w)), Typeable m, Typeable w, Typeable a)

=> Proxy m

Type constructor under test

-> Proxy t

Equality context for m

-> Proxy w

Writer monad

-> Proxy a

Value type

-> (forall u. Eq u => t -> m u -> m u -> Bool)

Equality test

-> (w -> m ())

tell

-> (forall u. m u -> m (u, w))

draft

-> (forall u. m u -> m (u, w))

listen

-> (forall u. m (u, w -> w) -> m u)

pass

-> TestTree

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)

testWriterMonadEquivalenceListen

Arguments

:: (Monad m, Eq w, Eq a, Show t, Show (m a), Arbitrary t, Arbitrary (m a))

=> Proxy m

Type constructor under test

-> Proxy t

Equality context for m

-> Proxy w

Writer monad

-> Proxy a

Value type

-> (forall u. Eq u => t -> m u -> m u -> Bool)

Equality test

-> (w -> m ())

tell

-> (forall u. m u -> m (u, w))

draft

-> (forall u. m u -> m (u, w))

listen

-> TestTree

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

testWriterMonadEquivalencePass

Arguments

:: (Monad m, Eq w, Eq a, Show t, Show (m (a, w -> w)), Arbitrary t, Arbitrary (m (a, w -> w)))

=> Proxy m

Type constructor under test

-> Proxy t

Equality context for m

-> Proxy w

Writer type

-> Proxy a

Value type

-> (forall u. Eq u => t -> m u -> m u -> Bool)

Equality test

-> (w -> m ())

tell

-> (forall u. m u -> m (u, w))

draft

-> (forall u. m (a, w -> w) -> m a)

pass

-> TestTree

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

testWriterMonadEquivalenceDraft

Arguments

:: (Monoid w, Monad m, Eq w, Eq a, Show t, Show (m a), Arbitrary t, Arbitrary (m a))

=> Proxy m

Type constructor under test

-> Proxy t

Equality context for m

-> Proxy w

Writer type

-> Proxy a

Value type

-> (forall u. Eq u => t -> m u -> m u -> Bool)

Equality test

-> (forall u. m u -> m (u, w))

draft

-> (forall u. m u -> m (u, w))

listen

-> (forall u. m (u, w -> w) -> m u)

pass

-> TestTree

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