Improve documentation for Real

[Ben Franksen]

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