Add laws for 'toInteger' and 'toRational'

CLC discussion here:
https://github.com/haskell/core-libraries-committee/issues/58

3 files changed, 21 insertions, 0 deletions

diff --git a/libraries/base/GHC/Float.hs b/libraries/base/GHC/Float.hs
index 6f15997981..1d02acb2f1 100644
--- a/libraries/base/GHC/Float.hs
+++ b/libraries/base/GHC/Float.hs
@@ -335,6 +335,9 @@ instance  Real Float  where
 --
 -- >>> 0/0 * (recip 0/0 :: Float)
 -- NaN
+--
+-- Additionally, because of @NaN@ this instance does not obey the left-inverse
+-- law for 'toRational'/'fromRational'.
 instance  Fractional Float  where
     (/) x y             =  divideFloat x y
     {-# INLINE fromRational #-}
@@ -564,6 +567,9 @@ instance  Real Double  where
 --
 -- >>> 0/0 * (recip 0/0 :: Double)
 -- NaN
+--
+-- Additionally, because of @NaN@ this instance does not obey the left-inverse
+-- law for 'toRational'/'fromRational'.
 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 c7d0425eab..1b76cd1bbc 100644
--- a/libraries/base/GHC/Num.hs
+++ b/libraries/base/GHC/Num.hs
@@ -56,6 +56,8 @@ default ()              -- Double isn't available yet,
 -- @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)@
+-- [__Coherence with 'toInteger'__]: if the type also implements 'GHC.Real.Integral', then
+-- 'fromInteger' is a left inverse for 'GHC.Real.toInteger', i.e. @fromInteger (toInteger i) == i@
 --
 -- 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
diff --git a/libraries/base/GHC/Real.hs b/libraries/base/GHC/Real.hs
index 666034bdac..aaff2ea3a9 100644
--- a/libraries/base/GHC/Real.hs
+++ b/libraries/base/GHC/Real.hs
@@ -135,6 +135,13 @@ denominator (_ :% y)    =  y
 -- Standard numeric classes
 --------------------------------------------------------------
 
+-- | Real numbers.
+--
+-- The Haskell report defines no laws for 'Real', however 'Real' instances
+-- are customarily expected to adhere to the following law:
+--
+-- [__Coherence with 'fromRational'__]: if the type also implements 'Fractional',
+-- then 'fromRational' is a left inverse for 'toRational', i.e. @fromRational (toRational i) = i@
 class  (Num a, Ord a) => Real a  where
     -- | the rational equivalent of its real argument with full precision
     toRational          ::  a -> Rational
@@ -153,6 +160,9 @@ class  (Num a, Ord a) => Real a  where
 --
 -- An example of a suitable Euclidean function, for 'Integer'\'s instance, is
 -- 'abs'.
+--
+-- In addition, 'toInteger` should be total, and 'fromInteger' should be a left
+-- inverse for it, i.e. @fromInteger (toInteger i) = i@.
 class  (Real a, Enum a) => Integral a  where
     -- | integer division truncated toward zero
     --
@@ -211,6 +221,9 @@ class  (Real a, Enum a) => Integral a  where
 --
 -- [__'recip' gives the multiplicative inverse__]:
 -- @x * recip x@ = @recip x * x@ = @fromInteger 1@
+-- [__Totality of 'toRational'__]: 'toRational' is total
+-- [__Coherence with 'toRational'__]: if the type also implements 'Real',
+-- then 'fromRational' is a left inverse for 'toRational', i.e. @fromRational (toRational i) = i@
 --
 -- Note that it /isn't/ customarily expected that a type instance of
 -- 'Fractional' implement a field. However, all instances in @base@ do.