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

module Hedgehog.Classes.Applicative (applicativeLaws) where

import Control.Applicative (Applicative(..))

import Hedgehog
import Hedgehog.Classes.Common

-- | Tests the following 'Applicative' laws:
--
-- [__Identity__]: @'pure' 'id' '<*>' v@ ≡ @v@
-- [__Composition__]: @'pure' ('.') '<*>' u '<*>' v '<*>' w@ ≡ @u '<*>' (v '<*>' w)@
-- [__Homomorphism__]: @'pure' f '<*>' 'pure'@ x ≡ @'pure' (f x)@
-- [__Interchange__]: @u '<*>' 'pure' y@ ≡ @'pure' ('$' y) '<*>' u@
-- [__LiftA2 1__]: @'liftA2' 'id' f x@ ≡ @f '<*>' x@
-- [__LiftA2 2__]: @'liftA2' f x y@ ≡ @f '<$>' x '<*>' y@
applicativeLaws ::
  ( Applicative f
  , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
  ) => (forall x. Gen x -> Gen (f x)) -> Laws
applicativeLaws :: forall (f :: * -> *).
(Applicative f, forall x. Eq x => Eq (f x),
 forall x. Show x => Show (f x)) =>
(forall x. Gen x -> Gen (f x)) -> Laws
applicativeLaws forall x. Gen x -> Gen (f x)
gen = String -> [(String, Property)] -> Laws
Laws String
"Applicative"
  [ (String
"Identity", forall (f :: * -> *). ApplicativeProp f
applicativeIdentity forall x. Gen x -> Gen (f x)
gen)
  , (String
"Composition", forall (f :: * -> *). ApplicativeProp f
applicativeComposition forall x. Gen x -> Gen (f x)
gen)
  , (String
"Homomorphism", forall (f :: * -> *). ApplicativeProp f
applicativeHomomorphism forall x. Gen x -> Gen (f x)
gen)
  , (String
"Interchange", forall (f :: * -> *). ApplicativeProp f
applicativeInterchange forall x. Gen x -> Gen (f x)
gen)
  , (String
"LiftA2 Part 1", forall (f :: * -> *). ApplicativeProp f
applicativeLiftA2_1 forall x. Gen x -> Gen (f x)
gen)
  , (String
"LiftA2 Part 2", forall (f :: * -> *). ApplicativeProp f
applicativeLiftA2_2 forall x. Gen x -> Gen (f x)
gen) 
  ]

type ApplicativeProp f =
  ( Applicative f
  , forall x. Eq x => Eq (f x), forall x. Show x => Show (f x)
  ) => (forall x. Gen x -> Gen (f x)) -> Property

applicativeIdentity :: forall f. ApplicativeProp f
applicativeIdentity :: forall (f :: * -> *). ApplicativeProp f
applicativeIdentity forall x. Gen x -> Gen (f x)
fgen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  f Integer
a <- 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 = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. a -> a
id forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f Integer
a
  let rhs :: f Integer
rhs = f Integer
a
  let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ LawContext
        { lawContextLawName :: String
lawContextLawName = String
"Identity", lawContextLawBody :: String
lawContextLawBody = String
"pure id <*> v" String -> String -> String
`congruency` String
"v"
        , lawContextTcName :: String
lawContextTcName = String
"Applicative", lawContextTcProp :: String
lawContextTcProp =
             let showA :: String
showA = forall a. Show a => a -> String
show f Integer
a
             in [String] -> String
lawWhere
                 [ String
"pure id <*> v" String -> String -> String
`congruency` String
"v, where"
                 , String
"v = " forall a. [a] -> [a] -> [a]
++ String
showA
                 ]
        , lawContextReduced :: String
lawContextReduced = forall a. Show a => a -> a -> String
reduced f Integer
lhs f Integer
rhs
        }
  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

applicativeComposition :: forall f. ApplicativeProp f
applicativeComposition :: forall (f :: * -> *). ApplicativeProp f
applicativeComposition forall x. Gen x -> Gen (f x)
fgen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  f QuadraticEquation
u' <- 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 QuadraticEquation
genQuadraticEquation
  f QuadraticEquation
v' <- 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 QuadraticEquation
genQuadraticEquation
  Integer
w' <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen Integer
genSmallInteger
  let u :: f (Integer -> Integer)
