Few Digits is a collection of Haskell modules that implement exact real arithmetic.
CReal data type is an instance of of the standard
Floating class, but there are some caveats. Currently the
show throws an error. This may change in the future. Also the
(==) function returns
false if the two
CReals are different, and does not terminate if the two
CReals have the same value. Neither of these functions should ever be called. Also be aware that dividing by zero, or taking the logarithm of zero will not terminate.
There are two modules,
Data.Real.ICReal that export similar interfaces.
Data.Real.ICReal module has a more sophisticated implemenation and is easier to use, but is less flexible.
The code is not particularly well documented, but there is a pre-print of a paper describing the theory behind the implementation.
The source code of Few Digits is available at 〈//r6.ca/FewDigits/FewDigits.tar.gz〉 or via darcs.
darcs get --tag 0.5.0 //r6.ca/FewDigits/
The development version of Few Digits is avaiable via darcs.
darcs get //r6.ca/FewDigits/
Until Few Digits reaches version 1.0, I reserve the right to change the interface arbitrarily.
In addition to all the functions entailed by satisfying the
Floating interface, there are other functions you may find useful.
erf :: CReal -> CReal
erfcomputes the error function.
Few Digits is not fast. Few Digits is part of my Ph. D. research. My goal is to implement an exact real arithmetic package in Coq that is proven correct (with respect to C-CoRN) and is sufficiently fast. The goal is to be fast enough to prove the inequalities required by Hales’s proof of Kepler’s Conjecture. Few Digits is my prototype written in Haskell. It should be simple enough that I can prove the correctness of the algorithms used. Therefore Few Digits will never compete with real exact real arithmetic packages.