{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
module Hedgehog.Classes.Monad (monadLaws) where
import Control.Monad (ap)
import Hedgehog
import Hedgehog.Classes.Common
monadLaws ::
( Monad f
, forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
) => (forall x. Gen x -> Gen (f x)) -> Laws
monadLaws :: forall (f :: * -> *).
(Monad f, forall x. Eq x => Eq (f x),
forall x. Show x => Show (f x)) =>
(forall x. Gen x -> Gen (f x)) -> Laws
monadLaws forall x. Gen x -> Gen (f x)
gen = String -> [(String, Property)] -> Laws
Laws String
"Monad"
[ (String
"Left Identity", forall (f :: * -> *). MonadProp f
monadLeftIdentity forall x. Gen x -> Gen (f x)
gen)
, (String
"Right Identity", forall (f :: * -> *). MonadProp f
monadRightIdentity forall x. Gen x -> Gen (f x)
gen)
, (String
"Associativity", forall (f :: * -> *). MonadProp f
monadAssociativity forall x. Gen x -> Gen (f x)
gen)
, (String
"Return", forall (f :: * -> *). MonadProp f
monadReturn forall x. Gen x -> Gen (f x)
gen)
, (String
"Ap", forall (f :: * -> *). MonadProp f
monadAp forall x. Gen x -> Gen (f x)
gen)
]
type MonadProp f =
( Monad f
, forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
) => (forall x. Gen x -> Gen (f x)) -> Property
monadLeftIdentity :: forall f. MonadProp f
monadLeftIdentity :: forall (f :: * -> *). MonadProp f
monadLeftIdentity forall x. Gen x -> Gen (f x)
_ = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
LinearEquationM f
k' :: LinearEquationM f <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall (m :: * -> *). Applicative m => Gen (LinearEquationM m)
genLinearEquationM
Integer
a <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$ Gen Integer
genSmallInteger
let k :: Integer -> f Integer
k = forall (m :: * -> *).
Functor m =>
LinearEquationM m -> Integer -> m Integer
runLinearEquationM LinearEquationM f
k'
let lhs :: f Integer
lhs = forall (m :: * -> *) a. Monad m => a -> m a
return Integer
a forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Integer -> f Integer
k
let rhs :: f Integer
rhs = Integer -> f Integer
k Integer
a
let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ LawContext
{ lawContextLawName :: String
lawContextLawName = String
"Left Identity", lawContextTcName :: String
lawContextTcName = String
"Monad"
, lawContextLawBody :: String
lawContextLawBody = String
"return a >>= k" String -> String -> String
`congruency` String
"k a"
, lawContextReduced :: String
lawContextReduced = forall a. Show a => a -> a -> String
reduced f Integer
lhs f Integer
rhs
, lawContextTcProp :: String
lawContextTcProp =
let showK :: String
showK = forall a. Show a => a -> String
show LinearEquationM f
k'
showA :: String
showA = forall a. Show a => a -> String
show Integer
a
in [String] -> String
lawWhere
[ String
"return a >>= k" String -> String -> String
`congruency` String
"k a, where"
, String
"k = " forall a. [a] -> [a] -> [a]
++ String
showK
, String
"a = " forall a. [a] -> [a] -> [a]
++ String
showA
]
}
forall (m :: * -> *) a (f :: * -> *).
(MonadTest m, HasCallStack, Eq a, Show a,
forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)) =>
f a -> f a -> Context -> m ()
heqCtx1 f Integer
lhs f Integer
rhs Context
ctx
monadRightIdentity :: forall f. MonadProp f
monadRightIdentity :: forall (f :: * -> *). MonadProp f
monadRightIdentity forall x. Gen x -> Gen (f x)
fgen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
f Integer
m <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$ forall x. Gen x -> Gen (f x)
fgen Gen Integer
genSmallInteger
let lhs :: f Integer
lhs = f Integer
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *) a. Monad m => a -> m a
return
let rhs :: f Integer
rhs = f Integer
m
let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ LawContext
{ lawContextLawName :: String
lawContextLawName = String
"Right Identity", lawContextTcName :: String
lawContextTcName = String
"Monad"
, lawContextLawBody :: String
lawContextLawBody = String
"m >>= return" String -> String -> String
`congruency` String
"m"
, lawContextReduced :: String
lawContextReduced = forall a. Show a => a -> a -> String
reduced f Integer
lhs f Integer
rhs
, lawContextTcProp :: String
lawContextTcProp =
let showM :: String
showM = forall a. Show a => a -> String
show f Integer
m
in [String] -> String
lawWhere
[ String
"m >>= return" String -> String -> String
`congruency` String
"m, where"
, String
"m = " forall a. [a] -> [a] -> [a]
++ String
showM
]
}
forall (m :: * -> *) a (f :: * -> *).
(MonadTest m, HasCallStack, Eq a, Show a,
forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)) =>
f a -> f a -> Context -> m ()
heqCtx1 f Integer
lhs f Integer
rhs Context
ctx
monadAssociativity :: forall f. MonadProp f
monadAssociativity :: forall (f :: * -> *). MonadProp f
monadAssociativity forall x. Gen x -> Gen (f x)
fgen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
f Integer
m <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$ forall x. Gen x -> Gen (f x)
fgen Gen Integer
genSmallInteger
LinearEquationM f
k' :: LinearEquationM f <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall (m :: * -> *). Applicative m => Gen (LinearEquationM m)
genLinearEquationM
LinearEquationM f
h' :: LinearEquationM f <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall (m :: * -> *). Applicative m => Gen (LinearEquationM m)
genLinearEquationM
let k :: Integer -> f Integer
k = forall (m :: * -> *).
Functor m =>
LinearEquationM m -> Integer -> m Integer
runLinearEquationM LinearEquationM f
k'
h :: Integer -> f Integer
h = forall (m :: * -> *).
Functor m =>
LinearEquationM m -> Integer -> m Integer
runLinearEquationM LinearEquationM f
h'
let lhs :: f Integer
lhs = f Integer
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\Integer
x -> Integer -> f Integer
k Integer
x forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Integer -> f Integer
h)
let rhs :: f Integer
rhs = (f Integer
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Integer -> f Integer
k) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Integer -> f Integer
h
let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ LawContext
{ lawContextLawName :: String
lawContextLawName = String
"Associativity", lawContextTcName :: String
lawContextTcName = String
"Monad"
, lawContextLawBody :: String
lawContextLawBody = String
"m >>= (\\x -> k x >>= h)" String -> String -> String
`congruency` String
"(m >>= k) >>= h"
, lawContextReduced :: String
lawContextReduced = forall a. Show a => a -> a -> String
reduced f Integer
lhs f Integer
rhs
, lawContextTcProp :: String
lawContextTcProp =
let showM :: String
showM = forall a. Show a => a -> String
show f Integer
m
showK :: String
showK = forall a. Show a => a -> String
show LinearEquationM f
k'
showH :: String
showH = forall a. Show a => a -> String
show LinearEquationM f
h'
in [String] -> String
lawWhere
[ String
"m >>= (\\x -> k x >>= h)" String -> String -> String
`congruency` String
"(m >>= k) >>= h, where"
, String
"m = " forall a. [a] -> [a] -> [a]
++ String
showM
, String
"k = " forall a. [a] -> [a] -> [a]
++ String
showK
, String
"h = " forall a. [a] -> [a] -> [a]
++ String
showH
]
}
forall (m :: * -> *) a (f :: * -> *).
(MonadTest m, HasCallStack, Eq a, Show a,
forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)) =>
f a -> f a -> Context -> m ()
heqCtx1 f Integer
lhs f Integer
rhs Context
ctx
monadReturn :: forall f. MonadProp f
monadReturn :: forall (f :: * -> *). MonadProp f
monadReturn forall x. Gen x -> Gen (f x)
_ = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
Integer
x <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen Integer
genSmallInteger
let lhs :: f Integer
lhs = forall (m :: * -> *) a. Monad m => a -> m a
return Integer
x
let rhs :: f Integer
rhs = forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
x :: f Integer
let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ LawContext
{ lawContextLawName :: String
lawContextLawName = String
"Return", lawContextTcName :: String
lawContextTcName = String
"Monad"
, lawContextLawBody :: String
lawContextLawBody = String
"return" String -> String -> String
`congruency` String
"pure"
, lawContextReduced :: String
lawContextReduced = forall a. Show a => a -> a -> String
reduced f Integer
lhs f Integer
rhs
, lawContextTcProp :: String
lawContextTcProp =
let showX :: String
showX = forall a. Show a => a -> String
show Integer
x
in [String] -> String
lawWhere
[ String
"return x" String -> String -> String
`congruency` String
"pure x, where"
, String
"x = " forall a. [a] -> [a] -> [a]
++ String
showX
]
}
forall (m :: * -> *) a (f :: * -> *).
(MonadTest m, HasCallStack, Eq a, Show a,
forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)) =>
f a -> f a -> Context -> m ()
heqCtx1 f Integer
lhs f Integer
rhs Context
ctx
monadAp :: forall f. MonadProp f
monadAp :: forall (f :: * -> *). MonadProp f
monadAp forall x. Gen x -> Gen (f x)
_ = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
f QuadraticEquation
f' :: f QuadraticEquation <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen QuadraticEquation
genQuadraticEquation
f Integer
x :: f Integer <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Applicative f => a -> f a
pure forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Integer
genSmallInteger
let f :: f (Integer -> Integer)
f = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap QuadraticEquation -> Integer -> Integer
runQuadraticEquation f QuadraticEquation
f'
let lhs :: f Integer
lhs = forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap f (Integer -> Integer)
f f Integer
x
let rhs :: f Integer
rhs = f (Integer -> Integer)
f forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f Integer
x
let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ LawContext
{ lawContextLawName :: String
lawContextLawName = String
"Ap", lawContextTcName :: String
lawContextTcName = String
"Monad"
, lawContextLawBody :: String
lawContextLawBody = String
"ap f" String -> String -> String
`congruency` String
"f <*>"
, lawContextReduced :: String
lawContextReduced = forall a. Show a => a -> a -> String
reduced f Integer
lhs f Integer
rhs
, lawContextTcProp :: String
lawContextTcProp =
let showX :: String
showX = forall a. Show a => a -> String
show f Integer
x
showF :: String
showF = forall a. Show a => a -> String
show f QuadraticEquation
f'
in [String] -> String
lawWhere
[ String
"ap f x" String -> String -> String
`congruency` String
"f <*> x, where"
, String
"f = " forall a. [a] -> [a] -> [a]
++ String
showF
, String
"x = " forall a. [a] -> [a] -> [a]
++ String
showX
]
}
forall (m :: * -> *) a (f :: * -> *).
(MonadTest m, HasCallStack, Eq a, Show a,
forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)) =>
f a -> f a -> Context -> m ()
heqCtx1 f Integer
lhs f Integer
rhs Context
ctx