License  MIT 

Maintainer  douglas.mcclean@gmail.com 
Stability  experimental 
Safe Haskell  None 
Language  Haskell2010 
Extensions 

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.
 data ExactPi' = ExactPi' TypeInt Nat Nat
 class KnownExactPi v where
 exactPiVal :: Proxy v > ExactPi
 type family a * b :: ExactPi'
 type family a / b :: ExactPi'
 type family Recip a :: ExactPi'
 type ExactNatural n = ExactPi' Zero n 1
 type One = ExactNatural 1
 type Pi = ExactPi' Pos1 1 1
 type MinCtxt v a = (KnownExactPi v, MinCtxt' v a, KnownMinCtxt (MinCtxt' v))
 type family MinCtxt' v :: * > Constraint
 injMin :: forall v a. MinCtxt v a => Proxy v > a
Type Level ExactPi Values
A typelevel representation of a nonnegative 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 nonzero.
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.
class KnownExactPi v where Source
A KnownDimension is one for which we can construct a termlevel representation.
Each validly constructed type of kind ExactPi'
has a KnownExactPi
instance, provided that
its denominator is nonzero.
(KnownTypeInt z, KnownNat p, KnownNat q, (<=) 1 q) => KnownExactPi (ExactPi' z p q) Source 
Arithmetic
type ExactNatural n = ExactPi' Zero n 1 Source
Converts a typelevel natural to an ExactPi'
type.
type One = ExactNatural 1 Source
The ExactPi'
type representing the number 1.
Conversion to Term Level
type MinCtxt v a = (KnownExactPi v, MinCtxt' v a, KnownMinCtxt (MinCtxt' v)) Source
type family MinCtxt' v :: * > Constraint Source
Determines the minimum context required for a numeric type to hold the value
associated with a specific ExactPi'
type.
injMin :: forall v a. MinCtxt v a => Proxy v > a Source
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
.