Few Digits 0.5.0

Few Digits is a collection of Haskell modules that implement exact real arithmetic. The 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.CReal and Data.Real.ICReal that export similar interfaces. The 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.

Download

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/

Unstable

Until Few Digits reaches version 1.0, I reserve the right to change the interface arbitrarily.

Library Functions

In addition to all the functions entailed by satisfying the Floating interface, there are other functions you may find useful.

erf :: CReal -> CReal

erf computes the error function.

Why?

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.