Rework EuclideanRing laws, fixes #99.

This change that fixes the EuclideanRing laws so that they do actually
describe a euclidean ring (I have discussed some problems with the
current set of laws in #99).

This change to the laws actually invalidates the `EuclideanRing Unit`
and `Field Unit` instances, but they remain in for now so that we can
publish this without it being a breaking change. These instances have
been marked as deprecated and will be removed in the next major release.

Also add more explanation about division by zero in the EuclideanRing
class.

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