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