Geometric operations are an important class of numerical functions with unusual identities; for example, rotation six times by sixty degrees should be the identity operation. These identities hold neither in floating point nor in interval arithmetic. However, standard techniques for exact arithmetic with equality do not support sines and cosines, which are necessary for geometric operations.

We introduce ExactNum, an OCaml library for exact real arithmetic that uses Chebyshev polynomials to support exact sines and cosines of rational multiples of $\pi$. Besides these trigonometric operations, ExactNum supports all of the ordered field operations, sufficient for the implementation of common geometric algorithms.

ExactNum uses Chebyshev fields (splitting fields of Chebyshev polynomials) as its core value representation. Elements of Chebyshev fields admit a simple canonical form as variable-length lists of rational numbers, and support efficient implementations of the field operations. ExactNum uses interval arithmetic to compare values, leveraging canonical form equality to provide decidable comparison. Furthermore, Chebyshev fields form a category with coproducts, an algebraic structure necessary to allow operations between sines and cosines of different angles.

We use ExactNum to implement a simple CAD library that supports basic shapes, their intersections and unions, and their translations and rotations. Despite providing exact arithmetic with equality for a complex array of operations, ExactNum is still reasonably fast, out-performing computed-real arithmetic and even the inexact MPFR library, and is between two and three orders of magnitude slower than direct floating-point computation.