Test.QuickCheck.Laws.Data

checkBooleanAlgebraGen :: forall a. BooleanAlgebra a => Eq a => Gen a -> Effect Unit

checkBooleanAlgebra :: forall a. Arbitrary a => BooleanAlgebra a => Eq a => Proxy a -> Effect Unit

• Excluded middle: a || not a = tt

checkBoundedGen :: forall a. Bounded a => Ord a => Gen a -> Effect Unit

checkBounded :: forall a. Arbitrary a => Bounded a => Ord a => Proxy a -> Effect Unit

• Ordering: bottom <= a <= top

checkBoundedEnumGen :: forall a. BoundedEnum a => Ord a => Gen a -> Effect Unit

checkBoundedEnum :: forall a. Arbitrary a => BoundedEnum a => Ord a => Proxy a -> Effect Unit

• succ: succ bottom >>= succ >>= succ ... succ [cardinality - 1 times] = top
• pred: pred top >>= pred >>= pred ... pred [cardinality - 1 times] = bottom
• predsucc: forall a > bottom: pred a >>= succ = Just a
• succpred: forall a < top: succ a >>= pred = Just a
• enumpred: forall a > bottom: fromEnum <$> pred a = Just (fromEnum a - 1)
• enumsucc: forall a < top: fromEnum <$> succ a = Just (fromEnum a + 1)
• compare: compare e1 e2 = compare (fromEnum e1) (fromEnum e2)
• tofromenum: toEnum (fromEnum a) = Just a

checkCommutativeRingGen :: forall a. CommutativeRing a => Eq a => Gen a -> Effect Unit

checkCommutativeRing :: forall a. CommutativeRing a => Arbitrary a => Eq a => Proxy a -> Effect Unit

• Commutative multiplication: a * b = b * a

checkDivisionRingGen :: forall a. DivisionRing a => Eq a => Gen a -> Effect Unit

checkDivisionRing :: forall a. DivisionRing a => Arbitrary a => Eq a => Proxy a -> Effect Unit

Non-zero ring: one /= zero Non-zero multiplicative inverse: recip a * a = a * recip a = one for all non-zero a

checkEnumGen :: forall a. Enum a => Ord a => Gen a -> Effect Unit

checkEnum :: forall a. Arbitrary a => Enum a => Ord a => Proxy a -> Effect Unit

checkEqGen :: forall a. Eq a => Gen a -> Effect Unit

checkEq :: forall a. Arbitrary a => Eq a => Proxy a -> Effect Unit

• Reflexivity: x == x = true
• Symmetry: x == y = y == x
• Transitivity: if x == y and y == z then x == z
• Negation: x /= y = not (x == y)

checkEuclideanRingGen :: forall a. EuclideanRing a => Eq a => Gen a -> Effect Unit

checkEuclideanRing :: forall a. EuclideanRing a => Arbitrary a => Eq a => Proxy a -> Effect Unit

• Integral domain: one /= zero, and if a and b are both nonzero then so is their product a * b
• Euclidean function degree:
  • Nonnegativity: For all nonzero a, degree a >= 0
  • Quotient/remainder: For all a and b, where b is nonzero, let q = a / b and r = a `mod` b; then a = q*b + r, and also either r = zero or degree r < degree b
• Submultiplicative euclidean function:
  • For all nonzero a and b, degree a <= degree (a * b)

checkFieldGen :: forall a. Field a => Eq a => Gen a -> Effect Unit

checkField :: forall a. Field a => Arbitrary a => Eq a => Proxy a -> Effect Unit

• Non-zero multiplicative inverse: a `mod` b = 0 for all a and b

checkFoldableGen :: forall f. Foldable f => Gen (f A) -> Effect Unit

checkFoldableFunctorGen :: forall f. Foldable f => Functor f => Gen (f A) -> Effect Unit

checkFoldableFunctor :: forall f. Foldable f => Functor f => Arbitrary (f A) => Proxy f -> Effect Unit

