License	MIT
Maintainer	douglas.mcclean@gmail.com
Stability	experimental
Safe Haskell	None
Language	Haskell2010
Extensions	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

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 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

(KnownTypeInt z, KnownNat p, KnownNat q, (<=) 1 q) => KnownExactPi (ExactPi' z p q) Source

Arithmetic

type family a * b :: ExactPi' 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 / b :: ExactPi' 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' Source

Forms the reciprocal of an ExactPi' type.

Equations

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

type ExactNatural n = 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 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.

Equations

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

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.