infinite (fractional) precision

[David Lester]

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