foldMap: foldMap = fold <<< map

checkFoldable :: forall f. Foldable f => Arbitrary (f A) => Proxy f -> Effect Unit

• foldr: foldr = foldrDefault
• foldl: foldl = foldlDefault

checkFunctorGen :: forall f. Functor f => Eq (f A) => Gen (f A) -> Effect Unit

checkFunctor :: forall f. Functor f => Arbitrary (f A) => Eq (f A) => Proxy f -> Effect Unit

• Identity: (<$>) id = id
• Composition: (<$>) (f <<< g) = (f <$>) <<< (g <$>)

checkFunctorWithIndexGen :: forall f i. FunctorWithIndex i f => Coarbitrary i => Eq (f A) => Gen (f A) -> Effect Unit

checkFunctorWithIndex :: forall f i. FunctorWithIndex i f => Arbitrary (f A) => Coarbitrary i => Eq (f A) => Proxy f -> Effect Unit

• Identity: mapWithIndex (\_ a → a) = identity
• Composition: mapWithIndex f . mapWithIndex g = mapWithIndex (\i → f i <<< g i)

checkHeytingAlgebraGen :: forall a. HeytingAlgebra a => Eq a => Gen a -> Effect Unit

checkHeytingAlgebra :: forall a. Arbitrary a => HeytingAlgebra a => Eq a => Proxy a -> Effect Unit

• Associativity:
  • a || (b || c) = (a || b) || c
  • a && (b && c) = (a && b) && c
• Commutativity:
  • a || b = b || a
  • a && b = b && a
• Absorption:
  • a || (a && b) = a
  • a && (a || b) = a
• Idempotent:
  • a || a = a
  • a && a = a
• Identity:
  • a || ff = a
  • a && tt = a
• Implication:
  • a `implies` a = tt
  • a && (a `implies` b) = a && b
  • b && (a `implies` b) = b
  • a `implies` (b && c) = (a `implies` b) && (a `implies` c)
• Complemented:
  • not a = a `implies` ff

checkMonoidGen :: forall m. Monoid m => Eq m => Gen m -> Effect Unit

checkMonoid :: forall m. Monoid m => Arbitrary m => Eq m => Proxy m -> Effect Unit

• Left identity: mempty <> x = x
• Right identity: x <> mempty = x

checkOrdGen :: forall a. Ord a => Gen a -> Effect Unit

checkOrd :: forall a. Arbitrary a => Ord a => Proxy a -> Effect Unit

• Reflexivity: a <= a
• Antisymmetry: if a <= b and b <= a then a = b
• Transitivity: if a <= b and b <= c then a <= c

checkRingGen :: forall a. Ring a => Eq a => Gen a -> Effect Unit

checkRing :: forall a. Ring a => Arbitrary a => Eq a => Proxy a -> Effect Unit

• Additive inverse: a - a = a + (-a) = (-a) + a = zero

checkSemigroupGen :: forall s. Semigroup s => Eq s => Gen s -> Effect Unit

checkSemigroup :: forall s. Semigroup s => Arbitrary s => Eq s => Proxy s -> Effect Unit

• Associativity: (x <> y) <> z = x <> (y <> z)

checkSemiringGen :: forall a. Semiring a => Eq a => Gen a -> Effect Unit

checkSemiring :: forall a. Semiring a => Arbitrary a => Eq a => Proxy a -> Effect Unit

• Commutative monoid under addition:
  • Associativity: (a + b) + c = a + (b + c)
  • Identity: zero + a = a + zero = a
  • Commutative: a + b = b + a
• Monoid under multiplication:
  • Associativity: (a * b) * c = a * (b * c)
  • Identity: one * a = a * one = a
• Multiplication distributes over addition:
  • Left distributivity: a * (b + c) = (a * b) + (a * c)
  • Right distributivity: (a + b) * c = (a * c) + (b * c)
• Annihiliation: zero * a = a * zero = zero