exact-pi-0.5.0.2: Exact rational multiples of pi (and integer powers of pi)

License | MIT
Maintainer | douglas.mcclean@gmail.com
Stability | experimental
Safe Haskell | Safe-Inferred
Language | Haskell2010

Extensions

- Cpp
- UndecidableInstances
- MonoLocalBinds
- ScopedTypeVariables
- TypeFamilies
- ConstraintKinds
- DataKinds
- FlexibleContexts
- KindSignatures
- TypeOperators
- ExplicitNamespaces
- ExplicitForAll

Data.ExactPi.TypeLevel

Contents

- Type Level ExactPi Values
- Arithmetic
- Conversion to Term Level

Description

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.

Synopsis

- data ExactPi' = ExactPi' TypeInt Nat Nat
- class KnownExactPi (v :: ExactPi') where
  - exactPiVal :: Proxy v -> ExactPi
- type family (a :: ExactPi') * (b :: ExactPi') :: ExactPi' where ...
- type family (a :: ExactPi') / (b :: ExactPi') :: ExactPi' where ...
- type family Recip (a :: ExactPi') :: ExactPi' where ...
- type ExactNatural (n :: Nat) = 'ExactPi' 'Zero n 1
- type One = ExactNatural 1
- type Pi = 'ExactPi' 'Pos1 1 1
- type MinCtxt (v :: ExactPi') a = (KnownExactPi v, MinCtxt' v a, KnownMinCtxt (MinCtxt' v))
- type family MinCtxt' (v :: ExactPi') :: Type -> Constraint where ...
- injMin :: forall (v :: ExactPi') a. MinCtxt v a => Proxy v -> a

# Type Level ExactPi Values

data ExactPi' Source #

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.

Constructors

ExactPi' TypeInt Nat Nat |

class KnownExactPi (v :: ExactPi') where Source #

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.

Methods

exactPiVal :: Proxy v -> ExactPi Source #

Converts an `ExactPi'` type to an `ExactPi` value.

#### Instances

Instances details

(KnownTypeInt z, KnownNat p, KnownNat q, 1 <= q) => KnownExactPi ('ExactPi' z p q) Source # |
Instance details Defined in Data.ExactPi.TypeLevel Methods exactPiVal :: Proxy ('ExactPi' z p q) -> ExactPi Source #

# Arithmetic

type family (a :: ExactPi') * (b :: ExactPi') :: ExactPi' where ... Source #

Forms the product of `ExactPi'` types (in the arithmetic sense).

Equations

('ExactPi' z p q) * ('ExactPi' z' p' q') = 'ExactPi' (z + z') (p * p') (q * q') |

type family (a :: ExactPi') / (b :: ExactPi') :: ExactPi' where ... Source #

Forms the quotient of `ExactPi'` types (in the arithmetic sense).

Equations

('ExactPi' z p q) / ('ExactPi' z' p' q') = 'ExactPi' (z - z') (p * q') (q * p') |

type family Recip (a :: ExactPi') :: ExactPi' where ... Source #

Forms the reciprocal of an `ExactPi'` type.

Equations

Recip ('ExactPi' z p q) = 'ExactPi' (Negate z) q p |

type ExactNatural (n :: Nat) = 'ExactPi' 'Zero n 1 Source #

Converts a type-level natural to an `ExactPi'` type.

type One = ExactNatural 1 Source #

The `ExactPi'` type representing the number 1.

type Pi = 'ExactPi' 'Pos1 1 1 Source #

The `ExactPi'` type representing the number `pi`.

# Conversion to Term Level

type MinCtxt (v :: ExactPi') a = (KnownExactPi v, MinCtxt' v a, KnownMinCtxt (MinCtxt' v)) Source #

type family MinCtxt' (v :: ExactPi') :: Type -> Constraint where ... Source #

Determines the minimum context required for a numeric type to hold the value associated with a specific `ExactPi'` type.

Equations

MinCtxt' ('ExactPi' 'Zero p 1) = Num |
MinCtxt' ('ExactPi' 'Zero p q) = Fractional |
MinCtxt' ('ExactPi' z p q) = Floating |

injMin :: forall (v :: ExactPi') 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`.