tasty-quickcheck-laws-0.0.1: Pre-built tasty trees for checking lawful class properties using QuickCheck

Copyright2018 Automattic Inc.
LicenseGPL-3
MaintainerNathan Bloomfield (nbloomf@gmail.com)
Stabilityexperimental
PortabilityPOSIX
Safe HaskellNone
LanguageHaskell2010

Test.Tasty.QuickCheck.Laws.WriterMonad

Contents

Description

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.

Synopsis

Documentation

testWriterMonadLaws Source #

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 Source #

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 Source #

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 Source #

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 Source #

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

testWriterMonadLawDraftBind Source #

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 Source #

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 Source #

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 Source #

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 Source #

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