Bounded and floating types

[kahl at cas.mcmaster.ca]

Conal Elliott wrote:

 > Pure values have
 > time minBound, while eternally unknowable values (non-occurring events) have
 > time maxBound.  Hm.  Now that I put it that way, I realize that I don't want
 > to use existing minBound and maxBound if they're finite.  (My event types
 > are temporally polymorphic.)  I'm mainly interested in Float/Double times,
 > which have infinities in practice but apparently not guaranteed by the
 > language standard.

And even in the current implementation with infinities,
maxBound would be NaN, not +Inf:

Prelude> let z = 0 :: Double
Prelude> 0 / z
NaN
Prelude> 1 / z
Infinity
Prelude> (-1) / z
-Infinity
Prelude> (0 / z) `compare` (1 / z)
GT
Prelude> (0 / z) `compare` ((-1) / z)
GT

This is another case where the linear ordering provided by Ord
has an arbitrary flavour, since the type of IEEE doubles
does not have a ``natural'' linear ordering.
(And I consider this as independent of
 whether the IEEE standard prescribes this ordering or not.)

For Conal it is probably going to be the question
whether he identifies a different interface as serving his purposes better
(supported by ``I don't want to use existing minBound and maxBound
  if they're finite'' and ``For now, (b)'')
or whether he thinks that Bounded ``feels right'' for his purposes,
and does a newtype for Double without NaN, with the infinities as bounds.


My arguments consistently assume the following specification:

\begin{spec}
forall a . (Ord a, Bounded a) =>
  forall x :: a . minBound <= x && x <= maxBound
\end{spec}
(I.e., if a type has both Ord and Bounded instances,
 then for all |x| of that type,
 |minBound <= x| and |x <= maxBound| are |True| if defined.

 Normally one would expect, as part of the specification of Ord,
 that |x <= y| is defined
 at least when both |x| and |y| are fully defined,
 i.e., do not contain |undefined| anywhere.

 So I would not accept |(Nan <= Infinity) = undefined|,
 but would insist on mapping Nan itself to undefined.
)

Yitzchak Gale pointed out:

 > Where are these axioms? I only see the Haddocks in the Prelude:
 > 
 > "Ord is not a superclass of Bounded since types that are not
 > totally ordered may also have upper and lower bounds."

This does not contradict my specification,
but also does not imply it, although it could be argued that the sentence

 | The Bounded class is used to name the upper and lower limits of a type.

might be understood to imply it --- supported by the discussion.

I think the absence of such a specification would be very bad practice,
since it relegates Bounded to just provide two arbitrary elements
about which nothing can be assumed by any library function.

(And I would prefer to have Ord as superclass of Bounded.)



While we are looking at the Prelude --- it also has the following:

 | For any type that is an instance of class Bounded as well as Enum, the
 | following should hold:
 | 
 |   * The calls succ maxBound and pred minBound should result in a runtime
 |     error.
 |   * fromEnum and toEnum should give a runtime error if the result value is
 |     not representable in the result type. For example, toEnum 7 :: Bool is
 |     an error.
 |   * enumFrom and enumFromThen should be defined with an implicit bound,
 |     thus:
 | 
 |         enumFrom     x   = enumFromTo     x maxBound
 |         enumFromThen x y = enumFromThenTo x y bound
 |           where
 |             bound | fromEnum y >= fromEnum x = maxBound
 |                   | otherwise                = minBound


However, GHC-6.6.1 says:

Prelude> succ (1/z)
Infinity
Prelude> succ (0/z)
NaN
Prelude> succ ((-1)/z)
-Infinity
Prelude> pred ((-1)/z)
-Infinity


So Double cannot be an instance of Bounded...



(Aside: Notice:


Prelude> succ (maxBound :: Int)
*** Exception: Prelude.Enum.succ{Int}: tried to take `succ' of maxBound
Prelude> 1 + (maxBound :: Int)
-2147483648

 so don't use (1 +) unless you want wrap-around.
)

And don't use succ, pred, fromEnum, and toEnum unless you are prepared
to have run-time errors --- the specification of these run-time errors
does not even require an Eq instance, so there is no general way
to catch or prevent these.

I think a MonadError-based interface would be much better
(I also believe that |fail| should not be a member of the class Monad).



(I also agree with the Indexable argument,
 but consider that issue as separate.)


Wolfram