diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,7 @@ +Changelog for tasty-quickcheck-laws +=================================== + +0.0.1 +----- + +* Initial Release diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,29 @@ +BSD 3-Clause License + +Copyright (c) 2018, Nathan Bloomfield +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + +* Redistributions of source code must retain the above copyright notice, this + list of conditions and the following disclaimer. + +* Redistributions in binary form must reproduce the above copyright notice, + this list of conditions and the following disclaimer in the documentation + and/or other materials provided with the distribution. + +* Neither the name of the copyright holder nor the names of its + contributors may be used to endorse or promote products derived from + this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" +AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE +IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE +DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE +FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL +DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR +SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER +CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, +OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,18 @@ +tasty-quickcheck-laws +===================== + +[![Build Status](https://travis-ci.org/nbloomf/tasty-quickcheck-laws.svg?branch=master)](https://travis-ci.org/nbloomf/tasty-quickcheck-laws) + +Pre-built [tasty](http://hackage.haskell.org/package/tasty) trees for checking your lawful class instances with QuickCheck. + +Currently includes laws for the following type classes: + +* Eq +* Monoid +* Functor +* Applicative +* Monad +* State Monad +* Reader Monad +* Writer Monad +* Error Monad diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/app/Main.hs b/app/Main.hs new file mode 100644 --- /dev/null +++ b/app/Main.hs @@ -0,0 +1,4 @@ +module Main where + +main :: IO () +main = return () diff --git a/src/Test/Tasty/QuickCheck/Laws.hs b/src/Test/Tasty/QuickCheck/Laws.hs new file mode 100644 --- /dev/null +++ b/src/Test/Tasty/QuickCheck/Laws.hs @@ -0,0 +1,33 @@ +{- | +Module : Test.Tasty.QuickCheck.Laws +Description : Prefab tasty trees of quickcheck properties for lawful type classes +Copyright : 2018, Automattic, Inc. +License : GPL-3 +Maintainer : Nathan Bloomfield (nbloomf@gmail.com) +Stability : experimental +Portability : POSIX +-} + +module Test.Tasty.QuickCheck.Laws ( + module Test.Tasty.QuickCheck.Laws.Applicative + , module Test.Tasty.QuickCheck.Laws.Class + , module Test.Tasty.QuickCheck.Laws.Eq + , module Test.Tasty.QuickCheck.Laws.ErrorMonad + , module Test.Tasty.QuickCheck.Laws.Functor + , module Test.Tasty.QuickCheck.Laws.Monad + , module Test.Tasty.QuickCheck.Laws.Monoid + , module Test.Tasty.QuickCheck.Laws.ReaderMonad + , module Test.Tasty.QuickCheck.Laws.StateMonad + , module Test.Tasty.QuickCheck.Laws.WriterMonad +) where + +import Test.Tasty.QuickCheck.Laws.Applicative +import Test.Tasty.QuickCheck.Laws.Class +import Test.Tasty.QuickCheck.Laws.Eq +import Test.Tasty.QuickCheck.Laws.ErrorMonad +import Test.Tasty.QuickCheck.Laws.Functor +import Test.Tasty.QuickCheck.Laws.Monad +import Test.Tasty.QuickCheck.Laws.Monoid +import Test.Tasty.QuickCheck.Laws.ReaderMonad +import Test.Tasty.QuickCheck.Laws.StateMonad +import Test.Tasty.QuickCheck.Laws.WriterMonad diff --git a/src/Test/Tasty/QuickCheck/Laws/Applicative.hs b/src/Test/Tasty/QuickCheck/Laws/Applicative.hs new file mode 100644 --- /dev/null +++ b/src/Test/Tasty/QuickCheck/Laws/Applicative.hs @@ -0,0 +1,302 @@ +{- | +Module : Test.Tasty.QuickCheck.Laws.Applicative +Description : Prefab tasty trees of quickcheck properties for the Applicative laws +Copyright : 2018, Automattic, Inc. +License : GPL-3 +Maintainer : Nathan Bloomfield (nbloomf@gmail.com) +Stability : experimental +Portability : POSIX + +Prebuilt tasty test trees for the @Applicative@ functor laws. To get started, look at @testApplicativeLaws@. +-} + + + +{-# LANGUAGE Rank2Types #-} +module Test.Tasty.QuickCheck.Laws.Applicative ( + testApplicativeLaws + + -- * Applicative Laws + , testApplicativeLawIdentity + , testApplicativeLawHomomorphism + , testApplicativeLawInterchange + , testApplicativeLawComposite + + -- * Test Trees + , testApplicativeLaws1 + , testApplicativeLaws2 + , testApplicativeLaws3 +) where + + + +import Data.Proxy + ( Proxy(..) ) +import Data.Typeable + ( Typeable, typeRep ) +import Test.Tasty + ( TestTree, testGroup ) +import Test.Tasty.QuickCheck + ( testProperty, Property, Arbitrary(..), CoArbitrary(..) ) +import Text.Show.Functions + () + +import Test.Tasty.QuickCheck.Laws.Class + + + +-- | Constructs a @TestTree@ checking that the four @Applicative@ class laws hold for @f@ with value types @a@, @b@, and @c@, using a given equality test for values of type @forall u. f u@. The equality context type @t@ is for constructors @f@ from which we can only extract a value within a context, such as reader-like constructors. +testApplicativeLaws + :: ( Applicative f + , Eq a, Eq b, Eq c + , Show a, Show t + , Show (f a), Show (f (a -> b)), Show (f (b -> c)) + , Arbitrary a, Arbitrary b, Arbitrary t + , Arbitrary (f a), Arbitrary (f (a -> b)), Arbitrary (f (b -> c)) + , CoArbitrary a + , Typeable f, Typeable a, Typeable b, Typeable c + ) + => Proxy f -- ^ Type constructor under test + -> Proxy t -- ^ Equality context for @f@ + -> Proxy a -- ^ Value type + -> Proxy b -- ^ Value type + -> Proxy c -- ^ Value type + -> (forall u. (Eq u) => t -> f u -> f u -> Bool) -- ^ Equality test + -> TestTree +testApplicativeLaws pf pt pa pb pc eq = + let + label = "Applicative Laws for " ++ (show $ typeRep pf) ++ " with " ++ + "a :: " ++ (show $ typeRep pa) ++ ", " ++ + "b :: " ++ (show $ typeRep pb) ++ ", " ++ + "c :: " ++ (show $ typeRep pc) + in + testGroup label + [ testApplicativeLawIdentity pf pt pa eq + , testApplicativeLawHomomorphism pf pt pa pb eq + , testApplicativeLawInterchange pf pt pa pb eq + , testApplicativeLawComposite pf pt pa pb pc eq + ] + + + +-- | @pure id \<*> x === x@ +testApplicativeLawIdentity + :: ( Applicative f + , Eq a + , Show (f a), Show t + , Arbitrary (f a), Arbitrary t + ) + => Proxy f -- ^ Type constructor under test + -> Proxy t -- ^ Equality context for @f@ + -> Proxy a -- ^ Value type + -> (forall u. (Eq u) => t -> f u -> f u -> Bool) -- ^ Equality test + -> TestTree +testApplicativeLawIdentity pf pt pa eq = + testProperty "pure id <*> x === x" $ + applicativeLawIdentity pf pt pa eq + +applicativeLawIdentity + :: (Applicative f, Eq a) + => Proxy f -> Proxy t -> Proxy a + -> (forall u. (Eq u) => t -> f u -> f u -> Bool) -- ^ Equality test + -> t -> f a -> Bool +applicativeLawIdentity _ _ _ eq t x = + (eq t) (pure id <*> x) x + + + +-- | @pure f \<*> pure a === pure (f a)@ +testApplicativeLawHomomorphism + :: ( Applicative f + , Eq b + , Show a, Show t + , Arbitrary a, Arbitrary b, Arbitrary t + , CoArbitrary a + ) + => Proxy f -- ^ Type constructor under test + -> Proxy t -- ^ Equality context for @f@ + -> Proxy a -- ^ Value type + -> Proxy b -- ^ Value type + -> (forall u. (Eq u) => t -> f u -> f u -> Bool) -- ^ Equality test + -> TestTree +testApplicativeLawHomomorphism pf pt pa pb eq = + testProperty "pure f <*> pure a === pure (f a)" $ + applicativeLawHomomorphism pf pt pa pb eq + +applicativeLawHomomorphism + :: (Applicative f, Eq b) + => Proxy f -> Proxy t -> Proxy a -> Proxy b + -> (forall u. (Eq u) => t -> f u -> f u -> Bool) -- ^ Equality test + -> t -> (a -> b) -> a -> Bool +applicativeLawHomomorphism _ _ _ _ eq t f a = + (eq t) (pure f <*> pure a) (pure (f a)) + + + +-- | @x \<*> pure a === pure ($ a) \<*> x@ +testApplicativeLawInterchange + :: ( Applicative f + , Eq b + , Show a, Show t + , Show (f (a -> b)) + , Arbitrary a, Arbitrary t + , Arbitrary (f (a -> b)) + ) + => Proxy f -- ^ Type constructor under test + -> Proxy t -- ^ Equality context for @f@ + -> Proxy a -- ^ Value type + -> Proxy b -- ^ Value type + -> (forall u. (Eq u) => t -> f u -> f u -> Bool) -- ^ Equality test + -> TestTree +testApplicativeLawInterchange pf pt pa pb eq = + testProperty "x <*> pure a === pure ($ a) <*> x" $ + applicativeLawInterchange pf pt pa pb eq + +applicativeLawInterchange + :: (Applicative f, Eq b) + => Proxy f -> Proxy t -> Proxy a -> Proxy b + -> (forall u. (Eq u) => t -> f u -> f u -> Bool) -- ^ Equality test + -> t -> f (a -> b) -> a -> Bool +applicativeLawInterchange _ _ _ _ eq t x a = + (eq t) (x <*> pure a) (pure ($ a) <*> x) + + + +-- | @pure (.) \<*> x \<*> y \<*> z = x \<*> (y \<*> z)@ +testApplicativeLawComposite + :: ( Applicative f + , Eq c + , Show t, Show (f a), Show (f (b -> c)), Show (f (a -> b)) + , Arbitrary t, Arbitrary (f a), Arbitrary (f (b -> c)), Arbitrary (f (a -> b)) + ) + => Proxy f -- ^ Type constructor under test + -> Proxy t -- ^ Equality context for @f@ + -> Proxy a -- ^ Value type + -> Proxy b -- ^ Value type + -> Proxy c -- ^ Value type + -> (forall u. (Eq u) => t -> f u -> f u -> Bool) -- ^ Equality test + -> TestTree +testApplicativeLawComposite pf pt pa pb pc eq = + testProperty "pure (.) <*> x <*> y <*> z = x <*> (y <*> z)" $ + applicativeLawComposite pf pt pa pb pc eq + +applicativeLawComposite + :: (Applicative f, Eq c) + => Proxy f -> Proxy t -> Proxy a -> Proxy b -> Proxy c + -> (forall u. (Eq u) => t -> f u -> f u -> Bool) + -> t -> f (b -> c) -> f (a -> b) -> f a -> Bool +applicativeLawComposite _ _ _ _ _ eq t x y z = + (eq t) (pure (.) <*> x <*> y <*> z) (x <*> (y <*> z)) + + + + + +-- | All possible value type selections for @testApplicativeLaws@ from one choice +testApplicativeLaws1 + :: ( Applicative f + , Checkable a + , Show (f a), Show t + , Show (f (a -> a)) + , Arbitrary (f a), Arbitrary t + , Arbitrary (f (a -> a)) + , Typeable f + ) + => Proxy f -- ^ Type constructor under test + -> Proxy t -- ^ Equality context type for @f@ + -> Proxy a -- ^ Value type + -> (forall u. (Eq u) => t -> f u -> f u -> Bool) -- ^ Equality test + -> TestTree +testApplicativeLaws1 pf pt pa eq = + let label = "Applicative Laws for " ++ (show $ typeRep pf) in + testGroup label + [ testApplicativeLaws pf pt pa pa pa eq + ] + + + +-- | All possible value type selections for @testApplicativeLaws@ from two choices +testApplicativeLaws2 + :: ( Applicative f + , Checkable a, Checkable b + , Show (f a), Show (f b), Show t + , Show (f (a -> a)), Show (f (a -> b)) + , Show (f (b -> a)), Show (f (b -> b)) + , Arbitrary (f a), Arbitrary (f b), Arbitrary t + , Arbitrary (f (a -> a)), Arbitrary (f (a -> b)) + , Arbitrary (f (b -> a)), Arbitrary (f (b -> b)) + , Typeable f + ) + => Proxy f -- ^ Type constructor under test + -> Proxy t -- ^ Equality context for @f@ + -> Proxy a -- ^ Value type + -> Proxy b -- ^ Value type + -> (forall u. (Eq u) => t -> f u -> f u -> Bool) -- ^ Equality test + -> TestTree +testApplicativeLaws2 pf pt pa pb eq = + let label = "Applicative Laws for " ++ (show $ typeRep pf) in + testGroup label + [ testApplicativeLaws pf pt pa pa pa eq + , testApplicativeLaws pf pt pa pa pb eq + , testApplicativeLaws pf pt pa pb pa eq + , testApplicativeLaws pf pt pa pb pb eq + , testApplicativeLaws pf pt pb pa pa eq + , testApplicativeLaws pf pt pb pa pb eq + , testApplicativeLaws pf pt pb pb pa eq + , testApplicativeLaws pf pt pb pb pb eq + ] + + + +-- | All possible value type selections for @testApplicativeLaws@ from three choices +testApplicativeLaws3 + :: ( Applicative f + , Checkable a, Checkable b, Checkable c + , Show (f a), Show (f b), Show (f c), Show t + , Show (f (a -> a)), Show (f (a -> b)), Show (f (a -> c)) + , Show (f (b -> a)), Show (f (b -> b)), Show (f (b -> c)) + , Show (f (c -> a)), Show (f (c -> b)), Show (f (c -> c)) + , Arbitrary (f a), Arbitrary (f b), Arbitrary (f c), Arbitrary t + , Arbitrary (f (a -> a)), Arbitrary (f (a -> b)), Arbitrary (f (a -> c)) + , Arbitrary (f (b -> a)), Arbitrary (f (b -> b)), Arbitrary (f (b -> c)) + , Arbitrary (f (c -> a)), Arbitrary (f (c -> b)), Arbitrary (f (c -> c)) + , Typeable f + ) + => Proxy f -- ^ Type constructor under test + -> Proxy t -- ^ Equality context for @f@ + -> Proxy a -- ^ Value type + -> Proxy b -- ^ Value type + -> Proxy c -- ^ Value type + -> (forall u. (Eq u) => t -> f u -> f u -> Bool) -- ^ Equality test + -> TestTree +testApplicativeLaws3 pf pt pa pb pc eq = + let label = "Applicative Laws for " ++ (show $ typeRep pf) in + testGroup label + [ testApplicativeLaws pf pt pa pa pa eq + , testApplicativeLaws pf pt pa pa pb eq + , testApplicativeLaws pf pt pa pa pc eq + , testApplicativeLaws pf pt pa pb pa eq + , testApplicativeLaws pf pt pa pb pb eq + , testApplicativeLaws pf pt pa pb pc eq + , testApplicativeLaws pf pt pa pc pa eq + , testApplicativeLaws pf pt pa pc pb eq + , testApplicativeLaws pf pt pa pc pc eq + , testApplicativeLaws pf pt pb pa pa eq + , testApplicativeLaws pf pt pb pa pb eq + , testApplicativeLaws pf pt pb pa pc eq + , testApplicativeLaws pf pt pb pb pa eq + , testApplicativeLaws pf pt pb pb pb eq + , testApplicativeLaws pf pt pb pb pc eq + , testApplicativeLaws pf pt pb pc pa eq + , testApplicativeLaws pf pt pb pc pb eq + , testApplicativeLaws pf pt pb pc pc eq + , testApplicativeLaws pf pt pc pa pa eq + , testApplicativeLaws pf pt pc pa pb eq + , testApplicativeLaws pf pt pc pa pc eq + , testApplicativeLaws pf pt pc pb pa eq + , testApplicativeLaws pf pt pc pb pb eq + , testApplicativeLaws pf pt pc pb pc eq + , testApplicativeLaws pf pt pc pc pa eq + , testApplicativeLaws pf pt pc pc pb eq + , testApplicativeLaws pf pt pc pc pc eq + ] diff --git a/src/Test/Tasty/QuickCheck/Laws/Class.hs b/src/Test/Tasty/QuickCheck/Laws/Class.hs new file mode 100644 --- /dev/null +++ b/src/Test/Tasty/QuickCheck/Laws/Class.hs @@ -0,0 +1,38 @@ +{- | +Module : Test.Tasty.QuickCheck.Laws.Class +Description : Convenience typeclass +Copyright : 2018, Automattic, Inc. +License : GPL-3 +Maintainer : Nathan Bloomfield (nbloomf@gmail.com) +Stability : experimental +Portability : POSIX + +Convenience typeclass for type signatures. +-} + +module Test.Tasty.QuickCheck.Laws.Class ( + Checkable +) where + +import Data.Typeable + ( Typeable ) +import Test.QuickCheck + ( Arbitrary, CoArbitrary ) + +-- | Alias for convenience. +class (Eq a, Show a, Arbitrary a, CoArbitrary a, Typeable a) => Checkable a + +instance Checkable () +instance Checkable Bool +instance Checkable Int +instance Checkable Integer +instance Checkable Double +instance Checkable Char + +instance (Checkable a) => Checkable [a] +instance (Checkable a) => Checkable (Maybe a) + +instance (Checkable a, Checkable b) => Checkable (a,b) +instance (Checkable a, Checkable b) => Checkable (Either a b) + +instance (Checkable a, Checkable b, Checkable c) => Checkable (a,b,c) diff --git a/src/Test/Tasty/QuickCheck/Laws/Eq.hs b/src/Test/Tasty/QuickCheck/Laws/Eq.hs new file mode 100644 --- /dev/null +++ b/src/Test/Tasty/QuickCheck/Laws/Eq.hs @@ -0,0 +1,100 @@ +{- | +Module : Test.Tasty.QuickCheck.Laws.Eq +Description : Prefab tasty trees of quickcheck properties for the Eq laws +Copyright : 2018, Automattic, Inc. +License : GPL-3 +Maintainer : Nathan Bloomfield (nbloomf@gmail.com) +Stability : experimental +Portability : POSIX +-} + + + +module Test.Tasty.QuickCheck.Laws.Eq ( + testEqLaws + + -- * Eq Laws + , testEqLawReflexive + , testEqLawSymmetric + , testEqLawTransitive +) where + +import Data.Proxy + ( Proxy(..) ) +import Data.Typeable + ( Typeable, typeRep ) +import Test.Tasty + ( TestTree, testGroup ) +import Test.Tasty.QuickCheck + ( testProperty, Property, Arbitrary(..) ) + +import Test.Tasty.QuickCheck.Laws.Class + + + +-- | Constructs a @TestTree@ checking that the @Eq@ class laws hold for @a@. +testEqLaws + :: (Eq a, Show a, Arbitrary a, Typeable a) + => Proxy a + -> TestTree +testEqLaws pa = + let label = "Eq Laws for " ++ (show $ typeRep pa) in + testGroup label + [ testEqLawReflexive pa + , testEqLawSymmetric pa + , testEqLawTransitive pa + ] + + + +-- | @a == a@ +testEqLawReflexive + :: (Eq a, Show a, Arbitrary a) + => Proxy a + -> TestTree +testEqLawReflexive pa = + testProperty "a == a" $ + eqLawReflexive pa + +eqLawReflexive + :: (Eq a) + => Proxy a + -> a -> Bool +eqLawReflexive _ a = + a == a + + + +-- | @(a == b) == (b == a)@ +testEqLawSymmetric + :: (Eq a, Show a, Arbitrary a) + => Proxy a + -> TestTree +testEqLawSymmetric pa = + testProperty "(a == b) == (b == a)" $ + eqLawSymmetric pa + +eqLawSymmetric + :: (Eq a) + => Proxy a + -> a -> a -> Bool +eqLawSymmetric _ a b = + (a == b) == (b == a) + + + +-- | @if (a == b) && (b == c) then (a == c)@ +testEqLawTransitive + :: (Eq a, Show a, Arbitrary a) + => Proxy a + -> TestTree +testEqLawTransitive pa = + testProperty "if (a == b) && (b == c) then (a == c)" $ + eqLawTransitive pa + +eqLawTransitive + :: (Eq a) + => Proxy a + -> a -> a -> a -> Bool +eqLawTransitive _ a b c = + if (a == b) && (b == c) then a == c else True diff --git a/src/Test/Tasty/QuickCheck/Laws/ErrorMonad.hs b/src/Test/Tasty/QuickCheck/Laws/ErrorMonad.hs new file mode 100644 --- /dev/null +++ b/src/Test/Tasty/QuickCheck/Laws/ErrorMonad.hs @@ -0,0 +1,202 @@ +{- | +Module : Test.Tasty.QuickCheck.Laws.ErrorMonad +Description : Prefab tasty trees of quickcheck properties for error monad laws +Copyright : 2018, Automattic, Inc. +License : GPL-3 +Maintainer : Nathan Bloomfield (nbloomf@gmail.com) +Stability : experimental +Portability : POSIX +-} + + + +{-# LANGUAGE Rank2Types, ScopedTypeVariables #-} +module Test.Tasty.QuickCheck.Laws.ErrorMonad ( + testErrorMonadLaws + + -- * Error Monad Laws + , testErrorMonadLawCatchReturn + , testErrorMonadLawCatchThrow + , testErrorMonadLawCatchThrowThrow + , testErrorMonadLawThrowBind +) where + + + +import Data.Proxy + ( Proxy(..) ) +import Data.Typeable + ( Typeable, typeRep ) +import Test.Tasty + ( TestTree, testGroup ) +import Test.Tasty.QuickCheck + ( testProperty, Property, Arbitrary(..), CoArbitrary(..) ) +import Text.Show.Functions + () + +import Test.Tasty.QuickCheck.Laws.Class + + + +-- | Constructs a @TestTree@ checking that the error monad laws hold for @m@ with error type @e@ 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. +testErrorMonadLaws + :: ( Monad m + , Eq a, Eq b + , Show t, Show e, Show a + , Arbitrary t, Arbitrary e, Arbitrary a + , Arbitrary (m a), Arbitrary (m b) + , CoArbitrary e, CoArbitrary a + , Typeable m, Typeable e, Typeable a, Typeable b + ) + => Proxy m -- ^ Type constructor under test + -> Proxy t -- ^ Equality context for @m@ + -> Proxy e -- ^ Error type + -> Proxy a -- ^ Value type + -> Proxy b -- ^ Value type + -> (forall u. (Eq u) => t -> m u -> m u -> Bool) -- ^ Equality test + -> (forall u. e -> m u) -- ^ @throw@ + -> (m a -> (e -> m a) -> m a) -- ^ @catch@ + -> TestTree +testErrorMonadLaws pm pt pe pa pb eq throw catch = + let + label = "Error Monad Laws for " ++ (show $ typeRep pm) ++ " with " ++ + "e :: " ++ (show $ typeRep pe) ++ ", " ++ + "a :: " ++ (show $ typeRep pa) ++ ", " ++ + "b :: " ++ (show $ typeRep pb) + in + testGroup label + [ testErrorMonadLawCatchReturn pm pt pe pa eq catch + , testErrorMonadLawCatchThrow pm pt pe pa eq throw catch + , testErrorMonadLawCatchThrowThrow pm pt pe pa eq throw catch + , testErrorMonadLawThrowBind pm pt pe pa pb eq throw + ] + + + +-- | @catch (return a) h === return a@ +testErrorMonadLawCatchReturn + :: ( Monad m + , Eq a + , Show t, Show a + , Arbitrary t, Arbitrary a + , Arbitrary (m a) + , CoArbitrary e + ) + => Proxy m -- ^ Type constructor under test + -> Proxy t -- ^ Equality context for @m@ + -> Proxy e -- ^ Error type + -> Proxy a -- ^ Value type + -> (forall u. (Eq u) => t -> m u -> m u -> Bool) -- ^ Equality test + -> (m a -> (e -> m a) -> m a) -- ^ @catch@ + -> TestTree +testErrorMonadLawCatchReturn pm pt pe pa eq catch = + testProperty "catch (return a) h === return a" $ + errorMonadLawCatchReturn pm pt pe pa eq catch + +errorMonadLawCatchReturn + :: (Monad m, Eq a) + => Proxy m -- ^ Type constructor under test + -> Proxy t -- ^ Equality context for @m@ + -> Proxy e -- ^ Error type + -> Proxy a -- ^ Value type + -> (forall u. (Eq u) => t -> m u -> m u -> Bool) -- ^ Equality test + -> (m a -> (e -> m a) -> m a) -- ^ @catch@ + -> t -> a -> (e -> m a) -> Bool +errorMonadLawCatchReturn _ _ _ _ eq catch t a h = + (eq t) (catch (return a) h) (return a) + + + +-- | @catch (throw e) h === h e@ +testErrorMonadLawCatchThrow + :: ( Monad m + , Eq a + , Show t, Show e + , Arbitrary t, Arbitrary e + , Arbitrary (m a) + , CoArbitrary e + ) + => Proxy m -- ^ Type constructor under test + -> Proxy t -- ^ Equality context for @m@ + -> Proxy e -- ^ Error type + -> Proxy a -- ^ Value type + -> (forall u. (Eq u) => t -> m u -> m u -> Bool) -- ^ Equality test + -> (forall u. e -> m u) -- ^ @throw@ + -> (m a -> (e -> m a) -> m a) -- ^ @catch@ + -> TestTree +testErrorMonadLawCatchThrow pm pt pe pa eq throw catch = + testProperty "catch (throw e) h === h e" $ + errorMonadLawCatchThrow pm pt pe pa eq throw catch + +errorMonadLawCatchThrow + :: (Monad m, Eq a) + => Proxy m -> Proxy t -> Proxy e -> Proxy a + -> (forall u. (Eq u) => t -> m u -> m u -> Bool) -- ^ Equality test + -> (forall u. e -> m u) -- ^ @throw@ + -> (m a -> (e -> m a) -> m a) -- ^ @catch@ + -> t -> e -> (e -> m a) -> Bool +errorMonadLawCatchThrow _ _ _ _ eq throw catch t e h = + (eq t) (catch (throw e) h) (h e) + + + +-- | @catch (throw e) throw === throw e@ +testErrorMonadLawCatchThrowThrow + :: ( Monad m + , Eq a + , Show t, Show e + , Arbitrary t, Arbitrary e + ) + => Proxy m -- ^ Type constructor under test + -> Proxy t -- ^ Equality context for @m@ + -> Proxy e -- ^ Error type + -> Proxy a -- ^ Value type + -> (forall u. (Eq u) => t -> m u -> m u -> Bool) -- ^ Equality test + -> (forall u. e -> m u) -- ^ @throw@ + -> (m a -> (e -> m a) -> m a) -- ^ @catch@ + -> TestTree +testErrorMonadLawCatchThrowThrow pm pt pe pa eq throw catch = + testProperty "catch (throw e) throw === throw e" $ + errorMonadLawCatchThrowThrow pm pt pe pa eq throw catch + +errorMonadLawCatchThrowThrow + :: (Monad m, Eq a) + => Proxy m -> Proxy t -> Proxy e -> Proxy a + -> (forall u. (Eq u) => t -> m u -> m u -> Bool) -- ^ Equality test + -> (forall u. e -> m u) -- ^ @throw@ + -> (m a -> (e -> m a) -> m a) -- ^ @catch@ + -> t -> e -> Bool +errorMonadLawCatchThrowThrow _ _ _ _ eq throw catch t e = + (eq t) (catch (throw e) throw) (throw e) + + + +-- | @throw e >>= f === throw e@ +testErrorMonadLawThrowBind + :: ( Monad m + , Eq b + , Show t, Show e + , Arbitrary t, Arbitrary e + , Arbitrary (m b) + , CoArbitrary a + ) + => Proxy m -- ^ Type constructor under test + -> Proxy t -- ^ Equality context for @m@ + -> Proxy e -- ^ Error type + -> Proxy a -- ^ Value type + -> Proxy b -- ^ Value type + -> (forall u. (Eq u) => t -> m u -> m u -> Bool) -- ^ Equality test + -> (forall u. e -> m u) -- ^ @throw@ + -> TestTree +testErrorMonadLawThrowBind pm pt pe pa pb eq throw = + testProperty "throw e >>= f === throw e" $ + errorMonadLawThrowBind pm pt pe pa pb eq throw + +errorMonadLawThrowBind + :: (Monad m, Eq b) + => Proxy m -> Proxy t -> Proxy e -> Proxy a -> Proxy b + -> (forall u. (Eq u) => t -> m u -> m u -> Bool) -- ^ Equality test + -> (forall u. e -> m u) -- ^ throw + -> t -> e -> (a -> m b) -> Bool +errorMonadLawThrowBind _ _ _ _ _ eq throw t e f = + (eq t) (throw e >>= f) (throw e) diff --git a/src/Test/Tasty/QuickCheck/Laws/Functor.hs b/src/Test/Tasty/QuickCheck/Laws/Functor.hs new file mode 100644 --- /dev/null +++ b/src/Test/Tasty/QuickCheck/Laws/Functor.hs @@ -0,0 +1,226 @@ +{- | +Module : Test.Tasty.QuickCheck.Laws.Functor +Description : Prefab tasty trees of quickcheck properties for the Functor laws +Copyright : 2018, Automattic, Inc. +License : GPL-3 +Maintainer : Nathan Bloomfield (nbloomf@gmail.com) +Stability : experimental +Portability : POSIX +-} + + + +{-# LANGUAGE Rank2Types #-} +module Test.Tasty.QuickCheck.Laws.Functor ( + testFunctorLaws + + -- * Functor Laws + , testFunctorLawIdentity + , testFunctorLawComposite + + -- * Test Trees + , testFunctorLaws1 + , testFunctorLaws2 + , testFunctorLaws3 +) where + +import Data.Proxy + ( Proxy(..) ) +import Data.Typeable + ( Typeable, typeRep ) +import Test.Tasty + ( TestTree, testGroup ) +import Test.Tasty.QuickCheck + ( testProperty, Property, Arbitrary(..), CoArbitrary(..) ) +import Text.Show.Functions + () + +import Test.Tasty.QuickCheck.Laws.Class + + + +-- | Constructs a @TestTree@ checking that the functor laws hold for @f@ with value types @a@, @b@, and @c@, using a given equality test for values of type @forall u. f u@. The equality context type @t@ is for constructors @f@ from which we can only extract a value within a context, such as reader-like constructors. +testFunctorLaws + :: ( Functor f + , Eq a, Eq c + , Show t, Show (f a) + , Arbitrary t, Arbitrary b, Arbitrary c + , Arbitrary (f a) + , CoArbitrary a, CoArbitrary b + , Typeable f, Typeable a, Typeable b, Typeable c + ) + => Proxy f -- ^ Type constructor under test + -> Proxy t -- ^ Equality context for @f@ + -> Proxy a -- ^ Value type + -> Proxy b -- ^ Value type + -> Proxy c -- ^ Value type + -> (forall u. (Eq u) => t -> f u -> f u -> Bool) -- ^ Equality test + -> TestTree +testFunctorLaws pf pt pa pb pc eq = + let + label = "Functor Laws for " ++ (show $ typeRep pf) ++ " with " ++ + "a :: " ++ (show $ typeRep pa) ++ ", " ++ + "b :: " ++ (show $ typeRep pb) ++ ", " ++ + "c :: " ++ (show $ typeRep pc) + in + testGroup label + [ testFunctorLawIdentity pf pt pa eq + , testFunctorLawComposite pf pt pa pb pc eq + ] + + + +-- | @fmap id x === x@ +testFunctorLawIdentity + :: ( Functor f + , Eq a + , Show t, Show (f a) + , Arbitrary t, Arbitrary (f a) + ) + => Proxy f -- ^ Type constructor under test + -> Proxy t -- ^ Equality context for @f@ + -> Proxy a -- ^ Value type + -> (forall u. (Eq u) => t -> f u -> f u -> Bool) -- ^ Equality test + -> TestTree +testFunctorLawIdentity pf pt pa eq = + testProperty "fmap id x === x" $ + functorLawIdentity pf pt pa eq + +functorLawIdentity + :: (Functor f, Eq a) + => Proxy f -> Proxy t -> Proxy a + -> (forall u. (Eq u) => t -> f u -> f u -> Bool) -- ^ Equality test + -> t -> f a -> Bool +functorLawIdentity _ _ _ eq t x = + (eq t) (fmap id x) x + + + +-- | @fmap (f . g) x === (fmap f . fmap g) x@ +testFunctorLawComposite + :: ( Functor f + , Eq c + , Show t, Show (f a) + , Arbitrary t, Arbitrary b, Arbitrary c + , Arbitrary (f a) + , CoArbitrary a, CoArbitrary b + ) + => Proxy f -- ^ Type constructor under test + -> Proxy t -- ^ Equality context for @f@ + -> Proxy a -- ^ Value type + -> Proxy b -- ^ Value type + -> Proxy c -- ^ Value type + -> (forall u. (Eq u) => t -> f u -> f u -> Bool) -- ^ Equality test + -> TestTree +testFunctorLawComposite pf pt pa pb pc eq = + testProperty "fmap (f . g) x === (fmap f . fmap g) x" $ + functorLawComposite pf pt pa pb pc eq + +functorLawComposite + :: (Functor f, Eq c) + => Proxy f -> Proxy t -> Proxy a -> Proxy b -> Proxy c + -> (forall u. (Eq u) => t -> f u -> f u -> Bool) + -> t -> (f a) -> (b -> c) -> (a -> b) -> Bool +functorLawComposite _ _ _ _ _ eq t x f g = + (eq t) (fmap (f . g) x) ((fmap f . fmap g) x) + + + + + +-- | All possible value type selections for @testFunctorLaws@ from one choice +testFunctorLaws1 + :: ( Functor f + , Checkable a + , Show t, Show (f a) + , Arbitrary t, Arbitrary (f a) + , Typeable f + ) + => Proxy f -- ^ Type constructor under test + -> Proxy t -- ^ Equality context for @f@ + -> Proxy a -- ^ Value type + -> (forall u. (Eq u) => t -> f u -> f u -> Bool) -- ^ Equality test + -> TestTree +testFunctorLaws1 pf pt pa eq = + let label = "Functor Laws for " ++ (show $ typeRep pf) in + testGroup label + [ testFunctorLaws pf pt pa pa pa eq + ] + + + +-- | All possible value type selections for @testFunctorLaws@ from two choices +testFunctorLaws2 + :: ( Functor f + , Checkable a, Checkable b + , Show t, Show (f a), Show (f b) + , Arbitrary t, Arbitrary (f a), Arbitrary (f b) + , Typeable f + ) + => Proxy f -- ^ Type constructor under test + -> Proxy t -- ^ Equality context for @f@ + -> Proxy a -- ^ Value type + -> Proxy b -- ^ Value type + -> (forall u. (Eq u) => t -> f u -> f u -> Bool) -- ^ Equality test + -> TestTree +testFunctorLaws2 pf pt pa pb eq = + let label = "Functor Laws for " ++ (show $ typeRep pf) in + testGroup label + [ testFunctorLaws pf pt pa pa pa eq + , testFunctorLaws pf pt pa pa pb eq + , testFunctorLaws pf pt pa pb pa eq + , testFunctorLaws pf pt pa pb pb eq + , testFunctorLaws pf pt pb pa pa eq + , testFunctorLaws pf pt pb pa pb eq + , testFunctorLaws pf pt pb pb pa eq + , testFunctorLaws pf pt pb pb pb eq + ] + + + +-- | All possible value type selections for @testFunctorLaws@ from three choices +testFunctorLaws3 + :: ( Functor f + , Checkable a, Checkable b, Checkable c + , Show t, Show (f a), Show (f b), Show (f c) + , Arbitrary t, Arbitrary (f a), Arbitrary (f b), Arbitrary (f c) + , Typeable f + ) + => Proxy f -- ^ Type constructor under test + -> Proxy t -- ^ Equality context for @f@ + -> Proxy a -- ^ Value type + -> Proxy b -- ^ Value type + -> Proxy c -- ^ Value type + -> (forall u. (Eq u) => t -> f u -> f u -> Bool) -- ^ Equality test + -> TestTree +testFunctorLaws3 pf pt pa pb pc eq = + let label = "Functor Laws for " ++ (show $ typeRep pf) in + testGroup label + [ testFunctorLaws pf pt pa pa pa eq + , testFunctorLaws pf pt pa pa pb eq + , testFunctorLaws pf pt pa pa pc eq + , testFunctorLaws pf pt pa pb pa eq + , testFunctorLaws pf pt pa pb pb eq + , testFunctorLaws pf pt pa pb pc eq + , testFunctorLaws pf pt pa pc pa eq + , testFunctorLaws pf pt pa pc pb eq + , testFunctorLaws pf pt pa pc pc eq + , testFunctorLaws pf pt pb pa pa eq + , testFunctorLaws pf pt pb pa pb eq + , testFunctorLaws pf pt pb pa pc eq + , testFunctorLaws pf pt pb pb pa eq + , testFunctorLaws pf pt pb pb pb eq + , testFunctorLaws pf pt pb pb pc eq + , testFunctorLaws pf pt pb pc pa eq + , testFunctorLaws pf pt pb pc pb eq + , testFunctorLaws pf pt pb pc pc eq + , testFunctorLaws pf pt pc pa pa eq + , testFunctorLaws pf pt pc pa pb eq + , testFunctorLaws pf pt pc pa pc eq + , testFunctorLaws pf pt pc pb pa eq + , testFunctorLaws pf pt pc pb pb eq + , testFunctorLaws pf pt pc pb pc eq + , testFunctorLaws pf pt pc pc pa eq + , testFunctorLaws pf pt pc pc pb eq + , testFunctorLaws pf pt pc pc pc eq + ] diff --git a/src/Test/Tasty/QuickCheck/Laws/Monad.hs b/src/Test/Tasty/QuickCheck/Laws/Monad.hs new file mode 100644 --- /dev/null +++ b/src/Test/Tasty/QuickCheck/Laws/Monad.hs @@ -0,0 +1,257 @@ +{- | +Module : Test.Tasty.QuickCheck.Laws.Monad +Description : Prefab tasty trees of quickcheck properties for the Monad laws +Copyright : 2018, Automattic, Inc. +License : GPL-3 +Maintainer : Nathan Bloomfield (nbloomf@gmail.com) +Stability : experimental +Portability : POSIX + +Prebuilt tasty test trees for the @Monad@ laws. To get started, look at @testMonadLaws@. +-} + + + +{-# LANGUAGE Rank2Types #-} +module Test.Tasty.QuickCheck.Laws.Monad ( + testMonadLaws + + -- * Monad Laws + , testMonadLawRightIdentity + , testMonadLawLeftIdentity + , testMonadLawAssociativity + + -- * Test Trees + , testMonadLaws1 + , testMonadLaws2 + , testMonadLaws3 +) where + + + +import Data.Proxy + ( Proxy(..) ) +import Data.Typeable + ( Typeable, typeRep ) +import Test.Tasty + ( TestTree, testGroup ) +import Test.Tasty.QuickCheck + ( testProperty, Property, Arbitrary(..), CoArbitrary(..) ) +import Text.Show.Functions + () + +import Test.Tasty.QuickCheck.Laws.Class + + + +-- | Constructs a @TestTree@ checking that the @Monad@ class laws hold for @m@ with value types @a@, @b@, and @c@, 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. +testMonadLaws + :: ( Monad m + , Eq a, Eq b, Eq c + , Show a, Show t, Show (m a) + , Arbitrary a, Arbitrary t, Arbitrary (m a), Arbitrary (m b), Arbitrary (m c) + , CoArbitrary a, CoArbitrary b + , Typeable m, Typeable a, Typeable b, Typeable c + ) + => Proxy m -- ^ Type constructor under test + -> Proxy t -- ^ Equality context for @m@ + -> Proxy a -- ^ Value type + -> Proxy b -- ^ Value type + -> Proxy c -- ^ Value type + -> (forall u. (Eq u) => t -> m u -> m u -> Bool) -- ^ Equality test + -> TestTree +testMonadLaws pm pt pa pb pc eq = + let + label = "Monad Laws for " ++ (show $ typeRep pm) ++ " with " ++ + "a :: " ++ (show $ typeRep pa) ++ ", " ++ + "b :: " ++ (show $ typeRep pb) ++ ", " ++ + "c :: " ++ (show $ typeRep pc) + in + testGroup label + [ testMonadLawRightIdentity pm pt pa eq + , testMonadLawLeftIdentity pm pt pa pb eq + , testMonadLawAssociativity pm pt pa pb pc eq + ] + + + +-- | @x >>= return === x@ +testMonadLawRightIdentity + :: ( Monad m + , 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 a -- ^ Value type + -> (forall u. (Eq u) => t -> m u -> m u -> Bool) -- ^ Equality test + -> TestTree +testMonadLawRightIdentity pm pt pa eq = + testProperty "x >>= return === x" $ + monadLawRightIdentity pm pt pa eq + +monadLawRightIdentity + :: (Monad m, Eq a) + => Proxy m -- ^ Type constructor under test + -> Proxy t -- ^ Equality context for @m@ + -> Proxy a -- ^ Value type + -> (forall u. (Eq u) => t -> m u -> m u -> Bool) + -> t -> m a -> Bool +monadLawRightIdentity _ _ _ eq t x = + (eq t) (x >>= return) (x) + + + +-- | @return a >>= f === f a@ +testMonadLawLeftIdentity + :: ( Monad m + , Eq b + , Show a, Show t + , Arbitrary a, Arbitrary t, Arbitrary (m b) + , CoArbitrary a + ) + => Proxy m -- ^ Type constructor under test + -> Proxy t -- ^ Equality context for @m@ + -> Proxy a -- ^ Value type + -> Proxy b -- ^ Value type + -> (forall u. (Eq u) => t -> m u -> m u -> Bool) -- ^ Equality test + -> TestTree +testMonadLawLeftIdentity pm pt pa pb eq = + testProperty "return a >>= f === f a" $ + monadLawLeftIdentity pm pt pa pb eq + +monadLawLeftIdentity + :: (Monad m, Eq b) + => Proxy m -> Proxy t -> Proxy a -> Proxy b + -> (forall u. (Eq u) => t -> m u -> m u -> Bool) + -> t -> a -> (a -> m b) -> Bool +monadLawLeftIdentity _ _ _ _ eq t x f = + (eq t) ((return x) >>= f) (f x) + + + +-- | @(x >>= f) >>= g === x >>= (\\z -> f z >>= g)@ +testMonadLawAssociativity + :: ( Monad m + , Eq c + , Show t, Show (m a) + , Arbitrary t, Arbitrary (m a), Arbitrary (m b), Arbitrary (m c) + , CoArbitrary a, CoArbitrary b + ) + => Proxy m -- ^ Type constructor under test + -> Proxy t -- ^ Equality context for @m@ + -> Proxy a -- ^ Value type + -> Proxy b -- ^ Value type + -> Proxy c -- ^ Value type + -> (forall u. (Eq u) => t -> m u -> m u -> Bool) -- ^ Equality test + -> TestTree +testMonadLawAssociativity pm pt pa pb pc eq = + testProperty "(x >>= f) >>= g === x >>= (\\z -> f z >>= g)" $ + monadLawAssociativity pm pt pa pb pc eq + +monadLawAssociativity + :: ( Monad m + , Eq c + ) + => Proxy m -> Proxy t -> Proxy a -> Proxy b -> Proxy c + -> (forall u. (Eq u) => t -> m u -> m u -> Bool) + -> t -> m a -> (a -> m b) -> (b -> m c) -> Bool +monadLawAssociativity _ _ _ _ _ eq t x f g = + (eq t) ((x >>= f) >>= g) (x >>= (\z -> f z >>= g)) + + + + + +-- | All possible value type selections for @testMonadLaws@ from one choice +testMonadLaws1 + :: ( Monad m + , Checkable a + , Show t, Show (m a) + , Arbitrary t, Arbitrary (m a) + , Typeable m + ) + => Proxy m -- ^ Type constructor under test + -> Proxy t -- ^ Equality context for @m@ + -> Proxy a -- ^ Value type + -> (forall u. (Eq u) => t -> m u -> m u -> Bool) -- ^ Equality test + -> TestTree +testMonadLaws1 pm pt pa eq = + let label = "Monad Laws for " ++ (show $ typeRep pm) in + testGroup label + [ testMonadLaws pm pt pa pa pa eq + ] + + + +-- | All possible value type selections for @testMonadLaws@ from two choices +testMonadLaws2 + :: ( Monad m + , Checkable a, Checkable b + , Show t, Show (m a), Show (m b) + , Arbitrary t, Arbitrary (m a), Arbitrary (m b) + , Typeable m + ) + => Proxy m -> Proxy t -> Proxy a -> Proxy b + -> (forall u. (Eq u) => t -> m u -> m u -> Bool) -- ^ Equality test + -> TestTree +testMonadLaws2 pm pt pa pb eq = + let label = "Monad Laws for " ++ (show $ typeRep pm) in + testGroup label + [ testMonadLaws pm pt pa pa pa eq + , testMonadLaws pm pt pa pa pb eq + , testMonadLaws pm pt pa pb pa eq + , testMonadLaws pm pt pa pb pb eq + , testMonadLaws pm pt pb pa pa eq + , testMonadLaws pm pt pb pa pb eq + , testMonadLaws pm pt pb pb pa eq + , testMonadLaws pm pt pb pb pb eq + ] + + + +-- | All possible value type selections for @testMonadLaws@ from three choices +testMonadLaws3 + :: ( Monad m + , Checkable a, Checkable b, Checkable c + , Show t, Show (m a), Show (m b), Show (m c) + , Arbitrary t, Arbitrary (m a), Arbitrary (m b), Arbitrary (m c) + , Typeable m + ) + => Proxy m -> Proxy t -> Proxy a -> Proxy b -> Proxy c + -> (forall u. (Eq u) => t -> m u -> m u -> Bool) -- ^ Equality test + -> TestTree +testMonadLaws3 pm pt pa pb pc eq = + let label = "Monad Laws for " ++ (show $ typeRep pm) in + testGroup label + [ testMonadLaws pm pt pa pa pa eq + , testMonadLaws pm pt pa pa pb eq + , testMonadLaws pm pt pa pa pc eq + , testMonadLaws pm pt pa pb pa eq + , testMonadLaws pm pt pa pb pb eq + , testMonadLaws pm pt pa pb pc eq + , testMonadLaws pm pt pa pc pa eq + , testMonadLaws pm pt pa pc pb eq + , testMonadLaws pm pt pa pc pc eq + , testMonadLaws pm pt pb pa pa eq + , testMonadLaws pm pt pb pa pb eq + , testMonadLaws pm pt pb pa pc eq + , testMonadLaws pm pt pb pb pa eq + , testMonadLaws pm pt pb pb pb eq + , testMonadLaws pm pt pb pb pc eq + , testMonadLaws pm pt pb pc pa eq + , testMonadLaws pm pt pb pc pb eq + , testMonadLaws pm pt pb pc pc eq + , testMonadLaws pm pt pc pa pa eq + , testMonadLaws pm pt pc pa pb eq + , testMonadLaws pm pt pc pa pc eq + , testMonadLaws pm pt pc pb pa eq + , testMonadLaws pm pt pc pb pb eq + , testMonadLaws pm pt pc pb pc eq + , testMonadLaws pm pt pc pc pa eq + , testMonadLaws pm pt pc pc pb eq + , testMonadLaws pm pt pc pc pc eq + ] diff --git a/src/Test/Tasty/QuickCheck/Laws/Monoid.hs b/src/Test/Tasty/QuickCheck/Laws/Monoid.hs new file mode 100644 --- /dev/null +++ b/src/Test/Tasty/QuickCheck/Laws/Monoid.hs @@ -0,0 +1,82 @@ +{- | +Module : Test.Tasty.QuickCheck.Laws.Monoid +Description : Prefab tasty trees of quickcheck properties for the Monoid laws +Copyright : 2018, Automattic, Inc. +License : GPL-3 +Maintainer : Nathan Bloomfield (nbloomf@gmail.com) +Stability : experimental +Portability : POSIX +-} + + + +module Test.Tasty.QuickCheck.Laws.Monoid ( + testMonoidLaws + + -- * Monoid Laws + , testMonoidLawIdentity + , testMonoidLawAssociative +) where + +import Data.Proxy + ( Proxy(..) ) +import Data.Typeable + ( Typeable, typeRep ) +import Test.Tasty + ( TestTree, testGroup ) +import Test.Tasty.QuickCheck + ( testProperty, Property, Arbitrary(..) ) + +import Test.Tasty.QuickCheck.Laws.Class + + + +-- | Constructs a @TestTree@ checking that the @Monoid@ class laws hold for @a@. +testMonoidLaws + :: (Monoid a, Eq a, Show a, Arbitrary a, Typeable a) + => Proxy a + -> TestTree +testMonoidLaws pa = + let label = "Monoid Laws for " ++ (show $ typeRep pa) in + testGroup label + [ testMonoidLawIdentity pa + , testMonoidLawAssociative pa + ] + + + + + +-- | @mappend mempty a === mappend a mempty === a@ +testMonoidLawIdentity + :: (Monoid a, Eq a, Show a, Arbitrary a) + => Proxy a + -> TestTree +testMonoidLawIdentity pa = + testProperty "mempty <> a === mappend a mempty === a" $ + monoidLawIdentity pa + +monoidLawIdentity + :: (Monoid a, Eq a) + => Proxy a + -> a -> Bool +monoidLawIdentity _ a = + (mappend mempty a == a) && (mappend a mempty == a) + + + +-- | @mappend (mappend a b) c === mappend a (mappend b c)@ +testMonoidLawAssociative + :: (Monoid a, Eq a, Show a, Arbitrary a) + => Proxy a + -> TestTree +testMonoidLawAssociative pa = + testProperty "mappend (mappend a b) c === mappend a (mappend b c)" $ + monoidLawAssociative pa + +monoidLawAssociative + :: (Monoid a, Eq a) + => Proxy a + -> a -> a -> a -> Bool +monoidLawAssociative _ a b c = + mappend (mappend a b) c == mappend a (mappend b c) diff --git a/src/Test/Tasty/QuickCheck/Laws/ReaderMonad.hs b/src/Test/Tasty/QuickCheck/Laws/ReaderMonad.hs new file mode 100644 --- /dev/null +++ b/src/Test/Tasty/QuickCheck/Laws/ReaderMonad.hs @@ -0,0 +1,234 @@ +{- | +Module : Test.Tasty.QuickCheck.Laws.ReaderMonad +Description : Prefab tasty trees of quickcheck properties for the reader monad laws +Copyright : 2018, Automattic, Inc. +License : GPL-3 +Maintainer : Nathan Bloomfield (nbloomf@gmail.com) +Stability : experimental +Portability : POSIX +-} + + + +{-# LANGUAGE Rank2Types #-} +module Test.Tasty.QuickCheck.Laws.ReaderMonad ( + testReaderMonadLaws + + -- * Reader Monad Laws + , testReaderMonadLawLocalAsk + , testReaderMonadLawLocalLocal + , testReaderMonadLawLocalThenAsk + , testReaderMonadLawLocalReturn + , testReaderMonadLawLocalBind +) where + + + +import Data.Proxy + ( Proxy(..) ) +import Data.Typeable + ( Typeable, typeRep ) +import Test.Tasty + ( TestTree, testGroup ) +import Test.Tasty.QuickCheck + ( testProperty, Property, Arbitrary(..), CoArbitrary(..) ) +import Text.Show.Functions + () + +import Test.Tasty.QuickCheck.Laws.Class + + + +-- | Constructs a @TestTree@ checking that the reader monad laws hold for @m@ with reader type @r@ 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. +testReaderMonadLaws + :: ( Monad m + , Eq r, Eq a, Eq b + , Show t, Show a + , Show (m a) + , Arbitrary t, Arbitrary r, Arbitrary a + , Arbitrary (m a), Arbitrary (m b) + , CoArbitrary r, CoArbitrary a + , Typeable m, Typeable r, Typeable a + ) + => Proxy m -- ^ Type constructor under test + -> Proxy t -- ^ Equality context for @m@ + -> Proxy r -- ^ Reader type + -> Proxy a -- ^ Value type + -> Proxy b -- ^ Value type + -> (forall u. (Eq u) => t -> m u -> m u -> Bool) -- ^ Equality test + -> m r -- ^ @ask@ + -> (forall u. (r -> r) -> m u -> m u) -- ^ @local@ + -> TestTree +testReaderMonadLaws pm pt pr pa pb eq ask local = + let + label = "Reader Monad Laws for " ++ (show $ typeRep pm) ++ " with " ++ + "r :: " ++ (show $ typeRep pr) ++ ", " ++ + "a :: " ++ (show $ typeRep pa) + in + testGroup label + [ testReaderMonadLawLocalAsk pm pt pr eq ask local + , testReaderMonadLawLocalLocal pm pt pr pa eq local + , testReaderMonadLawLocalThenAsk pm pt pr pa eq ask local + , testReaderMonadLawLocalReturn pm pt pr pa eq local + , testReaderMonadLawLocalBind pm pt pr pa pb eq local + ] + + + +-- | @local u ask === fmap u ask@ +testReaderMonadLawLocalAsk + :: ( Monad m + , Eq r + , Show t + , Arbitrary t, Arbitrary r + , CoArbitrary r + ) + => Proxy m -- ^ Type constructor under test + -> Proxy t -- ^ Equality context for @m@ + -> Proxy r -- ^ Reader type + -> (forall u. (Eq u) => t -> m u -> m u -> Bool) -- ^ Equality test + -> m r -- ^ @ask@ + -> (forall u. (r -> r) -> m u -> m u) -- ^ @local@ + -> TestTree +testReaderMonadLawLocalAsk pm pt pr eq ask local = + testProperty "local u ask === fmap u ask" $ + readerMonadLawLocalAsk pm pt pr eq ask local + +readerMonadLawLocalAsk + :: (Monad m, Eq r) + => Proxy m -> Proxy t -> Proxy r + -> (forall u. (Eq u) => t -> m u -> m u -> Bool) -- ^ Equality test + -> m r -- ^ ask + -> (forall u. (r -> r) -> m u -> m u) -- ^ local + -> t -> (r -> r) -> Bool +readerMonadLawLocalAsk _ _ _ eq ask local t u = + (eq t) (local u ask) (fmap u ask) + + + +-- | @local u (local v x) === local (u . v) x@ +testReaderMonadLawLocalLocal + :: ( Monad m + , Eq a + , Show t + , Show (m a) + , Arbitrary t, Arbitrary r + , Arbitrary (m a) + , CoArbitrary r + ) + => Proxy m -- ^ Type constructor under test + -> Proxy t -- ^ Equality context for @m@ + -> Proxy r -- ^ Reader type + -> Proxy a -- ^ Value type + -> (forall u. (Eq u) => t -> m u -> m u -> Bool) -- ^ Equality test + -> (forall u. (r -> r) -> m u -> m u) -- ^ @local@ + -> TestTree +testReaderMonadLawLocalLocal pm pt pr pa eq local = + testProperty "local u (local v x) === local (u . v) x" $ + readerMonadLawLocalLocal pm pt pr pa eq local + +readerMonadLawLocalLocal + :: (Monad m, Eq a) + => Proxy m -> Proxy t -> Proxy r -> Proxy a + -> (forall u. (Eq u) => t -> m u -> m u -> Bool) -- ^ Equality test + -> (forall u. (r -> r) -> m u -> m u) -- ^ local + -> t -> (r -> r) -> (r -> r) -> m a -> Bool +readerMonadLawLocalLocal _ _ _ _ eq local t u v x = + (eq t) (local u (local v x)) (local (u . v) x) + + + +-- | @local u ask === fmap u ask@ +testReaderMonadLawLocalThenAsk + :: ( Monad m + , Eq r + , Show t + , Show (m a) + , Arbitrary t, Arbitrary r + , Arbitrary (m a) + , CoArbitrary r + ) + => Proxy m -- ^ Type constructor under test + -> Proxy t -- ^ Equality context for @m@ + -> Proxy r -- ^ Reader type + -> Proxy a -- ^ Value type + -> (forall u. (Eq u) => t -> m u -> m u -> Bool) -- ^ Equality test + -> m r -- ^ @ask@ + -> (forall u. (r -> r) -> m u -> m u) -- ^ @local@ + -> TestTree +testReaderMonadLawLocalThenAsk pm pt pr pa eq ask local = + testProperty "local u ask === fmap u ask" $ + readerMonadLawLocalThenAsk pm pt pr pa eq ask local + +readerMonadLawLocalThenAsk + :: (Monad m, Eq r) + => Proxy m -> Proxy t -> Proxy r -> Proxy a + -> (forall u. (Eq u) => t -> m u -> m u -> Bool) -- ^ Equality test + -> m r -- ^ ask + -> (forall u. (r -> r) -> m u -> m u) -- ^ local + -> t -> (r -> r) -> m a -> Bool +readerMonadLawLocalThenAsk _ _ _ _ eq ask local t u x = + (eq t) (local u x >> ask) (ask >>= \r -> local u x >> return r) + + + +-- | @local u (return a) === return a@ +testReaderMonadLawLocalReturn + :: ( Monad m + , Eq a + , Show t, Show a + , Arbitrary t, Arbitrary r, Arbitrary a + , CoArbitrary r + ) + => Proxy m -- ^ Type constructor under test + -> Proxy t -- ^ Equality context for @m@ + -> Proxy r -- ^ Reader type + -> Proxy a -- ^ Value type + -> (forall u. (Eq u) => t -> m u -> m u -> Bool) -- ^ Equality test + -> (forall u. (r -> r) -> m u -> m u) -- ^ @local@ + -> TestTree +testReaderMonadLawLocalReturn pm pt pr pa eq local = + testProperty "local u (return a) === return a" $ + readerMonadLawLocalReturn pm pt pr pa eq local + +readerMonadLawLocalReturn + :: (Monad m, Eq a) + => Proxy m -> Proxy t -> Proxy r -> Proxy a + -> (forall u. (Eq u) => t -> m u -> m u -> Bool) -- ^ Equality test + -> (forall u. (r -> r) -> m u -> m u) -- ^ local + -> t -> (r -> r) -> a -> Bool +readerMonadLawLocalReturn _ _ _ _ eq local t u a = + (eq t) (local u (return a)) (return a) + + + +-- | @local u (x >>= f) === local u x >>= (local u . f)@ +testReaderMonadLawLocalBind + :: ( Monad m + , Eq b + , Show t, Show a + , Show (m a) + , Arbitrary t, Arbitrary r, Arbitrary a + , Arbitrary (m a), Arbitrary (m b) + , CoArbitrary r, CoArbitrary a + ) + => Proxy m -- ^ Type constructor under test + -> Proxy t -- ^ Equality context for @m@ + -> Proxy r -- ^ Reader type + -> Proxy a -- ^ Value type + -> Proxy b -- ^ Value type + -> (forall u. (Eq u) => t -> m u -> m u -> Bool) -- ^ Equality test + -> (forall u. (r -> r) -> m u -> m u) -- ^ local + -> TestTree +testReaderMonadLawLocalBind pm pt pr pa pb eq local = + testProperty "local u (x >>= f) === local u x >>= (local u . f)" $ + readerMonadLawLocalBind pm pt pr pa pb eq local + +readerMonadLawLocalBind + :: (Monad m, Eq b) + => Proxy m -> Proxy t -> Proxy r -> Proxy a -> Proxy b + -> (forall u. (Eq u) => t -> m u -> m u -> Bool) -- ^ Equality test + -> (forall u. (r -> r) -> m u -> m u) -- ^ local + -> t -> (r -> r) -> m a -> (a -> m b) -> Bool +readerMonadLawLocalBind _ _ _ _ _ eq local t u x f = + (eq t) (local u (x >>= f)) (local u x >>= (local u . f)) diff --git a/src/Test/Tasty/QuickCheck/Laws/StateMonad.hs b/src/Test/Tasty/QuickCheck/Laws/StateMonad.hs new file mode 100644 --- /dev/null +++ b/src/Test/Tasty/QuickCheck/Laws/StateMonad.hs @@ -0,0 +1,187 @@ +{- | +Module : Test.Tasty.QuickCheck.Laws.StateMonad +Description : Prefab tasty trees of quickcheck properties for the state monad laws +Copyright : 2018, Automattic, Inc. +License : GPL-3 +Maintainer : Nathan Bloomfield (nbloomf@gmail.com) +Stability : experimental +Portability : POSIX + +State axioms taken from Gibbons and Hinze, /Just do it: simple monadic reasoning/, at http://www.cs.ox.ac.uk/jeremy.gibbons/publications/mr.pdf. +-} + + + +{-# LANGUAGE Rank2Types #-} +module Test.Tasty.QuickCheck.Laws.StateMonad ( + testStateMonadLaws + + -- * State Monad Laws + , testStateMonadLawPutPut + , testStateMonadLawPutGet + , testStateMonadLawGetPut + , testStateMonadLawGetGet +) where + + + +import Data.Proxy + ( Proxy(..) ) +import Data.Typeable + ( Typeable, typeRep ) +import Test.Tasty + ( TestTree, testGroup ) +import Test.Tasty.QuickCheck + ( testProperty, Property, Arbitrary(..), CoArbitrary(..) ) +import Text.Show.Functions + () + +import Test.Tasty.QuickCheck.Laws.Class + + + +-- | Constructs a @TestTree@ checking that the state monad laws hold for @m@ with state type @s@ 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. +testStateMonadLaws + :: ( Monad m + , Eq s, Eq a + , Show t, Show s + , Arbitrary t, Arbitrary s + , Arbitrary (m a) + , CoArbitrary s + , Typeable m, Typeable s, Typeable a + ) + => Proxy m -- ^ Type constructor under test + -> Proxy t -- ^ Equality context for @m@ + -> Proxy s -- ^ State type + -> Proxy a -- ^ Value type + -> (forall u. (Eq u) => t -> m u -> m u -> Bool) -- ^ Equality test + -> m s -- ^ @get@ + -> (s -> m ()) -- ^ @put@ + -> TestTree +testStateMonadLaws pm pt ps pa eq get put = + let + label = "State Monad Laws for " ++ (show $ typeRep pm) ++ " with " ++ + "s :: " ++ (show $ typeRep ps) ++ ", " ++ + "a :: " ++ (show $ typeRep pa) + in + testGroup label + [ testStateMonadLawPutPut pm pt ps eq put + , testStateMonadLawPutGet pm pt ps eq get put + , testStateMonadLawGetPut pm pt ps eq get put + , testStateMonadLawGetGet pm pt ps pa eq get + ] + + + +-- | @put s1 >> put s2 === put s2@ +testStateMonadLawPutPut + :: ( Monad m + , Show t, Show s + , Arbitrary t, Arbitrary s + ) + => Proxy m -- ^ Type constructor under test + -> Proxy t -- ^ Equality context for @m@ + -> Proxy s -- ^ State type + -> (forall u. (Eq u) => t -> m u -> m u -> Bool) -- ^ Equality test + -> (s -> m ()) -- ^ @put@ + -> TestTree +testStateMonadLawPutPut pm pt ps eq put = + testProperty "put s1 >> put s2 === put s2" $ + stateMonadLawPutPut pm pt ps eq put + +stateMonadLawPutPut + :: (Monad m) + => Proxy m -> Proxy t -> Proxy s + -> (forall u. (Eq u) => t -> m u -> m u -> Bool) + -> (s -> m ()) -- ^ put + -> t -> s -> s -> Bool +stateMonadLawPutPut _ _ _ eq put t s1 s2 = + (eq t) (put s1 >> put s2) (put s2) + + + +-- | @put s >> get === put s >> return s@ +testStateMonadLawPutGet + :: ( Monad m + , Eq s + , Show t, Show s + , Arbitrary t, Arbitrary s + ) + => Proxy m -- ^ Type constructor under test + -> Proxy t -- ^ Equality context for @m@ + -> Proxy s -- ^ State type + -> (forall u. (Eq u) => t -> m u -> m u -> Bool) -- ^ Equality test + -> m s -- ^ @get@ + -> (s -> m ()) -- ^ @put@ + -> TestTree +testStateMonadLawPutGet pm pt ps eq get put = + testProperty "put s >> get === put s >> return s" $ + stateMonadLawPutGet pm pt ps eq get put + +stateMonadLawPutGet + :: (Monad m, Eq s) + => Proxy m -> Proxy t -> Proxy s + -> (forall u. (Eq u) => t -> m u -> m u -> Bool) -- ^ Equality test + -> m s -> (s -> m ()) + -> t -> s -> Bool +stateMonadLawPutGet _ _ _ eq get put t s = + (eq t) (put s >> get) (put s >> return s) + + + +-- | @get >>= put === return ()@ +testStateMonadLawGetPut + :: ( Monad m + , Show t + , Arbitrary t + ) + => Proxy m -- ^ Type constructor under test + -> Proxy t -- ^ Equality context for @m@ + -> Proxy s -- ^ State type + -> (forall u. (Eq u) => t -> m u -> m u -> Bool) -- ^ Equality test + -> m s -- ^ @get@ + -> (s -> m ()) -- ^ @put@ + -> TestTree +testStateMonadLawGetPut pm pt ps eq get put = + testProperty "get >>= put === return ()" $ + stateMonadLawGetPut pm pt ps eq get put + +stateMonadLawGetPut + :: (Monad m) + => Proxy m -> Proxy t -> Proxy s + -> (forall u. (Eq u) => t -> m u -> m u -> Bool) -- ^ Equality test + -> m s -> (s -> m ()) + -> t -> Bool +stateMonadLawGetPut _ _ _ eq get put t = + (eq t) (get >>= put) (return ()) + + + +-- | @get >>= \\s -> get >>= k s === get >>= \\s -> k s s@ +testStateMonadLawGetGet + :: ( Monad m + , Eq a + , Show t + , Arbitrary t + , Arbitrary (m a) + , CoArbitrary s + ) + => Proxy m -- ^ Type constructor under test + -> Proxy t -- ^ Equality context for @m@ + -> Proxy s -- ^ State type + -> Proxy a -- ^ Value type + -> (forall u. (Eq u) => t -> m u -> m u -> Bool) -- ^ Equality test + -> m s -- ^ @get@ + -> TestTree +testStateMonadLawGetGet pm pt ps pa eq get = + testProperty "get >>= \\s -> get >>= k s === get >>= \\s -> k s s" $ + stateMonadLawGetGet pm pt ps pa eq get + +stateMonadLawGetGet + :: (Monad m, Eq a) + => Proxy m -> Proxy t -> Proxy s -> Proxy a + -> (forall u. (Eq u) => t -> m u -> m u -> Bool) -- ^ Equality test + -> m s + -> t -> (s -> s -> m a) -> Bool +stateMonadLawGetGet _ _ _ _ eq get t k = + (eq t) (get >>= \s -> get >>= k s) (get >>= \s -> k s s) diff --git a/src/Test/Tasty/QuickCheck/Laws/WriterMonad.hs b/src/Test/Tasty/QuickCheck/Laws/WriterMonad.hs new file mode 100644 --- /dev/null +++ b/src/Test/Tasty/QuickCheck/Laws/WriterMonad.hs @@ -0,0 +1,503 @@ +{- | +Module : Test.Tasty.QuickCheck.Laws.WriterMonad +Description : Prefab tasty trees of quickcheck properties for writer monad laws +Copyright : 2018, Automattic, Inc. +License : GPL-3 +Maintainer : Nathan Bloomfield (nbloomf@gmail.com) +Stability : experimental +Portability : POSIX + +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. +-} + + + +{-# LANGUAGE Rank2Types #-} +module Test.Tasty.QuickCheck.Laws.WriterMonad ( + testWriterMonadLaws + + -- * Writer Monad Laws + , testWriterMonadLawDraftTell + , testWriterMonadLawTellMempty + , testWriterMonadLawTellMappend + , testWriterMonadLawDraftReturn + , testWriterMonadLawDraftBind + + -- * Alternate Primitives + , testWriterMonadEquivalences + , testWriterMonadEquivalenceListen + , testWriterMonadEquivalencePass + , testWriterMonadEquivalenceDraft +) where + + + +import Data.Proxy + ( Proxy(..) ) +import Data.Typeable + ( Typeable, typeRep ) +import Test.Tasty + ( TestTree, testGroup ) +import Test.Tasty.QuickCheck + ( testProperty, Property, Arbitrary(..), CoArbitrary(..) ) +import Text.Show.Functions + () + +import Test.Tasty.QuickCheck.Laws.Class + + +-- | 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@. +testWriterMonadLaws + :: ( 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 +testWriterMonadLaws pm pt pw pa pb eq tell draft = + let + label = "Writer Monad Laws for " ++ (show $ typeRep pm) ++ " with " ++ + "w :: " ++ (show $ typeRep pw) ++ ", " ++ + "a :: " ++ (show $ typeRep pa) + in + testGroup label + [ testWriterMonadLawDraftTell pm pt pw eq tell draft + , testWriterMonadLawTellMempty pm pt pw eq tell + , testWriterMonadLawTellMappend pm pt pw eq tell + , testWriterMonadLawDraftReturn pm pt pw pa eq draft + , testWriterMonadLawDraftBind pm pt pw pa pb eq draft + ] + + + +-- | @draft (tell w) === return ((),w)@ +testWriterMonadLawDraftTell + :: ( 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 +testWriterMonadLawDraftTell pm pt pw eq tell draft = + testProperty "draft (tell w) === tell w >> return ((),w)" $ + writerMonadLawDraftTell pm pt pw eq tell draft + +writerMonadLawDraftTell + :: (Monad m, Eq w) + => Proxy m -> Proxy t -> Proxy w + -> (forall u. (Eq u) => t -> m u -> m u -> Bool) -- ^ Equality test + -> (w -> m ()) -- ^ tell + -> (forall u. m u -> m (u,w)) -- ^ draft + -> t -> w -> Bool +writerMonadLawDraftTell _ _ _ eq tell draft t w = + (eq t) (draft (tell w)) (return ((),w)) + + + +-- | @tell mempty === return ()@ +testWriterMonadLawTellMempty + :: ( 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 +testWriterMonadLawTellMempty pm pt pw eq tell = + testProperty "tell mempty === return ()" $ + writerMonadLawTellMempty pm pt pw eq tell + +writerMonadLawTellMempty + :: (Monoid w, Monad m) + => Proxy m -> Proxy t -> Proxy w + -> (forall u. (Eq u) => t -> m u -> m u -> Bool) -- ^ Equality test + -> (w -> m ()) -- ^ tell + -> t -> Bool +writerMonadLawTellMempty _ _ _ eq tell t = + (eq t) (tell mempty) (return ()) + + + +-- | @tell w1 >> tell w2 === tell (mappend w1 w2)@ +testWriterMonadLawTellMappend + :: ( 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 +testWriterMonadLawTellMappend pm pt pw eq tell = + testProperty "tell mempty === return ()" $ + writerMonadLawTellMappend pm pt pw eq tell + +writerMonadLawTellMappend + :: (Monoid w, Monad m) + => Proxy m -> Proxy t -> Proxy w + -> (forall u. (Eq u) => t -> m u -> m u -> Bool) -- ^ Equality test + -> (w -> m ()) -- ^ tell + -> t -> w -> w -> Bool +writerMonadLawTellMappend _ _ _ eq tell t w1 w2 = + (eq t) (tell w1 >> tell w2) (tell (mappend w1 w2)) + + + +-- | @draft (return a) === return a@ +testWriterMonadLawDraftReturn + :: ( 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 +testWriterMonadLawDraftReturn pm pt pw pa eq draft = + testProperty "draft (return a) === return a" $ + writerMonadLawDraftReturn pm pt pw pa eq draft + +writerMonadLawDraftReturn + :: (Monoid w, Monad m, Eq a, Eq w) + => Proxy m -> Proxy t -> Proxy w -> Proxy a + -> (forall u. (Eq u) => t -> m u -> m u -> Bool) -- ^ Equality test + -> (forall u. m u -> m (u,w)) -- ^ draft + -> t -> a -> Bool +writerMonadLawDraftReturn _ _ _ _ eq draft t a = + (eq t) (draft (return a)) (return (a, mempty)) + + + +-- | @draft (x >>= f) === draft x >>= (draft' f)@ where @draft' f (a,w) = mapsnd (mappend w) <$> draft (f a)@ +testWriterMonadLawDraftBind + :: ( 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 +testWriterMonadLawDraftBind pm pt pw pa pb eq draft = + testProperty "draft (x >>= f) === draft x >>= draft' f" $ + writerMonadLawDraftBind pm pt pw pa pb eq draft + +writerMonadLawDraftBind + :: (Monoid w, Monad m, Eq w, Eq b) + => Proxy m -> Proxy t -> Proxy w -> Proxy a -> Proxy b + -> (forall u. (Eq u) => t -> m u -> m u -> Bool) -- ^ Equality test + -> (forall u. m u -> m (u,w)) -- ^ draft + -> t -> m a -> (a -> m b) -> Bool +writerMonadLawDraftBind _ _ _ _ _ eq draft t x f = + let mapsnd g (u,v) = (u, g v) in + let draft' g (b,v) = mapsnd (mappend v) <$> draft (g b) in + (eq t) (draft (x >>= f)) (draft x >>= draft' f) + + + +-- | 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) +testWriterMonadEquivalences + :: ( 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 +testWriterMonadEquivalences pm pt pw pa eq tell draft listen pass = + let + label = "Writer Monad Equivalence for " ++ (show $ typeRep pm) ++ " with " ++ + "w :: " ++ (show $ typeRep pw) ++ ", " ++ + "a :: " ++ (show $ typeRep pa) + in + testGroup label + [ testWriterMonadEquivalenceListen pm pt pw pa eq tell draft listen + , testWriterMonadEquivalencePass pm pt pw pa eq tell draft pass + , testWriterMonadEquivalenceDraft pm pt pw pa eq draft listen pass + ] + + + +-- | @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 +testWriterMonadEquivalenceListen + :: ( 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 +testWriterMonadEquivalenceListen pm pt pw pa eq tell draft listen = + testProperty "listen x === do (a,w) <- draft x; tell w; return (a,w)" $ + writerMonadEquivalenceListen pm pt pw pa eq tell draft listen + +writerMonadEquivalenceListen + :: (Monad m, Eq a, Eq w) + => Proxy m -> Proxy t -> Proxy w -> Proxy a + -> (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 + -> t -> m a -> Bool +writerMonadEquivalenceListen _ _ _ _ eq tell draft listen t x = + (eq t) (listen x) (do (a,w) <- draft x; tell w; return (a,w)) + + + +-- | @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 +testWriterMonadEquivalencePass + :: ( 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 +testWriterMonadEquivalencePass pm pt pw pa eq tell draft pass = + testProperty "pass u === do ((a,f),w) <- draft u; tell (f w); return a" $ + writerMonadEquivalencePass pm pt pw pa eq tell draft pass + +writerMonadEquivalencePass + :: (Monad m, Eq a, Eq w) + => Proxy m -> Proxy t -> Proxy w -> Proxy a + -> (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 + -> t -> m (a, w -> w) -> Bool +writerMonadEquivalencePass _ _ _ _ eq tell draft pass t u = + (eq t) (pass u) (do ((a,f),w) <- draft u; tell (f w); return a) + + + +-- | @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 +testWriterMonadEquivalenceDraft + :: ( 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 +testWriterMonadEquivalenceDraft pm pt pw pa eq draft listen pass = + testProperty "draft x === pass $ do (a,w) <- listen x; return ((a,w), const mempty)" $ + writerMonadEquivalenceDraft pm pt pw pa eq draft listen pass + +writerMonadEquivalenceDraft + :: (Monoid w, Monad m, Eq a, Eq w) + => Proxy m -> Proxy t -> Proxy w -> Proxy a + -> (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 + -> t -> m a -> Bool +writerMonadEquivalenceDraft _ _ _ _ eq draft listen pass t x = + (eq t) (draft x) (pass $ do (a,w) <- listen x; return ((a,w), const mempty)) diff --git a/tasty-quickcheck-laws.cabal b/tasty-quickcheck-laws.cabal new file mode 100644 --- /dev/null +++ b/tasty-quickcheck-laws.cabal @@ -0,0 +1,74 @@ +name: tasty-quickcheck-laws +version: 0.0.1 +description: Please see the README on GitHub at +homepage: https://github.com/nbloomf/tasty-quickcheck-laws#readme +bug-reports: https://github.com/nbloomf/tasty-quickcheck-laws/issues +author: Nathan Bloomfield +maintainer: nathan.bloomfield@a8c.com +copyright: 2018 Automattic, Inc. +license: BSD3 +license-file: LICENSE +build-type: Simple +cabal-version: >= 1.10 +category: testing, tasty, quickcheck +synopsis: Pre-built tasty trees for checking lawful class properties using QuickCheck + +extra-source-files: + CHANGELOG.md + README.md + +source-repository head + type: git + location: https://github.com/nbloomf/tasty-quickcheck-laws + + + +library + default-language: Haskell2010 + hs-source-dirs: src + + build-depends: + base >=4.7 && <5 + , QuickCheck >=2.10.1 + , tasty >=1.0.1.1 + , tasty-quickcheck >=0.9.2 + + exposed-modules: + Test.Tasty.QuickCheck.Laws + Test.Tasty.QuickCheck.Laws.Applicative + Test.Tasty.QuickCheck.Laws.Class + Test.Tasty.QuickCheck.Laws.Eq + Test.Tasty.QuickCheck.Laws.ErrorMonad + Test.Tasty.QuickCheck.Laws.Functor + Test.Tasty.QuickCheck.Laws.Monad + Test.Tasty.QuickCheck.Laws.Monoid + Test.Tasty.QuickCheck.Laws.ReaderMonad + Test.Tasty.QuickCheck.Laws.StateMonad + Test.Tasty.QuickCheck.Laws.WriterMonad + + + +executable tasty-quickcheck-laws-demo + default-language: Haskell2010 + main-is: Main.hs + hs-source-dirs: app + ghc-options: -threaded -rtsopts -with-rtsopts=-N + + build-depends: + base >=4.7 && <5 + , tasty-quickcheck-laws + + + +test-suite tasty-quickcheck-laws-test + default-language: Haskell2010 + type: exitcode-stdio-1.0 + main-is: Main.hs + hs-source-dirs: test + ghc-options: -threaded -rtsopts -with-rtsopts=-N + + build-depends: + base >=4.7 && <5 + , tasty-quickcheck-laws + , QuickCheck >=2.10.1 + , tasty >=1.0.1.1 diff --git a/test/Main.hs b/test/Main.hs new file mode 100644 --- /dev/null +++ b/test/Main.hs @@ -0,0 +1,268 @@ +module Main where + +import Test.Tasty +import Data.Proxy +import System.Environment +import Control.Monad (ap) +import Test.QuickCheck + +import Test.Tasty.QuickCheck.Laws + + + +main :: IO () +main = do + setEnv "NUM_TASTY_THREADS" "6" + defaultMain $ testGroup "Laws" + [ testGroup "Eq Laws" + [ testEqLaws pU + , testEqLaws pB + , testEqLaws pI + ] + , testGroup "Monoid Laws" + [ testMonoidLaws (Proxy :: Proxy [()]) + , testMonoidLaws (Proxy :: Proxy [Bool]) + , testMonoidLaws (Proxy :: Proxy (Maybe [()])) + ] + , testGroup "Functor Laws" + [ testFunctorLaws1 pMb pU pU (const (==)) + , testFunctorLaws1 pEi pU pU (const (==)) + , testFunctorLaws1 pLs pU pU (const (==)) + , testFunctorLaws2 pMb pU pU pB (const (==)) + , testFunctorLaws2 pEi pU pU pB (const (==)) + , testFunctorLaws2 pLs pU pU pB (const (==)) + , testFunctorLaws3 pMb pU pU pB pI (const (==)) + , testFunctorLaws3 pEi pU pU pB pI (const (==)) + , testFunctorLaws3 pLs pU pU pB pI (const (==)) + ] + , testGroup "Applicative Laws" + [ testApplicativeLaws1 pMb pU pU (const (==)) + , testApplicativeLaws1 pEi pU pU (const (==)) + , testApplicativeLaws1 pLs pU pU (const (==)) + , testApplicativeLaws2 pMb pU pU pB (const (==)) + , testApplicativeLaws2 pEi pU pU pB (const (==)) + , testApplicativeLaws2 pLs pU pU pB (const (==)) + , testApplicativeLaws3 pMb pU pU pB pI (const (==)) + , testApplicativeLaws3 pEi pU pU pB pI (const (==)) + , testApplicativeLaws3 pLs pU pU pB pI (const (==)) + ] + , testGroup "Monad Laws" + [ testMonadLaws1 pMb pU pU (const (==)) + , testMonadLaws1 pEi pU pU (const (==)) + , testMonadLaws1 pLs pU pU (const (==)) + , testMonadLaws2 pMb pU pU pB (const (==)) + , testMonadLaws2 pEi pU pU pB (const (==)) + , testMonadLaws2 pLs pU pU pB (const (==)) + , testMonadLaws3 pMb pU pU pB pI (const (==)) + , testMonadLaws3 pEi pU pU pB pI (const (==)) + , testMonadLaws3 pLs pU pU pB pI (const (==)) + ] + , testGroup "State Monad Laws" + [ testStateMonadLaws pSU pU pU pU stateEq get put + , testStateMonadLaws pSB pB pB pB stateEq get put + , testStateMonadLaws pSI pI pI pI stateEq get put + ] + , testGroup "Reader Monad Laws" + [ testReaderMonadLaws pRU pU pU pU pU readerEq ask local + , testReaderMonadLaws pRB pB pB pB pB readerEq ask local + , testReaderMonadLaws pRI pI pI pI pI readerEq ask local + ] + , testGroup "Error Monad Laws" + [ testErrorMonadLaws pEU pU pU pU pU (const (==)) throw catch + , testErrorMonadLaws pEB pU pB pU pU (const (==)) throw catch + , testErrorMonadLaws pEI pU pI pU pU (const (==)) throw catch + ] + , testGroup "Writer Monads" + [ testGroup "Writer Monad Laws" + [ testWriterMonadLaws pWU pU pU pU pU (const (==)) tell draft + , testWriterMonadLaws (pWLs pB) pU (pLs' pB) pU pU (const (==)) tell draft + , testWriterMonadLaws (pWLs pI) pU (pLs' pI) pU pU (const (==)) tell draft + ] + , testGroup "Writer Monad Equivalences" + [ testWriterMonadEquivalences pWU pU pU pU (const (==)) tell draft listen pass + , testWriterMonadEquivalences (pWLs pB) pU (pLs' pB) pU (const (==)) tell draft listen pass + , testWriterMonadEquivalences (pWLs pI) pU (pLs' pI) pU (const (==)) tell draft listen pass + ] + ] + ] + + + +pU = Proxy :: Proxy () +pB = Proxy :: Proxy Bool +pI = Proxy :: Proxy Int + +pMb = Proxy :: Proxy Maybe +pEi = Proxy :: Proxy (Either Int) +pLs = Proxy :: Proxy [] + +pLs' = const Proxy :: Proxy a -> Proxy [a] + +pSU = Proxy :: Proxy (State ()) +pSB = Proxy :: Proxy (State Bool) +pSI = Proxy :: Proxy (State Int) + +pRU = Proxy :: Proxy (Reader ()) +pRB = Proxy :: Proxy (Reader Bool) +pRI = Proxy :: Proxy (Reader Int) + +pEU = Proxy :: Proxy (Error ()) +pEB = Proxy :: Proxy (Error Bool) +pEI = Proxy :: Proxy (Error Int) + +pWU = Proxy :: Proxy (Writer ()) +pWLs = const Proxy :: Proxy a -> Proxy (Writer [a]) + + + +-- Basic State Monad + +data State s a = State + { runState :: s -> (a,s) } + +stateEq + :: (Eq s, Eq a) + => s -> State s a -> State s a -> Bool +stateEq s x y = (runState x s) == (runState y s) + +instance Monad (State s) where + return a = State $ \s -> (a,s) + + x >>= f = State $ \s1 -> + let (a,s2) = runState x s1 + in runState (f a) s2 + +instance Applicative (State s) where + pure = return + (<*>) = ap + +instance Functor (State s) where + fmap f x = x >>= (return . f) + +instance (Arbitrary a) => Arbitrary (State s a) where + arbitrary = return <$> arbitrary + +get :: State s s +get = State $ \s -> (s,s) + +put :: s -> State s () +put s = State $ \_ -> ((),s) + + + +-- Basic Reader Monad + +data Reader r a = Reader + { runReader :: r -> a } + +readerEq + :: (Eq a) + => r -> Reader r a -> Reader r a -> Bool +readerEq r x y = (runReader x r) == (runReader y r) + +instance Monad (Reader r) where + return a = Reader $ \_ -> a + + x >>= f = Reader $ \r -> + let a = runReader x r + in runReader (f a) r + +instance Applicative (Reader r) where + pure = return + (<*>) = ap + +instance Functor (Reader r) where + fmap f x = x >>= (return . f) + +instance (Arbitrary a) => Arbitrary (Reader r a) where + arbitrary = return <$> arbitrary + +instance Show (Reader r a) where + show _ = "" + +ask :: Reader r r +ask = Reader $ \r -> r + +local :: (r -> r) -> Reader r a -> Reader r a +local u x = Reader $ \r -> runReader x (u r) + + + +-- Basic Error Monad + +data Error e a = Error + { runError :: Either e a + } deriving (Eq, Show) + +instance Monad (Error e) where + return a = Error (Right a) + + x >>= f = case x of + Error (Left e) -> Error (Left e) + Error (Right a) -> f a + +instance Applicative (Error e) where + pure = return + (<*>) = ap + +instance Functor (Error e) where + fmap f x = x >>= (return . f) + +instance (Arbitrary a, Arbitrary e) => Arbitrary (Error e a) where + arbitrary = Error <$> arbitrary + +throw :: e -> Error e a +throw e = Error (Left e) + +catch :: Error e a -> (e -> Error e a) -> Error e a +catch x h = case x of + Error (Right a) -> Error (Right a) + Error (Left e) -> h e + + + +-- Basic Writer Monad + +data Writer w a = Writer + { runWriter :: (a,w) + } deriving (Eq, Show) + +instance (Monoid w) => Monad (Writer w) where + return a = Writer (a, mempty) + + x >>= f = + let + (a,w1) = runWriter x + (b,w2) = runWriter (f a) + in + Writer (b, mappend w1 w2) + +instance (Monoid w) => Applicative (Writer w) where + pure = return + (<*>) = ap + +instance (Monoid w) => Functor (Writer w) where + fmap f x = x >>= (return . f) + +instance (Arbitrary w, Arbitrary a) => Arbitrary (Writer w a) where + arbitrary = Writer <$> arbitrary + +tell :: w -> Writer w () +tell w = Writer ((),w) + +draft :: (Monoid w) => Writer w a -> Writer w (a,w) +draft x = + let (a,w) = runWriter x + in Writer ((a,w), mempty) + +listen :: Writer w a -> Writer w (a,w) +listen x = + let (a,w) = runWriter x + in Writer ((a,w), w) + +pass :: Writer w (a, w -> w) -> Writer w a +pass x = + let + ((a,f),w) = runWriter x + in + Writer (a, f w)