u = QuadraticEquation -> Integer -> Integer
runQuadraticEquation forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f QuadraticEquation
u'
      v :: f (Integer -> Integer)
v = QuadraticEquation -> Integer -> Integer
runQuadraticEquation forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f QuadraticEquation
v'
      w :: f Integer
w = forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
w'
  let lhs :: f Integer
lhs = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f (Integer -> Integer)
u forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f (Integer -> Integer)
v forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f Integer
w
  let rhs :: f Integer
rhs = f (Integer -> Integer)
u forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (f (Integer -> Integer)
v forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f Integer
w)
  let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ LawContext
        { lawContextLawName :: String
lawContextLawName = String
"Composition", lawContextLawBody :: String
lawContextLawBody = String
"pure (.) <*> u <*> v <*> w == u <*> (v <*> w)"
        , lawContextTcName :: String
lawContextTcName = String
"Applicative", lawContextTcProp :: String
lawContextTcProp =
            let showU :: String
showU = forall a. Show a => a -> String
show f QuadraticEquation
u'; showV :: String
showV = forall a. Show a => a -> String
show f QuadraticEquation
v'; showW :: String
showW = forall a. Show a => a -> String
show Integer
w';
            in [String] -> String
lawWhere
                 [ String
"pure (.) <*> u <*> v <*> w", String
congruent, String
"u <*> (v <*> w), where"
                 , String
"u = " forall a. [a] -> [a] -> [a]
++ String
showU
                 , String
"v = " forall a. [a] -> [a] -> [a]
++ String
showV
                 , String
"w = " forall a. [a] -> [a] -> [a]
++ String
showW
                 ]
        , lawContextReduced :: String
lawContextReduced = forall a. Show a => a -> a -> String
reduced f Integer
lhs f Integer
rhs
        }

  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

applicativeHomomorphism :: forall f. ApplicativeProp f
applicativeHomomorphism :: forall (f :: * -> *). ApplicativeProp f
applicativeHomomorphism forall x. Gen x -> Gen (f x)
_ = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  QuadraticEquation
e <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen QuadraticEquation
genQuadraticEquation
  Integer
a <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen Integer
genSmallInteger
  let f :: Integer -> Integer
f = QuadraticEquation -> Integer -> Integer
runQuadraticEquation QuadraticEquation
e
  let lhs :: f Integer
lhs = forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer -> Integer
f forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
a
  let rhs :: f Integer
rhs = forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> Integer
f Integer
a) :: f Integer
  let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ LawContext
        { lawContextLawName :: String
lawContextLawName = String
"Homomorphism", lawContextLawBody :: String
lawContextLawBody = String
"pure f <*> pure x" String -> String -> String
`congruency` String
"pure (f x)"
        , lawContextTcName :: String
lawContextTcName = String
"Applicative", lawContextTcProp :: String
lawContextTcProp =
            let showF :: String
showF = forall a. Show a => a -> String
show QuadraticEquation
e; showX :: String
showX = forall a. Show a => a -> String
show Integer
a;
            in [String] -> String
lawWhere
              [ String
"pure f <*> pure x", String
congruent, String
"pure (f x), where"
              , String
"f = " forall a. [a] -> [a] -> [a]
++ String
showF
              , String
"x = " forall a. [a] -> [a] -> [a]
++ String
showX
              ]
        , lawContextReduced :: String
lawContextReduced = forall a. Show a => a -> a -> String
reduced f Integer
lhs f Integer
rhs
        }
  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

applicativeInterchange :: forall f. ApplicativeProp f
applicativeInterchange :: forall (f :: * -> *). ApplicativeProp f
applicativeInterchange forall x. Gen x -> Gen (f x)
fgen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  f QuadraticEquation
u' <- 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 QuadraticEquation
genQuadraticEquation
  Integer
y <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen Integer
genSmallInteger
  let u :: f (Integer -> Integer)
u = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap QuadraticEquation -> Integer -> Integer
runQuadraticEquation f QuadraticEquation
u'
  let lhs :: f Integer
lhs = (f (Integer -> Integer)
u forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
y)
  let rhs :: f Integer
