{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}

module Hedgehog.Classes.Monad (monadLaws) where

import Control.Monad (ap)

import Hedgehog
import Hedgehog.Classes.Common

-- | Tests the following 'Monad' laws:
--
-- [__Left Identity__]: @'return' a '>>=' k@ ≡ @k a@
-- [__Right Identity__]: @m '>>=' 'return'@ ≡ @m@
-- [__Associativity__]: @m '>>=' (\\x -> k x '>>=' h)@ ≡ @(m '>>=' k) '>>=' h@
-- [__Return__]: @'return'@ ≡ @'pure'@
-- [__Ap__]: @'ap' f x@ ≡ @f '<*>' x@
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 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 x. Gen x -> Gen (f x)) -> Property
forall (f :: * -> *). MonadProp f
monadLeftIdentity forall x. Gen x -> Gen (f x)
gen)
  , (String
"Right Identity", (forall x. Gen x -> Gen (f x)) -> Property
forall (f :: * -> *). MonadProp f
monadRightIdentity forall x. Gen x -> Gen (f x)
gen)
  , (String
"Associativity", (forall x. Gen x -> Gen (f x)) -> Property
forall (f :: * -> *). MonadProp f
monadAssociativity forall x. Gen x -> Gen (f x)
gen)
  , (String
"Return", (forall x. Gen x -> Gen (f x)) -> Property
forall (f :: * -> *). MonadProp f
monadReturn forall x. Gen x -> Gen (f x)
gen)
  , (String
"Ap", (forall x. Gen x -> Gen (f x)) -> Property
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 x. Gen x -> Gen (f x)) -> Property
monadLeftIdentity forall x. Gen x -> Gen (f x)
_ = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
  LinearEquationM f
k' :: LinearEquationM f <- Gen (LinearEquationM f) -> PropertyT IO (LinearEquationM f)
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen (LinearEquationM f)
forall (m :: * -> *). Applicative m => Gen (LinearEquationM m)
genLinearEquationM
  Integer
a <- Gen Integer -> PropertyT IO Integer
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (Gen Integer -> PropertyT IO Integer)
-> Gen Integer -> PropertyT IO Integer
forall a b. (a -> b) -> a -> b
$ Gen Integer
genSmallInteger
  let k :: Integer -> f Integer
k = LinearEquationM f -> Integer -> f Integer
forall (m :: * -> *).
Functor m =>
LinearEquationM m -> Integer -> m Integer
runLinearEquationM LinearEquationM f
k'

  let lhs :: f Integer
lhs = Integer -> f Integer
forall (m :: * -> *) a. Monad m => a -> m a
return Integer
a f Integer -> (Integer -> f Integer) -> f Integer
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 (LawContext -> Context) -> LawContext -> Context
forall a b. (a -> b) -> a -> b
$ LawContext :: String -> String -> String -> String -> String -> LawContext
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 = f Integer -> f Integer -> String
forall a. Show a => a -> a -> String
reduced f Integer
lhs f Integer
rhs
        , lawContextTcProp :: String
lawContextTcProp =
            let showK :: String
showK = LinearEquationM f -> String
forall a. Show a => a -> String
show LinearEquationM f
k'
                showA :: String
showA = Integer -> String
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 = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showK
              , String
"a = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showA
              ]
        }
  f Integer -> f Integer -> Context -> PropertyT IO ()
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 x. Gen x -> Gen (f x)) -> Property
monadRightIdentity forall x. Gen x -> Gen (f x)
fgen = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
  f Integer
m <- Gen (f Integer) -> PropertyT IO (f Integer)
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (Gen (f Integer) -> PropertyT IO (f Integer))
-> Gen (f Integer) -> PropertyT IO (f Integer)
forall a b. (a -> b) -> a -> b
$ Gen Integer -> Gen (f Integer)
forall x. Gen x -> Gen (f x)
fgen Gen Integer
genSmallInteger
  let lhs :: f Integer
lhs = f Integer
m f Integer -> (Integer -> f Integer) -> f Integer
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Integer -> f Integer
forall (m :: * -> *) a. Monad m => a -> m a
return
  let rhs :: f Integer
rhs = f Integer
m
  let ctx :: Context
ctx = LawContext -> Context
contextualise (LawContext -> Context) -> LawContext -> Context
forall a b. (a -> b) -> a -> b
$ LawContext :: String -> String -> String -> String -> String -> LawContext
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 = f Integer -> f Integer -> String
forall a. Show a => a -> a -> String
reduced f Integer
lhs f Integer
rhs
        , lawContextTcProp :: String
lawContextTcProp =
            let showM :: String
showM = f Integer -> String
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 = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showM
              ]
        }
  f Integer -> f Integer -> Context -> PropertyT IO ()
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 x. Gen x -> Gen (f x)) -> Property
monadAssociativity forall x. Gen x -> Gen (f x)
fgen = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
  f Integer
m <- Gen (f Integer) -> PropertyT IO (f Integer)
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (Gen (f Integer) -> PropertyT IO (f Integer))
-> Gen (f Integer) -> PropertyT IO (f Integer)
forall a b. (a -> b) -> a -> b
$ Gen Integer -> Gen (f Integer)
forall x. Gen x -> Gen (f x)
fgen Gen Integer
genSmallInteger
  LinearEquationM f
k' :: LinearEquationM f <- Gen (LinearEquationM f) -> PropertyT IO (LinearEquationM f)
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen (LinearEquationM f)
forall (m :: * -> *). Applicative m => Gen (LinearEquationM m)
genLinearEquationM
  LinearEquationM f
