Module

Test.StrongCheck.Laws.Data

Package
purescript-strongcheck-laws
Repository
garyb/purescript-strongcheck-laws

Re-exports from Test.StrongCheck.Laws.Data.BooleanAlgebra

#checkBooleanAlgebra Source

checkBooleanAlgebra :: forall a. Arbitrary a => BooleanAlgebra a => Eq a => Proxy a -> Effect Unit
  • Excluded middle: a || not a = tt

Re-exports from Test.StrongCheck.Laws.Data.Bounded

#checkBounded Source

checkBounded :: forall a. Arbitrary a => Bounded a => Ord a => Proxy a -> Effect Unit
  • Ordering: bottom <= a <= top

Re-exports from Test.StrongCheck.Laws.Data.CommutativeRing

#checkCommutativeRing Source

checkCommutativeRing :: forall a. CommutativeRing a => Arbitrary a => Eq a => Proxy a -> Effect Unit
  • Commutative multiplication: a * b = b * a

Re-exports from Test.StrongCheck.Laws.Data.DivisionRing

#checkDivisionRing Source

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

Re-exports from Test.StrongCheck.Laws.Data.Eq

#checkEq Source

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)

Re-exports from Test.StrongCheck.Laws.Data.EuclideanRing

#checkEuclideanRing Source

checkEuclideanRing :: forall a. EuclideanRing a => Arbitrary a => Eq a => Proxy a -> Effect Unit
  • Integral domain: a /= 0 and b /= 0 implies a * b /= 0
  • Multiplicative Euclidean function: a = (a / b) * b + (a `mod` b) where degree a > 0 and degree a <= degree (a * b)

Re-exports from Test.StrongCheck.Laws.Data.Field

#checkField Source

checkField :: forall a. Field a => Arbitrary a => Eq a => Proxy a -> Effect Unit
  • Non-zero multiplicative inverse: `amodb = 0 for all a and b

Re-exports from Test.StrongCheck.Laws.Data.Functor

#checkFunctor Source

checkFunctor :: forall f. Functor f => Arbitrary (f A) => Eq (f A) => Proxy2 f -> Effect Unit
  • Identity: (<$>) id = id
  • Composition: (<$>) (f <<< g) = (f <$>) <<< (g <$>)

Re-exports from Test.StrongCheck.Laws.Data.HeytingAlgebra

#checkHeytingAlgebra Source

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

Re-exports from Test.StrongCheck.Laws.Data.Monoid

#checkMonoid Source

checkMonoid :: forall m. Monoid m => Arbitrary m => Eq m => Proxy m -> Effect Unit
  • Left identity: mempty <> x = x
  • Right identity: x <> mempty = x

Re-exports from Test.StrongCheck.Laws.Data.Ord

#checkOrd Source

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

Re-exports from Test.StrongCheck.Laws.Data.Ring

#checkRing Source

checkRing :: forall a. Ring a => Arbitrary a => Eq a => Proxy a -> Effect Unit
  • Additive inverse: a - a = a + (-a) = (-a) + a = zero

Re-exports from Test.StrongCheck.Laws.Data.Semigroup

#checkSemigroup Source

checkSemigroup :: forall s. Semigroup s => Arbitrary s => Eq s => Proxy s -> Effect Unit
  • Associativity: (x <> y) <> z = x <> (y <> z)

Re-exports from Test.StrongCheck.Laws.Data.Semiring

#checkSemiring Source

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