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