h' :: LinearEquationM f <- Gen (LinearEquationM f) -> PropertyT IO (LinearEquationM f)
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen (LinearEquationM f)
forall (m :: * -> *). Applicative m => Gen (LinearEquationM m)
genLinearEquationM
  let k :: Integer -> f Integer
k = LinearEquationM f -> Integer -> f Integer
forall (m :: * -> *).
Functor m =>
LinearEquationM m -> Integer -> m Integer
runLinearEquationM LinearEquationM f
k'
      h :: Integer -> f Integer
h = LinearEquationM f -> Integer -> f Integer
forall (m :: * -> *).
Functor m =>
LinearEquationM m -> Integer -> m Integer
runLinearEquationM LinearEquationM f
h'
  let lhs :: f Integer
lhs = f Integer
m f Integer -> (Integer -> f Integer) -> f Integer
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\Integer
x -> Integer -> f Integer
k Integer
x f Integer -> (Integer -> f Integer) -> f Integer
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 f Integer -> (Integer -> f Integer) -> f Integer
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Integer -> f Integer
k) f Integer -> (Integer -> f Integer) -> f Integer
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Integer -> f Integer
h
  let ctx :: Context
ctx = LawContext -> Context
contextualise (LawContext -> Context) -> LawContext -> Context
forall a b. (a -> b) -> a -> b
$ LawContext :: String -> String -> String -> String -> String -> LawContext
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 = f Integer -> f Integer -> String
forall a. Show a => a -> a -> String
reduced f Integer
lhs f Integer
rhs
        , lawContextTcProp :: String
lawContextTcProp =
            let showM :: String
showM = f Integer -> String
forall a. Show a => a -> String
show f Integer
m
                showK :: String
showK = LinearEquationM f -> String
forall a. Show a => a -> String
show LinearEquationM f
k'
                showH :: String
showH = LinearEquationM f -> String
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 = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showM
              , String
"k = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showK
              , String
"h = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showH
              ]
        }
  f Integer -> f Integer -> Context -> PropertyT IO ()
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 x. Gen x -> Gen (f x)) -> Property
monadReturn forall x. Gen x -> Gen (f x)
_ = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
  Integer
x <- Gen Integer -> PropertyT IO Integer
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen Integer
genSmallInteger
  let lhs :: f Integer
lhs = Integer -> f Integer
forall (m :: * -> *) a. Monad m => a -> m a
return Integer
x
  let rhs :: f Integer
rhs = Integer -> f Integer
forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
x :: f Integer
  let ctx :: Context
ctx = LawContext -> Context
contextualise (LawContext -> Context) -> LawContext -> Context
forall a b. (a -> b) -> a -> b
$ LawContext :: String -> String -> String -> String -> String -> LawContext
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 = f Integer -> f Integer -> String
forall a. Show a => a -> a -> String
reduced f Integer
lhs f Integer
rhs
        , lawContextTcProp :: String
lawContextTcProp =
            let showX :: String
showX = Integer -> String
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 = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showX
              ]
        }
  f Integer -> f Integer -> Context -> PropertyT IO ()
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 x. Gen x -> Gen (f x)) -> Property
monadAp forall x. Gen x -> Gen (f x)
_ = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
  f QuadraticEquation
f' :: f QuadraticEquation <- Gen (f QuadraticEquation) -> PropertyT IO (f QuadraticEquation)
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (Gen (f QuadraticEquation) -> PropertyT IO (f QuadraticEquation))
-> Gen (f QuadraticEquation) -> PropertyT IO (f QuadraticEquation)
forall a b. (a -> b) -> a -> b
$ QuadraticEquation -> f QuadraticEquation
forall (f :: * -> *) a. Applicative f => a -> f a
pure (QuadraticEquation -> f QuadraticEquation)
-> GenT Identity QuadraticEquation -> Gen (f QuadraticEquation)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenT Identity QuadraticEquation
genQuadraticEquation
  f Integer
x :: f Integer <- Gen (f Integer) -> PropertyT IO (f Integer)
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (Gen (f Integer) -> PropertyT IO (f Integer))
-> Gen (f Integer) -> PropertyT IO (f Integer)
forall a b. (a -> b) -> a -> b
$ Integer -> f Integer
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> f Integer) -> Gen Integer -> Gen (f Integer)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Integer
genSmallInteger
  let f :: f (Integer -> Integer)
f = (QuadraticEquation -> Integer -> Integer)
-> f QuadraticEquation -> f (Integer -> Integer)
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 = f (Integer -> Integer) -> f Integer -> f Integer
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 f (Integer -> Integer) -> f Integer -> f Integer
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f Integer
x
  let ctx :: Context
ctx = LawContext -> Context
contextualise (LawContext -> Context) -> LawContext -> Context
forall a b. (a -> b) -> a -> b
$ LawContext :: String -> String -> String -> String -> String -> LawContext
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 = f Integer -> f Integer -> String
forall a. Show a => a -> a -> String
reduced f Integer
lhs f Integer
rhs
        , lawContextTcProp :: String
lawContextTcProp =
            let showX :: String
showX = f Integer -> String
forall a. Show a => a -> String
show f Integer
x
                showF :: String
showF = f QuadraticEquation -> String
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 = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showF
              , String
"x = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
showX
              ]
        }
  f Integer -> f Integer -> Context -> PropertyT IO ()
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