{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE QuantifiedConstraints #-}
module Hedgehog.Classes.Category (categoryLaws, commutativeCategoryLaws) where
import Hedgehog
import Hedgehog.Classes.Common
import Control.Category(Category(..))
import Prelude hiding (id, (.))
categoryLaws :: forall f.
( Category f
, forall x y. (Eq x, Eq y) => Eq (f x y)
, forall x y. (Show x, Show y) => Show (f x y)
) => (forall x y. Gen x -> Gen y -> Gen (f x y)) -> Laws
categoryLaws :: forall (f :: * -> * -> *).
(Category f, forall x y. (Eq x, Eq y) => Eq (f x y),
forall x y. (Show x, Show y) => Show (f x y)) =>
(forall x y. Gen x -> Gen y -> Gen (f x y)) -> Laws
categoryLaws forall x y. Gen x -> Gen y -> Gen (f x y)
gen = String -> [(String, Property)] -> Laws
Laws String
"Category"
[ (String
"Left Identity", forall (f :: * -> * -> *).
(Category f, forall x y. (Eq x, Eq y) => Eq (f x y),
forall x y. (Show x, Show y) => Show (f x y)) =>
(forall x y. Gen x -> Gen y -> Gen (f x y)) -> Property
categoryLeftIdentity forall x y. Gen x -> Gen y -> Gen (f x y)
gen)
, (String
"Right Identity", forall (f :: * -> * -> *).
(Category f, forall x y. (Eq x, Eq y) => Eq (f x y),
forall x y. (Show x, Show y) => Show (f x y)) =>
(forall x y. Gen x -> Gen y -> Gen (f x y)) -> Property
categoryRightIdentity forall x y. Gen x -> Gen y -> Gen (f x y)
gen)
, (String
"Associativity", forall (f :: * -> * -> *).
(Category f, forall x y. (Eq x, Eq y) => Eq (f x y),
forall x y. (Show x, Show y) => Show (f x y)) =>
(forall x y. Gen x -> Gen y -> Gen (f x y)) -> Property
categoryAssociativity forall x y. Gen x -> Gen y -> Gen (f x y)
gen)
]
commutativeCategoryLaws :: forall f.
( Category f
, forall x y. (Eq x, Eq y) => Eq (f x y)
, forall x y. (Show x, Show y) => Show (f x y)
) => (forall x y. Gen x -> Gen y -> Gen (f x y)) -> Laws
commutativeCategoryLaws :: forall (f :: * -> * -> *).
(Category f, forall x y. (Eq x, Eq y) => Eq (f x y),
forall x y. (Show x, Show y) => Show (f x y)) =>
(forall x y. Gen x -> Gen y -> Gen (f x y)) -> Laws
commutativeCategoryLaws forall x y. Gen x -> Gen y -> Gen (f x y)
gen = String -> [(String, Property)] -> Laws
Laws String
"Commutative Category"
[ (String
"Commutativity", forall (f :: * -> * -> *).
(Category f, forall x y. (Eq x, Eq y) => Eq (f x y),
forall x y. (Show x, Show y) => Show (f x y)) =>
(forall x y. Gen x -> Gen y -> Gen (f x y)) -> Property
categoryCommutativity forall x y. Gen x -> Gen y -> Gen (f x y)
gen)
]
categoryRightIdentity :: forall f.
( Category f
, forall x y. (Eq x, Eq y) => Eq (f x y)
, forall x y. (Show x, Show y) => Show (f x y)
) => (forall x y. Gen x -> Gen y -> Gen (f x y)) -> Property
categoryRightIdentity :: forall (f :: * -> * -> *).
(Category f, forall x y. (Eq x, Eq y) => Eq (f x y),
forall x y. (Show x, Show y) => Show (f x y)) =>
(forall x y. Gen x -> Gen y -> Gen (f x y)) -> Property
categoryRightIdentity forall x y. Gen x -> Gen y -> Gen (f x y)
fgen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
f Integer Integer
x <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$ forall x y. Gen x -> Gen y -> Gen (f x y)
fgen Gen Integer
genSmallInteger Gen Integer
genSmallInteger
(f Integer Integer
x forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id) forall (m :: * -> *) a b (f :: * -> * -> *).
(MonadTest m, HasCallStack, Eq a, Eq b, Show a, Show b,
forall x y. (Eq x, Eq y) => Eq (f x y),
forall x y. (Show x, Show y) => Show (f x y)) =>
f a b -> f a b -> m ()
`heq2` f Integer Integer
x
categoryLeftIdentity :: forall f.
( Category f
, forall x y. (Eq x, Eq y) => Eq (f x y)
, forall x y. (Show x, Show y) => Show (f x y)
) => (forall x y. Gen x -> Gen y -> Gen (f x y)) -> Property
categoryLeftIdentity :: forall (f :: * -> * -> *).
(Category f, forall x y. (Eq x, Eq y) => Eq (f x y),
forall x y. (Show x, Show y) => Show (f x y)) =>
(forall x y. Gen x -> Gen y -> Gen (f x y)) -> Property
categoryLeftIdentity forall x y. Gen x -> Gen y -> Gen (f x y)
fgen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
f Integer Integer
x <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$ forall x y. Gen x -> Gen y -> Gen (f x y)
fgen Gen Integer
genSmallInteger Gen Integer
genSmallInteger
(forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. f Integer Integer
x) forall (m :: * -> *) a b (f :: * -> * -> *).
(MonadTest m, HasCallStack, Eq a, Eq b, Show a, Show b,
forall x y. (Eq x, Eq y) => Eq (f x y),
forall x y. (Show x, Show y) => Show (f x y)) =>
f a b -> f a b -> m ()
`heq2` f Integer Integer
x
categoryAssociativity :: forall f.
( Category f
, forall x y. (Eq x, Eq y) => Eq (f x y)
, forall x y. (Show x, Show y) => Show (f x y)
) => (forall x y. Gen x -> Gen y -> Gen (f x y)) -> Property
categoryAssociativity :: forall (f :: * -> * -> *).
(Category f, forall x y. (Eq x, Eq y) => Eq (f x y),
forall x y. (Show x, Show y) => Show (f x y)) =>
(forall x y. Gen x -> Gen y -> Gen (f x y)) -> Property
categoryAssociativity forall x y. Gen x -> Gen y -> Gen (f x y)
fgen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
f Integer Integer
f <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$ forall x y. Gen x -> Gen y -> Gen (f x y)
fgen Gen Integer
genSmallInteger Gen Integer
genSmallInteger
f Integer Integer
g <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$ forall x y. Gen x -> Gen y -> Gen (f x y)
fgen Gen Integer
genSmallInteger Gen Integer
genSmallInteger
f Integer Integer
h <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$ forall x y. Gen x -> Gen y -> Gen (f x y)
fgen Gen Integer
genSmallInteger Gen Integer
genSmallInteger
(f Integer Integer
f forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (f Integer Integer
g forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. f Integer Integer
h)) forall (m :: * -> *) a b (f :: * -> * -> *).
(MonadTest m, HasCallStack, Eq a, Eq b, Show a, Show b,
forall x y. (Eq x, Eq y) => Eq (f x y),
forall x y. (Show x, Show y) => Show (f x y)) =>
f a b -> f a b -> m ()
`heq2` ((f Integer Integer
f forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. f Integer Integer
g) forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. f Integer Integer
h)
categoryCommutativity :: forall f.
( Category f
, forall x y. (Eq x, Eq y) => Eq (f x y)
, forall x y. (Show x, Show y) => Show (f x y)
) => (forall x y. Gen x -> Gen y -> Gen (f x y)) -> Property
categoryCommutativity :: forall (f :: * -> * -> *).
(Category f, forall x y. (Eq x, Eq y) => Eq (f x y),
forall x y. (Show x, Show y) => Show (f x y)) =>
(forall x y. Gen x -> Gen y -> Gen (f x y)) -> Property
categoryCommutativity forall x y. Gen x -> Gen y -> Gen (f x y)
fgen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
f Integer Integer
f <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$ forall x y. Gen x -> Gen y -> Gen (f x y)
fgen Gen Integer
genSmallInteger Gen Integer
genSmallInteger
f Integer Integer
g <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$ forall x y. Gen x -> Gen y -> Gen (f x y)
fgen Gen Integer
genSmallInteger Gen Integer
genSmallInteger
(f Integer Integer
f forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. f Integer Integer
g) forall (m :: * -> *) a b (f :: * -> * -> *).
(MonadTest m, HasCallStack, Eq a, Eq b, Show a, Show b,
forall x y. (Eq x, Eq y) => Eq (f x y),
forall x y. (Show x, Show y) => Show (f x y)) =>
f a b -> f a b -> m ()
`heq2` (f Integer Integer
g forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. f Integer Integer
f)