From dd53c28122fbf5600209c65ee5591c76495a2aa0 Mon Sep 17 00:00:00 2001
From: Gary Burgess <gary.burgess@gmail.com>
Date: Sun, 3 Mar 2019 18:25:05 +0000
Subject: [PATCH] Add laws for 'Data' classes

---
 src/Data/BooleanAlgebra/Laws.purs  |  9 +++++
 src/Data/Bounded/Laws.purs         |  7 ++++
 src/Data/CommutativeRing/Laws.purs |  7 ++++
 src/Data/DivisionRing/Laws.purs    | 13 +++++++
 src/Data/Eq/Laws.purs              | 15 ++++++++
 src/Data/EuclideanRing/Laws.purs   | 39 +++++++++++++++++++
 src/Data/Functor/Laws.purs         | 13 +++++++
 src/Data/HeytingAlgebra.purs       |  7 ++--
 src/Data/HeytingAlgebra/Laws.purs  | 62 ++++++++++++++++++++++++++++++
 src/Data/Monoid.purs               |  6 +--
 src/Data/Monoid/Laws.purs          | 13 +++++++
 src/Data/Ord/Laws.purs             | 15 ++++++++
 src/Data/Ring/Laws.purs            |  7 ++++
 src/Data/Semigroup/Laws.purs       |  9 +++++
 src/Data/Semiring/Laws.purs        | 37 ++++++++++++++++++
 src/Laws/Algebraic.purs            | 39 +++++++++++++++++++
 16 files changed, 291 insertions(+), 7 deletions(-)
 create mode 100644 src/Data/BooleanAlgebra/Laws.purs
 create mode 100644 src/Data/Bounded/Laws.purs
 create mode 100644 src/Data/CommutativeRing/Laws.purs
 create mode 100644 src/Data/DivisionRing/Laws.purs
 create mode 100644 src/Data/Eq/Laws.purs
 create mode 100644 src/Data/EuclideanRing/Laws.purs
 create mode 100644 src/Data/Functor/Laws.purs
 create mode 100644 src/Data/HeytingAlgebra/Laws.purs
 create mode 100644 src/Data/Monoid/Laws.purs
 create mode 100644 src/Data/Ord/Laws.purs
 create mode 100644 src/Data/Ring/Laws.purs
 create mode 100644 src/Data/Semigroup/Laws.purs
 create mode 100644 src/Data/Semiring/Laws.purs
 create mode 100644 src/Laws/Algebraic.purs

