Improve documentation for Real

The Real class has one method: -- | the rational equivalent of its real argument with full precision toRational :: a -> Rational This is ... pretty weird. What does "full precision" mean? For integral and floating point types, it's fine. It's not at all meaningful for 1. Computable reals 2. Real algebraic numbers 3. Real numbers expressible in radicals 4. Rational numbers augmented with some extra numbers like pi 5. Geometrically constructable reals 6. Etc. Can we settle on a meaning for toRational? The properFraction method of the RealFrac class has basically the same issue.

On Wed, 23 Dec 2020, David Feuer wrote:
The Real class has one method: -- | the rational equivalent of its real argument with full precision
toRational :: a -> Rational
This is ... pretty weird. What does "full precision" mean? For integral and floating point types, it's fine. It's not at all meaningful for
1. Computable reals 2. Real algebraic numbers 3. Real numbers expressible in radicals 4. Rational numbers augmented with some extra numbers like pi 5. Geometrically constructable reals 6. Etc.
They cannot have Real instances, then. Right?

Perhaps that's the answer, but it seems frankly bizarre to call a class Real if `Real s` actually means that `s` is a subset of the rational numbers. On Wed, Dec 23, 2020, 8:02 PM Henning Thielemann < lemming@henning-thielemann.de> wrote:
On Wed, 23 Dec 2020, David Feuer wrote:
The Real class has one method: -- | the rational equivalent of its real argument with full precision
toRational :: a -> Rational
This is ... pretty weird. What does "full precision" mean? For integral and floating point types, it's fine. It's not at all meaningful for
1. Computable reals 2. Real algebraic numbers 3. Real numbers expressible in radicals 4. Rational numbers augmented with some extra numbers like pi 5. Geometrically constructable reals 6. Etc.
They cannot have Real instances, then. Right?

Wouldn't it make more sense to get at the idea from another direction or
two? One obvious idea is to compare to a rational number:
compareRational :: a -> Rational -> Ordering
Neither this nor Ord can be supported by computable reals, so maybe there
should be a superclass for numbers that can be *approximated by* rationals
to an arbitrary precise degree.
On Wed, Dec 23, 2020, 8:06 PM David Feuer
Perhaps that's the answer, but it seems frankly bizarre to call a class Real if `Real s` actually means that `s` is a subset of the rational numbers.
On Wed, Dec 23, 2020, 8:02 PM Henning Thielemann < lemming@henning-thielemann.de> wrote:
On Wed, 23 Dec 2020, David Feuer wrote:
The Real class has one method: -- | the rational equivalent of its real argument with full precision
toRational :: a -> Rational
This is ... pretty weird. What does "full precision" mean? For integral and floating point types, it's fine. It's not at all meaningful for
1. Computable reals 2. Real algebraic numbers 3. Real numbers expressible in radicals 4. Rational numbers augmented with some extra numbers like pi 5. Geometrically constructable reals 6. Etc.
They cannot have Real instances, then. Right?

Am 24.12.20 um 03:46 schrieb David Feuer:
Wouldn't it make more sense to get at the idea from another direction or two? One obvious idea is to compare to a rational number:
compareRational :: a -> Rational -> Ordering
Neither this nor Ord can be supported by computable reals,
Disclaimer: I have only a vague idea what computable reals are, which may explain why this is totally non-obvious to me! I mean, for Ord: yes, I do understand ahy this is not computable, but compareRational? Could you post a pointer or reference? Cheers Ben

On Sun, Dec 27, 2020 at 11:35:23AM +0100, Ben Franksen wrote:
Am 24.12.20 um 03:46 schrieb David Feuer:
Wouldn't it make more sense to get at the idea from another direction or two? One obvious idea is to compare to a rational number:
compareRational :: a -> Rational -> Ordering
Neither this nor Ord can be supported by computable reals,
Disclaimer: I have only a vague idea what computable reals are, which may explain why this is totally non-obvious to me!
I mean, for Ord: yes, I do understand ahy this is not computable, but compareRational? Could you post a pointer or reference?
There is no terminating algorithm that determines whether a computable real number that is (secretly) equal to zero is actually equal to zero. All you get to see is a sequence of approximations that make it look increasingly likely that the number could be zero, but there's no way to know that this is the case indefinitely and it is just very small. The equivalent situation with Foldable is the divergence of: all (== 0) $ repeat 0 the short-circuit never happens. So equality is not decidable, and the direction of strict inequality is only decidable for actually unequal numbers. -- Viktor.

Am 27.12.20 um 11:55 schrieb Viktor Dukhovni:
On Sun, Dec 27, 2020 at 11:35:23AM +0100, Ben Franksen wrote:
Am 24.12.20 um 03:46 schrieb David Feuer:
Wouldn't it make more sense to get at the idea from another direction or two? One obvious idea is to compare to a rational number:
compareRational :: a -> Rational -> Ordering
Neither this nor Ord can be supported by computable reals,
Disclaimer: I have only a vague idea what computable reals are, which may explain why this is totally non-obvious to me!
I mean, for Ord: yes, I do understand ahy this is not computable, but compareRational? Could you post a pointer or reference?
There is no terminating algorithm that determines whether a computable real number that is (secretly) equal to zero is actually equal to zero.
All you get to see is a sequence of approximations that make it look increasingly likely that the number could be zero, but there's no way to know that this is the case indefinitely and it is just very small.
The equivalent situation with Foldable is the divergence of:
all (== 0) $ repeat 0
the short-circuit never happens. So equality is not decidable, and the direction of strict inequality is only decidable for actually unequal numbers.
Thanks for this explanation. It is pretty obvious now! My inuition about computable reals was that they are something like (Integer,[Digit]) with an infinite sequence of decimals for the "fractional" part; and that when we compare with a rational, we /eventually/ come to a point where we can decide the comparison. But of course that is true only /if/ they are actually different; if they are equal, comparing the decimals won't terminate. Cheers Ben
participants (4)
-
Ben Franksen
-
David Feuer
-
Henning Thielemann
-
Viktor Dukhovni