Update class hierarchies

Author: garyb

src/Data/BooleanAlgebra.purs

@@ -1,63 +1,20 @@
 module Data.BooleanAlgebra
-  ( class BooleanAlgebra, conj, disj, not
-  , (&&), (||)
+  ( class BooleanAlgebra
+  , module Data.HeytingAlgebra
   ) where
 
-import Data.Bounded (class Bounded)
-import Data.Unit (Unit, unit)
+import Data.HeytingAlgebra (class HeytingAlgebra, ff, tt, implies, conj, disj, not)
+import Data.Unit (Unit)
 
 -- | The `BooleanAlgebra` type class represents types that behave like boolean
 -- | values.
 -- |
--- | Instances should satisfy the following laws in addition to the `Bounded`
--- | laws:
+-- | Instances should satisfy the following laws in addition to the
+-- | `HeytingAlgebra` law:
 -- |
--- | - Associativity:
--- |   - `a || (b || c) = (a || b) || c`
--- |   - `a && (b && c) = (a && b) && c`
--- | - Commutativity:
--- |   - `a || b = b || a`
--- |   - `a && b = b && a`
--- | - Distributivity:
--- |   - `a && (b || c) = (a && b) || (a && c)`
--- |   - `a || (b && c) = (a || b) && (a || c)`
--- | - Identity:
--- |   - `a || bottom = a`
--- |   - `a && top = a`
--- | - Idempotent:
--- |   - `a || a = a`
--- |   - `a && a = a`
--- | - Absorption:
--- |   - `a || (a && b) = a`
--- |   - `a && (a || b) = a`
--- | - Annhiliation:
--- |   - `a || top = top`
--- | - Complementation:
--- |   - `a && not a = bottom`
--- |   - `a || not a = top`
-class Bounded a <= BooleanAlgebra a where
-  conj :: a -> a -> a
-  disj :: a -> a -> a
-  not :: a -> a
+-- | - Excluded middle:
+-- |   - `a || not a = tt`
+class HeytingAlgebra a <= BooleanAlgebra a
 
-infixr 3 conj as &&
-infixr 2 disj as ||
-
-instance booleanAlgebraBoolean :: BooleanAlgebra Boolean where
-  conj = boolConj
-  disj = boolDisj
-  not = boolNot
-
-instance booleanAlgebraUnit :: BooleanAlgebra Unit where
-  conj _ _ = unit
-  disj _ _ = unit
-  not _ = unit
-
-instance booleanAlgebraFn :: BooleanAlgebra b => BooleanAlgebra (a -> b) where
-  conj fx fy a = fx a `conj` fy a
-  disj fx fy a = fx a `disj` fy a
-  not fx a = not (fx a)
-
-foreign import boolConj :: Boolean -> Boolean -> Boolean
-foreign import boolDisj :: Boolean -> Boolean -> Boolean
-foreign import boolNot :: Boolean -> Boolean
+instance booleanAlgebraBoolean :: BooleanAlgebra Boolean
+instance booleanAlgebraUnit :: BooleanAlgebra Unit

src/Data/Bounded.purs

@@ -1,18 +1,20 @@
-module Data.Bounded (class Bounded, bottom, top) where
-
+module Data.Bounded
+  ( class Bounded
+  , bottom
+  , top
+  , module Data.Ord
+  ) where
+
+import Data.Ord (class Ord, Ordering(..), compare, (<), (<=), (>), (>=))
 import Data.Unit (Unit, unit)
 
--- | The `Bounded` type class represents types that have an upper and lower
--- | boundary.
+-- | The `Bounded` type class represents totally ordered types that have an
+-- | upper and lower boundary.
 -- |
--- | Although there are no "internal" laws for `Bounded`, every value of `a`
--- | should be considered less than or equal to `top` by some means, and greater
--- | than or equal to `bottom`.
+-- | Instances should satisfy the following law in addition to the `Ord` laws:
 -- |
--- | The lack of explicit `Ord` constraint allows flexibility in the use of
--- | `Bounded` so it can apply to total and partially ordered sets, boolean
--- | algebras, etc.
-class Bounded a where
+-- | - Bounded: `bottom <= a <= top`
+class Ord a <= Bounded a where
   top :: a
   bottom :: a
 
@@ -35,10 +37,10 @@ instance boundedChar :: Bounded Char where
 foreign import topChar :: Char
 foreign import bottomChar :: Char
 
+instance boundedOrdering :: Bounded Ordering where
+  top = GT
+  bottom = LT
+
 instance boundedUnit :: Bounded Unit where
   top = unit
   bottom = unit
-
-instance boundedFn :: Bounded b => Bounded (a -> b) where
-  top _ = top
-  bottom _ = bottom

src/Data/BoundedOrd.purs

@@ -0,0 +1,22 @@
+module Data.CommutativeRing
+  ( class CommutativeRing
+  , module Data.Ring
+  , module Data.Semiring
+  ) where
+
+import Data.Ring (class Ring)
+import Data.Semiring (class Semiring, add, mul, one, zero, (*), (+))
+import Data.Unit (Unit)
+
+-- | The `CommutativeRing` class is for rings where multiplication is
+-- | commutative.
+-- |
+-- | Instances must satisfy the following law in addition to the `Ring`
+-- | laws:
+-- |
+-- | - Commutative multiplication: `a * b = b * a`
+class Ring a <= CommutativeRing a
+
+instance commutativeRingInt :: CommutativeRing Int
+instance commutativeRingNumber :: CommutativeRing Number
+instance commutativeRingUnit :: CommutativeRing Unit

src/Data/CommutativeRing.purs

@@ -1,6 +1,10 @@
 "use strict";
 
-// module Data.ModuloSemiring
+// module Data.EuclideanRing
+
+exports.intDegree = function (x) {
+  return Math.abs(x);
+};
 
 exports.intDiv = function (x) {
   return function (y) {

src/Data/DivisionRing.purs

@@ -0,0 +1,47 @@
+module Data.EuclideanRing
+  ( class EuclideanRing, degree, div, mod, (/)
+  , module Data.CommutativeRing
+  , module Data.Ring
+  , module Data.Semiring
+  ) where
+
+import Data.CommutativeRing (class CommutativeRing)
+import Data.Ring (class Ring, sub, (-))
+import Data.Semiring (class Semiring, add, mul, one, zero, (*), (+))
+import Data.Unit (Unit, unit)
+
+-- | The `EuclideanRing` class is for commutative rings that support division.
+-- |
+-- | Instances must satisfy the following law in addition to the `Ring`
+-- | laws:
+-- |
+-- | - 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)`
+class CommutativeRing a <= EuclideanRing a where
+  degree :: a -> Int
+  div :: a -> a -> a
+  mod :: a -> a -> a
+
+infixl 7 div as /
+
+instance euclideanRingInt :: EuclideanRing Int where
+  degree = intDegree
+  div = intDiv
+  mod = intMod
+
+instance euclideanRingNumber :: EuclideanRing Number where
+  degree _ = 1
+  div = numDiv
+  mod _ _ = 0.0
+
+instance euclideanRingUnit :: EuclideanRing Unit where
+  degree _ = 1
+  div _ _ = unit
+  mod _ _ = unit
+
+foreign import intDegree :: Int -> Int
+foreign import intDiv :: Int -> Int -> Int
+foreign import intMod :: Int -> Int -> Int
+
+foreign import numDiv :: Number -> Number -> Number

src/Data/ModuloSemiring.js renamed to src/Data/EuclideanRing.js

@@ -0,0 +1,24 @@
+module Data.Field
+  ( class Field
+  , module Data.CommutativeRing
+  , module Data.EuclideanRing
+  , module Data.Ring
+  , module Data.Semiring
+  ) where
+
+import Data.CommutativeRing (class CommutativeRing)
+import Data.EuclideanRing (class EuclideanRing, degree, div, mod, (/))
+import Data.Ring (class Ring, negate, sub)
+import Data.Semiring (class Semiring, add, mul, one, zero, (*), (+))
+import Data.Unit (Unit)
+
+-- | The `Field` class is for types that are commutative fields.
+-- |
+-- | Instances must satisfy the following law in addition to the
+-- | `CommutativeRing` and `EuclideanRing` laws:
+-- |
+-- | - Non-zero multiplicative inverse: ``a `mod` b = 0` for all `a` and `b`
+class (CommutativeRing a, EuclideanRing a) <= Field a
+
+instance fieldNumber :: Field Number
+instance fieldUnit :: Field Unit

src/Data/EuclideanRing.purs

@@ -1,6 +1,6 @@
 "use strict";
 
-// module Data.BooleanAlgebra
+// module Data.HeytingAlgebra
 
 exports.boolConj = function (b1) {
   return function (b2) {

src/Data/Field.purs

@@ -0,0 +1,70 @@
+module Data.HeytingAlgebra
+  ( class HeytingAlgebra, tt, ff, implies, conj, disj, not
+  , (&&), (||)
+  ) where
+
+import Data.Unit (Unit, unit)
+
+-- | The `HeytingAlgebra` type class represents types are bounded lattices with
+-- | an implication operator such that the following laws hold:
+-- |
+-- | - 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``
+class HeytingAlgebra a where
+  ff :: a
+  tt :: a
+  implies :: a -> a -> a
+  conj :: a -> a -> a
+  disj :: a -> a -> a
+  not :: a -> a
+
+infixr 3 conj as &&
+infixr 2 disj as ||
+
+instance heytingAlgebraBoolean :: HeytingAlgebra Boolean where
+  ff = false
+  tt = true
+  implies a b = not a || b
+  conj = boolConj
+  disj = boolDisj
+  not = boolNot
+
+instance heytingAlgebraUnit :: HeytingAlgebra Unit where
+  ff = unit
+  tt = unit
+  implies _ _ = unit
+  conj _ _ = unit
+  disj _ _ = unit
+  not _ = unit
+
+instance heytingAlgebraFunction :: HeytingAlgebra b => HeytingAlgebra (a -> b) where
+  ff _ = ff
+  tt _ = tt
+  implies f g a = f a `implies` g a
+  conj f g a = f a && g a
+  disj f g a = f a || g a
+  not f a = not (f a)
+
+foreign import boolConj :: Boolean -> Boolean -> Boolean
+foreign import boolDisj :: Boolean -> Boolean -> Boolean
+foreign import boolNot :: Boolean -> Boolean