Improve documentation of Eq, Ord instances for Float and Double

Reviewers: sjakobi, dfeuer, bgamari, hvr

Reviewed By: sjakobi, bgamari

Subscribers: rwbarton, thomie, carter

GHC Trac Issues: #15078

Differential Revision: https://phabricator.haskell.org/D4736

6 files changed, 190 insertions, 9 deletions

diff --git a/libraries/base/Data/Complex.hs b/libraries/base/Data/Complex.hs
index 073f5c5e86..a544a5bf6c 100644
--- a/libraries/base/Data/Complex.hs
+++ b/libraries/base/Data/Complex.hs
@@ -55,6 +55,10 @@ infix  6  :+
 -- has the phase of @z@, but unit magnitude.
 --
 -- The 'Foldable' and 'Traversable' instances traverse the real part first.
+--
+-- Note that `Complex`'s instances inherit the deficiencies from the type
+-- parameter's. For example, @Complex Float@'s 'Ord' instance has similar
+-- problems to `Float`'s.
 data Complex a
   = !a :+ !a    -- ^ forms a complex number from its real and imaginary
                 -- rectangular components.
diff --git a/libraries/base/Foreign/C/Types.hs b/libraries/base/Foreign/C/Types.hs
index b2e723f724..411327f548 100644
--- a/libraries/base/Foreign/C/Types.hs
+++ b/libraries/base/Foreign/C/Types.hs
@@ -68,7 +68,11 @@ module Foreign.C.Types
           -- 'Prelude.Eq', 'Prelude.Ord', 'Prelude.Num', 'Prelude.Read',
           -- 'Prelude.Show', 'Prelude.Enum', 'Typeable', 'Storable',
           -- 'Prelude.Real', 'Prelude.Fractional', 'Prelude.Floating',
