Data.Number.IReal.Rounded

This module uses type-level literals to provide types Rounded lit where lit is a positive integer literal. Values of this type are IReals where (sub-)expressions are computed with a precision of at most lit decimals. This is very different from multi-precision floating point numbers; Rounded values are intervals, indicating the precision in the computed result.

To use this module in ghci you must :set -XDataKinds. Example usage:

>>> import Data.Number.IReal.FAD
>>> import Data.Number.IReal.Rounded
>>> let f x = cos x * cos (2*x) + sin x * sin (2 * x)
>>> :set +s
>>> :set -XDataKinds
>>> (deriv 200 f 1 :: Rounded 120) ? 40
0.54030230586813971740[| 0803811043 .. 1069403842 |]
(0.13 secs, 114501688 bytes)
>>> (deriv 200 f 1 :: Rounded 150) ? 40
0.5403023058681397174009366074429766037324
(0.13 secs, 120063280 bytes)

Note that function f is in fact an obfuscated version of the cosine function, using a trigonometric identity on cos (2x - x). So we can check the result, but the derivatives are computed using the rules for differentiation.

We compute the 200'th derivative of f, evaluated at 1 (i.e., cos 1) with 40 significant digits. First we try to do this at type Rounded 120, i.e. with 120 decimals in all intermediate computations. As we see, this is not precision enough; we get as result an interval of width circa 2e-22. Redoing it at type Rounded 150 gives sufficient precision.

Documentation

newtype Rounded p

Constructors

R

Fields

unRound :: IReal

Instances

Precision k p => Eq (Rounded k p)

Precision k p => Floating (Rounded k p)

Precision k p => Fractional (Rounded k p)

Precision k p => Num (Rounded k p)

Precision k p => Ord (Rounded k p)

Precision k p => Show (Rounded k p)

Precision k p => Powers (Rounded k p)

Precision k p => VarPrec (Rounded k p)

Precision k p => Scalable (Rounded k p)

class Precision p where

Methods

precision :: proxy p -> Int

Instances

KnownNat n => Precision Nat n

r :: Precision p => IReal -> Rounded p

proxyPrecision :: Rounded p -> Proxy p

(?) :: Rounded k t -> Int -> IO () infix 3

(??) :: Rounded k t -> Int -> IO () infix 3

(=?=) :: Precision p => Rounded p -> Rounded p -> Int -> Bool infix 3

(<!) :: Precision p => Rounded p -> Rounded p -> Int -> Bool infix 3

(>!) :: Precision p => Rounded p -> Rounded p -> Int -> Bool infix 3

(+-) :: Precision p => Rational -> Rational -> Rounded p infix 6

(-+-) :: Precision p => Rounded p -> Rounded p -> Rounded p infix 6

showIReal :: Precision p => Int -> Rounded p -> String

mid :: Precision p => Rounded p -> Rounded p

rad :: Precision p => Rounded p -> Rounded p

lower :: Precision p => Rounded p -> Rounded p

upper :: Precision p => Rounded p -> Rounded p

hull :: Precision p => [Rounded p] -> Rounded p

containedIn :: Precision p => Rounded p -> Rounded p -> Int -> Bool

intersection :: Precision p => Rounded p -> Rounded p -> Maybe (Rounded p)