{-# LANGUAGE ScopedTypeVariables, FlexibleContexts, KindSignatures
           , Rank2Types, TypeApplications, TypeOperators, CPP
  #-}

----------------------------------------------------------------------
-- |
-- Module      :  Test.QuickCheck.Classes
-- Copyright   :  (c) Conal Elliott 2008
-- License     :  BSD3
--
-- Maintainer  :  conal@conal.net
-- Stability   :  experimental
--
-- Some QuickCheck properties for standard type classes
----------------------------------------------------------------------

module Test.QuickCheck.Classes
  ( ordRel, ord, ordMorphism, semanticOrd
  , semigroup
  , monoid, monoidMorphism, semanticMonoid
  , functor, functorMorphism, semanticFunctor, functorMonoid
  , apply, applyMorphism, semanticApply
  , applicative, applicativeMorphism, semanticApplicative
  , bind, bindMorphism, semanticBind, bindApply
  , monad, monadMorphism, semanticMonad, monadFunctor
  , monadApplicative, arrow, arrowChoice, foldable, foldableFunctor, bifoldable, bifoldableBifunctor, traversable
  , monadPlus, monadOr, alt, alternative
  )
  where

import Data.Bifoldable (Bifoldable (..))
import Data.Bifunctor hiding (first, second)
import Data.Foldable (Foldable(..))
import Data.Functor.Apply (Apply ((<.>)))
import Data.Functor.Alt (Alt ((<!>)))
import Data.Functor.Bind (Bind ((>>-)), apDefault)
import qualified Data.Functor.Bind as B (Bind (join))
import Data.Functor.Compose (Compose (..))
import Data.Functor.Identity (Identity (..))
import Data.List.NonEmpty (NonEmpty(..))
import Data.Semigroup (Semigroup (..))
import Data.Monoid (Endo(..), Dual(..), Sum(..), Product(..))
import Data.Traversable (fmapDefault, foldMapDefault)
import Control.Applicative (Alternative(..))
import Control.Monad (MonadPlus (..), ap, join)
import Control.Arrow (Arrow,ArrowChoice,first,second,left,right,(>>>),arr)
import Test.QuickCheck
import Text.Show.Functions ()

import Test.QuickCheck.Checkers
import Test.QuickCheck.Instances.Char ()


-- | Total ordering.
--
-- @gen a@ ought to generate values @b@ satisfying @a `rel` b@ fairly often.
ordRel :: forall a. (Ord a, Show a, Arbitrary a) =>
          BinRel a -> (a -> Gen a) -> TestBatch
ordRel :: BinRel a -> (a -> Gen a) -> TestBatch
ordRel BinRel a
rel a -> Gen a
gen =
  ( [Char]
"ord"
  , [ ([Char]
"reflexive"    , BinRel a -> Property
forall a. (Arbitrary a, Show a) => BinRel a -> Property
reflexive     BinRel a
rel    )
    , ([Char]
"transitive"   , BinRel a -> (a -> Gen a) -> Property
forall a.
(Arbitrary a, Show a) =>
BinRel a -> (a -> Gen a) -> Property
transitive    BinRel a
rel a -> Gen a
gen)
    , ([Char]
"antiSymmetric", BinRel a -> Property
forall a. (Arbitrary a, Show a, Eq a) => BinRel a -> Property
antiSymmetric BinRel a
rel    )
    ]
  )

-- | 'Ord' laws.
--
-- @gen a@ ought to generate values @b@ satisfying @a `rel` b@ fairly often.
ord :: forall a. (Ord a, Show a, Arbitrary a) =>
       (a -> Gen a) -> TestBatch
ord :: (a -> Gen a) -> TestBatch
ord a -> Gen a
gen =
    ( [Char]
"Ord"
    , [ ([Char]
"Reflexivity of (<=)", BinRel a -> Property
forall a. (Arbitrary a, Show a) => BinRel a -> Property
reflexive BinRel a
le)
      , ([Char]
"Transitivity of (<=)", BinRel a -> (a -> Gen a) -> Property
forall a.
(Arbitrary a, Show a) =>
BinRel a -> (a -> Gen a) -> Property
transitive BinRel a
le a -> Gen a
gen)
      , ([Char]
"Antisymmetry of (<=)", BinRel a -> Property
forall a. (Arbitrary a, Show a, Eq a) => BinRel a -> Property
antiSymmetric BinRel a
le)
      , ([Char]
"x >= y = y <= x", (a -> a -> Property) -> Property
p (\a
x a
y -> (a
x BinRel a
forall a. Ord a => a -> a -> Bool
>= a
y) Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== (a
y BinRel a
forall a. Ord a => a -> a -> Bool
<= a
x)))
      , ([Char]
"x < y = x <= y && x /= y", (a -> a -> Property) -> Property
p (\a
x a
y -> (a
x BinRel a
forall a. Ord a => a -> a -> Bool
< a
y) Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== (a
x BinRel a
forall a. Ord a => a -> a -> Bool
<= a
y Bool -> Bool -> Bool
&& a
x BinRel a
forall a. Eq a => a -> a -> Bool
/= a
y)))
      , ([Char]
"x > y = y < x", (a -> a -> Property) -> Property
p (\a
x a
y -> (a
x BinRel a
forall a. Ord a => a -> a -> Bool
> a
y) Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== (a
y BinRel a
forall a. Ord a => a -> a -> Bool
< a
x)))
      , ([Char]
"x < y = compare x y == LT", (a -> a -> Property) -> Property
p (\a
x a
y -> (a
x BinRel a
forall a. Ord a => a -> a -> Bool
< a
y) Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== (a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
x a
y Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
LT)))
      , ([Char]
"x > y = compare x y == GT", (a -> a -> Property) -> Property
p (\a
x a
y -> (a
x BinRel a
forall a. Ord a => a -> a -> Bool
> a
y) Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== (a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
x a
y Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
GT)))
      , ([Char]
"x == y = compare x y == EQ", (a -> a -> Property) -> Property
p (\a
x a
y -> (a
x BinRel a
forall a. Eq a => a -> a -> Bool
== a
y) Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== (a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
x a
y Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
EQ)))
      , ([Char]
"min x y == if x <= y then x else y = True", (a -> a -> Property) -> Property
p (\a
x a
y -> a -> a -> a
forall a. Ord a => a -> a -> a
min a
x a
y a -> a -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== if a
x BinRel a
forall a. Ord a => a -> a -> Bool
<= a
y then a
x else a
y))
      , ([Char]
"max x y == if x >= y then x else y = True", (a -> a -> Property) -> Property
p (\a
x a
y -> a -> a -> a
forall a. Ord a => a -> a -> a
max a
x a
y a -> a -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== if a
x BinRel a
forall a. Ord a => a -> a -> Bool
>= a
y then a
x else a
y))
      ]
    )
  where
    le :: a -> a -> Bool
    le :: BinRel a
le = BinRel a
forall a. Ord a => a -> a -> Bool
(<=)
    p :: (a -> a -> Property) -> Property
    p :: (a -> a -> Property) -> Property
p = (a -> a -> Property) -> Property
forall prop. Testable prop => prop -> Property
property

-- | 'Ord' morphism properties.  @h@ is an 'Ord' morphism iff:
--
-- >    a <= b = h a <= h b
-- >
-- >    h (a `min` b) = h a `min` h b
-- >    h (a `max` b) = h a `max` h b
ordMorphism :: (Ord a, Ord b, EqProp b, Show a, Arbitrary a) =>
               (a -> b) -> TestBatch

ordMorphism :: (a -> b) -> TestBatch
ordMorphism a -> b
h = ( [Char]
"ord morphism"
                , [ ([Char]
"(<=)", (forall a. Ord a => a -> a -> Bool) -> Property
forall d. EqProp d => (forall c. Ord c => c -> c -> d) -> Property
distrib' forall a. Ord a => a -> a -> Bool
(<=))
                  , ([Char]
"min" , (forall a. Ord a => a -> a -> a) -> Property
distrib  forall a. Ord a => a -> a -> a
min )
                  , ([Char]
"max" , (forall a. Ord a => a -> a -> a) -> Property
distrib  forall a. Ord a => a -> a -> a
max )
                  ]
                )
 where
   distrib  :: (forall c. Ord c => c -> c -> c) -> Property
   distrib :: (forall a. Ord a => a -> a -> a) -> Property
distrib  forall a. Ord a => a -> a -> a
op = (a -> a -> Property) -> Property
forall prop. Testable prop => prop -> Property
property ((a -> a -> Property) -> Property)
-> (a -> a -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \ a
u a
v -> a -> b
h (a
u a -> a -> a
forall a. Ord a => a -> a -> a
`op` a
v) b -> b -> Property
forall a. EqProp a => a -> a -> Property
=-= a -> b
h a
u b -> b -> b
forall a. Ord a => a -> a -> a
`op` a -> b
h a
v

   distrib' :: EqProp d => (forall c. Ord c => c -> c -> d) -> Property
   distrib' :: (forall c. Ord c => c -> c -> d) -> Property
distrib' forall c. Ord c => c -> c -> d
op = (a -> a -> Property) -> Property
forall prop. Testable prop => prop -> Property
property ((a -> a -> Property) -> Property)
-> (a -> a -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \ a
u a
v -> a
u a -> a -> d
forall c. Ord c => c -> c -> d
`op` a
v d -> d -> Property
forall a. EqProp a => a -> a -> Property
=-= a -> b
h a
u b -> b -> d
forall c. Ord c => c -> c -> d
`op` a -> b
h a
v

-- | The semantic function ('model') for @a@ is an 'ordMorphism'.
semanticOrd :: forall a b.
  ( Model a b
  , Ord a, Ord b
  , Show a
  , Arbitrary a
  , EqProp b
  ) =>
  a -> TestBatch
semanticOrd :: a -> TestBatch
semanticOrd = TestBatch -> a -> TestBatch
forall a b. a -> b -> a
const (([Char] -> [Char]) -> TestBatch -> TestBatch
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first ([Char]
"semantic " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++)
                      ((a -> b) -> TestBatch
forall a b.
(Ord a, Ord b, EqProp b, Show a, Arbitrary a) =>
(a -> b) -> TestBatch
ordMorphism (a -> b
forall a b. Model a b => a -> b
model :: a -> b)))


-- | Properties to check that the 'Monoid' 'a' satisfies the monoid
-- properties.  The argument value is ignored and is present only for its
-- type.
monoid :: forall a. (Monoid a, Show a, Arbitrary a, EqProp a) =>
          a -> TestBatch
monoid :: a -> TestBatch
monoid = TestBatch -> a -> TestBatch
forall a b. a -> b -> a
const ( [Char]
"monoid"
               , [ ([Char]
"left  identity", (a -> a -> a) -> a -> Property
forall a i.
(Show a, Arbitrary a, EqProp a) =>
(i -> a -> a) -> i -> Property
leftId  a -> a -> a
forall a. Monoid a => a -> a -> a
mappend (a
forall a. Monoid a => a
mempty :: a))
                 , ([Char]
"right identity", (a -> a -> a) -> a -> Property
forall a i.
(Show a, Arbitrary a, EqProp a) =>
(a -> i -> a) -> i -> Property
rightId a -> a -> a
forall a. Monoid a => a -> a -> a
mappend (a
forall a. Monoid a => a
mempty :: a))
                 , ([Char]
"associativity" , (a -> a -> a) -> Property
forall a.
(EqProp a, Show a, Arbitrary a) =>
(a -> a -> a) -> Property
isAssoc (a -> a -> a
forall a. Monoid a => a -> a -> a
mappend :: Binop a))
#if MIN_VERSION_base(4,11,0)
                 , ([Char]
"mappend = (<>)", (a -> a -> Property) -> Property
forall prop. Testable prop => prop -> Property
property a -> a -> Property
monoidSemigroupP)
#endif
                 , ([Char]
"mconcat", ([a] -> Property) -> Property
forall prop. Testable prop => prop -> Property
property [a] -> Property
mconcatP)
                 ]
               )
  where
#if MIN_VERSION_base(4,11,0)
    monoidSemigroupP :: a -> a -> Property
    monoidSemigroupP :: a -> a -> Property
monoidSemigroupP a
x a
y = a -> a -> a
forall a. Monoid a => a -> a -> a
mappend a
x a
y a -> a -> Property
forall a. EqProp a => a -> a -> Property
=-= a
x a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
y
#endif
    mconcatP :: [a] -> Property
    mconcatP :: [a] -> Property
mconcatP [a]
as = [a] -> a
forall a. Monoid a => [a] -> a
mconcat [a]
as a -> a -> Property
forall a. EqProp a => a -> a -> Property
=-= (a -> a -> a) -> a -> [a] -> a
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr a -> a -> a
forall a. Monoid a => a -> a -> a
mappend a
forall a. Monoid a => a
mempty [a]
as

-- | Properties to check that the 'Semigroup' 'a' satisfies the semigroup
-- properties.  The argument value is ignored and is present only for its
-- type.
--
-- @since 0.5.0
semigroup :: forall a n.
             ( Semigroup a, Show a, Arbitrary a, EqProp a
             , Integral n, Show n, Arbitrary n) =>
             (a, n) -> TestBatch
semigroup :: (a, n) -> TestBatch
semigroup = TestBatch -> (a, n) -> TestBatch
forall a b. a -> b -> a
const ( [Char]
"semigroup"
                  , [([Char]
"associativity", (a -> a -> a) -> Property
forall a.
(EqProp a, Show a, Arbitrary a) =>
(a -> a -> a) -> Property
isAssoc (a -> a -> a
forall a. Semigroup a => a -> a -> a
(<>) :: Binop a))
                    ,([Char]
"sconcat", (a -> [a] -> Property) -> Property
forall prop. Testable prop => prop -> Property
property a -> [a] -> Property
sconcatP)
                    ,([Char]
"stimes", (Positive n -> a -> Property) -> Property
forall prop. Testable prop => prop -> Property
property Positive n -> a -> Property
stimesP)
                    ]
                  )
  where
    sconcatP :: a -> [a] -> Property
    sconcatP :: a -> [a] -> Property
sconcatP a
a [a]
as = NonEmpty a -> a
forall a. Semigroup a => NonEmpty a -> a
sconcat (a
a a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:| [a]
as) a -> a -> Property
forall a. EqProp a => a -> a -> Property
=-= (a -> a -> a) -> NonEmpty a -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 a -> a -> a
forall a. Semigroup a => a -> a -> a
(<>) (a
a a -> [a] -> NonEmpty a
forall a. a -> [a] -> NonEmpty a
:| [a]
as)
    stimesP :: Positive n -> a -> Property
    stimesP :: Positive n -> a -> Property
stimesP (Positive n
n) a
a = n -> a -> a
forall a b. (Semigroup a, Integral b) => b -> a -> a
stimes n
n a
a a -> a -> Property
forall a. EqProp a => a -> a -> Property
=-= (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 a -> a -> a
forall a. Semigroup a => a -> a -> a
(<>) (Int -> a -> [a]
forall a. Int -> a -> [a]
replicate (n -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral n
n) a
a)

-- | Monoid homomorphism properties.  See also 'homomorphism'.
monoidMorphism :: (Monoid a, Monoid b, EqProp b, Show a, Arbitrary a) =>
                  (a -> b) -> TestBatch
monoidMorphism :: (a -> b) -> TestBatch
monoidMorphism a -> b
q = ([Char]
"monoid morphism", MonoidD a -> MonoidD b -> (a -> b) -> [Test]
forall b a.
(EqProp b, Show a, Arbitrary a) =>
MonoidD a -> MonoidD b -> (a -> b) -> [Test]
homomorphism MonoidD a
forall a. Monoid a => MonoidD a
monoidD MonoidD b
forall a. Monoid a => MonoidD a
monoidD a -> b
q)

semanticMonoid :: forall a b.
  ( Model a b
  , Monoid a, Monoid b
  , Show a
  , Arbitrary a
  , EqProp b
  ) =>
  a -> TestBatch

-- | The semantic function ('model') for @a@ is a 'monoidMorphism'.
semanticMonoid :: a -> TestBatch
semanticMonoid = TestBatch -> a -> TestBatch
forall a b. a -> b -> a
const (([Char] -> [Char]) -> TestBatch -> TestBatch
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first ([Char]
"semantic " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++)
                              ((a -> b) -> TestBatch
forall a b.
(Monoid a, Monoid b, EqProp b, Show a, Arbitrary a) =>
(a -> b) -> TestBatch
monoidMorphism (a -> b
forall a b. Model a b => a -> b
model:: a -> b)))

functorMonoid :: forall m a b.
  ( Functor m
  , Monoid (m a)
  , Monoid (m b)
  , CoArbitrary a
  , Arbitrary b
  , Arbitrary (m a)
  , Show (m a)
  , EqProp (m b)) =>
  m (a,b) -> TestBatch
functorMonoid :: m (a, b) -> TestBatch
functorMonoid = TestBatch -> m (a, b) -> TestBatch
forall a b. a -> b -> a
const ([Char]
"functor-monoid"
                      , [ ( [Char]
"identity",((a -> b) -> Property) -> Property
forall prop. Testable prop => prop -> Property
property (a -> b) -> Property
identityP )
                        , ( [Char]
"binop", ((a -> b) -> m a -> m a -> Property) -> Property
forall prop. Testable prop => prop -> Property
property (a -> b) -> m a -> m a -> Property
binopP )
                        ]
                      )
  where
    identityP :: (a->b) -> Property
    identityP :: (a -> b) -> Property
identityP a -> b
f = ((a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f) (m a
forall a. Monoid a => a
mempty :: m a) m b -> m b -> Property
forall a. EqProp a => a -> a -> Property
=-= (m b
forall a. Monoid a => a
mempty :: m b)
    binopP :: (a->b) -> (m a) -> (m a) -> Property
    binopP :: (a -> b) -> m a -> m a -> Property
binopP a -> b
f m a
u m a
v = ((a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f) (m a
u m a -> m a -> m a
forall a. Monoid a => a -> a -> a
`mappend` m a
v) m b -> m b -> Property
forall a. EqProp a => a -> a -> Property
=-= ((a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f m a
u) m b -> m b -> m b
forall a. Monoid a => a -> a -> a
`mappend` ((a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f m a
v)

-- <camio> There I have an attempt at doing this. I eventually implemented
-- those semanticMorphisms as their own functions. I'm not too thrilled with
-- that implementation, but it works.

-- TODO: figure out out to eliminate the redundancy.

-- | Properties to check that the 'Functor' @m@ satisfies the functor
-- properties.
functor :: forall m a b c.
           ( Functor m
           , Arbitrary b, Arbitrary c
           , CoArbitrary a, CoArbitrary b
           , Show (m a), Arbitrary (m a), EqProp (m a), EqProp (m c)) =>
           m (a,b,c) -> TestBatch
functor :: m (a, b, c) -> TestBatch
functor = TestBatch -> m (a, b, c) -> TestBatch
forall a b. a -> b -> a
const ( [Char]
"functor"
                , [ ([Char]
"identity", Property -> Property
forall prop. Testable prop => prop -> Property
property Property
identityP)
                  , ([Char]
"compose" , ((b -> c) -> (a -> b) -> Property) -> Property
forall prop. Testable prop => prop -> Property
property (b -> c) -> (a -> b) -> Property
composeP) ]
                )
 where
   identityP :: Property
   composeP  :: (b -> c) -> (a -> b) -> Property

   identityP :: Property
identityP = (a -> a) -> m a -> m a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> a
forall a. a -> a
id (m a -> m a) -> (m a -> m a) -> Property
forall a. EqProp a => a -> a -> Property
=-= (m a -> m a
forall a. a -> a
id :: m a -> m a)
   composeP :: (b -> c) -> (a -> b) -> Property
composeP b -> c
g a -> b
f = (b -> c) -> m b -> m c
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> c
g (m b -> m c) -> (m a -> m b) -> m a -> m c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f (m a -> m c) -> (m a -> m c) -> Property
forall a. EqProp a => a -> a -> Property
=-= ((a -> c) -> m a -> m c
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (b -> c
g(b -> c) -> (a -> b) -> a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
.a -> b
f) :: m a -> m c)

-- Note the similarity between 'functor' and 'monoidMorphism'.  The
-- functor laws say that 'fmap' is a homomorphism w.r.t '(.)':
--
--   functor = const ("functor", homomorphism endoMonoidD endoMonoidD fmap)
--
-- However, I don't think the types can work out, since 'fmap' is used at
-- three different types.


-- | 'Functor' morphism (natural transformation) properties
functorMorphism :: forall f g.
                   ( Functor f, Functor g
                   , Arbitrary (f NumT), Show (f NumT)
                   , EqProp (g T)
                   ) =>
                  (forall a. f a -> g a) -> TestBatch
functorMorphism :: (forall a. f a -> g a) -> TestBatch
functorMorphism forall a. f a -> g a
q = ([Char]
"functor morphism", [([Char]
"fmap", ((Int -> Char) -> Property) -> Property
forall prop. Testable prop => prop -> Property
property (Int -> Char) -> Property
fmapP)])
 where
   -- fmapP :: (NumT -> T) -> f NumT -> Property
   -- fmapP h l = q (fmap h l) =-= fmap h (q l)
   fmapP :: (NumT -> T) -> Property
   fmapP :: (Int -> Char) -> Property
fmapP Int -> Char
h = f Char -> g Char
forall a. f a -> g a
q (f Char -> g Char) -> (f Int -> f Char) -> f Int -> g Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Char) -> f Int -> f Char
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Char
h (f Int -> g Char) -> (f Int -> g Char) -> Property
forall a. EqProp a => a -> a -> Property
=-= (Int -> Char) -> g Int -> g Char
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Char
h (g Int -> g Char) -> (f Int -> g Int) -> f Int -> g Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f Int -> g Int
forall a. f a -> g a
q

-- Note: monomorphism prevent us from saying @commutes (.) q (fmap h)@,
-- since @fmap h@ is used at two different types.

-- | The semantic function ('model1') for @f@ is a 'functorMorphism'.
semanticFunctor :: forall f g.
  ( Model1 f g
  , Functor f
  , Functor g
  , Arbitrary (f NumT)
  , Show (f NumT)
  , EqProp (g T)
  ) =>
  f () -> TestBatch
semanticFunctor :: f () -> TestBatch
semanticFunctor = TestBatch -> f () -> TestBatch
forall a b. a -> b -> a
const ((forall a. f a -> g a) -> TestBatch
forall (f :: * -> *) (g :: * -> *).
(Functor f, Functor g, Arbitrary (f Int), Show (f Int),
 EqProp (g Char)) =>
(forall a. f a -> g a) -> TestBatch
functorMorphism (forall a. f a -> g a
forall (f :: * -> *) (g :: * -> *) a. Model1 f g => f a -> g a
model1 :: forall b. f b -> g b))


-- | Properties to check that the 'Apply' @m@ satisfies the apply
-- properties
apply :: forall m a b c.
         ( Apply m
         , CoArbitrary a, Arbitrary b, CoArbitrary b
         , Arbitrary c, Arbitrary (m a)
         , Arbitrary (m (b -> c)), Show (m (b -> c))
         , Arbitrary (m (a -> b)), Show (m (a -> b))
         , Show (m a)
         , EqProp (m c)
         ) =>
         m (a,b,c) -> TestBatch
apply :: m (a, b, c) -> TestBatch
apply = TestBatch -> m (a, b, c) -> TestBatch
forall a b. a -> b -> a
const ( [Char]
"apply"
              , [ ([Char]
"associativity", (m (b -> c) -> m (a -> b) -> m a -> Property) -> Property
forall prop. Testable prop => prop -> Property
property m (b -> c) -> m (a -> b) -> m a -> Property
associativityP)
                , ([Char]
"left"       , ((a -> b) -> m (b -> c) -> m a -> Property) -> Property
forall prop. Testable prop => prop -> Property
property (a -> b) -> m (b -> c) -> m a -> Property
leftP)
                , ([Char]
"right"      , ((b -> c) -> m (a -> b) -> m a -> Property) -> Property
forall prop. Testable prop => prop -> Property
property (b -> c) -> m (a -> b) -> m a -> Property
rightP)
                ]
              )
 where
   associativityP :: m (b -> c) -> m (a -> b) -> m a -> Property
   rightP         :: (b -> c) -> m (a -> b) -> m a -> Property
   leftP          :: (a -> b) -> m (b -> c) -> m a -> Property

   associativityP :: m (b -> c) -> m (a -> b) -> m a -> Property
associativityP m (b -> c)
u m (a -> b)
v m a
w = ((b -> c) -> (a -> b) -> a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) ((b -> c) -> (a -> b) -> a -> c)
-> m (b -> c) -> m ((a -> b) -> a -> c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (b -> c)
u m ((a -> b) -> a -> c) -> m (a -> b) -> m (a -> c)
forall (f :: * -> *) a b. Apply f => f (a -> b) -> f a -> f b
<.> m (a -> b)
v m (a -> c) -> m a -> m c
forall (f :: * -> *) a b. Apply f => f (a -> b) -> f a -> f b
<.> m a
w) m c -> m c -> Property
forall a. EqProp a => a -> a -> Property
=-= (m (b -> c)
u m (b -> c) -> m b -> m c
forall (f :: * -> *) a b. Apply f => f (a -> b) -> f a -> f b
<.> (m (a -> b)
v m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Apply f => f (a -> b) -> f a -> f b
<.> m a
w))
   leftP :: (a -> b) -> m (b -> c) -> m a -> Property
leftP a -> b
f m (b -> c)
x m a
y          = (m (b -> c)
x m (b -> c) -> m b -> m c
forall (f :: * -> *) a b. Apply f => f (a -> b) -> f a -> f b
<.> (a -> b
f (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m a
y)) m c -> m c -> Property
forall a. EqProp a => a -> a -> Property
=-= (((b -> c) -> (a -> b) -> a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f) ((b -> c) -> a -> c) -> m (b -> c) -> m (a -> c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (b -> c)
x m (a -> c) -> m a -> m c
forall (f :: * -> *) a b. Apply f => f (a -> b) -> f a -> f b
<.> m a
y)
   rightP :: (b -> c) -> m (a -> b) -> m a -> Property
rightP b -> c
f m (a -> b)
x m a
y         = (b -> c
f (b -> c) -> m b -> m c
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (m (a -> b)
x m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Apply f => f (a -> b) -> f a -> f b
<.> m a
y)) m c -> m c -> Property
forall a. EqProp a => a -> a -> Property
=-= ((b -> c
f (b -> c) -> (a -> b) -> a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((a -> b) -> a -> c) -> m (a -> b) -> m (a -> c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (a -> b)
x m (a -> c) -> m a -> m c
forall (f :: * -> *) a b. Apply f => f (a -> b) -> f a -> f b
<.> m a
y)


-- | 'Apply' morphism properties
applyMorphism :: forall f g.
                 ( Apply f, Apply g
                 , Show (f NumT), Arbitrary (f NumT)
                 , EqProp (g T)
                 , Show (f (NumT -> T))
                 , Arbitrary (f (NumT -> T))
                 ) =>
                 (forall a. f a -> g a) -> TestBatch
applyMorphism :: (forall a. f a -> g a) -> TestBatch
applyMorphism forall a. f a -> g a
q =
  ( [Char]
"apply morphism"
  , [ ([Char]
"apply", (f (Int -> Char) -> f Int -> Property) -> Property
forall prop. Testable prop => prop -> Property
property f (Int -> Char) -> f Int -> Property
applyP)] )
 where
   applyP :: f (NumT->T) -> f NumT -> Property
   applyP :: f (Int -> Char) -> f Int -> Property
applyP f (Int -> Char)
mf f Int
mx = f Char -> g Char
forall a. f a -> g a
q (f (Int -> Char)
mf f (Int -> Char) -> f Int -> f Char
forall (f :: * -> *) a b. Apply f => f (a -> b) -> f a -> f b
<.> f Int
mx) g Char -> g Char -> Property
forall a. EqProp a => a -> a -> Property
=-= (f (Int -> Char) -> g (Int -> Char)
forall a. f a -> g a
q f (Int -> Char)
mf g (Int -> Char) -> g Int -> g Char
forall (f :: * -> *) a b. Apply f => f (a -> b) -> f a -> f b
<.> f Int -> g Int
forall a. f a -> g a
q f Int
mx)


-- | The semantic function ('model1') for @f@ is an 'applyMorphism'.
semanticApply :: forall f g.
                 ( Model1 f g
                 , Apply f, Apply g
                 , Arbitrary (f NumT), Arbitrary (f (NumT -> T))
                 , EqProp (g T)
                 , Show (f NumT), Show (f (NumT -> T))
                 ) =>
                 f () -> TestBatch
semanticApply :: f () -> TestBatch
semanticApply =
  TestBatch -> f () -> TestBatch
forall a b. a -> b -> a
const ((forall a. f a -> g a) -> TestBatch
forall (f :: * -> *) (g :: * -> *).
(Apply f, Apply g, Show (f Int), Arbitrary (f Int),
 EqProp (g Char), Show (f (Int -> Char)),
 Arbitrary (f (Int -> Char))) =>
(forall a. f a -> g a) -> TestBatch
applyMorphism (forall a. f a -> g a
forall (f :: * -> *) (g :: * -> *) a. Model1 f g => f a -> g a
model1 :: forall b. f b -> g b))


-- | Properties to check that the 'Applicative' @m@ satisfies the applicative
-- properties
applicative :: forall m a b c.
               ( Applicative m
               , Arbitrary a, CoArbitrary a, Arbitrary b, Arbitrary (m a)
               , Arbitrary (m (b -> c)), Show (m (b -> c))
               , Arbitrary (m (a -> b)), Show (m (a -> b))
               , Show a, Show (m a)
               , EqProp (m a), EqProp (m b), EqProp (m c)
               ) =>
               m (a,b,c) -> TestBatch
applicative :: m (a, b, c) -> TestBatch
applicative = TestBatch -> m (a, b, c) -> TestBatch
forall a b. a -> b -> a
const ( [Char]
"applicative"
                    , [ ([Char]
"identity"    , (m a -> Property) -> Property
forall prop. Testable prop => prop -> Property
property m a -> Property
identityP)
                      , ([Char]
"composition" , (m (b -> c) -> m (a -> b) -> m a -> Property) -> Property
forall prop. Testable prop => prop -> Property
property m (b -> c) -> m (a -> b) -> m a -> Property
compositionP)
                      , ([Char]
"homomorphism", ((a -> b) -> a -> Property) -> Property
forall prop. Testable prop => prop -> Property
property (a -> b) -> a -> Property
homomorphismP)
                      , ([Char]
"interchange" , (m (a -> b) -> a -> Property) -> Property
forall prop. Testable prop => prop -> Property
property m (a -> b) -> a -> Property
interchangeP)
                      , ([Char]
"functor"     , ((a -> b) -> m a -> Property) -> Property
forall prop. Testable prop => prop -> Property
property (a -> b) -> m a -> Property
functorP)
                      ]
                    )
 where
   identityP     :: m a -> Property
   compositionP  :: m (b -> c) -> m (a -> b) -> m a -> Property
   homomorphismP :: (a -> b) -> a -> Property
   interchangeP  :: m (a -> b) -> a -> Property
   functorP      :: (a -> b) -> m a -> Property

   identityP :: m a -> Property
identityP m a
v        = ((a -> a) -> m (a -> a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure a -> a
forall a. a -> a
id m (a -> a) -> m a -> m a
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> m a
v) m a -> m a -> Property
forall a. EqProp a => a -> a -> Property
=-= m a
v
   compositionP :: m (b -> c) -> m (a -> b) -> m a -> Property
compositionP m (b -> c)
u m (a -> b)
v m a
w = (((b -> c) -> (a -> b) -> a -> c)
-> m ((b -> c) -> (a -> b) -> a -> c)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (b -> c) -> (a -> b) -> a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) m ((b -> c) -> (a -> b) -> a -> c)
-> m (b -> c) -> m ((a -> b) -> a -> c)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> m (b -> c)
u m ((a -> b) -> a -> c) -> m (a -> b) -> m (a -> c)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> m (a -> b)
v m (a -> c) -> m a -> m c
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> m a
w) m c -> m c -> Property
forall a. EqProp a => a -> a -> Property
=-= (m (b -> c)
u m (b -> c) -> m b -> m c
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (m (a -> b)
v m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> m a
w))
   homomorphismP :: (a -> b) -> a -> Property
homomorphismP a -> b
f a
x  = ((a -> b) -> m (a -> b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure a -> b
f m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x) m b -> m b -> Property
forall a. EqProp a => a -> a -> Property
=-= (b -> m b
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> b
f a
x) :: m b)
   interchangeP :: m (a -> b) -> a -> Property
interchangeP m (a -> b)
u a
y   = (m (a -> b)
u m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
y) m b -> m b -> Property
forall a. EqProp a => a -> a -> Property
=-= (((a -> b) -> b) -> m ((a -> b) -> b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ a
y) m ((a -> b) -> b) -> m (a -> b) -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> m (a -> b)
u)
   functorP :: (a -> b) -> m a -> Property
functorP a -> b
f m a
x       = ((a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f m a
x) m b -> m b -> Property
forall a. EqProp a => a -> a -> Property
=-= ((a -> b) -> m (a -> b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure a -> b
f m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> m a
x)


-- | 'Applicative' morphism properties
applicativeMorphism :: forall f g.
                       ( Applicative f, Applicative g
                       , Show (f NumT), Arbitrary (f NumT)
                       , EqProp (g NumT), EqProp (g T)
                       , Show (f (NumT -> T))
                       , Arbitrary (f (NumT -> T))
                       ) =>
                       (forall a. f a -> g a) -> TestBatch
applicativeMorphism :: (forall a. f a -> g a) -> TestBatch
applicativeMorphism forall a. f a -> g a
q =
  ( [Char]
"applicative morphism"
  , [([Char]
"pure", (Int -> Property) -> Property
forall prop. Testable prop => prop -> Property
property Int -> Property
pureP), ([Char]
"apply", (f (Int -> Char) -> f Int -> Property) -> Property
forall prop. Testable prop => prop -> Property
property f (Int -> Char) -> f Int -> Property
applyP)] )
 where
   pureP  :: NumT -> Property
   applyP :: f (NumT->T) -> f NumT -> Property

   pureP :: Int -> Property
pureP Int
a = f Int -> g Int
forall a. f a -> g a
q (Int -> f Int
forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
a) g Int -> g Int -> Property
forall a. EqProp a => a -> a -> Property
=-= Int -> g Int
forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
a
   applyP :: f (Int -> Char) -> f Int -> Property
applyP f (Int -> Char)
mf f Int
mx = f Char -> g Char
forall a. f a -> g a
q (f (Int -> Char)
mf f (Int -> Char) -> f Int -> f Char
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f Int
mx) g Char -> g Char -> Property
forall a. EqProp a => a -> a -> Property
=-= (f (Int -> Char) -> g (Int -> Char)
forall a. f a -> g a
q f (Int -> Char)
mf g (Int -> Char) -> g Int -> g Char
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f Int -> g Int
forall a. f a -> g a
q f Int
mx)


-- | The semantic function ('model1') for @f@ is an 'applicativeMorphism'.
semanticApplicative :: forall f g.
  ( Model1 f g
  , Applicative f, Applicative g
  , Arbitrary (f NumT), Arbitrary (f (NumT -> T))
  , EqProp (g NumT), EqProp (g T)
  , Show (f NumT), Show (f (NumT -> T))
  ) =>
  f () -> TestBatch
semanticApplicative :: f () -> TestBatch
semanticApplicative =
  TestBatch -> f () -> TestBatch
forall a b. a -> b -> a
const ((forall a. f a -> g a) -> TestBatch
forall (f :: * -> *) (g :: * -> *).
(Applicative f, Applicative g, Show (f Int), Arbitrary (f Int),
 EqProp (g Int), EqProp (g Char), Show (f (Int -> Char)),
 Arbitrary (f (Int -> Char))) =>
(forall a. f a -> g a) -> TestBatch
applicativeMorphism (forall a. f a -> g a
forall (f :: * -> *) (g :: * -> *) a. Model1 f g => f a -> g a
model1 :: forall b. f b -> g b))


-- | Properties to check that the 'bind' @m@ satisfies the bind properties
bind :: forall m a b c.
        ( Bind m
        , CoArbitrary a, CoArbitrary b
        , Arbitrary (m a), EqProp (m a), Show (m a)
        , Arbitrary (m b)
        , Arbitrary (m c), EqProp (m c)
        , Arbitrary (m (m (m a))), Show (m (m (m a)))
        ) =>
        m (a,b,c) -> TestBatch
bind :: m (a, b, c) -> TestBatch
bind = TestBatch -> m (a, b, c) -> TestBatch
forall a b. a -> b -> a
const ( [Char]
"bind laws"
              , [ ([Char]
"join associativity", (m (m (m a)) -> Property) -> Property
forall prop. Testable prop => prop -> Property
property m (m (m a)) -> Property
joinAssocP)
                , ([Char]
"bind associativity", (m a -> (a -> m b) -> (b -> m c) -> Property) -> Property
forall prop. Testable prop => prop -> Property
property m a -> (a -> m b) -> (b -> m c) -> Property
bindAssocP)
                ]
              )
 where
   bindAssocP :: m a -> (a -> m b) -> (b -> m c) -> Property
   joinAssocP :: m (m (m a)) -> Property

   bindAssocP :: m a -> (a -> m b) -> (b -> m c) -> Property
bindAssocP m a
m a -> m b
f b -> m c
g = ((m a
m m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Bind m => m a -> (a -> m b) -> m b
>>- a -> m b
f) m b -> (b -> m c) -> m c
forall (m :: * -> *) a b. Bind m => m a -> (a -> m b) -> m b
>>- b -> m c
g) m c -> m c -> Property
forall a. EqProp a => a -> a -> Property
=-= (m a
m m a -> (a -> m c) -> m c
forall (m :: * -> *) a b. Bind m => m a -> (a -> m b) -> m b
>>- (\a
x -> a -> m b
f a
x m b -> (b -> m c) -> m c
forall (m :: * -> *) a b. Bind m => m a -> (a -> m b) -> m b
>>- b -> m c
g))
   joinAssocP :: m (m (m a)) -> Property
joinAssocP m (m (m a))
mmma = m (m a) -> m a
forall (m :: * -> *) a. Bind m => m (m a) -> m a
B.join (m (m (m a)) -> m (m a)
forall (m :: * -> *) a. Bind m => m (m a) -> m a
B.join m (m (m a))
mmma) m a -> m a -> Property
forall a. EqProp a => a -> a -> Property
=-= m (m a) -> m a
forall (m :: * -> *) a. Bind m => m (m a) -> m a
B.join ((m (m a) -> m a) -> m (m (m a)) -> m (m a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap m (m a) -> m a
forall (m :: * -> *) a. Bind m => m (m a) -> m a
B.join m (m (m a))
mmma)

bindApply :: forall m a b.
             ( Bind m
             , EqProp (m b)
             , Show (m a), Arbitrary (m a)
             , Show (m (a -> b)), Arbitrary (m (a -> b))) =>
             m (a, b) -> TestBatch
bindApply :: m (a, b) -> TestBatch
bindApply = TestBatch -> m (a, b) -> TestBatch
forall a b. a -> b -> a
const ( [Char]
"bind apply"
                  , [ ([Char]
"ap", (m (a -> b) -> m a -> Property) -> Property
forall prop. Testable prop => prop -> Property
property m (a -> b) -> m a -> Property
apP) ]
                  )
 where
   apP :: m (a -> b) -> m a -> Property
   apP :: m (a -> b) -> m a -> Property
apP m (a -> b)
f m a
x = (m (a -> b)
f m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Apply f => f (a -> b) -> f a -> f b
<.> m a
x) m b -> m b -> Property
forall a. EqProp a => a -> a -> Property
=-= (m (a -> b)
f m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Bind f => f (a -> b) -> f a -> f b
`apDefault` m a
x)

-- | 'bind' morphism properties
bindMorphism :: forall f g.
                ( Bind f, Bind g
                , Show (f NumT)
                , Show (f (f (NumT -> T)))
                , Arbitrary (f NumT), Arbitrary (f T)
                , Arbitrary (f (f (NumT -> T)))
                , EqProp (g T)
                , EqProp (g (NumT -> T))
                ) =>
                (forall a. f a -> g a) -> TestBatch
bindMorphism :: (forall a. f a -> g a) -> TestBatch
bindMorphism forall a. f a -> g a
q =
  ( [Char]
"bind morphism"
  , [ ([Char]
"bind", (f Int -> (Int -> f Char) -> Property) -> Property
forall prop. Testable prop => prop -> Property
property f Int -> (Int -> f Char) -> Property
bindP), ([Char]
"join", (f (f (Int -> Char)) -> Property) -> Property
forall prop. Testable prop => prop -> Property
property f (f (Int -> Char)) -> Property
joinP) ] )
 where
   bindP :: f NumT -> (NumT -> f T) -> Property
   joinP :: f (f (NumT->T)) -> Property

   bindP :: f Int -> (Int -> f Char) -> Property
bindP f Int
u Int -> f Char
k = f Char -> g Char
forall a. f a -> g a
q (f Int
u f Int -> (Int -> f Char) -> f Char
forall (m :: * -> *) a b. Bind m => m a -> (a -> m b) -> m b
>>- Int -> f Char
k)  g Char -> g Char -> Property
forall a. EqProp a => a -> a -> Property
=-= (f Int -> g Int
forall a. f a -> g a
q f Int
u g Int -> (Int -> g Char) -> g Char
forall (m :: * -> *) a b. Bind m => m a -> (a -> m b) -> m b
>>- f Char -> g Char
forall a. f a -> g a
q (f Char -> g Char) -> (Int -> f Char) -> Int -> g Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> f Char
k)
   joinP :: f (f (Int -> Char)) -> Property
joinP f (f (Int -> Char))
uu  = f (Int -> Char) -> g (Int -> Char)
forall a. f a -> g a
q (f (f (Int -> Char)) -> f (Int -> Char)
forall (m :: * -> *) a. Bind m => m (m a) -> m a
B.join f (f (Int -> Char))
uu)  g (Int -> Char) -> g (Int -> Char) -> Property
forall a. EqProp a => a -> a -> Property
=-= g (g (Int -> Char)) -> g (Int -> Char)
forall (m :: * -> *) a. Bind m => m (m a) -> m a
B.join ((f (Int -> Char) -> g (Int -> Char))
-> g (f (Int -> Char)) -> g (g (Int -> Char))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (Int -> Char) -> g (Int -> Char)
forall a. f a -> g a
q (f (f (Int -> Char)) -> g (f (Int -> Char))
forall a. f a -> g a
q f (f (Int -> Char))
uu))

-- | The semantic function ('model1') for @f@ is a 'bindMorphism'.
semanticBind :: forall f g.
  ( Model1 f g
  , Bind f, Bind g
  , EqProp (g T)
  , EqProp (g (NumT -> T))
  , Arbitrary (f T) , Arbitrary (f NumT)
  , Arbitrary (f (f (NumT -> T)))
  , Show (f (f (NumT -> T)))
  , Show (f NumT)
  ) =>
  f () -> TestBatch
semanticBind :: f () -> TestBatch
semanticBind = TestBatch -> f () -> TestBatch
forall a b. a -> b -> a
const ((forall a. f a -> g a) -> TestBatch
forall (f :: * -> *) (g :: * -> *).
(Bind f, Bind g, Show (f Int), Show (f (f (Int -> Char))),
 Arbitrary (f Int), Arbitrary (f Char),
 Arbitrary (f (f (Int -> Char))), EqProp (g Char),
 EqProp (g (Int -> Char))) =>
(forall a. f a -> g a) -> TestBatch
bindMorphism (forall a. f a -> g a
forall (f :: * -> *) (g :: * -> *) a. Model1 f g => f a -> g a
model1 :: forall b. f b -> g b))


-- | Properties to check that the 'Monad' @m@ satisfies the monad properties
monad :: forall m a b c.
         ( Monad m
         , Show a, Arbitrary a, CoArbitrary a, CoArbitrary b
         , Arbitrary (m a), EqProp (m a), Show (m a)
         , Arbitrary (m b), EqProp (m b)
         , Arbitrary (m c), EqProp (m c)
         , Show (m (a -> b)), Arbitrary (m (a -> b))
         ) =>
         m (a,b,c) -> TestBatch
monad :: m (a, b, c) -> TestBatch
monad = TestBatch -> m (a, b, c) -> TestBatch
forall a b. a -> b -> a
const ( [Char]
"monad laws"
              , [ ([Char]
"left  identity", ((a -> m b) -> a -> Property) -> Property
forall prop. Testable prop => prop -> Property
property (a -> m b) -> a -> Property
leftP)
                , ([Char]
"right identity", (m a -> Property) -> Property
forall prop. Testable prop => prop -> Property
property m a -> Property
rightP)
                , ([Char]
"associativity" , (m a -> (a -> m b) -> (b -> m c) -> Property) -> Property
forall prop. Testable prop => prop -> Property
property m a -> (a -> m b) -> (b -> m c) -> Property
assocP)
                , ([Char]
"pure", (a -> Property) -> Property
forall prop. Testable prop => prop -> Property
property a -> Property
pureP)
                , ([Char]
"ap", (m (a -> b) -> m a -> Property) -> Property
forall prop. Testable prop => prop -> Property
property m (a -> b) -> m a -> Property
apP)
                ]
              )
 where
   leftP  :: (a -> m b) -> a -> Property
   rightP :: m a -> Property
   assocP :: m a -> (a -> m b) -> (b -> m c) -> Property
   pureP :: a -> Property
   apP :: m (a -> b) -> m a -> Property

   leftP :: (a -> m b) -> a -> Property
leftP a -> m b
f a
a    = (a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> m b
f)  m b -> m b -> Property
forall a. EqProp a => a -> a -> Property
=-= a -> m b
f a
a
   rightP :: m a -> Property
rightP m a
m     = (m a
m m a -> (a -> m a) -> m a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return)    m a -> m a -> Property
forall a. EqProp a => a -> a -> Property
=-=  m a
m
   assocP :: m a -> (a -> m b) -> (b -> m c) -> Property
assocP m a
m a -> m b
f b -> m c
g = ((m a
m m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> m b
f) m b -> (b -> m c) -> m c
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= b -> m c
g) m c -> m c -> Property
forall a. EqProp a => a -> a -> Property
=-= (m a
m m a -> (a -> m c) -> m c
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\a
x -> a -> m b
f a
x m b -> (b -> m c) -> m c
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= b -> m c
g))
   pureP :: a -> Property
pureP a
x = (a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x :: m a) m a -> m a -> Property
forall a. EqProp a => a -> a -> Property
=-= a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x
   apP :: m (a -> b) -> m a -> Property
apP m (a -> b)
f m a
x = (m (a -> b)
f m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> m a
x) m b -> m b -> Property
forall a. EqProp a => a -> a -> Property
=-= (m (a -> b)
f m (a -> b) -> m a -> m b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
`ap` m a
x)

-- | Law for monads that are also instances of 'Functor'.
--
-- Note that instances that satisfy 'applicative' and 'monad'
-- are implied to satisfy this property too.
monadFunctor :: forall m a b.
                ( Monad m
                , Arbitrary b, CoArbitrary a
                , Arbitrary (m a), Show (m a), EqProp (m b)) =>
                m (a, b) -> TestBatch
monadFunctor :: m (a, b) -> TestBatch
monadFunctor = TestBatch -> m (a, b) -> TestBatch
forall a b. a -> b -> a
const ( [Char]
"monad functor"
                     , [([Char]
"bind return", ((a -> b) -> m a -> Property) -> Property
forall prop. Testable prop => prop -> Property
property (a -> b) -> m a -> Property
bindReturnP)])
 where
   bindReturnP :: (a -> b) -> m a -> Property
   bindReturnP :: (a -> b) -> m a -> Property
bindReturnP a -> b
f m a
xs = (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f m a
xs m b -> m b -> Property
forall a. EqProp a => a -> a -> Property
=-= (m a
xs m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= b -> m b
forall (m :: * -> *) a. Monad m => a -> m a
return (b -> m b) -> (a -> b) -> a -> m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f)

-- | Note that 'monad' also contains these properties.
monadApplicative :: forall m a b.
                    ( Monad m
                    , EqProp (m a), EqProp (m b)
                    , Show a, Arbitrary a
                    , Show (m a), Arbitrary (m a)
                    , Show (m (a -> b)), Arbitrary (m (a -> b))) =>
                    m (a, b) -> TestBatch
monadApplicative :: m (a, b) -> TestBatch
monadApplicative = TestBatch -> m (a, b) -> TestBatch
forall a b. a -> b -> a
const ( [Char]
"monad applicative"
                         , [ ([Char]
"pure", (a -> Property) -> Property
forall prop. Testable prop => prop -> Property
property a -> Property
pureP)
                           , ([Char]
"ap", (m (a -> b) -> m a -> Property) -> Property
forall prop. Testable prop => prop -> Property
property m (a -> b) -> m a -> Property
apP)
                           ]
                         )
 where
   pureP :: a -> Property
   apP :: m (a -> b) -> m a -> Property

   pureP :: a -> Property
pureP a
x = (a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x :: m a) m a -> m a -> Property
forall a. EqProp a => a -> a -> Property
=-= a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x
   apP :: m (a -> b) -> m a -> Property
apP m (a -> b)
f m a
x = (m (a -> b)
f m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> m a
x) m b -> m b -> Property
forall a. EqProp a => a -> a -> Property
=-= (m (a -> b)
f m (a -> b) -> m a -> m b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
`ap` m a
x)

-- | 'Monad' morphism properties

-- | 'Applicative' morphism properties
monadMorphism :: forall f g.
                 ( Monad f, Monad g
                 , Show (f NumT)
                 , Show (f (f (NumT -> T)))
                 , Arbitrary (f NumT), Arbitrary (f T)
                 , Arbitrary (f (f (NumT -> T)))
                 , EqProp (g NumT), EqProp (g T)
                 , EqProp (g (NumT -> T))
                 ) =>
                (forall a. f a -> g a) -> TestBatch
monadMorphism :: (forall a. f a -> g a) -> TestBatch
monadMorphism forall a. f a -> g a
q =
  ( [Char]
"monad morphism"
  , [ ([Char]
"return", (Int -> Property) -> Property
forall prop. Testable prop => prop -> Property
property Int -> Property
returnP), ([Char]
"bind", (f Int -> (Int -> f Char) -> Property) -> Property
forall prop. Testable prop => prop -> Property
property f Int -> (Int -> f Char) -> Property
bindP), ([Char]
"join", (f (f (Int -> Char)) -> Property) -> Property
forall prop. Testable prop => prop -> Property
property f (f (Int -> Char)) -> Property
joinP) ] )
 where
   returnP :: NumT -> Property
   bindP :: f NumT -> (NumT -> f T) -> Property
   joinP :: f (f (NumT->T)) -> Property

   returnP :: Int -> Property
returnP Int
a = f Int -> g Int
forall a. f a -> g a
q (Int -> f Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
a) g Int -> g Int -> Property
forall a. EqProp a => a -> a -> Property
=-= Int -> g Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
a
   bindP :: f Int -> (Int -> f Char) -> Property
bindP f Int
u Int -> f Char
k = f Char -> g Char
forall a. f a -> g a
q (f Int
u f Int -> (Int -> f Char) -> f Char
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Int -> f Char
k)  g Char -> g Char -> Property
forall a. EqProp a => a -> a -> Property
=-= (f Int -> g Int
forall a. f a -> g a
q f Int
u g Int -> (Int -> g Char) -> g Char
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= f Char -> g Char
forall a. f a -> g a
q (f Char -> g Char) -> (Int -> f Char) -> Int -> g Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> f Char
k)
   joinP :: f (f (Int -> Char)) -> Property
joinP f (f (Int -> Char))
uu  = f (Int -> Char) -> g (Int -> Char)
forall a. f a -> g a
q (f (f (Int -> Char)) -> f (Int -> Char)
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join f (f (Int -> Char))
uu)  g (Int -> Char) -> g (Int -> Char) -> Property
forall a. EqProp a => a -> a -> Property
=-= g (g (Int -> Char)) -> g (Int -> Char)
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join ((f (Int -> Char) -> g (Int -> Char))
-> g (f (Int -> Char)) -> g (g (Int -> Char))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (Int -> Char) -> g (Int -> Char)
forall a. f a -> g a
q (f (f (Int -> Char)) -> g (f (Int -> Char))
forall a. f a -> g a
q f (f (Int -> Char))
uu))

-- The join and bind properties are redundant.  Pick one.

--      q (join uu)
--   == q (uu >>= id)
--   == q uu >>= q . id
--   == q uu >>= q
--   == join (fmap q (q uu))

--      q (u >>= k)
--   == q (fmap k (join u))
--   == fmap k (q (join u))  -- if also a functor morphism
--   == fmap k (join (fmap q (q uu)))
--   == fmap k (q u >>= q)
--   == ???

-- I'm stuck at the end here.  What's missing?

-- | The semantic function ('model1') for @f@ is a 'monadMorphism'.
semanticMonad :: forall f g.
  ( Model1 f g
  , Monad f, Monad g
  , EqProp (g T) , EqProp (g NumT)
  , EqProp (g (NumT -> T))
  , Arbitrary (f T) , Arbitrary (f NumT)
  , Arbitrary (f (f (NumT -> T)))
  , Show (f (f (NumT -> T)))
  , Show (f NumT)
  ) =>
  f () -> TestBatch
semanticMonad :: f () -> TestBatch
semanticMonad = TestBatch -> f () -> TestBatch
forall a b. a -> b -> a
const ((forall a. f a -> g a) -> TestBatch
forall (f :: * -> *) (g :: * -> *).
(Monad f, Monad g, Show (f Int), Show (f (f (Int -> Char))),
 Arbitrary (f Int), Arbitrary (f Char),
 Arbitrary (f (f (Int -> Char))), EqProp (g Int), EqProp (g Char),
 EqProp (g (Int -> Char))) =>
(forall a. f a -> g a) -> TestBatch
monadMorphism (forall a. f a -> g a
forall (f :: * -> *) (g :: * -> *) a. Model1 f g => f a -> g a
model1 :: forall b. f b -> g b))

-- | Laws for MonadPlus instances with left distribution.
monadPlus :: forall m a b.
             ( MonadPlus m, Show (m a)
             , CoArbitrary a, Arbitrary (m a), Arbitrary (m b)
             , EqProp (m a), EqProp (m b)) =>
             m (a, b) -> TestBatch
monadPlus :: m (a, b) -> TestBatch
monadPlus = TestBatch -> m (a, b) -> TestBatch
forall a b. a -> b -> a
const ( [Char]
"MonadPlus laws"
                  , [ ([Char]
"left zero", ((a -> m b) -> Property) -> Property
forall prop. Testable prop => prop -> Property
property (a -> m b) -> Property
leftZeroP)
                    , ([Char]
"left identity", (m a -> m a -> m a) -> m a -> Property
forall a i.
(Show a, Arbitrary a, EqProp a) =>
(i -> a -> a) -> i -> Property
leftId m a -> m a -> m a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus (m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero :: m a))
                    , ([Char]
"right identity", (m a -> m a -> m a) -> m a -> Property
forall a i.
(Show a, Arbitrary a, EqProp a) =>
(a -> i -> a) -> i -> Property
rightId m a -> m a -> m a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus (m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero :: m a))
                    , ([Char]
"associativity" , (m a -> m a -> m a) -> Property
forall a.
(EqProp a, Show a, Arbitrary a) =>
(a -> a -> a) -> Property
isAssoc (m a -> m a -> m a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus :: Binop (m a)))
                    , ([Char]
"left distribution", (m a -> m a -> (a -> m b) -> Property) -> Property
forall prop. Testable prop => prop -> Property
property m a -> m a -> (a -> m b) -> Property
leftDistP)
                    ]
                  )
 where
   leftZeroP :: (a -> m b) -> Property
   leftDistP :: m a -> m a -> (a -> m b) -> Property

   leftZeroP :: (a -> m b) -> Property
leftZeroP a -> m b
k = (m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> m b
k) m b -> m b -> Property
forall a. EqProp a => a -> a -> Property
=-= m b
forall (m :: * -> *) a. MonadPlus m => m a
mzero
   leftDistP :: m a -> m a -> (a -> m b) -> Property
leftDistP m a
a m a
b a -> m b
k = (m a
a m a -> m a -> m a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` m a
b m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> m b
k) m b -> m b -> Property
forall a. EqProp a => a -> a -> Property
=-= ((m a
a m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> m b
k) m b -> m b -> m b
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` (m a
b m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> m b
k))

-- | Laws for MonadPlus instances with left catch.
monadOr :: forall m a b.
           ( MonadPlus m, Show a, Show (m a)
           , Arbitrary a, CoArbitrary a, Arbitrary (m a), Arbitrary (m b)
           , EqProp (m a), EqProp (m b)) =>
           m (a, b) -> TestBatch
monadOr :: m (a, b) -> TestBatch
monadOr = TestBatch -> m (a, b) -> TestBatch
forall a b. a -> b -> a
const ( [Char]
"MonadOr laws"
                , [ ([Char]
"left zero", ((a -> m b) -> Property) -> Property
forall prop. Testable prop => prop -> Property
property (a -> m b) -> Property
leftZeroP)
                  , ([Char]
"left identity", (m a -> m a -> m a) -> m a -> Property
forall a i.
(Show a, Arbitrary a, EqProp a) =>
(i -> a -> a) -> i -> Property
leftId m a -> m a -> m a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus (m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero :: m a))
                  , ([Char]
"right identity", (m a -> m a -> m a) -> m a -> Property
forall a i.
(Show a, Arbitrary a, EqProp a) =>
(a -> i -> a) -> i -> Property
rightId m a -> m a -> m a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus (m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero :: m a))
                  , ([Char]
"associativity" , (m a -> m a -> m a) -> Property
forall a.
(EqProp a, Show a, Arbitrary a) =>
(a -> a -> a) -> Property
isAssoc (m a -> m a -> m a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus :: Binop (m a)))
                  , ([Char]
"left catch", (a -> m a -> Property) -> Property
forall prop. Testable prop => prop -> Property
property a -> m a -> Property
leftCatchP)
                  ]
                )
 where
   leftZeroP :: (a -> m b) -> Property
   leftCatchP :: a -> m a -> Property

   leftZeroP :: (a -> m b) -> Property
leftZeroP a -> m b
k = (m a
forall (m :: * -> *) a. MonadPlus m => m a
mzero m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> m b
k) m b -> m b -> Property
forall a. EqProp a => a -> a -> Property
=-= m b
forall (m :: * -> *) a. MonadPlus m => m a
mzero
   leftCatchP :: a -> m a -> Property
leftCatchP a
a m a
b = a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a m a -> m a -> m a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` m a
b m a -> m a -> Property
forall a. EqProp a => a -> a -> Property
=-= a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a

-- | Check Alt Semigroup law
alt :: forall f a. ( Alt f, Arbitrary (f a)
                   , EqProp (f a), Show (f a)) =>
       f a -> TestBatch
alt :: f a -> TestBatch
alt = TestBatch -> f a -> TestBatch
forall a b. a -> b -> a
const ( [Char]
"Alt laws"
            , [ ([Char]
"associativity", (f a -> f a -> f a) -> Property
forall a.
(EqProp a, Show a, Arbitrary a) =>
(a -> a -> a) -> Property
isAssoc (f a -> f a -> f a
forall (f :: * -> *) a. Alt f => f a -> f a -> f a
(<!>) :: Binop (f a))) ] )


-- | Check Alternative Monoid laws
alternative :: forall f a. ( Alternative f, Arbitrary (f a)
                           , EqProp (f a), Show (f a)) =>
               f a -> TestBatch
alternative :: f a -> TestBatch
alternative = TestBatch -> f a -> TestBatch
forall a b. a -> b -> a
const ( [Char]
"Alternative laws"
                    , [ ([Char]
"left identity", (f a -> f a -> f a) -> f a -> Property
forall a i.
(Show a, Arbitrary a, EqProp a) =>
(i -> a -> a) -> i -> Property
leftId f a -> f a -> f a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>) (f a
forall (f :: * -> *) a. Alternative f => f a
empty :: f a))
                      , ([Char]
"right identity", (f a -> f a -> f a) -> f a -> Property
forall a i.
(Show a, Arbitrary a, EqProp a) =>
(a -> i -> a) -> i -> Property
rightId f a -> f a -> f a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>) (f a
forall (f :: * -> *) a. Alternative f => f a
empty :: f a))
                      , ([Char]
"associativity", (f a -> f a -> f a) -> Property
forall a.
(EqProp a, Show a, Arbitrary a) =>
(a -> a -> a) -> Property
isAssoc (f a -> f a -> f a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>) :: Binop (f a)))
                      ]
                    )


arrow :: forall a b c d e.
         ( Arrow a
         , Show (a d e), Show (a c d), Show (a b c)
         , Arbitrary (a d e), Arbitrary (a c d), Arbitrary (a b c)
         , Arbitrary c, Arbitrary d, Arbitrary e
         , CoArbitrary b, CoArbitrary c, CoArbitrary d
         , EqProp (a b e), EqProp (a b d)
         , EqProp (a (b,d) c)
         , EqProp (a (b,d) (c,d)), EqProp (a (b,e) (d,e))
         , EqProp (a (b,d) (c,e))
         ) =>
         a b (c,d,e) -> TestBatch
arrow :: a b (c, d, e) -> TestBatch
arrow = TestBatch -> a b (c, d, e) -> TestBatch
forall a b. a -> b -> a
const ([Char]
"arrow laws"
              , [ ([Char]
"associativity"           , (a b c -> a c d -> a d e -> Property) -> Property
forall prop. Testable prop => prop -> Property
property a b c -> a c d -> a d e -> Property
assocP)
                , ([Char]
"arr distributes"         , ((b -> c) -> (c -> d) -> Property) -> Property
forall prop. Testable prop => prop -> Property
property (b -> c) -> (c -> d) -> Property
arrDistributesP)
-- TODO: how to define h is onto or one-to-one?
--                , ("extensionality principle"     , property extensionalityP)
--                , ("extensionality dual"          , property extensionalityDualP)
                 , ([Char]
"first works as funs"    , ((b -> c) -> Property) -> Property
forall prop. Testable prop => prop -> Property
property (b -> c) -> Property
firstAsFunP)
                 , ([Char]
"first keeps composition", (a b c -> a c d -> Property) -> Property
forall prop. Testable prop => prop -> Property
property a b c -> a c d -> Property
firstKeepCompP)
                 , ([Char]
"first works as fst"     , (a b c -> Property) -> Property
forall prop. Testable prop => prop -> Property
property a b c -> Property
firstIsFstP)
                 , ([Char]
"second can move"        , (a b c -> (d -> e) -> Property) -> Property
forall prop. Testable prop => prop -> Property
property a b c -> (d -> e) -> Property
secondMovesP)
                 ]
              )
  where
    assocP :: a b c -> a c d -> a d e -> Property
    assocP :: a b c -> a c d -> a d e -> Property
assocP a b c
f a c d
g a d e
h = ((a b c
f a b c -> a c d -> a b d
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> a c d
g) a b d -> a d e -> a b e
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> a d e
h) a b e -> a b e -> Property
forall a. EqProp a => a -> a -> Property
=-= (a b c
f a b c -> a c e -> a b e
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> (a c d
g a c d -> a d e -> a c e
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> a d e
h))

    arrDistributesP :: (b -> c) -> (c -> d) -> Property
    arrDistributesP :: (b -> c) -> (c -> d) -> Property
arrDistributesP b -> c
f c -> d
g = (((b -> d) -> a b d
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (b -> c
f (b -> c) -> (c -> d) -> b -> d
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> c -> d
g)) :: a b d) a b d -> a b d -> Property
forall a. EqProp a => a -> a -> Property
=-= ((b -> c) -> a b c
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr b -> c
f a b c -> a c d -> a b d
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> (c -> d) -> a c d
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr c -> d
g)

    firstAsFunP :: (b -> c) -> Property
    firstAsFunP :: (b -> c) -> Property
firstAsFunP b -> c
f = (a b c -> a (b, d) (c, d)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first ((b -> c) -> a b c
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr b -> c
f) :: a (b,d) (c,d)) a (b, d) (c, d) -> a (b, d) (c, d) -> Property
forall a. EqProp a => a -> a -> Property
=-= ((b, d) -> (c, d)) -> a (b, d) (c, d)
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr ((b -> c) -> (b, d) -> (c, d)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first b -> c
f)

    firstKeepCompP :: a b c -> a c d -> Property
    firstKeepCompP :: a b c -> a c d -> Property
firstKeepCompP a b c
f a c d
g =
      ((a b d -> a (b, e) (d, e)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (a b c
f a b c -> a c d -> a b d
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> a c d
g)) :: (a (b,e) (d,e))) a (b, e) (d, e) -> a (b, e) (d, e) -> Property
forall a. EqProp a => a -> a -> Property
=-= (a b c -> a (b, e) (c, e)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first a b c
f a (b, e) (c, e) -> a (c, e) (d, e) -> a (b, e) (d, e)
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> a c d -> a (c, e) (d, e)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first a c d
g)

    firstIsFstP :: a b c -> Property
    firstIsFstP :: a b c -> Property
firstIsFstP a b c
f = ((a b c -> a (b, d) (c, d)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first a b c
f :: a (b,d) (c,d)) a (b, d) (c, d) -> a (c, d) c -> a (b, d) c
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> ((c, d) -> c) -> a (c, d) c
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (c, d) -> c
forall a b. (a, b) -> a
fst)
                      a (b, d) c -> a (b, d) c -> Property
forall a. EqProp a => a -> a -> Property
=-= (((b, d) -> b) -> a (b, d) b
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr (b, d) -> b
forall a b. (a, b) -> a
fst a (b, d) b -> a b c -> a (b, d) c
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> a b c
f)

    secondMovesP :: (a b c) -> (d -> e) -> Property
    secondMovesP :: a b c -> (d -> e) -> Property
secondMovesP a b c
f d -> e
g = (a b c -> a (b, d) (c, d)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first a b c
f a (b, d) (c, d) -> a (c, d) (c, e) -> a (b, d) (c, e)
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> a d e -> a (c, d) (c, e)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second ((d -> e) -> a d e
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr d -> e
g))
                         a (b, d) (c, e) -> a (b, d) (c, e) -> Property
forall a. EqProp a => a -> a -> Property
=-= ((a d e -> a (b, d) (b, e)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second ((d -> e) -> a d e
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr d -> e
g)) a (b, d) (b, e) -> a (b, e) (c, e) -> a (b, d) (c, e)
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> a b c -> a (b, e) (c, e)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first a b c
f)

arrowChoice :: forall a b c d e.
               ( ArrowChoice a
               , Show (a b c)
               , Arbitrary (a b c)
               , Arbitrary c, Arbitrary e
               , CoArbitrary b, CoArbitrary d
               , EqProp (a (Either b d) (Either c e))
               , EqProp (a (Either b d) (Either c d))
               ) =>
               a b (c,d,e) -> TestBatch
arrowChoice :: a b (c, d, e) -> TestBatch
arrowChoice = TestBatch -> a b (c, d, e) -> TestBatch
forall a b. a -> b -> a
const ([Char]
"arrow choice laws"
                    , [ ([Char]
"left works as funs", ((b -> c) -> Property) -> Property
forall prop. Testable prop => prop -> Property
property (b -> c) -> Property
leftAsFunP)
                      , ([Char]
"right can move"    , (a b c -> (d -> e) -> Property) -> Property
forall prop. Testable prop => prop -> Property
property a b c -> (d -> e) -> Property
rightMovesP)
                      ]
                    )
  where
    leftAsFunP :: (b -> c) -> Property
    leftAsFunP :: (b -> c) -> Property
leftAsFunP b -> c
f = (a b c -> a (Either b d) (Either c d)
forall (a :: * -> * -> *) b c d.
ArrowChoice a =>
a b c -> a (Either b d) (Either c d)
left ((b -> c) -> a b c
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr b -> c
f) :: a (Either b d) (Either c d))
                     a (Either b d) (Either c d)
-> a (Either b d) (Either c d) -> Property
forall a. EqProp a => a -> a -> Property
=-= (Either b d -> Either c d) -> a (Either b d) (Either c d)
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr ((b -> c) -> Either b d -> Either c d
forall (a :: * -> * -> *) b c d.
ArrowChoice a =>
a b c -> a (Either b d) (Either c d)
left b -> c
f)

    rightMovesP :: (a b c) -> (d -> e) -> Property
    rightMovesP :: a b c -> (d -> e) -> Property
rightMovesP a b c
f d -> e
g = (a b c -> a (Either b d) (Either c d)
forall (a :: * -> * -> *) b c d.
ArrowChoice a =>
a b c -> a (Either b d) (Either c d)
left a b c
f a (Either b d) (Either c d)
-> a (Either c d) (Either c e) -> a (Either b d) (Either c e)
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> a d e -> a (Either c d) (Either c e)
forall (a :: * -> * -> *) b c d.
ArrowChoice a =>
a b c -> a (Either d b) (Either d c)
right ((d -> e) -> a d e
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr d -> e
g))
                        a (Either b d) (Either c e)
-> a (Either b d) (Either c e) -> Property
forall a. EqProp a => a -> a -> Property
=-= ((a d e -> a (Either b d) (Either b e)
forall (a :: * -> * -> *) b c d.
ArrowChoice a =>
a b c -> a (Either d b) (Either d c)
right ((d -> e) -> a d e
forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr d -> e
g)) a (Either b d) (Either b e)
-> a (Either b e) (Either c e) -> a (Either b d) (Either c e)
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> a b c -> a (Either b e) (Either c e)
forall (a :: * -> * -> *) b c d.
ArrowChoice a =>
a b c -> a (Either b d) (Either c d)
left a b c
f)

traversable :: forall t a b c m f g.
               ( Traversable t, Applicative f, Applicative g, Monoid m
               , Arbitrary (t a), Arbitrary (t b), Arbitrary (f b), Arbitrary (g c)
               , Arbitrary (t (f (g a)))
               , Arbitrary m, Arbitrary b
               , CoArbitrary a, CoArbitrary b
               , Show (t a), Show (t b), Show (t (f (g a)))
               , EqProp (t b), EqProp m, EqProp (f (g (t a))), EqProp (f (g (t c)))) => t (f a, g b, c, m)
  -> TestBatch
traversable :: t (f a, g b, c, m) -> TestBatch
traversable = TestBatch -> t (f a, g b, c, m) -> TestBatch
forall a b. a -> b -> a
const ( [Char]
"Traversable"
                    , [ ([Char]
"identity", Property -> Property
forall prop. Testable prop => prop -> Property
property Property
identityP)
                      , ([Char]
"composition", ((a -> f b) -> (b -> g c) -> Property) -> Property
forall prop. Testable prop => prop -> Property
property (a -> f b) -> (b -> g c) -> Property
compositionP)
                      -- , ("naturality", property $ \(f :: f Int -> g Int) -> naturalityP f)
                      , ([Char]
"fmap", ((a -> b) -> t a -> Property) -> Property
forall prop. Testable prop => prop -> Property
property (a -> b) -> t a -> Property
fmapP)
                      , ([Char]
"foldMap", ((a -> m) -> t a -> Property) -> Property
forall prop. Testable prop => prop -> Property
property (a -> m) -> t a -> Property
foldMapP)
                      , ([Char]
"sequenceA identity", Property -> Property
forall prop. Testable prop => prop -> Property
property Property
sequenceIdentityP)
                      , ([Char]
"sequenceA composition", Property -> Property
forall prop. Testable prop => prop -> Property
property Property
sequenceCompositionP)
                      -- , ("sequenceA naturality", property $ \(f :: f a -> g a) -> sequenceNaturalityP f)
                      ]
                    )
 where
   identityP :: Property
   identityP :: Property
identityP = (b -> Identity b) -> t b -> Identity (t b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse @t @_ @b b -> Identity b
forall a. a -> Identity a
Identity (t b -> Identity (t b)) -> (t b -> Identity (t b)) -> Property
forall a. EqProp a => a -> a -> Property
=-= t b -> Identity (t b)
forall a. a -> Identity a
Identity

   compositionP :: (a -> f b) -> (b -> g c) -> Property
   compositionP :: (a -> f b) -> (b -> g c) -> Property
compositionP a -> f b
f b -> g c
g = (a -> Compose f g c) -> t a -> Compose f g (t c)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse @t (f (g c) -> Compose f g c
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f (g c) -> Compose f g c) -> (a -> f (g c)) -> a -> Compose f g c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b -> g c) -> f b -> f (g c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> g c
g (f b -> f (g c)) -> (a -> f b) -> a -> f (g c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> f b
f) (t a -> Compose f g (t c))
-> (t a -> Compose f g (t c)) -> Property
forall a. EqProp a => a -> a -> Property
=-= f (g (t c)) -> Compose f g (t c)
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f (g (t c)) -> Compose f g (t c))
-> (t a -> f (g (t c))) -> t a -> Compose f g (t c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (t b -> g (t c)) -> f (t b) -> f (g (t c))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((b -> g c) -> t b -> g (t c)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse b -> g c
g) (f (t b) -> f (g (t c))) -> (t a -> f (t b)) -> t a -> f (g (t c))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> f b) -> t a -> f (t b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> f b
f

   --FIXME: Does not compile due to rank2 type.
   --naturalityP :: (forall x. (f x -> g x)) -> (a -> f b) -> Property
   --naturalityP t f = t . traverse @t f =-= traverse (t . f)

   fmapP :: (a -> b) -> t a -> Property
   fmapP :: (a -> b) -> t a -> Property
fmapP a -> b
f t a
x = a -> b
f (a -> b) -> t a -> t b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` t a
x t b -> t b -> Property
forall a. EqProp a => a -> a -> Property
=-= a -> b
f (a -> b) -> t a -> t b
forall (t :: * -> *) a b. Traversable t => (a -> b) -> t a -> t b
`fmapDefault` t a
x

   foldMapP :: (a -> m) -> t a -> Property
   foldMapP :: (a -> m) -> t a -> Property
foldMapP a -> m
f t a
x = a -> m
f (a -> m) -> t a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
`foldMap` t a
x m -> m -> Property
forall a. EqProp a => a -> a -> Property
=-= (a -> m
f (a -> m) -> t a -> m
forall (t :: * -> *) m a.
(Traversable t, Monoid m) =>
(a -> m) -> t a -> m
`foldMapDefault` t a
x :: m)

   sequenceIdentityP :: Property
   sequenceIdentityP :: Property
sequenceIdentityP = Applicative Identity => t (Identity b) -> Identity (t b)
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA @t @_ @b (t (Identity b) -> Identity (t b))
-> (t b -> t (Identity b)) -> t b -> Identity (t b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b -> Identity b) -> t b -> t (Identity b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> Identity b
forall a. a -> Identity a
Identity (t b -> Identity (t b)) -> (t b -> Identity (t b)) -> Property
forall a. EqProp a => a -> a -> Property
=-= t b -> Identity (t b)
forall a. a -> Identity a
Identity

   sequenceCompositionP :: Property
   sequenceCompositionP :: Property
sequenceCompositionP = Applicative (Compose f g) => t (Compose f g a) -> Compose f g (t a)
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA @t @(Compose f g) @a (t (Compose f g a) -> Compose f g (t a))
-> (t (f (g a)) -> t (Compose f g a))
-> t (f (g a))
-> Compose f g (t a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (g a) -> Compose f g a) -> t (f (g a)) -> t (Compose f g a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (g a) -> Compose f g a
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (t (f (g a)) -> Compose f g (t a))
-> (t (f (g a)) -> Compose f g (t a)) -> Property
forall a. EqProp a => a -> a -> Property
=-= f (g (t a)) -> Compose f g (t a)
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f (g (t a)) -> Compose f g (t a))
-> (t (f (g a)) -> f (g (t a))) -> t (f (g a)) -> Compose f g (t a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (t (g a) -> g (t a)) -> f (t (g a)) -> f (g (t a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap t (g a) -> g (t a)
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA (f (t (g a)) -> f (g (t a)))
-> (t (f (g a)) -> f (t (g a))) -> t (f (g a)) -> f (g (t a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t (f (g a)) -> f (t (g a))
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA

   --FIXME: Does not compile due to rank2 type.
   --sequenceNaturalityP :: (forall x. (f x -> g x)) -> Property
   --sequenceNaturalityP t = t . sequenceA @t @_ @a =-= sequenceA . fmap t

-- | Note that 'foldable' doesn't check the strictness of 'foldl'', `foldr'' and `foldMap''.
--
-- @since 0.4.13

-- The (Arbitrary m) constraint is required with base >= 4.13, where we have an
-- additional property for checking foldMap'.
foldable :: forall t a b m n o.
            ( Foldable t
            , CoArbitrary a, CoArbitrary b
            , Arbitrary a, Arbitrary b, Arbitrary m, Arbitrary o, Arbitrary (t a), Arbitrary (t m), Arbitrary (t n), Arbitrary (t o)
            , Monoid m
            , Num n
            , Ord o
            , EqProp m, EqProp n, EqProp b, EqProp o, EqProp a
            , Show (t m), Show (t n), Show (t o), Show b, Show (t a), Show o) =>
            t (a, b, m, n, o) -> TestBatch
foldable :: t (a, b, m, n, o) -> TestBatch
foldable = TestBatch -> t (a, b, m, n, o) -> TestBatch
forall a b. a -> b -> a
const ( [Char]
"Foldable"
                 , [ ([Char]
"foldr and foldMap", ((a -> b -> b) -> b -> t a -> Property) -> Property
forall prop. Testable prop => prop -> Property
property (a -> b -> b) -> b -> t a -> Property
foldrFoldMapP)
                   , ([Char]
"foldl and foldMap", ((b -> a -> b) -> b -> t a -> Property) -> Property
forall prop. Testable prop => prop -> Property
property (b -> a -> b) -> b -> t a -> Property
foldlFoldMapP)
                   , ([Char]
"fold and foldMap", (t m -> Property) -> Property
forall prop. Testable prop => prop -> Property
property t m -> Property
foldFoldMapP)
                   , ([Char]
"length", (t a -> Property) -> Property
forall prop. Testable prop => prop -> Property
property t a -> Property
lengthP)
#if MIN_VERSION_base(4,13,0)
                   , ([Char]
"foldMap'", ((a -> m) -> t a -> Property) -> Property
forall prop. Testable prop => prop -> Property
property (a -> m) -> t a -> Property
foldMap'P)
#endif
                   , ([Char]
"foldr'", ((a -> b -> b) -> b -> t a -> Property) -> Property
forall prop. Testable prop => prop -> Property
property (a -> b -> b) -> b -> t a -> Property
foldr'P)
                   , ([Char]
"foldl'", ((b -> a -> b) -> b -> t a -> Property) -> Property
forall prop. Testable prop => prop -> Property
property (b -> a -> b) -> b -> t a -> Property
foldl'P)
                   , ([Char]
"foldr1", ((a -> a -> a) -> t a -> Property) -> Property
forall prop. Testable prop => prop -> Property
property (a -> a -> a) -> t a -> Property
foldr1P)
                   , ([Char]
"foldl1", ((a -> a -> a) -> t a -> Property) -> Property
forall prop. Testable prop => prop -> Property
property (a -> a -> a) -> t a -> Property
foldl1P)
                   , ([Char]
"toList", (t a -> Property) -> Property
forall prop. Testable prop => prop -> Property
property t a -> Property
toListP)
                   , ([Char]
"null", (t a -> Property) -> Property
forall prop. Testable prop => prop -> Property
property t a -> Property
nullP)
                   , ([Char]
"elem", (o -> t o -> Property) -> Property
forall prop. Testable prop => prop -> Property
property o -> t o -> Property
elemP)
                   , ([Char]
"maximum", (t o -> Property) -> Property
forall prop. Testable prop => prop -> Property
property t o -> Property
maximumP)
                   , ([Char]
"minimum", (t o -> Property) -> Property
forall prop. Testable prop => prop -> Property
property t o -> Property
minimumP)
                   , ([Char]
"sum", (t n -> Property) -> Property
forall prop. Testable prop => prop -> Property
property t n -> Property
sumP)
                   , ([Char]
"product", (t n -> Property) -> Property
forall prop. Testable prop => prop -> Property
property t n -> Property
productP)
                   ]
                 )
  where
    foldrFoldMapP :: (a -> b -> b) -> b -> t a -> Property
    foldrFoldMapP :: (a -> b -> b) -> b -> t a -> Property
foldrFoldMapP a -> b -> b
f b
z t a
t = (a -> b -> b) -> b -> t a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr a -> b -> b
f b
z t a
t b -> b -> Property
forall a. EqProp a => a -> a -> Property
=-= Endo b -> b -> b
forall a. Endo a -> a -> a
appEndo ((a -> Endo b) -> t a -> Endo b
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((b -> b) -> Endo b
forall a. (a -> a) -> Endo a
Endo ((b -> b) -> Endo b) -> (a -> b -> b) -> a -> Endo b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b -> b
f) t a
t ) b
z
    foldlFoldMapP :: (b -> a -> b) -> b -> t a -> Property
    foldlFoldMapP :: (b -> a -> b) -> b -> t a -> Property
foldlFoldMapP b -> a -> b
f b
z t a
t = (b -> a -> b) -> b -> t a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl b -> a -> b
f b
z t a
t b -> b -> Property
forall a. EqProp a => a -> a -> Property
=-= Endo b -> b -> b
forall a. Endo a -> a -> a
appEndo (Dual (Endo b) -> Endo b
forall a. Dual a -> a
getDual ((a -> Dual (Endo b)) -> t a -> Dual (Endo b)
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Endo b -> Dual (Endo b)
forall a. a -> Dual a
Dual (Endo b -> Dual (Endo b)) -> (a -> Endo b) -> a -> Dual (Endo b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b -> b) -> Endo b
forall a. (a -> a) -> Endo a
Endo ((b -> b) -> Endo b) -> (a -> b -> b) -> a -> Endo b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b -> a -> b) -> a -> b -> b
forall a b c. (a -> b -> c) -> b -> a -> c
flip b -> a -> b
f) t a
t)) b
z
    foldFoldMapP :: t m -> Property
    foldFoldMapP :: t m -> Property
foldFoldMapP t m
t = t m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold t m
t m -> m -> Property
forall a. EqProp a => a -> a -> Property
=-= (m -> m) -> t m -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap m -> m
forall a. a -> a
id t m
t
    lengthP :: t a -> Property
    lengthP :: t a -> Property
lengthP t a
t = t a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length t a
t Int -> Int -> Property
forall a. EqProp a => a -> a -> Property
=-= (Sum Int -> Int
forall a. Sum a -> a
getSum (Sum Int -> Int) -> (t a -> Sum Int) -> t a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Sum Int) -> t a -> Sum Int
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (Int -> Sum Int
forall a. a -> Sum a
Sum (Int -> Sum Int) -> (a -> Int) -> a -> Sum Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> a -> Int
forall a b. a -> b -> a
const  Int
1)) t a
t
#if MIN_VERSION_base(4,13,0)
    -- TODO: Check strictness
    foldMap'P :: (a -> m) -> t a -> Property
    foldMap'P :: (a -> m) -> t a -> Property
foldMap'P a -> m
f t a
t = (a -> m) -> t a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap' a -> m
f t a
t m -> m -> Property
forall a. EqProp a => a -> a -> Property
=-= (m -> a -> m) -> m -> t a -> m
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\m
acc a
a -> m
acc m -> m -> m
forall a. Semigroup a => a -> a -> a
<> a -> m
f a
a) m
forall a. Monoid a => a
mempty t a
t
#endif
    sumP :: t n -> Property
    sumP :: t n -> Property
sumP t n
t = t n -> n
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum t n
t n -> n -> Property
forall a. EqProp a => a -> a -> Property
=-= (Sum n -> n
forall a. Sum a -> a
getSum (Sum n -> n) -> (t n -> Sum n) -> t n -> n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (n -> Sum n) -> t n -> Sum n
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap n -> Sum n
forall a. a -> Sum a
Sum) t n
t
    productP :: t n -> Property
    productP :: t n -> Property
productP t n
t = t n -> n
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product t n
t n -> n -> Property
forall a. EqProp a => a -> a -> Property
=-= (Product n -> n
forall a. Product a -> a
getProduct (Product n -> n) -> (t n -> Product n) -> t n -> n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (n -> Product n) -> t n -> Product n
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap n -> Product n
forall a. a -> Product a
Product) t n
t
    maximumP :: t o -> Property
    maximumP :: t o -> Property
maximumP t o
t = Bool -> Bool
not (t o -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null t o
t) Bool -> Property -> Property
forall prop. Testable prop => Bool -> prop -> Property
==> t o -> o
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum t o
t o -> o -> Property
forall a. EqProp a => a -> a -> Property
=-= [o] -> o
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (t o -> [o]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList t o
t)
    minimumP :: t o -> Property
    minimumP :: t o -> Property
minimumP t o
t = Bool -> Bool
not (t o -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null t o
t) Bool -> Property -> Property
forall prop. Testable prop => Bool -> prop -> Property
==> t o -> o
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum t o
t o -> o -> Property
forall a. EqProp a => a -> a -> Property
=-= [o] -> o
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum (t o -> [o]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList t o
t)
    foldr1P :: (a -> a -> a) -> t a -> Property
    foldr1P :: (a -> a -> a) -> t a -> Property
foldr1P a -> a -> a
f t a
t = Bool -> Bool
not (t a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null t a
t) Bool -> Property -> Property
forall prop. Testable prop => Bool -> prop -> Property
==> (a -> a -> a) -> t a -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 a -> a -> a
f t a
t a -> a -> Property
forall a. EqProp a => a -> a -> Property
=-= (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 a -> a -> a
f (t a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList t a
t)
    foldl1P :: (a -> a -> a) -> t a -> Property
    foldl1P :: (a -> a -> a) -> t a -> Property
foldl1P a -> a -> a
f t a
t = Bool -> Bool
not (t a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null t a
t) Bool -> Property -> Property
forall prop. Testable prop => Bool -> prop -> Property
==> (a -> a -> a) -> t a -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 a -> a -> a
f t a
t a -> a -> Property
forall a. EqProp a => a -> a -> Property
=-= (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 a -> a -> a
f (t a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList t a
t)
    toListP :: t a -> Property
    toListP :: t a -> Property
toListP t a
t = t a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList t a
t [a] -> [a] -> Property
forall a. EqProp a => a -> a -> Property
=-= (a -> [a] -> [a]) -> [a] -> t a -> [a]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (:) [] t a
t
    nullP :: t a -> Property
    nullP :: t a -> Property
nullP t a
t = t a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null t a
t Bool -> Bool -> Property
forall a. EqProp a => a -> a -> Property
=-= (a -> Bool -> Bool) -> Bool -> t a -> Bool
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Bool -> Bool) -> a -> Bool -> Bool
forall a b. a -> b -> a
const (Bool -> Bool -> Bool
forall a b. a -> b -> a
const Bool
False)) Bool
True t a
t
    -- TODO: Check strictness
    foldr'P :: (a -> b -> b) -> b -> t a -> Property
    foldr'P :: (a -> b -> b) -> b -> t a -> Property
foldr'P a -> b -> b
f b
z t a
t = (a -> b -> b) -> b -> t a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr' a -> b -> b
f b
z t a
t b -> b -> Property
forall a. EqProp a => a -> a -> Property
=-= (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr' a -> b -> b
f b
z (t a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList t a
t)
    -- TODO: Check strictness
    foldl'P :: (b -> a -> b) -> b -> t a -> Property
    foldl'P :: (b -> a -> b) -> b -> t a -> Property
foldl'P b -> a -> b
f b
z t a
t = (b -> a -> b) -> b -> t a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' b -> a -> b
f b
z t a
t b -> b -> Property
forall a. EqProp a => a -> a -> Property
=-= (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' b -> a -> b
f b
z (t a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList t a
t)
    elemP :: o -> t o -> Property
    elemP :: o -> t o -> Property
elemP o
o t o
t = o -> t o -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem o
o t o
t Bool -> Bool -> Property
forall a. EqProp a => a -> a -> Property
=-= o -> [o] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem o
o (t o -> [o]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList t o
t)

-- | @since 0.4.13
foldableFunctor :: forall t a m.
                   ( Functor t, Foldable t
                   , CoArbitrary a
                   , Arbitrary m, Arbitrary (t a)
                   , EqProp m
                   , Monoid m
                   , Show (t a)) =>
                   t (a, m) -> TestBatch
foldableFunctor :: t (a, m) -> TestBatch
foldableFunctor = TestBatch -> t (a, m) -> TestBatch
forall a b. a -> b -> a
const ( [Char]
"Foldable Functor"
                        , [ ([Char]
"foldMap f = fold . fmap f", ((a -> m) -> t a -> Property) -> Property
forall prop. Testable prop => prop -> Property
property (a -> m) -> t a -> Property
foldMapP) ]
                        )
  where
    foldMapP :: (a -> m) -> t a -> Property
    foldMapP :: (a -> m) -> t a -> Property
foldMapP a -> m
f t a
t = (a -> m) -> t a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f t a
t m -> m -> Property
forall a. EqProp a => a -> a -> Property
=-= t m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold ((a -> m) -> t a -> t m
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> m
f t a
t)

-- | @since 0.5.7
bifoldable :: forall p a b c m.
               ( Bifoldable p, Monoid m
               , Show (p a b), Show (p m m)
               , Arbitrary (p a b), Arbitrary (p m m), Arbitrary m
               , CoArbitrary a, CoArbitrary b
               , EqProp m, EqProp c, CoArbitrary c, Arbitrary c, Show c) =>
               p a (b, c, m)  -> TestBatch
bifoldable :: p a (b, c, m) -> TestBatch
bifoldable = TestBatch -> p a (b, c, m) -> TestBatch
forall a b. a -> b -> a
const ( [Char]
"Bifoldable"
                    , [ ([Char]
"identity", Property -> Property
forall prop. Testable prop => prop -> Property
property Property
identityP)
                      , ([Char]
"bifoldMap f g ≡ bifoldr (mappend . f) (mappend . g) mempty", ((a -> m) -> (b -> m) -> Property) -> Property
forall prop. Testable prop => prop -> Property
property (a -> m) -> (b -> m) -> Property
bifoldMapBifoldrP)
                      , ([Char]
"bifoldr f g z t ≡ appEndo (bifoldMap (Endo . f) (Endo . g) t) z", ((a -> c -> c) -> (b -> c -> c) -> c -> p a b -> Property)
-> Property
forall prop. Testable prop => prop -> Property
property (a -> c -> c) -> (b -> c -> c) -> c -> p a b -> Property
bifoldrBifoldMapP)
                      ]
                    )
 where
   identityP :: Property
   identityP :: Property
identityP = p m m -> m
forall (p :: * -> * -> *) m. (Bifoldable p, Monoid m) => p m m -> m
bifold (p m m -> m) -> (p m m -> m) -> Property
forall a. EqProp a => a -> a -> Property
=-= ((m -> m) -> (m -> m) -> p m m -> m
forall (p :: * -> * -> *) m a b.
(Bifoldable p, Monoid m) =>
(a -> m) -> (b -> m) -> p a b -> m
bifoldMap m -> m
forall a. a -> a
id m -> m
forall a. a -> a
id :: p m m -> m)

   bifoldMapBifoldrP :: (a -> m) -> (b -> m) -> Property
   bifoldMapBifoldrP :: (a -> m) -> (b -> m) -> Property
bifoldMapBifoldrP a -> m
f b -> m
g = (a -> m) -> (b -> m) -> p a b -> m
forall (p :: * -> * -> *) m a b.
(Bifoldable p, Monoid m) =>
(a -> m) -> (b -> m) -> p a b -> m
bifoldMap a -> m
f b -> m
g (p a b -> m) -> (p a b -> m) -> Property
forall a. EqProp a => a -> a -> Property
=-= ((a -> m -> m) -> (b -> m -> m) -> m -> p a b -> m
forall (p :: * -> * -> *) a c b.
Bifoldable p =>
(a -> c -> c) -> (b -> c -> c) -> c -> p a b -> c
bifoldr (m -> m -> m
forall a. Monoid a => a -> a -> a
mappend (m -> m -> m) -> (a -> m) -> a -> m -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> m
f) (m -> m -> m
forall a. Monoid a => a -> a -> a
mappend (m -> m -> m) -> (b -> m) -> b -> m -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> m
g) m
forall a. Monoid a => a
mempty :: p a b -> m)

   bifoldrBifoldMapP :: (a -> c -> c) -> (b -> c -> c) -> c -> p a b -> Property
   bifoldrBifoldMapP :: (a -> c -> c) -> (b -> c -> c) -> c -> p a b -> Property
bifoldrBifoldMapP a -> c -> c
f b -> c -> c
g c
z p a b
t = (a -> c -> c) -> (b -> c -> c) -> c -> p a b -> c
forall (p :: * -> * -> *) a c b.
Bifoldable p =>
(a -> c -> c) -> (b -> c -> c) -> c -> p a b -> c
bifoldr a -> c -> c
f b -> c -> c
g c
z p a b
t c -> c -> Property
forall a. EqProp a => a -> a -> Property
=-= Endo c -> c -> c
forall a. Endo a -> a -> a
appEndo ((a -> Endo c) -> (b -> Endo c) -> p a b -> Endo c
forall (p :: * -> * -> *) m a b.
(Bifoldable p, Monoid m) =>
(a -> m) -> (b -> m) -> p a b -> m
bifoldMap ((c -> c) -> Endo c
forall a. (a -> a) -> Endo a
Endo ((c -> c) -> Endo c) -> (a -> c -> c) -> a -> Endo c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> c -> c
f) ((c -> c) -> Endo c
forall a. (a -> a) -> Endo a
Endo ((c -> c) -> Endo c) -> (b -> c -> c) -> b -> Endo c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> c -> c
g) p a b
t) c
z

-- | @since 0.5.7
bifoldableBifunctor :: forall p a b m.
                       ( Bifoldable p, Bifunctor p, Monoid m
                       , Show (p a b)
                       , Arbitrary (p a b), Arbitrary m, CoArbitrary a, CoArbitrary b
                       , EqProp m) =>
                       p a (b, m) -> TestBatch
bifoldableBifunctor :: p a (b, m) -> TestBatch
bifoldableBifunctor = TestBatch -> p a (b, m) -> TestBatch
forall a b. a -> b -> a
const ( [Char]
"Bifoldable Bifunctor"
                            , [ ([Char]
"bifoldMap f g ≡  bifold . bimap f g", ((a -> m) -> (b -> m) -> Property) -> Property
forall prop. Testable prop => prop -> Property
property (a -> m) -> (b -> m) -> Property
bifoldBimapP) ]
                            )
  where
    bifoldBimapP :: (a -> m) -> (b -> m) -> Property
    bifoldBimapP :: (a -> m) -> (b -> m) -> Property
bifoldBimapP a -> m
f b -> m
g = (a -> m) -> (b -> m) -> p a b -> m
forall (p :: * -> * -> *) m a b.
(Bifoldable p, Monoid m) =>
(a -> m) -> (b -> m) -> p a b -> m
bifoldMap a -> m
f b -> m
g (p a b -> m) -> (p a b -> m) -> Property
forall a. EqProp a => a -> a -> Property
=-= (p m m -> m
forall (p :: * -> * -> *) m. (Bifoldable p, Monoid m) => p m m -> m
bifold (p m m -> m) -> (p a b -> p m m) -> p a b -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> m) -> (b -> m) -> p a b -> p m m
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap a -> m
f b -> m
g :: p a b -> m)