Merge pull request #107 from purescript/rework-euclidean-ring

Rework EuclideanRing laws, fixes #99, #102

Author: hdgarrood

src/Data/EuclideanRing.purs

@@ -11,13 +11,37 @@ import Data.Semiring (class Semiring, add, mul, one, zero, (*), (+))
 import Data.Unit (Unit, unit)
 
 -- | The `EuclideanRing` class is for commutative rings that support division.
+-- | The mathematical structure this class is based on is sometimes also called
+-- | a *Euclidean domain*.
 -- |
--- | Instances must satisfy the following law in addition to the `Ring`
+-- | Instances must satisfy the following laws 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)`
+-- | - 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)`
+-- |
+-- | The behaviour of division by `zero` is unconstrained by these laws,
+-- | meaning that individual instances are free to choose how to behave in this
+-- | case. Similarly, there are no restrictions on what the result of
+-- | `degree zero` is; it doesn't make sense to ask for `degree zero` in the
+-- | same way that it doesn't make sense to divide by `zero`, so again,
+-- | individual instances may choose how to handle this case.
+-- |
+-- | For any `EuclideanRing` which is also a `Field`, one valid choice
+-- | for `degree` is simply `const 1`. In fact, unless there's a specific
+-- | reason not to, `Field` types should normally use this definition of
+-- | `degree`.
+-- |
+-- | The `Unit` instance is provided for backwards compatibility, but it is
+-- | not law-abiding, because `Unit` fails to form an integral domain. This
+-- | instance will be removed in a future release.
 class CommutativeRing a <= EuclideanRing a where
   degree :: a -> Int
   div :: a -> a -> a

src/Data/Field.purs

@@ -18,6 +18,10 @@ import Data.Unit (Unit)
 -- | `EuclideanRing` laws:
 -- |
 -- | - Non-zero multiplicative inverse: ``a `mod` b = zero`` for all `a` and `b`
+-- |
+-- | The `Unit` instance is provided for backwards compatibility, but it is
+-- | not law-abiding, because `Unit` does not obey the `EuclideanRing` laws.
+-- | This instance will be removed in a future release.
 class EuclideanRing a <= Field a
 
 instance fieldNumber :: Field Number