
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