diff --git a/src/Data/BooleanAlgebra/Laws.purs b/src/Data/BooleanAlgebra/Laws.purs
new file mode 100644
index 00000000..41472fb0
--- /dev/null
+++ b/src/Data/BooleanAlgebra/Laws.purs
@@ -0,0 +1,9 @@
+module Data.BooleanAlgebra.Laws where
+
+import Prelude
+
+import Data.BooleanAlgebra (tt)
+
+-- | `a || not a = tt`
+excludedMiddle :: forall a. Eq a => BooleanAlgebra a => a -> Boolean
+excludedMiddle a = (a || not a) == tt
diff --git a/src/Data/Bounded/Laws.purs b/src/Data/Bounded/Laws.purs
new file mode 100644
index 00000000..0f316eff
--- /dev/null
+++ b/src/Data/Bounded/Laws.purs
@@ -0,0 +1,7 @@
+module Data.Bounded.Laws where
+
+import Prelude
+
+-- | `bottom <= a <= top`
+ordering ∷ ∀ a. Bounded a ⇒ a → Boolean
+ordering a = bottom <= a && a <= top
diff --git a/src/Data/CommutativeRing/Laws.purs b/src/Data/CommutativeRing/Laws.purs
new file mode 100644
index 00000000..bb1d4db6
--- /dev/null
+++ b/src/Data/CommutativeRing/Laws.purs
@@ -0,0 +1,7 @@
+module Data.CommutativeRing.Laws where
+
+import Prelude
+
+-- | `a * b = b * a`
+commutativeMul :: forall a. Eq a => CommutativeRing a => a -> a -> Boolean
+commutativeMul a b = a * b == b * a
diff --git a/src/Data/DivisionRing/Laws.purs b/src/Data/DivisionRing/Laws.purs
new file mode 100644
index 00000000..af59cf80
--- /dev/null
+++ b/src/Data/DivisionRing/Laws.purs
@@ -0,0 +1,13 @@
+module Data.DivisionRing.Laws where
+
+import Prelude
+
+-- | `one /= zero`
+divisionRingIdentity :: forall proxy a. Eq a => DivisionRing a => proxy a -> Boolean
+divisionRingIdentity _ = one /= (zero :: a)
+
+-- | For all nonzero a `recip a * a = a * recip a = one`
+multiplicativeInverse :: forall a. Eq a => DivisionRing a => a -> a -> Boolean
+multiplicativeInverse a b
+  | a /= zero = (recip a * a == one) && (a * recip a == one)
+  | otherwise = true
diff --git a/src/Data/Eq/Laws.purs b/src/Data/Eq/Laws.purs
new file mode 100644
index 00000000..defd125a
--- /dev/null
+++ b/src/Data/Eq/Laws.purs
@@ -0,0 +1,15 @@
+module Data.Eq.Laws where
+
+import Prelude
+
+-- | `x == x = true`
+reflexivity ∷ ∀ a. Eq a ⇒ a → Boolean
+reflexivity x = (x == x) == true
+
+-- | `x == y = y == x`
+symmetry ∷ ∀ a. Eq a ⇒ a → a → Boolean
+symmetry x y = (x == y) == (y == x)
+
+-- | if `x == y` and `y == z` then `x == z`
+transitivity ∷ ∀ a. Eq a ⇒ a → a → a → Boolean
+transitivity x y z = if (x == y) && (y == z) then x == z else true
diff --git a/src/Data/EuclideanRing/Laws.purs b/src/Data/EuclideanRing/Laws.purs
new file mode 100644
index 00000000..86b358c0
--- /dev/null
+++ b/src/Data/EuclideanRing/Laws.purs
@@ -0,0 +1,39 @@
+module Data.EuclideanRing.Laws where
+
+import Prelude
+
+-- | `one /= zero`
+integralDomainIdentity :: forall proxy a. Eq a => EuclideanRing a => proxy a -> Boolean
+integralDomainIdentity _ = one /= (zero :: a)
+
+-- | if `a` and `b` are both nonzero then so is `a * b`
+integralDomainDivision :: forall a. Eq a => EuclideanRing a => a -> a -> Boolean
+integralDomainDivision a b
+  | a /= zero && b /= zero = a * b /= zero
+  | otherwise = true
+
+-- | For all nonzero `a`, `degree a >= zero`
+nonNegativeDegree :: forall a. Eq a => EuclideanRing a => a -> Boolean
+nonNegativeDegree a
+  | a /= zero = degree a >= zero
+  | otherwise = true
+
+-- | 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`.
+divisionWithRem :: forall a. Eq a => EuclideanRing a => a -> a -> Boolean
+divisionWithRem a b
+  | b /= zero =
+      let
+        q = a / b
+        r = a `mod` b
+      in
+        a == b * q + r && (r == zero || degree r < degree b)
+  | otherwise =
+      true
+
+-- | For all nonzero `a` and `b`, `degree a <= degree (a * b)`
+submultiplicativeDegree :: forall a. Eq a => EuclideanRing a => a -> a -> Boolean
+submultiplicativeDegree a b
+  | a /= zero && b /= zero = degree a < degree (a * b)
+  | otherwise = true
diff --git a/src/Data/Functor/Laws.purs b/src/Data/Functor/Laws.purs
new file mode 100644
index 00000000..8aa4331d
--- /dev/null
+++ b/src/Data/Functor/Laws.purs
@@ -0,0 +1,13 @@
+module Data.Functor.Laws where
+
+import Prelude hiding (identity)
+
+import Control.Category as C
+
+-- | `map identity = identity`
+identity ∷ ∀ f a. Functor f ⇒ Eq (f a) ⇒ f a → Boolean
+identity f = (map C.identity f) == C.identity f
+
+-- | `map (f <<< g) = map f <<< map g`
+composition ∷ ∀ f a b. Functor f ⇒ Eq (f a) ⇒ (b → a) → (a → b) → f a → Boolean
+composition f g x = (map (f <<< g) x) == (((map f) <<< (map g)) x)
diff --git a/src/Data/HeytingAlgebra.purs b/src/Data/HeytingAlgebra.purs
index 5b6920f1..aed52624 100644
--- a/src/Data/HeytingAlgebra.purs
+++ b/src/Data/HeytingAlgebra.purs
@@ -21,8 +21,7 @@ import Type.Data.RowList (RLProxy(..))
 -- |   - `a || b = b || a`
 -- |   - `a && b = b && a`
 -- | - Absorption:
--- |   - `a || (a && b) = a`
--- |   - `a && (a || b) = a`
+-- |   - `a || (a && b) = a && (a || b) = a`
 -- | - Idempotent:
 -- |   - `a || a = a`
 -- |   - `a && a = a`
@@ -31,8 +30,8 @@ import Type.Data.RowList (RLProxy(..))
 -- |   - `a && tt = a`
 -- | - Implication:
 -- |   - ``a `implies` a = tt``
--- |   - ``a && (a `implies` b) = a && b``
--- |   - ``b && (a `implies` b) = b``
+-- |   - ``(a && b) `implies` (b && c) = a `implies` c``
+-- |   - ``(a `implies` b) || (b `implies` a)``
 -- |   - ``a `implies` (b && c) = (a `implies` b) && (a `implies` c)``
 -- | - Complemented:
 -- |   - ``not a = a `implies` ff``
diff --git a/src/Data/HeytingAlgebra/Laws.purs b/src/Data/HeytingAlgebra/Laws.purs
new file mode 100644
index 00000000..373c33f5
--- /dev/null
+++ b/src/Data/HeytingAlgebra/Laws.purs
@@ -0,0 +1,62 @@
+module Data.HeytingAlgebra.Laws where
+
+import Prelude
+
+import Data.HeytingAlgebra (ff, implies, tt)
+import Laws.Algebraic as Laws
+
+-- | `a || (b || c) = (a || b) || c`
+associativeDisj :: forall a. Eq a => HeytingAlgebra a => a -> a -> a -> Boolean
+associativeDisj = Laws.associative (||)
+
+-- | `a && (b && c) = (a && b) && c`
+associativeConj :: forall a. Eq a => HeytingAlgebra a => a -> a -> a -> Boolean
+associativeConj = Laws.associative (&&)
+
+-- | `a || b = b || a`
+commutativeDisj :: forall a. Eq a => HeytingAlgebra a => a -> a -> Boolean
+commutativeDisj = Laws.commutative (||)
+
+-- | `a && b = b && a`
+commutativeConj :: forall a. Eq a => HeytingAlgebra a => a -> a -> Boolean
+commutativeConj = Laws.commutative (&&)
+
+-- | `a || (a && b) = a && (a || b) = a`
+absorption :: forall a. Eq a => HeytingAlgebra a => a -> a -> Boolean
+absorption = Laws.absorption (||) (&&)
+
+-- | `a || a = a`
+idempotentDisj :: forall a. Eq a => HeytingAlgebra a => a -> a -> Boolean
+idempotentDisj = Laws.idempotent (||)
+
+-- | `a && a = a`
+idempotentConj :: forall a. Eq a => HeytingAlgebra a => a -> a -> Boolean
+idempotentConj = Laws.idempotent (&&)
+
+-- | `a || ff = a`
+identityDisj :: forall a. Eq a => HeytingAlgebra a => a -> Boolean
+identityDisj = Laws.identity (||) ff
+
+-- | `a && tt = a`
+identityConj :: forall a. Eq a => HeytingAlgebra a => a -> Boolean
+identityConj = Laws.identity (&&) tt
+
+-- | ``a `implies` a = tt``
+reflexiveImplies :: forall a. Eq a => HeytingAlgebra a => a -> Boolean
+reflexiveImplies a = (a `implies` a) == tt
+
+-- | ``(a && b) `implies` (b && c) = a `implies` c``
+transitiveImplies :: forall a. Eq a => HeytingAlgebra a => a -> a -> a -> Boolean
+transitiveImplies a b c = (a && b) `implies` (b && c) == a `implies` c
+
+-- | ``(a `implies` b) || (b `implies` a)``
+totalImplies :: forall a. HeytingAlgebra a => a -> a -> a
+totalImplies a b = (a `implies` b) || (b `implies` a)
+
+-- | ``a `implies` (b && c) = (a `implies` b) && (a `implies` c)``
+leftDistributiveImplies :: forall a. Eq a => HeytingAlgebra a => a -> a -> a -> Boolean
+leftDistributiveImplies = Laws.leftDistributive implies (&&)
+
+-- | ``not a = a `implies` ff``
+complemented :: forall a. Eq a => HeytingAlgebra a => a -> Boolean
+complemented a = not a == (a `implies` ff)
diff --git a/src/Data/Monoid.purs b/src/Data/Monoid.purs
index 6ffa614d..f119115c 100644
--- a/src/Data/Monoid.purs
+++ b/src/Data/Monoid.purs
@@ -20,10 +20,10 @@ import Record.Unsafe (unsafeSet)
 import Type.Data.RowList (RLProxy(..))
 
 -- | A `Monoid` is a `Semigroup` with a value `mempty`, which is both a
--- | left and right unit for the associative operation `<>`:
+-- | left and right identity for the associative operation `<>`:
 -- |
--- | - Left unit: `(mempty <> x) = x`
--- | - Right unit: `(x <> mempty) = x`
+-- | - Left identity: `(mempty <> x) = x`
+-- | - Right identity: `(x <> mempty) = x`
 -- |
 -- | `Monoid`s are commonly used as the result of fold operations, where
 -- | `<>` is used to combine individual results, and `mempty` gives the result
diff --git a/src/Data/Monoid/Laws.purs b/src/Data/Monoid/Laws.purs
new file mode 100644
index 00000000..947bb5ea
--- /dev/null
+++ b/src/Data/Monoid/Laws.purs
@@ -0,0 +1,13 @@
+module Data.Monoid.Laws where
+
+import Prelude
+
+import Laws.Algebraic as Laws
+
+-- | `(mempty <> x) = x`
+leftIdentity ∷ ∀ a. Monoid a ⇒ Eq a ⇒ a → Boolean
+leftIdentity = Laws.leftIdentity (<>) mempty
+
+-- | `(x <> mempty) = x`
+rightIdentity ∷ ∀ a. Monoid a ⇒ Eq a ⇒ a → Boolean
+rightIdentity = Laws.rightIdentity (<>) mempty
diff --git a/src/Data/Ord/Laws.purs b/src/Data/Ord/Laws.purs
new file mode 100644
index 00000000..50be2094
--- /dev/null
+++ b/src/Data/Ord/Laws.purs
@@ -0,0 +1,15 @@
+module Data.Ord.Laws where
+
+import Prelude
+
+-- | `a <= a`
+reflexivity ∷ ∀ a. Ord a ⇒ a → Boolean
+reflexivity a = a <= a
+
+-- | if `a <= b` and `b <= a` then `a = b`
+antisymmetry ∷ ∀ a. Ord a ⇒ a → a → Boolean
+antisymmetry a b = if (a <= b) && (b <= a) then a == b else a /= b
+
+-- | if `a <= b` and `b <= c` then `a <= c`
+transitivity ∷ ∀ a. Ord a ⇒ a → a → a → Boolean
+transitivity a b c = if (a <= b) && (b <= c) then a <= c else true
diff --git a/src/Data/Ring/Laws.purs b/src/Data/Ring/Laws.purs
new file mode 100644
index 00000000..63e04e2c
--- /dev/null
+++ b/src/Data/Ring/Laws.purs
@@ -0,0 +1,7 @@
+module Data.Ring.Laws where
+
+import Prelude
+
+-- | `a - a = (zero - a) + a = zero`
+additiveInverse :: forall a. Eq a => Ring a => a -> Boolean
+additiveInverse a = a - a == (zero - a) + a && a - a == zero
diff --git a/src/Data/Semigroup/Laws.purs b/src/Data/Semigroup/Laws.purs
new file mode 100644
index 00000000..5f72ed49
--- /dev/null
+++ b/src/Data/Semigroup/Laws.purs
@@ -0,0 +1,9 @@
+module Data.Semigroup.Laws where
+
+import Prelude
+
+import Laws.Algebraic as Laws
+
+-- | ((x <> y) <> z) = (x <> (y <> z))
+associative ∷ ∀ a. Semigroup a ⇒ Eq a ⇒ a → a → a → Boolean
+associative = Laws.associative (<>)
diff --git a/src/Data/Semiring/Laws.purs b/src/Data/Semiring/Laws.purs
new file mode 100644
index 00000000..28918bbe
--- /dev/null
+++ b/src/Data/Semiring/Laws.purs
@@ -0,0 +1,37 @@
+module Data.Semiring.Laws where
+
+import Prelude
+
+import Laws.Algebraic as Laws
+
+-- | `(a + b) + c = a + (b + c)`
+associativeAdd :: forall a. Eq a => Semiring a => a -> a -> a -> Boolean
+associativeAdd = Laws.associative (+)
+
+-- | `zero + a = a + zero = a`
+identityAdd :: forall a. Eq a => Semiring a => a -> Boolean
+identityAdd = Laws.identity (+) zero
+
+-- | `a + b = b + a`
+commutativeAdd :: forall a. Eq a => Semiring a => a -> a -> Boolean
+commutativeAdd = Laws.commutative (+)
+
+-- | `(a * b) * c = a * (b * c)`
+associativeMul :: forall a. Eq a => Semiring a => a -> a -> a -> Boolean
+associativeMul = Laws.associative (*)
+
+-- | `one * a = a * one = a`
+identityMul :: forall a. Eq a => Semiring a => a -> Boolean
+identityMul = Laws.identity (*) one
+
+-- | `a * (b + c) = (a * b) + (a * c)`
+leftDistributive :: forall t7. Eq t7 => Semiring t7 => t7 -> t7 -> t7 -> Boolean
+leftDistributive = Laws.leftDistributive (*) (+)
+
+-- | `(a + b) * c = (a * c) + (b * c)`
+rightDistributive :: forall a. Eq a => Semiring a => a -> a -> a -> Boolean
+rightDistributive = Laws.rightDistributive (*) (+)
+
+-- | `zero * a = a * zero = zero`
+annihilation :: forall a. Eq a => Semiring a => a -> Boolean
+annihilation a = zero * a == zero && a * zero == zero
diff --git a/src/Laws/Algebraic.purs b/src/Laws/Algebraic.purs
new file mode 100644
index 00000000..59604858
--- /dev/null
+++ b/src/Laws/Algebraic.purs
@@ -0,0 +1,39 @@
+module Laws.Algebraic where
+
+import Prelude
+
+-- | `id • a = a`
+leftIdentity :: forall a id. Eq a => (id -> a -> a) -> id -> a -> Boolean
+leftIdentity op id x = (id `op` x) == x
+
+-- | `a • id = a`
+rightIdentity :: forall a id. Eq a => (a -> id -> a) -> id -> a -> Boolean
+rightIdentity op id x = (x `op` id) == x
+
+-- | `id • a = a • id = a`
+identity :: forall a. Eq a => (a -> a -> a) -> a -> a -> Boolean
+identity op id x = leftIdentity op id x && rightIdentity op id x
+
+-- | `a • (b • c) = (a • b) • c`
+associative :: forall a. Eq a => (a -> a -> a) -> a -> a -> a -> Boolean
+associative op a b c = (a `op` (b `op` c)) == ((a `op` b) `op` c)
+
+-- | `a • b = b • a`
+commutative :: forall a. Eq a => (a -> a -> a) -> a -> a -> Boolean
+commutative op a b = (a `op` b) == (b `op` a)
+
+-- | `a • (b ◆ c) = (a • b) ◆ (a • c)`
+leftDistributive :: forall a. Eq a => (a -> a -> a) -> (a -> a -> a) -> a -> a -> a -> Boolean
+leftDistributive op1 op2 a b c = a `op1` (b `op2` c) == (a `op1` b) `op2` (a `op1` c)
+
+-- | `(a ◆ b) • c = (a • c) ◆ (b • c)`
+rightDistributive :: forall a. Eq a => (a -> a -> a) -> (a -> a -> a) -> a -> a -> a -> Boolean
+rightDistributive op1 op2 a b c = (a `op2` b) `op1` c == (a `op1` c) `op2` (b `op1` c)
+
+-- | `a • a = a`
+idempotent :: forall a. Eq a => (a -> a -> a) -> a -> a -> Boolean
+idempotent op a b = a `op` a == a
+
+-- | `a • (a ◆ b) = a ◆ (a • b) = a`
+absorption :: forall a. Eq a => (a -> a -> a) -> (a -> a -> a) -> a -> a -> Boolean
+absorption op1 op2 a b = (a `op1` (a `op2` b)) == a && (a `op2` (a `op1` b)) == a