infinite (fractional) precision

David Lester
Thu, 10 Oct 2002 11:28:44 +0100 (BST)

Dear All,

A really, really simple version in Haskell 1.2 has been available from

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

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

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

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