infinite (fractional) precision
David Lester
dlester@cs.man.ac.uk
Thu, 10 Oct 2002 11:28:44 +0100 (BST)
Dear All,
A really, really simple version in Haskell 1.2 has been available from
ftp://ftp.cs.man.ac.uk/pub/arithmetic/Haskell/Era1/Era.hs
for some considerable time.
Of course the only reason for producing it was to show that the language
designers didn't get it right. Take it from me, they never do [Is he being
ironic here?].
In particular, although (<) and (==) are not computable functions over the
computable reals, min and max are! Similarly, signum isn't computable, but
abs is. The classes Ord and Num are a theoreticians nightmare.
[For the mathematically sophisticated, the problem with these operations
revolves around their continuity (in a weird numeric _and_ information
theoretic sense) properties given the discrete nature of their range.]
Then there's the rounding operation in Haskell 1.2. I must have wasted
more hours fixing bugs caused by my naive understanding of _that_
operation than an other single misapprehension about a programming
language construct in any langauge!
In other files hanging off of
http://www.cs.man.ac.uk/arch/dlester/exact.html
you'll find a PVS development that shows that (most of) the implementation
is correct. A paper on this theorem-proving work has been accepted for
TCS, but I don't know whether it'll be published in my life time; and, I'm
unsure about the ethics involved in puting up a copy of the paper on my
website.
However, a summary is: 4 bugs found, 3 only becoming manifest on doing the
PVS work. I guess there's something to this formal methods lark after all.
I'd planned to do a "Functional Pearl" about this library/package, but the
theoretical development is embarassingly inelegant when compared to
Richard Bird's classic functional pearls.
If you think it'd be worth it, I'll see what I can do.
I trust that this will save anyone wasting too much more time over this
topic.
David Lester.
On Thu, 10 Oct 2002, Ashley Yakeley wrote:
> At 2002-10-10 01:29, Ketil Z. Malde wrote:
>
> >I realize it's probably far from trivial, e.g. comparing two equal
> >numbers could easily not terminate, and memory exhaustion would
> >probably arise in many other cases.
>
> I considered doing something very like this for real (computable)
> numbers, but because I couldn't properly make the type an instance of Eq,
> I left it. Actually it was worse than that. Suppose I'm adding two
> numbers, both of which are actually 1, but I don't know that:
>
> 1.000000000.... +
> 0.999999999....
>
> The trouble is, as far as I know with a finite number of digits, the
> answer might be
>
> 1.9999999999937425
>
> or it might be
>
> 2.0000000000013565
>
> ...so I can't actually generate any digits at all. So I can't even make
> the type an instance of my Additive class. Not very useful...
>
>