rhs = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. (a -> b) -> a -> b
$ Integer
y) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f (Integer -> Integer)
u
  let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ LawContext
        { lawContextLawName :: String
lawContextLawName = String
"Interchange", lawContextLawBody :: String
lawContextLawBody = String
"u <*> pure y" String -> String -> String
`congruency` String
"pure ($ y) <*> u"
        , lawContextTcName :: String
lawContextTcName = String
"Applicative", lawContextTcProp :: String
lawContextTcProp =
            let showU :: String
showU = forall a. Show a => a -> String
show f QuadraticEquation
u'; showY :: String
showY = forall a. Show a => a -> String
show Integer
y;
            in [String] -> String
lawWhere
              [ String
"u <*> pure y", String
congruent, String
"pure ($ y) <*> u, where"
              , String
"u = " forall a. [a] -> [a] -> [a]
++ String
showU
              , String
"y = " forall a. [a] -> [a] -> [a]
++ String
showY
              ]
        , lawContextReduced :: String
lawContextReduced = forall a. Show a => a -> a -> String
reduced f Integer
lhs f Integer
rhs
        }
  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

applicativeLiftA2_1 :: forall f. ApplicativeProp f
applicativeLiftA2_1 :: forall (f :: * -> *). ApplicativeProp f
applicativeLiftA2_1 forall x. Gen x -> Gen (f x)
fgen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  f QuadraticEquation
f' <- 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 QuadraticEquation
genQuadraticEquation
  f 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. Gen x -> Gen (f x)
fgen 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 (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 forall a. a -> a
id 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
"LiftA2 1", lawContextLawBody :: String
lawContextLawBody = String
"liftA2 id f x" String -> String -> String
`congruency` String
"f <*> x"
        , lawContextTcName :: String
lawContextTcName = String
"Applicative", lawContextTcProp :: String
lawContextTcProp =
            let showF :: String
showF = forall a. Show a => a -> String
show f QuadraticEquation
f'; showX :: String
showX = forall a. Show a => a -> String
show f Integer
x;
            in [String] -> String
lawWhere
              [ String
"liftA2 id f x", String
congruent, String
"f <*> x, where"
              , String
"f = " forall a. [a] -> [a] -> [a]
++ String
showF
              , String
"x = " forall a. [a] -> [a] -> [a]
++ String
showX
              ]
        , lawContextReduced :: String
lawContextReduced = forall a. Show a => a -> a -> String
reduced f Integer
lhs f Integer
rhs
        }
  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

applicativeLiftA2_2 :: forall f. ApplicativeProp f
applicativeLiftA2_2 :: forall (f :: * -> *). ApplicativeProp f
applicativeLiftA2_2 forall x. Gen x -> Gen (f x)
fgen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  f 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. Gen x -> Gen (f x)
fgen Gen Integer
genSmallInteger
  f Integer
y <- 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
  LinearEquationTwo
f' <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a b. (a -> b) -> a -> b
$ Gen LinearEquationTwo
genLinearEquationTwo
  let f :: Integer -> Integer -> Integer
f = LinearEquationTwo -> Integer -> Integer -> Integer
runLinearEquationTwo LinearEquationTwo
f'
  let lhs :: f Integer
lhs = forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Integer -> Integer -> Integer
f f Integer
x f Integer
y
  let rhs :: f Integer
rhs = Integer -> Integer -> Integer
f forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f Integer
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f Integer
y
  let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ LawContext
        { lawContextLawName :: String
lawContextLawName = String
"LiftA2 2", lawContextLawBody :: String
lawContextLawBody = String
"liftA2 f x y == f <$> x <*> y"
        , lawContextTcName :: String
lawContextTcName = String
"Applicative", lawContextTcProp :: String
lawContextTcProp =
            let showF :: String
showF = forall a. Show a => a -> String
show LinearEquationTwo
f'; showX :: String
showX = forall a. Show a => a -> String
show f Integer
x; showY :: String
showY = forall a. Show a => a -> String
show f Integer
y;
            in [String] -> String
lawWhere
              [ String
"liftA2 f x y" String -> String -> String
`congruency` String
"f <$> x <*> y, where"
              , String
"f = " forall a. [a] -> [a] -> [a]
++ String
showF
              , String
"x = " forall a. [a] -> [a] -> [a]
++ String
showX
              , String
"y = " forall a. [a] -> [a] -> [a]
++ String
showY
              ]
        , lawContextReduced :: String
lawContextReduced = forall a. Show a => a -> a -> String
reduced f Integer
lhs f Integer
rhs
        }
  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