diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -1,20 +1,20 @@ -Copyright (c) 2015 Douglas McClean - -Permission is hereby granted, free of charge, to any person obtaining -a copy of this software and associated documentation files (the -"Software"), to deal in the Software without restriction, including -without limitation the rights to use, copy, modify, merge, publish, -distribute, sublicense, and/or sell copies of the Software, and to -permit persons to whom the Software is furnished to do so, subject to -the following conditions: - -The above copyright notice and this permission notice shall be included -in all copies or substantial portions of the Software. - -THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, -EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF -MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. -IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY -CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, -TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE -SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +Copyright (c) 2015 Douglas McClean + +Permission is hereby granted, free of charge, to any person obtaining +a copy of this software and associated documentation files (the +"Software"), to deal in the Software without restriction, including +without limitation the rights to use, copy, modify, merge, publish, +distribute, sublicense, and/or sell copies of the Software, and to +permit persons to whom the Software is furnished to do so, subject to +the following conditions: + +The above copyright notice and this permission notice shall be included +in all copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. +IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY +CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, +TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE +SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,5 +1,6 @@ -# exact-pi -Exact rational multiples of pi (and integer powers of pi) in Haskell - -[![Build Status](https://travis-ci.org/dmcclean/exact-pi.svg?branch=master)](https://travis-ci.org/dmcclean/exact-pi) -[![Hackage Version](https://img.shields.io/hackage/v/exact-pi.svg)](http://hackage.haskell.org/package/exact-pi) +# exact-pi +Exact rational multiples of pi (and integer powers of pi) in Haskell + +[![Build Status](https://travis-ci.org/dmcclean/exact-pi.svg?branch=master)](https://travis-ci.org/dmcclean/exact-pi) +[![Hackage Version](https://img.shields.io/hackage/v/exact-pi.svg)](http://hackage.haskell.org/package/exact-pi) +[![Stackage version](https://www.stackage.org/package/exact-pi/badge/lts?label=Stackage)](https://www.stackage.org/package/exact-pi) diff --git a/Setup.hs b/Setup.hs --- a/Setup.hs +++ b/Setup.hs @@ -1,2 +1,2 @@ -import Distribution.Simple -main = defaultMain +import Distribution.Simple +main = defaultMain diff --git a/changelog.md b/changelog.md --- a/changelog.md +++ b/changelog.md @@ -1,45 +1,49 @@ -0.4.1.2 -------- -* Bump base dependency. - -0.4.1.1 -------- -* Fixed infinite loop in definition of negate. - -0.4.1.0 -------- -* Added function for computing rational approximations of ExactPi values. - -0.4.0.0 -------- -* Added simpler constraints for converting ExactPi types to terms with the minimal context. - -0.3.1.0 -------- -* Added support for exactly comparing values. - -0.3.0.0 -------- -* Added a type-level representation of ExactPi values. - -0.2.1.2 -------- -* Fixed a bug in recip. -* Fixed approximation of exact values with a negative exponent for pi. - -0.2.1.1 -------- -* Fixed a missing case in isZero. - -0.2.1.0 -------- -* Added support for converting to exact integers or exact rationals. - -0.2.0.0 -------- -* Removed dependency on groups package, since it appears not to be widely used. -* Fixed a missing case alternative in recip. - -0.1.2.0 -------- -* Added support for GHC 7.8. +0.4.1.3 +------- +* Add Semigroup ExactPi instance. + +0.4.1.2 +------- +* Bump base dependency. + +0.4.1.1 +------- +* Fixed infinite loop in definition of negate. + +0.4.1.0 +------- +* Added function for computing rational approximations of ExactPi values. + +0.4.0.0 +------- +* Added simpler constraints for converting ExactPi types to terms with the minimal context. + +0.3.1.0 +------- +* Added support for exactly comparing values. + +0.3.0.0 +------- +* Added a type-level representation of ExactPi values. + +0.2.1.2 +------- +* Fixed a bug in recip. +* Fixed approximation of exact values with a negative exponent for pi. + +0.2.1.1 +------- +* Fixed a missing case in isZero. + +0.2.1.0 +------- +* Added support for converting to exact integers or exact rationals. + +0.2.0.0 +------- +* Removed dependency on groups package, since it appears not to be widely used. +* Fixed a missing case alternative in recip. + +0.1.2.0 +------- +* Added support for GHC 7.8. diff --git a/exact-pi.cabal b/exact-pi.cabal --- a/exact-pi.cabal +++ b/exact-pi.cabal @@ -1,35 +1,42 @@ --- Initial exact-pi.cabal generated by cabal init. For further --- documentation, see http://haskell.org/cabal/users-guide/ - -name: exact-pi -version: 0.4.1.2 -synopsis: Exact rational multiples of pi (and integer powers of pi) -description: Provides an exact representation for rational multiples of pi alongside an approximate representation of all reals. - Useful for storing and computing with conversion factors between physical units. -homepage: https://github.com/dmcclean/exact-pi/ -bug-reports: https://github.com/dmcclean/exact-pi/issues/ -license: MIT -license-file: LICENSE -author: Douglas McClean -maintainer: douglas.mcclean@gmail.com --- copyright: -category: Data -build-type: Simple -extra-source-files: README.md, - changelog.md -cabal-version: >=1.10 - -library - exposed-modules: Data.ExactPi, - Data.ExactPi.TypeLevel - -- other-modules: - -- other-extensions: - build-depends: base >=4.7 && <5, - numtype-dk >= 0.5 - ghc-options: -Wall - hs-source-dirs: src - default-language: Haskell2010 - -source-repository head - type: git - location: https://github.com/dmcclean/exact-pi.git +-- Initial exact-pi.cabal generated by cabal init. For further +-- documentation, see http://haskell.org/cabal/users-guide/ + +name: exact-pi +version: 0.4.1.3 +synopsis: Exact rational multiples of pi (and integer powers of pi) +description: Provides an exact representation for rational multiples of pi alongside an approximate representation of all reals. + Useful for storing and computing with conversion factors between physical units. +homepage: https://github.com/dmcclean/exact-pi/ +bug-reports: https://github.com/dmcclean/exact-pi/issues/ +license: MIT +license-file: LICENSE +author: Douglas McClean +maintainer: douglas.mcclean@gmail.com +-- copyright: +category: Data +build-type: Simple +extra-source-files: README.md, + changelog.md +cabal-version: >=1.10 +tested-with: GHC == 7.8.4, + GHC == 7.10.1, + GHC == 8.0.1, + GHC == 8.0.2, + GHC == 8.2.1, + GHC == 8.2.2, + GHC == 8.4.1 +library + exposed-modules: Data.ExactPi, + Data.ExactPi.TypeLevel + -- other-modules: + -- other-extensions: + build-depends: base >=4.7 && <5, + numtype-dk >= 0.5, + semigroups >= 0.9 && < 1.0 + ghc-options: -Wall + hs-source-dirs: src + default-language: Haskell2010 + +source-repository head + type: git + location: https://github.com/dmcclean/exact-pi.git diff --git a/src/Data/ExactPi.hs b/src/Data/ExactPi.hs --- a/src/Data/ExactPi.hs +++ b/src/Data/ExactPi.hs @@ -1,171 +1,176 @@ -{-# LANGUAGE RankNTypes #-} - -{-# OPTIONS_HADDOCK show-extensions #-} - -{-| -Module : Data.ExactPi -Description : Exact rational multiples of powers of pi -License : MIT -Maintainer : douglas.mcclean@gmail.com -Stability : experimental - -This type is sufficient to exactly express the closure of Q ∪ {π} under multiplication and division. -As a result it is useful for representing conversion factors -between physical units. Approximate values are included both to close the remainder -of the arithmetic operations in the `Num` typeclass and to encode conversion -factors defined experimentally. --} -module Data.ExactPi -( - ExactPi(..), - approximateValue, - isZero, - isExact, - isExactZero, - isExactOne, - areExactlyEqual, - isExactInteger, - toExactInteger, - isExactRational, - toExactRational, - rationalApproximations -) -where - -import Data.Monoid -import Data.Ratio ((%), numerator, denominator) -import Prelude - --- | Represents an exact or approximate real value. --- The exactly representable values are rational multiples of an integer power of pi. -data ExactPi = Exact Integer Rational -- ^ @'Exact' z q@ = q * pi^z. Note that this means there are many representations of zero. - | Approximate (forall a.Floating a => a) -- ^ An approximate value. This representation was chosen because it allows conversion to floating types using their native definition of 'pi'. - --- | Approximates an exact or approximate value, converting it to a `Floating` type. --- This uses the value of `pi` supplied by the destination type, to provide the appropriate --- precision. -approximateValue :: Floating a => ExactPi -> a -approximateValue (Exact z q) = (pi ^^ z) * (fromRational q) -approximateValue (Approximate x) = x - --- | Identifies whether an 'ExactPi' is an exact or approximate representation of zero. -isZero :: ExactPi -> Bool -isZero (Exact _ 0) = True -isZero (Approximate x) = x == (0 :: Double) -isZero _ = False - --- | Identifies whether an 'ExactPi' is an exact value. -isExact :: ExactPi -> Bool -isExact (Exact _ _) = True -isExact _ = False - --- | Identifies whether an 'ExactPi' is an exact representation of zero. -isExactZero :: ExactPi -> Bool -isExactZero (Exact _ 0) = True -isExactZero _ = False - --- | Identifies whether an 'ExactPi' is an exact representation of one. -isExactOne :: ExactPi -> Bool -isExactOne (Exact 0 1) = True -isExactOne _ = False - --- | Identifies whether two 'ExactPi' values are exactly equal. -areExactlyEqual :: ExactPi -> ExactPi -> Bool -areExactlyEqual (Exact z1 q1) (Exact z2 q2) = (z1 == z2 && q1 == q2) || (q1 == 0 && q2 == 0) -areExactlyEqual _ _ = False - --- | Identifies whether an 'ExactPi' is an exact representation of an integer. -isExactInteger :: ExactPi -> Bool -isExactInteger (Exact 0 q) | denominator q == 1 = True -isExactInteger _ = False - --- | Converts an 'ExactPi' to an exact 'Integer' or 'Nothing'. -toExactInteger :: ExactPi -> Maybe Integer -toExactInteger (Exact 0 q) | denominator q == 1 = Just $ numerator q -toExactInteger _ = Nothing - --- | Identifies whether an 'ExactPi' is an exact representation of a rational. -isExactRational :: ExactPi -> Bool -isExactRational (Exact 0 _) = True -isExactRational _ = False - --- | Converts an 'ExactPi' to an exact 'Rational' or 'Nothing'. -toExactRational :: ExactPi -> Maybe Rational -toExactRational (Exact 0 q) = Just q -toExactRational _ = Nothing - --- | Converts an 'ExactPi' to a list of increasingly accurate rational approximations, on alternating --- sides of the actual value. Note that 'Approximate' values are converted using the 'Real' instance --- for 'Double' into a singleton list. Note that exact rationals are also converted into a singleton list. --- --- Implementation based on work by Anders Kaseorg shared at http://qr.ae/RbXl8M. -rationalApproximations :: ExactPi -> [Rational] -rationalApproximations (Approximate x) = [toRational (x :: Double)] -rationalApproximations (Exact 0 q) = [q] -rationalApproximations (Exact z q) = fmap (\pi' -> q * (pi' ^^ z)) piConvergents - where - piConvergents :: [Rational] - piConvergents = go True 2 4 where - go s p' q' | ltPi m = [q' | not s] ++ go True m q' - | otherwise = [p' | s] ++ go False p' m where - m = (numerator p' + numerator q')%(denominator p' + denominator q') - ltPi :: Rational -> Bool - ltPi x = ok x 1 where - ok y i = - y <= (27*i - 12)%5 || - (y < (675*i - 216)%125 && - ok ((y - fromInteger (5*i - 2))*(3*(3*i + 1)*(3*i + 2)%(i*(2*i - 1)))) - (i + 1)) - -instance Show ExactPi where - show (Exact z q) | z == 0 = "Exactly " ++ show q - | z == 1 = "Exactly pi * " ++ show q - | otherwise = "Exactly pi^" ++ show z ++ " * " ++ show q - show (Approximate x) = "Approximately " ++ show (x :: Double) - -instance Num ExactPi where - fromInteger n = Exact 0 (fromInteger n) - (Exact z1 q1) * (Exact z2 q2) = Exact (z1 + z2) (q1 * q2) - (Exact _ 0) * _ = 0 - _ * (Exact _ 0) = 0 - x * y = Approximate $ approximateValue x * approximateValue y - (Exact z1 q1) + (Exact z2 q2) | z1 == z2 = Exact z1 (q1 + q2) -- by distributive property - x + y = Approximate $ approximateValue x + approximateValue y - abs (Exact z q) = Exact z (abs q) - abs (Approximate x) = Approximate $ abs x - signum (Exact _ q) = Exact 0 (signum q) - signum (Approximate x) = Approximate $ signum x -- we leave this tagged as approximate because we don't know "how" approximate the input was. a case could be made for exact answers here. - negate x = (Exact 0 (-1)) * x - -instance Fractional ExactPi where - fromRational = Exact 0 - recip (Exact z q) = Exact (negate z) (recip q) - recip (Approximate x) = Approximate (recip x) - -instance Floating ExactPi where - pi = Exact 1 1 - exp x | isExactZero x = 1 - | otherwise = approx1 exp x - log (Exact 0 1) = 0 - log x = approx1 log x - -- It would be possible to give tighter bounds to the trig functions, preserving exactness for arguments that have an exactly representable result. - sin = approx1 sin - cos = approx1 cos - tan = approx1 tan - asin = approx1 asin - atan = approx1 atan - acos = approx1 acos - sinh = approx1 sinh - cosh = approx1 cosh - tanh = approx1 tanh - asinh = approx1 asinh - acosh = approx1 acosh - atanh = approx1 atanh - -approx1 :: (forall a.Floating a => a -> a) -> ExactPi -> ExactPi -approx1 f x = Approximate (f (approximateValue x)) - --- | The multiplicative monoid over 'Rational's augmented with multiples of 'pi'. -instance Monoid ExactPi where - mempty = 1 - mappend = (*) +{-# LANGUAGE RankNTypes #-} + +{-# OPTIONS_HADDOCK show-extensions #-} + +{-| +Module : Data.ExactPi +Description : Exact rational multiples of powers of pi +License : MIT +Maintainer : douglas.mcclean@gmail.com +Stability : experimental + +This type is sufficient to exactly express the closure of Q ∪ {π} under multiplication and division. +As a result it is useful for representing conversion factors +between physical units. Approximate values are included both to close the remainder +of the arithmetic operations in the `Num` typeclass and to encode conversion +factors defined experimentally. +-} +module Data.ExactPi +( + ExactPi(..), + approximateValue, + isZero, + isExact, + isExactZero, + isExactOne, + areExactlyEqual, + isExactInteger, + toExactInteger, + isExactRational, + toExactRational, + rationalApproximations +) +where + +import Data.Monoid +import Data.Ratio ((%), numerator, denominator) +import Data.Semigroup +import Prelude + +-- | Represents an exact or approximate real value. +-- The exactly representable values are rational multiples of an integer power of pi. +data ExactPi = Exact Integer Rational -- ^ @'Exact' z q@ = q * pi^z. Note that this means there are many representations of zero. + | Approximate (forall a.Floating a => a) -- ^ An approximate value. This representation was chosen because it allows conversion to floating types using their native definition of 'pi'. + +-- | Approximates an exact or approximate value, converting it to a `Floating` type. +-- This uses the value of `pi` supplied by the destination type, to provide the appropriate +-- precision. +approximateValue :: Floating a => ExactPi -> a +approximateValue (Exact z q) = (pi ^^ z) * (fromRational q) +approximateValue (Approximate x) = x + +-- | Identifies whether an 'ExactPi' is an exact or approximate representation of zero. +isZero :: ExactPi -> Bool +isZero (Exact _ 0) = True +isZero (Approximate x) = x == (0 :: Double) +isZero _ = False + +-- | Identifies whether an 'ExactPi' is an exact value. +isExact :: ExactPi -> Bool +isExact (Exact _ _) = True +isExact _ = False + +-- | Identifies whether an 'ExactPi' is an exact representation of zero. +isExactZero :: ExactPi -> Bool +isExactZero (Exact _ 0) = True +isExactZero _ = False + +-- | Identifies whether an 'ExactPi' is an exact representation of one. +isExactOne :: ExactPi -> Bool +isExactOne (Exact 0 1) = True +isExactOne _ = False + +-- | Identifies whether two 'ExactPi' values are exactly equal. +areExactlyEqual :: ExactPi -> ExactPi -> Bool +areExactlyEqual (Exact z1 q1) (Exact z2 q2) = (z1 == z2 && q1 == q2) || (q1 == 0 && q2 == 0) +areExactlyEqual _ _ = False + +-- | Identifies whether an 'ExactPi' is an exact representation of an integer. +isExactInteger :: ExactPi -> Bool +isExactInteger (Exact 0 q) | denominator q == 1 = True +isExactInteger _ = False + +-- | Converts an 'ExactPi' to an exact 'Integer' or 'Nothing'. +toExactInteger :: ExactPi -> Maybe Integer +toExactInteger (Exact 0 q) | denominator q == 1 = Just $ numerator q +toExactInteger _ = Nothing + +-- | Identifies whether an 'ExactPi' is an exact representation of a rational. +isExactRational :: ExactPi -> Bool +isExactRational (Exact 0 _) = True +isExactRational _ = False + +-- | Converts an 'ExactPi' to an exact 'Rational' or 'Nothing'. +toExactRational :: ExactPi -> Maybe Rational +toExactRational (Exact 0 q) = Just q +toExactRational _ = Nothing + +-- | Converts an 'ExactPi' to a list of increasingly accurate rational approximations, on alternating +-- sides of the actual value. Note that 'Approximate' values are converted using the 'Real' instance +-- for 'Double' into a singleton list. Note that exact rationals are also converted into a singleton list. +-- +-- Implementation based on work by Anders Kaseorg shared at http://qr.ae/RbXl8M. +rationalApproximations :: ExactPi -> [Rational] +rationalApproximations (Approximate x) = [toRational (x :: Double)] +rationalApproximations (Exact 0 q) = [q] +rationalApproximations (Exact z q) = fmap (\pi' -> q * (pi' ^^ z)) piConvergents + where + piConvergents :: [Rational] + piConvergents = go True 2 4 where + go s p' q' | ltPi m = [q' | not s] ++ go True m q' + | otherwise = [p' | s] ++ go False p' m where + m = (numerator p' + numerator q')%(denominator p' + denominator q') + ltPi :: Rational -> Bool + ltPi x = ok x 1 where + ok y i = + y <= (27*i - 12)%5 || + (y < (675*i - 216)%125 && + ok ((y - fromInteger (5*i - 2))*(3*(3*i + 1)*(3*i + 2)%(i*(2*i - 1)))) + (i + 1)) + +instance Show ExactPi where + show (Exact z q) | z == 0 = "Exactly " ++ show q + | z == 1 = "Exactly pi * " ++ show q + | otherwise = "Exactly pi^" ++ show z ++ " * " ++ show q + show (Approximate x) = "Approximately " ++ show (x :: Double) + +instance Num ExactPi where + fromInteger n = Exact 0 (fromInteger n) + (Exact z1 q1) * (Exact z2 q2) = Exact (z1 + z2) (q1 * q2) + (Exact _ 0) * _ = 0 + _ * (Exact _ 0) = 0 + x * y = Approximate $ approximateValue x * approximateValue y + (Exact z1 q1) + (Exact z2 q2) | z1 == z2 = Exact z1 (q1 + q2) -- by distributive property + x + y = Approximate $ approximateValue x + approximateValue y + abs (Exact z q) = Exact z (abs q) + abs (Approximate x) = Approximate $ abs x + signum (Exact _ q) = Exact 0 (signum q) + signum (Approximate x) = Approximate $ signum x -- we leave this tagged as approximate because we don't know "how" approximate the input was. a case could be made for exact answers here. + negate x = (Exact 0 (-1)) * x + +instance Fractional ExactPi where + fromRational = Exact 0 + recip (Exact z q) = Exact (negate z) (recip q) + recip (Approximate x) = Approximate (recip x) + +instance Floating ExactPi where + pi = Exact 1 1 + exp x | isExactZero x = 1 + | otherwise = approx1 exp x + log (Exact 0 1) = 0 + log x = approx1 log x + -- It would be possible to give tighter bounds to the trig functions, preserving exactness for arguments that have an exactly representable result. + sin = approx1 sin + cos = approx1 cos + tan = approx1 tan + asin = approx1 asin + atan = approx1 atan + acos = approx1 acos + sinh = approx1 sinh + cosh = approx1 cosh + tanh = approx1 tanh + asinh = approx1 asinh + acosh = approx1 acosh + atanh = approx1 atanh + +approx1 :: (forall a.Floating a => a -> a) -> ExactPi -> ExactPi +approx1 f x = Approximate (f (approximateValue x)) + +-- | The multiplicative semigroup over 'Rational's augmented with multiples of 'pi'. +instance Semigroup ExactPi where + (<>) = mappend + +-- | The multiplicative monoid over 'Rational's augmented with multiples of 'pi'. +instance Monoid ExactPi where + mempty = 1 + mappend = (*) diff --git a/src/Data/ExactPi/TypeLevel.hs b/src/Data/ExactPi/TypeLevel.hs --- a/src/Data/ExactPi/TypeLevel.hs +++ b/src/Data/ExactPi/TypeLevel.hs @@ -1,132 +1,132 @@ -{-# OPTIONS_HADDOCK show-extensions #-} - -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE KindSignatures #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeOperators #-} - -{-| -Module : Data.ExactPi.TypeLevel -Description : Exact non-negative rational multiples of powers of pi at the type level -License : MIT -Maintainer : douglas.mcclean@gmail.com -Stability : experimental - -This kind is sufficient to exactly express the closure of Q⁺ ∪ {π} under multiplication and division. -As a result it is useful for representing conversion factors between physical units. --} -module Data.ExactPi.TypeLevel -( - -- * Type Level ExactPi Values - type ExactPi'(..), - KnownExactPi(..), - -- * Arithmetic - type (*), type (/), type Recip, - type ExactNatural, - type One, type Pi, - -- * Conversion to Term Level - type MinCtxt, type MinCtxt', - injMin -) -where - -import Data.ExactPi -import Data.Maybe (fromJust) -import Data.Proxy -import Data.Ratio -import GHC.Exts (Constraint) -import GHC.TypeLits hiding (type (*), type (^)) -import qualified GHC.TypeLits as N -import Numeric.NumType.DK.Integers hiding (type (*), type (/)) -import qualified Numeric.NumType.DK.Integers as Z - --- | A type-level representation of a non-negative rational multiple of an integer power of pi. --- --- Each type in this kind can be exactly represented at the term level by a value of type 'ExactPi', --- provided that its denominator is non-zero. --- --- Note that there are many representations of zero, and many representations of dividing by zero. --- These are not excluded because doing so introduces a lot of extra machinery. Play nice! Future --- versions may not include a representation for zero. --- --- Of course there are also many representations of every value, because the numerator need not be --- comprime to the denominator. For many purposes it is not necessary to maintain the types in reduced --- form, they will be appropriately reduced when converted to terms. -data ExactPi' = ExactPi' TypeInt -- Exponent of pi - Nat -- Numerator - Nat -- Denominator - --- | A KnownDimension is one for which we can construct a term-level representation. --- --- Each validly constructed type of kind 'ExactPi'' has a 'KnownExactPi' instance, provided that --- its denominator is non-zero. -class KnownExactPi (v :: ExactPi') where - -- | Converts an 'ExactPi'' type to an 'ExactPi' value. - exactPiVal :: Proxy v -> ExactPi - --- | Determines the minimum context required for a numeric type to hold the value --- associated with a specific 'ExactPi'' type. -type family MinCtxt' (v :: ExactPi') :: * -> Constraint where - MinCtxt' ('ExactPi' 'Zero p 1) = Num - MinCtxt' ('ExactPi' 'Zero p q) = Fractional - MinCtxt' ('ExactPi' z p q) = Floating - -type MinCtxt v a = (KnownExactPi v, MinCtxt' v a, KnownMinCtxt (MinCtxt' v)) - --- | A KnownMinCtxt is a contraint on values sufficient to allow us to inject certain --- 'ExactPi' values into types that satisfy the constraint. -class KnownMinCtxt (c :: * -> Constraint) where - -- | Injects an 'ExactPi' value into a specified type satisfying this constraint. - -- - -- The injection is permitted to fail if type constraint does not entail the 'MinCtxt' - -- required by the 'ExactPi'' representation of the supplied 'ExactPi' value. - inj :: c a => Proxy c -- ^ A proxy for identifying the required constraint. - -> ExactPi -- ^ The value to inject. - -> a -- ^ A value of the constrained type corresponding to the supplied 'ExactPi' value. - -instance KnownMinCtxt Num where - inj _ = fromInteger . fromJust . toExactInteger - -instance KnownMinCtxt Fractional where - inj _ = fromRational . fromJust . toExactRational - -instance KnownMinCtxt Floating where - inj _ = approximateValue - --- | Converts an 'ExactPi'' type to a numeric value with the minimum required context. --- --- When the value is known to be an integer, it can be returned as any instance of 'Num'. Similarly, --- rationals require 'Fractional', and values that involve 'pi' require 'Floating'. -injMin :: forall v a.(MinCtxt v a) => Proxy v -> a -injMin = inj (Proxy :: Proxy (MinCtxt' v)) . exactPiVal - -instance (KnownTypeInt z, KnownNat p, KnownNat q, 1 <= q) => KnownExactPi ('ExactPi' z p q) where - exactPiVal _ = Exact z' (p' % q') - where - z' = toNum (Proxy :: Proxy z) - p' = natVal (Proxy :: Proxy p) - q' = natVal (Proxy :: Proxy q) - --- | Forms the product of 'ExactPi'' types (in the arithmetic sense). -type family (a :: ExactPi') * (b :: ExactPi') :: ExactPi' where - ('ExactPi' z p q) * ('ExactPi' z' p' q') = 'ExactPi' (z Z.+ z') (p N.* p') (q N.* q') - --- | Forms the quotient of 'ExactPi'' types (in the arithmetic sense). -type family (a :: ExactPi') / (b :: ExactPi') :: ExactPi' where - ('ExactPi' z p q) / ('ExactPi' z' p' q') = 'ExactPi' (z Z.- z') (p N.* q') (q N.* p') - --- | Forms the reciprocal of an 'ExactPi'' type. -type family Recip (a :: ExactPi') :: ExactPi' where - Recip ('ExactPi' z p q) = 'ExactPi' (Negate z) q p - --- | Converts a type-level natural to an 'ExactPi'' type. -type ExactNatural n = 'ExactPi' 'Zero n 1 - --- | The 'ExactPi'' type representing the number 1. -type One = ExactNatural 1 - --- | The 'ExactPi'' type representing the number 'pi'. -type Pi = 'ExactPi' 'Pos1 1 1 +{-# OPTIONS_HADDOCK show-extensions #-} + +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} + +{-| +Module : Data.ExactPi.TypeLevel +Description : Exact non-negative rational multiples of powers of pi at the type level +License : MIT +Maintainer : douglas.mcclean@gmail.com +Stability : experimental + +This kind is sufficient to exactly express the closure of Q⁺ ∪ {π} under multiplication and division. +As a result it is useful for representing conversion factors between physical units. +-} +module Data.ExactPi.TypeLevel +( + -- * Type Level ExactPi Values + type ExactPi'(..), + KnownExactPi(..), + -- * Arithmetic + type (*), type (/), type Recip, + type ExactNatural, + type One, type Pi, + -- * Conversion to Term Level + type MinCtxt, type MinCtxt', + injMin +) +where + +import Data.ExactPi +import Data.Maybe (fromJust) +import Data.Proxy +import Data.Ratio +import GHC.Exts (Constraint) +import GHC.TypeLits hiding (type (*), type (^)) +import qualified GHC.TypeLits as N +import Numeric.NumType.DK.Integers hiding (type (*), type (/)) +import qualified Numeric.NumType.DK.Integers as Z + +-- | A type-level representation of a non-negative rational multiple of an integer power of pi. +-- +-- Each type in this kind can be exactly represented at the term level by a value of type 'ExactPi', +-- provided that its denominator is non-zero. +-- +-- Note that there are many representations of zero, and many representations of dividing by zero. +-- These are not excluded because doing so introduces a lot of extra machinery. Play nice! Future +-- versions may not include a representation for zero. +-- +-- Of course there are also many representations of every value, because the numerator need not be +-- comprime to the denominator. For many purposes it is not necessary to maintain the types in reduced +-- form, they will be appropriately reduced when converted to terms. +data ExactPi' = ExactPi' TypeInt -- Exponent of pi + Nat -- Numerator + Nat -- Denominator + +-- | A KnownDimension is one for which we can construct a term-level representation. +-- +-- Each validly constructed type of kind 'ExactPi'' has a 'KnownExactPi' instance, provided that +-- its denominator is non-zero. +class KnownExactPi (v :: ExactPi') where + -- | Converts an 'ExactPi'' type to an 'ExactPi' value. + exactPiVal :: Proxy v -> ExactPi + +-- | Determines the minimum context required for a numeric type to hold the value +-- associated with a specific 'ExactPi'' type. +type family MinCtxt' (v :: ExactPi') :: * -> Constraint where + MinCtxt' ('ExactPi' 'Zero p 1) = Num + MinCtxt' ('ExactPi' 'Zero p q) = Fractional + MinCtxt' ('ExactPi' z p q) = Floating + +type MinCtxt v a = (KnownExactPi v, MinCtxt' v a, KnownMinCtxt (MinCtxt' v)) + +-- | A KnownMinCtxt is a contraint on values sufficient to allow us to inject certain +-- 'ExactPi' values into types that satisfy the constraint. +class KnownMinCtxt (c :: * -> Constraint) where + -- | Injects an 'ExactPi' value into a specified type satisfying this constraint. + -- + -- The injection is permitted to fail if type constraint does not entail the 'MinCtxt' + -- required by the 'ExactPi'' representation of the supplied 'ExactPi' value. + inj :: c a => Proxy c -- ^ A proxy for identifying the required constraint. + -> ExactPi -- ^ The value to inject. + -> a -- ^ A value of the constrained type corresponding to the supplied 'ExactPi' value. + +instance KnownMinCtxt Num where + inj _ = fromInteger . fromJust . toExactInteger + +instance KnownMinCtxt Fractional where + inj _ = fromRational . fromJust . toExactRational + +instance KnownMinCtxt Floating where + inj _ = approximateValue + +-- | Converts an 'ExactPi'' type to a numeric value with the minimum required context. +-- +-- When the value is known to be an integer, it can be returned as any instance of 'Num'. Similarly, +-- rationals require 'Fractional', and values that involve 'pi' require 'Floating'. +injMin :: forall v a.(MinCtxt v a) => Proxy v -> a +injMin = inj (Proxy :: Proxy (MinCtxt' v)) . exactPiVal + +instance (KnownTypeInt z, KnownNat p, KnownNat q, 1 <= q) => KnownExactPi ('ExactPi' z p q) where + exactPiVal _ = Exact z' (p' % q') + where + z' = toNum (Proxy :: Proxy z) + p' = natVal (Proxy :: Proxy p) + q' = natVal (Proxy :: Proxy q) + +-- | Forms the product of 'ExactPi'' types (in the arithmetic sense). +type family (a :: ExactPi') * (b :: ExactPi') :: ExactPi' where + ('ExactPi' z p q) * ('ExactPi' z' p' q') = 'ExactPi' (z Z.+ z') (p N.* p') (q N.* q') + +-- | Forms the quotient of 'ExactPi'' types (in the arithmetic sense). +type family (a :: ExactPi') / (b :: ExactPi') :: ExactPi' where + ('ExactPi' z p q) / ('ExactPi' z' p' q') = 'ExactPi' (z Z.- z') (p N.* q') (q N.* p') + +-- | Forms the reciprocal of an 'ExactPi'' type. +type family Recip (a :: ExactPi') :: ExactPi' where + Recip ('ExactPi' z p q) = 'ExactPi' (Negate z) q p + +-- | Converts a type-level natural to an 'ExactPi'' type. +type ExactNatural n = 'ExactPi' 'Zero n 1 + +-- | The 'ExactPi'' type representing the number 1. +type One = ExactNatural 1 + +-- | The 'ExactPi'' type representing the number 'pi'. +type Pi = 'ExactPi' 'Pos1 1 1