-          -- 'Prelude.RealFrac' and 'Prelude.RealFloat'.
+          -- 'Prelude.RealFrac' and 'Prelude.RealFloat'. That does mean
+          -- that `CFloat`'s (respectively `CDouble`'s) instances of
+          -- 'Prelude.Eq', 'Prelude.Ord', 'Prelude.Num' and
+          -- 'Prelude.Fractional' are as badly behaved as `Prelude.Float`'s
+          -- (respectively `Prelude.Double`'s).
         , CFloat(..),   CDouble(..)
         -- XXX GHC doesn't support CLDouble yet
         -- , CLDouble(..)
diff --git a/libraries/base/GHC/Float.hs b/libraries/base/GHC/Float.hs
index db4200d874..26a5987ee6 100644
--- a/libraries/base/GHC/Float.hs
+++ b/libraries/base/GHC/Float.hs
@@ -64,6 +64,13 @@ infixr 8  **
 ------------------------------------------------------------------------
 
 -- | Trigonometric and hyperbolic functions and related functions.
+--
+-- The Haskell Report defines no laws for 'Floating'. However, '(+)', '(*)'
+-- and 'exp' are customarily expected to define an exponential field and have
+-- the following properties:
+--
+-- * @exp (a + b)@ = @exp a * exp b
+-- * @exp (fromInteger 0)@ = @fromInteger 1@
 class  (Fractional a) => Floating a  where
     pi                  :: a
     exp, log, sqrt      :: a -> a
@@ -245,7 +252,18 @@ class  (RealFrac a, Floating a) => RealFloat a  where
 ------------------------------------------------------------------------
 
 -- | @since 2.01
-instance  Num Float  where
+-- Note that due to the presence of @NaN@, not all elements of 'Float' have an
+-- additive inverse.
+--
+-- >>> 0/0 + (negate 0/0 :: Float)
+-- NaN
+--
+-- Also note that due to the presence of -0, `Float`'s 'Num' instance doesn't
+-- have an additive identity
+--
+-- >>> 0 + (-0 :: Float)
+-- 0.0
+instance Num Float where
     (+)         x y     =  plusFloat x y
     (-)         x y     =  minusFloat x y
     negate      x       =  negateFloat x
@@ -272,6 +290,11 @@ instance  Real Float  where
                     smallInteger m# :% shiftLInteger 1 (negateInt# e#)
 
 -- | @since 2.01
+-- Note that due to the presence of @NaN@, not all elements of 'Float' have an
+-- multiplicative inverse.
+--
+-- >>> 0/0 * (recip 0/0 :: Float)
+-- NaN
 instance  Fractional Float  where
     (/) x y             =  divideFloat x y
     {-# INLINE fromRational #-}
@@ -429,6 +452,17 @@ instance  Show Float  where
 ------------------------------------------------------------------------
 
 -- | @since 2.01
+-- Note that due to the presence of @NaN@, not all elements of 'Double' have an
+-- additive inverse.
+--
+-- >>> 0/0 + (negate 0/0 :: Double)
+-- NaN
+--
+-- Also note that due to the presence of -0, `Double`'s 'Num' instance doesn't
+-- have an additive identity
+--
+-- >>> 0 + (-0 :: Double)
+-- 0.0
 instance  Num Double  where
     (+)         x y     =  plusDouble x y
     (-)         x y     =  minusDouble x y
@@ -458,6 +492,11 @@ instance  Real Double  where
                 m :% shiftLInteger 1 (negateInt# e#)
 
 -- | @since 2.01
+-- Note that due to the presence of @NaN@, not all elements of 'Double' have an
+-- multiplicative inverse.
+--
+-- >>> 0/0 * (recip 0/0 :: Double)
+-- NaN
 instance  Fractional Double  where
     (/) x y             =  divideDouble x y
     {-# INLINE fromRational #-}
diff --git a/libraries/base/GHC/Num.hs b/libraries/base/GHC/Num.hs
index 795e74a4af..b31d186c90 100644
--- a/libraries/base/GHC/Num.hs
+++ b/libraries/base/GHC/Num.hs
@@ -35,6 +35,23 @@ default ()              -- Double isn't available yet,
                         -- and we shouldn't be using defaults anyway
 
 -- | Basic numeric class.
+--
+-- The Haskell Report defines no laws for 'Num'. However, '(+)' and '(*)' are
+-- customarily expected to define a ring and have the following properties:
+--
+-- [__Associativity of (+)__]: @(x + y) + z@ = @x + (y + z)@
+-- [__Commutativity of (+)__]: @x + y@ = @y + x@
+-- [__@fromInteger 0@ is the additive identity__]: @x + fromInteger 0@ = @x@
+-- [__'negate' gives the additive inverse__]: @x + negate x@ = @fromInteger 0@
+-- [__Associativity of (*)__]: @(x * y) * z@ = @x * (y * z)@
+-- [__@fromInteger 1@ is the multiplicative identity__]:
+-- @x * fromInteger 1@ = @x@ and @fromInteger 1 * x@ = @x@
+-- [__Distributivity of (*) with respect to (+)__]:
+-- @a * (b + c)@ = @(a * b) + (a * c)@ and @(b + c) * a@ = @(b * a) + (c * a)@
+--
+-- Note that it /isn't/ customarily expected that a type instance of both 'Num'
+-- and 'Ord' implement an ordered ring. Indeed, in 'base' only 'Integer' and
+-- 'Rational' do.
 class  Num a  where
     {-# MINIMAL (+), (*), abs, signum, fromInteger, (negate | (-)) #-}
 
@@ -109,7 +126,10 @@ instance  Num Integer  where
     signum = signumInteger
 
 #if defined(MIN_VERSION_integer_gmp)
--- | @since 4.8.0.0
+-- | Note that `Natural`'s 'Num' instance isn't a ring: no element but 0 has an
+-- additive inverse. It is a semiring though.
+--
+-- @since 4.8.0.0
 instance  Num Natural  where
     (+) = plusNatural
     (-) = minusNatural
@@ -121,7 +141,10 @@ instance  Num Natural  where
     signum = signumNatural
 
 #else
--- | @since 4.8.0.0
+-- | Note that `Natural`'s 'Num' instance isn't a ring: no element but 0 has an
+-- additive inverse. It is a semiring though.
+--
+-- @since 4.8.0.0
 instance Num Natural where
   Natural n + Natural m = Natural (n + m)
   {-# INLINE (+) #-}
diff --git a/libraries/base/GHC/Real.hs b/libraries/base/GHC/Real.hs
index f88666af40..00c8cf54b2 100644
--- a/libraries/base/GHC/Real.hs
+++ b/libraries/base/GHC/Real.hs
@@ -75,6 +75,10 @@ underflowError = raise# underflowException
 --------------------------------------------------------------
 
 -- | Rational numbers, with numerator and denominator of some 'Integral' type.
+--
+-- Note that `Ratio`'s instances inherit the deficiencies from the type
+-- parameter's. For example, @Ratio Natural@'s 'Num' instance has similar
+-- problems to `Numeric.Natural.Natural`'s.
 data  Ratio a = !a :% !a  deriving Eq -- ^ @since 2.01
 
 -- | Arbitrary-precision rational numbers, represented as a ratio of
@@ -131,6 +135,19 @@ class  (Num a, Ord a) => Real a  where
     toRational          ::  a -> Rational
 
 -- | Integral numbers, supporting integer division.
+--
+-- The Haskell Report defines no laws for 'Integral'. However, 'Integral'
+-- instances are customarily expected to define a Euclidean domain and have the
+-- following properties for the 'div'/'mod' and 'quot'/'rem' pairs, given
+-- suitable Euclidean functions @f@ and @g@:
+--
+-- * @x@ = @y * quot x y + rem x y@ with @rem x y@ = @fromInteger 0@ or
+-- @g (rem x y)@ < @g y@
+-- * @x@ = @y * div x y + mod x y@ with @mod x y@ = @fromInteger 0@ or
+-- @f (mod x y)@ < @f y@
+--
+-- An example of a suitable Euclidean function, for `Integer`'s instance, is
+-- 'abs'.
 class  (Real a, Enum a) => Integral a  where
     -- | integer division truncated toward zero
     quot                :: a -> a -> a
@@ -164,6 +181,16 @@ class  (Real a, Enum a) => Integral a  where
                            where qr@(q,r) = quotRem n d
 
 -- | Fractional numbers, supporting real division.
+--
+-- The Haskell Report defines no laws for 'Fractional'. However, '(+)' and
+-- '(*)' are customarily expected to define a division ring and have the
+-- following properties:
+--
+-- [__'recip' gives the multiplicative inverse__]:
+-- @x * recip x@ = @recip x * x@ = @fromInteger 1@
+--
+-- Note that it /isn't/ customarily expected that a type instance of
+-- 'Fractional' implement a field. However, all instances in 'base' do.
 class  (Num a) => Fractional a  where
     {-# MINIMAL fromRational, (recip | (/)) #-}
 
diff --git a/libraries/ghc-prim/GHC/Classes.hs b/libraries/ghc-prim/GHC/Classes.hs
index 4479ac0120..29f1149534 100644
--- a/libraries/ghc-prim/GHC/Classes.hs
+++ b/libraries/ghc-prim/GHC/Classes.hs
@@ -119,6 +119,21 @@ for the types in "GHC.Word" and "GHC.Int".
 -- and 'Eq' may be derived for any datatype whose constituents are also
 -- instances of 'Eq'.
 --
+-- The Haskell Report defines no laws for 'Eq'. However, '==' is customarily
+-- expected to implement an equivalence relationship where two values comparing
+-- equal are indistinguishable by "public" functions, with a "public" function
+-- being one not allowing to see implementation details. For example, for a
+-- type representing non-normalised natural numbers modulo 100, a "public"
+-- function doesn't make the difference between 1 and 201. It is expected to
+-- have the following properties:
+--
+-- [__Reflexivity__]: @x == x@ = 'True'
+-- [__Symmetry__]: @x == y@ = @y == x@
+-- [__Transitivity__]: if @x == y && y == z@ = 'True', then @x == z@ = 'True'
+-- [__Substitutivity__]: if @x == y@ = 'True' and @f@ is a "public" function
+-- whose return type is an instance of 'Eq', then @f x == f y@ = 'True'
+-- [__Negation__]: @x /= y@ = @not (x == y)@
+--
 -- Minimal complete definition: either '==' or '/='.
 --
 class  Eq a  where
@@ -207,6 +222,18 @@ eqChar, neChar :: Char -> Char -> Bool
 (C# x) `eqChar` (C# y) = isTrue# (x `eqChar#` y)
 (C# x) `neChar` (C# y) = isTrue# (x `neChar#` y)
 
+-- | Note that due to the presence of @NaN@, `Float`'s 'Eq' instance does not
+-- satisfy reflexivity.
+--
+-- >>> 0/0 == (0/0 :: Float)
+-- False
+--
+-- Also note that `Float`'s 'Eq' instance does not satisfy substitutivity:
+--
+-- >>> 0 == (-0 :: Float)
+-- True
+-- >>> recip 0 == recip (-0 :: Float)
+-- False
 instance Eq Float where
     (==) = eqFloat
 
@@ -215,6 +242,18 @@ instance Eq Float where
 eqFloat :: Float -> Float -> Bool
 (F# x) `eqFloat` (F# y) = isTrue# (x `eqFloat#` y)
 
+-- | Note that due to the presence of @NaN@, `Double`'s 'Eq' instance does not
+-- satisfy reflexivity.
+--
+-- >>> 0/0 == (0/0 :: Double)
+-- False
+--
+-- Also note that `Double`'s 'Eq' instance does not satisfy substitutivity:
+--
+-- >>> 0 == (-0 :: Double)
+-- True
+-- >>> recip 0 == recip (-0 :: Double)
+-- False
 instance Eq Double where
     (==) = eqDouble
 
@@ -261,11 +300,30 @@ instance Ord TyCon where
 
 -- | The 'Ord' class is used for totally ordered datatypes.
 --
--- Instances of 'Ord' can be derived for any user-defined
--- datatype whose constituent types are in 'Ord'.  The declared order
--- of the constructors in the data declaration determines the ordering
--- in derived 'Ord' instances.  The 'Ordering' datatype allows a single
--- comparison to determine the precise ordering of two objects.
+-- Instances of 'Ord' can be derived for any user-defined datatype whose
+-- constituent types are in 'Ord'. The declared order of the constructors in
+-- the data declaration determines the ordering in derived 'Ord' instances. The
+-- 'Ordering' datatype allows a single comparison to determine the precise
+-- ordering of two objects.
+--
+-- The Haskell Report defines no laws for 'Ord'. However, '<=' is customarily
+-- expected to implement a non-strict partial order and have the following
+-- properties:
+--
+-- [__Transitivity__]: if @x <= y && y <= z@ = 'True', then @x <= z@ = 'True'
+-- [__Reflexivity__]: @x <= x@ = 'True'
+-- [__Antisymmetry__]: if @x <= y && y <= x@ = 'True', then @x == y@ = 'True'
+--
+-- Note that the following operator interactions are expected to hold:
+--
+-- 1. @x >= y@ = @y <= x@
+-- 2. @x < y@ = @x <= y && x /= y@
+-- 3. @x > y@ = @y < x@
+-- 4. @x < y@ = @compare x y == LT@
+-- 5. @x > y@ = @compare x y == GT@
+-- 6. @x == y@ = @compare x y == EQ@
+-- 7. @min x y == if x <= y then x else y@ = 'True'
+-- 8. @max x y == if x >= y then x else y@ = 'True'
 --
 -- Minimal complete definition: either 'compare' or '<='.
 -- Using 'compare' can be more efficient for complex types.
@@ -350,6 +408,19 @@ instance Ord Char where
     (C# c1) <= (C# c2) = isTrue# (c1 `leChar#` c2)
     (C# c1) <  (C# c2) = isTrue# (c1 `ltChar#` c2)
 
+-- | Note that due to the presence of @NaN@, `Float`'s 'Ord' instance does not
+-- satisfy reflexivity.
+--
+-- >>> 0/0 <= (0/0 :: Float)
+-- False
+--
+-- Also note that, due to the same, `Ord`'s operator interactions are not
+-- respected by `Float`'s instance:
+--
+-- >>> (0/0 :: Float) > 1
+-- False
+-- >>> compare (0/0 :: Float) 1
+-- GT
 instance Ord Float where
     (F# x) `compare` (F# y)
         = if      isTrue# (x `ltFloat#` y) then LT
@@ -361,6 +432,19 @@ instance Ord Float where
     (F# x) >= (F# y) = isTrue# (x `geFloat#` y)
     (F# x) >  (F# y) = isTrue# (x `gtFloat#` y)
 
+-- | Note that due to the presence of @NaN@, `Double`'s 'Ord' instance does not
+-- satisfy reflexivity.
+--
+-- >>> 0/0 <= (0/0 :: Double)
+-- False
+--
+-- Also note that, due to the same, `Ord`'s operator interactions are not
+-- respected by `Double`'s instance:
+--
+-- >>> (0/0 :: Double) > 1
+-- False
+-- >>> compare (0/0 :: Double) 1
+-- GT
 instance Ord Double where
     (D# x) `compare` (D# y)
         = if      isTrue# (x <##  y) then LT