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.