Improve documentation for Real

[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.

-- 
    Viktor.