units-2.4.1.2: A domain-specific type system for dimensional analysis

Data.Metrology.Poly

Description

This module exports all the gubbins needed for type-checking your dimensioned quantities. See Metrology for some functions restricted to using a default LCSU, which is suitable for many applications. See also Vector for polymorphic functions suitable for use with the numerical classes from the vector-space package.

Synopsis

# Term-level combinators

The term-level arithmetic operators are defined by applying vertical bar(s) to the sides the dimensioned quantities acts on.

zero :: Num n => Qu dimspec l n Source #

The number 0, polymorphic in its dimension. Use of this will often require a type annotation.

(|+|) :: (d1 @~ d2, Num n) => Qu d1 l n -> Qu d2 l n -> Qu d1 l n infixl 6 Source #

(|-|) :: (d1 @~ d2, Num n) => Qu d1 l n -> Qu d2 l n -> Qu d1 l n infixl 6 Source #

Subtract two compatible quantities

qSum :: (Foldable f, Num n) => f (Qu d l n) -> Qu d l n Source #

Take the sum of a list of quantities

qNegate :: Num n => Qu d l n -> Qu d l n Source #

Negate a quantity

## Multiplicative operations between quantities

(|*|) :: Num n => Qu a l n -> Qu b l n -> Qu (Normalize (a @+ b)) l n infixl 7 Source #

Multiply two quantities

(|/|) :: Fractional n => Qu a l n -> Qu b l n -> Qu (Normalize (a @- b)) l n infixl 7 Source #

Divide two quantities

## Multiplicative operations between a quantity and a non-quantity

(*|) :: Num n => n -> Qu b l n -> Qu b l n infixl 7 Source #

Multiply a quantity by a scalar from the left

(|*) :: Num n => Qu a l n -> n -> Qu a l n infixl 7 Source #

Multiply a quantity by a scalar from the right

(/|) :: Fractional n => n -> Qu b l n -> Qu (Normalize ('[] @- b)) l n infixl 7 Source #

Divide a scalar by a quantity

(|/) :: Fractional n => Qu a l n -> n -> Qu a l n infixl 7 Source #

Divide a quantity by a scalar

## Exponentiation

(|^) :: (NonNegative z, Num n) => Qu a l n -> Sing z -> Qu (a @* z) l n infixr 8 Source #

Raise a quantity to a integer power, knowing at compile time that the integer is non-negative.

(|^^) :: Fractional n => Qu a l n -> Sing z -> Qu (a @* z) l n infixr 8 Source #

Raise a quantity to a integer power known at compile time

qNthRoot :: ((Zero < z) ~ True, Floating n) => Sing z -> Qu a l n -> Qu (a @/ z) l n Source #

Take the n'th root of a quantity, where n is known at compile time

qSq :: Num n => Qu a l n -> Qu (Normalize (a @+ a)) l n Source #

Square a quantity

qCube :: Num n => Qu a l n -> Qu (Normalize (Normalize (a @+ a) @+ a)) l n Source #

Cube a quantity

qSqrt :: Floating n => Qu a l n -> Qu (a @/ Two) l n Source #

Take the square root of a quantity

qCubeRoot :: Floating n => Qu a l n -> Qu (a @/ Three) l n Source #

Take the cubic root of a quantity

## Comparison

qCompare :: (d1 @~ d2, Ord n) => Qu d1 l n -> Qu d2 l n -> Ordering Source #

Compare two quantities

(|<|) :: (d1 @~ d2, Ord n) => Qu d1 l n -> Qu d2 l n -> Bool infix 4 Source #

Check if one quantity is less than a compatible one

(|>|) :: (d1 @~ d2, Ord n) => Qu d1 l n -> Qu d2 l n -> Bool infix 4 Source #

Check if one quantity is greater than a compatible one

(|<=|) :: (d1 @~ d2, Ord n) => Qu d1 l n -> Qu d2 l n -> Bool infix 4 Source #

Check if one quantity is less than or equal to a compatible one

(|>=|) :: (d1 @~ d2, Ord n) => Qu d1 l n -> Qu d2 l n -> Bool infix 4 Source #

Check if one quantity is greater than or equal to a compatible one

(|==|) :: (d1 @~ d2, Eq n) => Qu d1 l n -> Qu d2 l n -> Bool infix 4 Source #

Check if two quantities are equal (uses the equality of the underlying numerical type)

(|/=|) :: (d1 @~ d2, Eq n) => Qu d1 l n -> Qu d2 l n -> Bool infix 4 Source #

Check if two quantities are not equal

qApprox infix 4 Source #

Arguments

 :: (d0 @~ d1, d0 @~ d2, Num n, Ord n) => Qu d0 l n epsilon -> Qu d1 l n left hand side -> Qu d2 l n right hand side -> Bool

Compare two compatible quantities for approximate equality. If the difference between the left hand side and the right hand side arguments are less than or equal to the epsilon, they are considered equal.

qNapprox infix 4 Source #

Arguments

 :: (d0 @~ d1, d0 @~ d2, Num n, Ord n) => Qu d0 l n epsilon -> Qu d1 l n left hand side -> Qu d2 l n right hand side -> Bool

Compare two compatible quantities for approixmate inequality. qNapprox e a b = not \$ qApprox e a b

# Nondimensional units, conversion between quantities and numeric values

numIn :: forall unit dim lcsu n. (ValidDLU dim lcsu unit, Fractional n) => Qu dim lcsu n -> unit -> n Source #

Extracts a numerical value from a dimensioned quantity, expressed in the given unit. For example:

inMeters :: Length -> Double
inMeters x = numIn x Meter

or

inMeters x = x # Meter

(#) :: (ValidDLU dim lcsu unit, Fractional n) => Qu dim lcsu n -> unit -> n infix 5 Source #

Infix synonym for numIn

quOf :: forall unit dim lcsu n. (ValidDLU dim lcsu unit, Fractional n) => n -> unit -> Qu dim lcsu n Source #

Creates a dimensioned quantity in the given unit. For example:

height :: Length
height = quOf 2.0 Meter

or

height = 2.0 % Meter

(%) :: (ValidDLU dim lcsu unit, Fractional n) => n -> unit -> Qu dim lcsu n infix 5 Source #

Infix synonym for quOf

showIn :: (ValidDLU dim lcsu unit, Fractional n, Show unit, Show n) => Qu dim lcsu n -> unit -> String infix 1 Source #

Show a dimensioned quantity in a given unit. (The default Show instance always uses units as specified in the LCSU.)

unity :: Num n => Qu '[] l n Source #

The number 1, expressed as a unitless dimensioned quantity.

redim :: d @~ e => Qu d l n -> Qu e l n Source #

Cast between equivalent dimension within the same CSU. for example [kg m s] and [s m kg]. See the README for more info.

convert :: forall d l1 l2 n. (ConvertibleLCSUs d l1 l2, Fractional n) => Qu d l1 n -> Qu d l2 n Source #

Dimension-keeping cast between different CSUs.

defaultLCSU :: Qu dim DefaultLCSU n -> Qu dim DefaultLCSU n Source #

Use this to choose a default LCSU for a dimensioned quantity. The default LCSU uses the DefaultUnitOfDim representation for each dimension.

constant :: (d @~ e, ConvertibleLCSUs e DefaultLCSU l, Fractional n) => Qu d DefaultLCSU n -> Qu e l n Source #

Compute the argument in the DefaultLCSU, and present the result as lcsu-polymorphic dimension-polymorphic value. Named constant because one of its dominant usecase is to inject constant quantities into dimension-polymorphic expressions.

# Type-level unit combinators

data u1 :* u2 infixl 7 Source #

Multiply two units to get another unit. For example: type MetersSquared = Meter :* Meter

Constructors

 u1 :* u2 infixl 7
Instances
 (Show u1, Show u2) => Show (u1 :* u2) Source # Instance detailsDefined in Data.Metrology.Combinators MethodsshowsPrec :: Int -> (u1 :* u2) -> ShowS #show :: (u1 :* u2) -> String #showList :: [u1 :* u2] -> ShowS # (Dimension d1, Dimension d2) => Dimension (d1 :* d2) Source # Instance detailsDefined in Data.Metrology.Combinators Associated Typestype DimFactorsOf (d1 :* d2) :: [Factor Type] Source # (Unit u1, Unit u2) => Unit (u1 :* u2) Source # Instance detailsDefined in Data.Metrology.Combinators Associated Typestype BaseUnit (u1 :* u2) :: Type Source #type DimOfUnit (u1 :* u2) :: Type Source #type UnitFactorsOf (u1 :* u2) :: [Factor Type] Source # MethodsconversionRatio :: (u1 :* u2) -> Rational Source #canonicalConvRatio :: (u1 :* u2) -> Rational type DefaultUnitOfDim (d1 :* d2) Source # Instance detailsDefined in Data.Metrology.Combinators type DefaultUnitOfDim (d1 :* d2) = DefaultUnitOfDim d1 :* DefaultUnitOfDim d2 type DimFactorsOf (d1 :* d2) Source # Instance detailsDefined in Data.Metrology.Combinators type DimFactorsOf (d1 :* d2) = Normalize (DimFactorsOf d1 @+ DimFactorsOf d2) type BaseUnit (u1 :* u2) Source # Instance detailsDefined in Data.Metrology.Combinators type BaseUnit (u1 :* u2) = Canonical type DimOfUnit (u1 :* u2) Source # Instance detailsDefined in Data.Metrology.Combinators type DimOfUnit (u1 :* u2) = DimOfUnit u1 :* DimOfUnit u2 type UnitFactorsOf (u1 :* u2) Source # Instance detailsDefined in Data.Metrology.Combinators type UnitFactorsOf (u1 :* u2) = Normalize (UnitFactorsOf u1 @+ UnitFactorsOf u2)

data u1 :/ u2 infixl 7 Source #

Divide two units to get another unit

Constructors

 u1 :/ u2 infixl 7
Instances
 (Show u1, Show u2) => Show (u1 :/ u2) Source # Instance detailsDefined in Data.Metrology.Combinators MethodsshowsPrec :: Int -> (u1 :/ u2) -> ShowS #show :: (u1 :/ u2) -> String #showList :: [u1 :/ u2] -> ShowS # (Dimension d1, Dimension d2) => Dimension (d1 :/ d2) Source # Instance detailsDefined in Data.Metrology.Combinators Associated Typestype DimFactorsOf (d1 :/ d2) :: [Factor Type] Source # (Unit u1, Unit u2) => Unit (u1 :/ u2) Source # Instance detailsDefined in Data.Metrology.Combinators Associated Typestype BaseUnit (u1 :/ u2) :: Type Source #type DimOfUnit (u1 :/ u2) :: Type Source #type UnitFactorsOf (u1 :/ u2) :: [Factor Type] Source # MethodsconversionRatio :: (u1 :/ u2) -> Rational Source #canonicalConvRatio :: (u1 :/ u2) -> Rational type DefaultUnitOfDim (d1 :/ d2) Source # Instance detailsDefined in Data.Metrology.Combinators type DefaultUnitOfDim (d1 :/ d2) = DefaultUnitOfDim d1 :/ DefaultUnitOfDim d2 type DimFactorsOf (d1 :/ d2) Source # Instance detailsDefined in Data.Metrology.Combinators type DimFactorsOf (d1 :/ d2) = Normalize (DimFactorsOf d1 @- DimFactorsOf d2) type BaseUnit (u1 :/ u2) Source # Instance detailsDefined in Data.Metrology.Combinators type BaseUnit (u1 :/ u2) = Canonical type DimOfUnit (u1 :/ u2) Source # Instance detailsDefined in Data.Metrology.Combinators type DimOfUnit (u1 :/ u2) = DimOfUnit u1 :/ DimOfUnit u2 type UnitFactorsOf (u1 :/ u2) Source # Instance detailsDefined in Data.Metrology.Combinators type UnitFactorsOf (u1 :/ u2) = Normalize (UnitFactorsOf u1 @- UnitFactorsOf u2)

data unit :^ (power :: Z) infixr 8 Source #

Raise a unit to a power, known at compile time

Constructors

 unit :^ (Sing power) infixr 8
Instances
 (Show u1, SingI power) => Show (u1 :^ power) Source # Instance detailsDefined in Data.Metrology.Combinators MethodsshowsPrec :: Int -> (u1 :^ power) -> ShowS #show :: (u1 :^ power) -> String #showList :: [u1 :^ power] -> ShowS # Dimension dim => Dimension (dim :^ power) Source # Instance detailsDefined in Data.Metrology.Combinators Associated Typestype DimFactorsOf (dim :^ power) :: [Factor Type] Source # (Unit unit, SingI power) => Unit (unit :^ power) Source # Instance detailsDefined in Data.Metrology.Combinators Associated Typestype BaseUnit (unit :^ power) :: Type Source #type DimOfUnit (unit :^ power) :: Type Source #type UnitFactorsOf (unit :^ power) :: [Factor Type] Source # MethodsconversionRatio :: (unit :^ power) -> Rational Source #canonicalConvRatio :: (unit :^ power) -> Rational type DefaultUnitOfDim (d :^ z) Source # Instance detailsDefined in Data.Metrology.Combinators type DefaultUnitOfDim (d :^ z) = DefaultUnitOfDim d :^ z type DimFactorsOf (dim :^ power) Source # Instance detailsDefined in Data.Metrology.Combinators type DimFactorsOf (dim :^ power) = Normalize (DimFactorsOf dim @* power) type BaseUnit (unit :^ power) Source # Instance detailsDefined in Data.Metrology.Combinators type BaseUnit (unit :^ power) = Canonical type DimOfUnit (unit :^ power) Source # Instance detailsDefined in Data.Metrology.Combinators type DimOfUnit (unit :^ power) = DimOfUnit unit :^ power type UnitFactorsOf (unit :^ power) Source # Instance detailsDefined in Data.Metrology.Combinators type UnitFactorsOf (unit :^ power) = Normalize (UnitFactorsOf unit @* power)

data prefix :@ unit infixr 9 Source #

Multiply a conversion ratio by some constant. Used for defining prefixes.

Constructors

 prefix :@ unit infixr 9
Instances
 (Show prefix, Show unit) => Show (prefix :@ unit) Source # Instance detailsDefined in Data.Metrology.Combinators MethodsshowsPrec :: Int -> (prefix :@ unit) -> ShowS #show :: (prefix :@ unit) -> String #showList :: [prefix :@ unit] -> ShowS # ((unit == Canonical) ~ False, Unit unit, UnitPrefix prefix) => Unit (prefix :@ unit) Source # Instance detailsDefined in Data.Metrology.Combinators Associated Typestype BaseUnit (prefix :@ unit) :: Type Source #type DimOfUnit (prefix :@ unit) :: Type Source #type UnitFactorsOf (prefix :@ unit) :: [Factor Type] Source # MethodsconversionRatio :: (prefix :@ unit) -> Rational Source #canonicalConvRatio :: (prefix :@ unit) -> Rational type BaseUnit (prefix :@ unit) Source # Instance detailsDefined in Data.Metrology.Combinators type BaseUnit (prefix :@ unit) = unit type DimOfUnit (prefix :@ unit) Source # Instance detailsDefined in Data.Metrology.Combinators type DimOfUnit (prefix :@ unit) = DimOfUnit (BaseUnit (prefix :@ unit)) type UnitFactorsOf (prefix :@ unit) Source # Instance detailsDefined in Data.Metrology.Combinators type UnitFactorsOf (prefix :@ unit) = If (IsCanonical (prefix :@ unit)) (F (prefix :@ unit) One ': ([] :: [Factor Type])) (UnitFactorsOf (BaseUnit (prefix :@ unit)))

class UnitPrefix prefix where Source #

A class for user-defined prefixes

Methods

multiplier :: Fractional f => prefix -> f Source #

This should return the desired multiplier for the prefix being defined. This function must not inspect its argument.

# Type-level quantity combinators

type family (d1 :: *) %* (d2 :: *) :: * infixl 7 Source #

Multiply two quantity types to produce a new one. For example:

type Velocity = Length %/ Time
Instances
 type (Qu d1 l n) %* (Qu d2 l n) Source # Instance detailsDefined in Data.Metrology.Qu type (Qu d1 l n) %* (Qu d2 l n) = Qu (d1 @+ d2) l n

type family (d1 :: *) %/ (d2 :: *) :: * infixl 7 Source #

Divide two quantity types to produce a new one

Instances
 type (Qu d1 l n) %/ (Qu d2 l n) Source # Instance detailsDefined in Data.Metrology.Qu type (Qu d1 l n) %/ (Qu d2 l n) = Qu (d1 @- d2) l n

type family (d :: *) %^ (z :: Z) :: * infixr 8 Source #

Exponentiate a quantity type to an integer

Instances
 type (Qu d l n) %^ z Source # Instance detailsDefined in Data.Metrology.Qu type (Qu d l n) %^ z = Qu (d @* z) l n

# Creating quantity types

data Qu (a :: [Factor *]) (lcsu :: LCSU *) (n :: *) Source #

Qu adds a dimensional annotation to its numerical value type n. This is the representation for all quantities.

Instances

type MkQu_D dim = Qu (DimFactorsOf dim) DefaultLCSU Double Source #

Make a quantity type capable of storing a value of a given unit. This uses a Double for storage of the value. For example:

data LengthDim = LengthDim
instance Dimension LengthDim
data Meter = Meter
instance Unit Meter where
type BaseUnit Meter = Canonical
type DimOfUnit Meter = LengthDim
type instance DefaultUnitOfDim LengthDim = Meter
type Length = MkQu_D LengthDim

Note that the dimension must have an instance for the type family DefaultUnitOfDim for this to work.

type MkQu_DLN dim = Qu (DimFactorsOf dim) Source #

Make a quantity type with a custom numerical type and LCSU.

type MkQu_U unit = Qu (DimFactorsOf (DimOfUnit unit)) DefaultLCSU Double Source #

Make a quantity type with a given unit. It will be stored as a Double. Note that the corresponding dimension must have an appropriate instance for DefaultUnitOfDim for this to work.

type MkQu_ULN unit = Qu (DimFactorsOf (DimOfUnit unit)) Source #

Make a quantity type with a unit and LCSU with custom numerical type. The quantity will have the dimension corresponding to the unit.

# Creating new dimensions

class Dimension dim Source #

This class is used to mark abstract dimensions, such as Length, or Mass.

Instances
 Source # Instance detailsDefined in Data.Metrology.Units Associated Types Dimension dim => Dimension (dim :^ power) Source # Instance detailsDefined in Data.Metrology.Combinators Associated Typestype DimFactorsOf (dim :^ power) :: [Factor Type] Source # (Dimension d1, Dimension d2) => Dimension (d1 :/ d2) Source # Instance detailsDefined in Data.Metrology.Combinators Associated Typestype DimFactorsOf (d1 :/ d2) :: [Factor Type] Source # (Dimension d1, Dimension d2) => Dimension (d1 :* d2) Source # Instance detailsDefined in Data.Metrology.Combinators Associated Typestype DimFactorsOf (d1 :* d2) :: [Factor Type] Source #

# Creating new units

class DimOfUnitIsConsistent unit => Unit unit where Source #

Minimal complete definition

Nothing

Associated Types

type BaseUnit unit :: * Source #

The base unit of this unit: what this unit is defined in terms of. For units that are not defined in terms of anything else, the base unit should be Canonical.

type DimOfUnit unit :: * Source #

The dimension that this unit is associated with. This needs to be defined only for canonical units; other units are necessarily of the same dimension as their base.

Methods

conversionRatio :: unit -> Rational Source #

The conversion ratio from the base unit to this unit. If left out, a conversion ratio of 1 is assumed.

For example:

instance Unit Foot where
type BaseUnit Foot = Meter
conversionRatio _ = 0.3048

Implementations should never examine their argument!

Instances
 Source # Instance detailsDefined in Data.Metrology.Units Associated Typestype UnitFactorsOf Number :: [Factor Type] Source # Methods ((unit == Canonical) ~ False, Unit unit, UnitPrefix prefix) => Unit (prefix :@ unit) Source # Instance detailsDefined in Data.Metrology.Combinators Associated Typestype BaseUnit (prefix :@ unit) :: Type Source #type DimOfUnit (prefix :@ unit) :: Type Source #type UnitFactorsOf (prefix :@ unit) :: [Factor Type] Source # MethodsconversionRatio :: (prefix :@ unit) -> Rational Source #canonicalConvRatio :: (prefix :@ unit) -> Rational (Unit unit, SingI power) => Unit (unit :^ power) Source # Instance detailsDefined in Data.Metrology.Combinators Associated Typestype BaseUnit (unit :^ power) :: Type Source #type DimOfUnit (unit :^ power) :: Type Source #type UnitFactorsOf (unit :^ power) :: [Factor Type] Source # MethodsconversionRatio :: (unit :^ power) -> Rational Source #canonicalConvRatio :: (unit :^ power) -> Rational (Unit u1, Unit u2) => Unit (u1 :/ u2) Source # Instance detailsDefined in Data.Metrology.Combinators Associated Typestype BaseUnit (u1 :/ u2) :: Type Source #type DimOfUnit (u1 :/ u2) :: Type Source #type UnitFactorsOf (u1 :/ u2) :: [Factor Type] Source # MethodsconversionRatio :: (u1 :/ u2) -> Rational Source #canonicalConvRatio :: (u1 :/ u2) -> Rational (Unit u1, Unit u2) => Unit (u1 :* u2) Source # Instance detailsDefined in Data.Metrology.Combinators Associated Typestype BaseUnit (u1 :* u2) :: Type Source #type DimOfUnit (u1 :* u2) :: Type Source #type UnitFactorsOf (u1 :* u2) :: [Factor Type] Source # MethodsconversionRatio :: (u1 :* u2) -> Rational Source #canonicalConvRatio :: (u1 :* u2) -> Rational

data Canonical Source #

Dummy type use just to label canonical units. It does not have a Unit instance.

# Numbers, the only built-in unit

The dimension for the dimensionless quantities. It is also called "quantities of dimension one", but One is confusing with the type-level integer One.

Constructors

 Dimensionless
Instances
 Source # Instance detailsDefined in Data.Metrology.Units Associated Types Source # Instance detailsDefined in Data.Metrology.Units Source # Instance detailsDefined in Data.Metrology.Units type DimFactorsOf Dimensionless = ([] :: [Factor Type])

data Number Source #

The unit for unitless dimensioned quantities

Constructors

 Number
Instances
 Source # Instance detailsDefined in Data.Metrology.Units Associated Typestype UnitFactorsOf Number :: [Factor Type] Source # Methods type BaseUnit Number Source # Instance detailsDefined in Data.Metrology.Units type DimOfUnit Number Source # Instance detailsDefined in Data.Metrology.Units Source # Instance detailsDefined in Data.Metrology.Units type UnitFactorsOf Number = ([] :: [Factor Type])

The type of unitless dimensioned quantities. This is an instance of Num, though Haddock doesn't show it. This is parameterized by an LCSU and a number representation.

quantity :: n -> Qu '[] l n Source #

Convert a raw number into a unitless dimensioned quantity

# LCSUs (locally coherent system of units)

type family MkLCSU pairs where ... Source #

Make a local consistent set of units. The argument is a type-level list of tuple types, to be interpreted as an association list from dimensions to units. For example:

type MyLCSU = MkLCSU '[(Length, Foot), (Mass, Gram), (Time, Year)]

Equations

 MkLCSU pairs = MkLCSU_ (UsePromotedTuples pairs)

data LCSU star Source #

Constructors

 DefaultLCSU

type family DefaultUnitOfDim (dim :: *) :: * Source #

Assign a default unit for a dimension. Necessary only when using default LCSUs.

Instances
 Source # Instance detailsDefined in Data.Metrology.Units type DefaultUnitOfDim (d :^ z) Source # Instance detailsDefined in Data.Metrology.Combinators type DefaultUnitOfDim (d :^ z) = DefaultUnitOfDim d :^ z type DefaultUnitOfDim (d1 :/ d2) Source # Instance detailsDefined in Data.Metrology.Combinators type DefaultUnitOfDim (d1 :/ d2) = DefaultUnitOfDim d1 :/ DefaultUnitOfDim d2 type DefaultUnitOfDim (d1 :* d2) Source # Instance detailsDefined in Data.Metrology.Combinators type DefaultUnitOfDim (d1 :* d2) = DefaultUnitOfDim d1 :* DefaultUnitOfDim d2

# Validity checks and assertions

type family CompatibleUnit (lcsu :: LCSU *) (unit :: *) :: Constraint where ... Source #

Check if an LCSU has consistent entries for the given unit. i.e. can the lcsu describe the unit?

Equations

 CompatibleUnit lcsu unit = (ValidDLU (DimFactorsOf (DimOfUnit unit)) lcsu unit, UnitFactor (LookupList (DimFactorsOf (DimOfUnit unit)) lcsu))

type family CompatibleDim (lcsu :: LCSU *) (dim :: *) :: Constraint where ... Source #

Check if an LCSU can express the given dimension

Equations

 CompatibleDim lcsu dim = (UnitFactor (LookupList (DimFactorsOf dim) lcsu), DimOfUnit (Lookup dim lcsu) ~ dim)

type family ConvertibleLCSUs_D (dim :: *) (l1 :: LCSU *) (l2 :: LCSU *) :: Constraint where ... Source #

Like ConvertibleLCSUs, but takes a dimension, not a dimension factors.

Equations

 ConvertibleLCSUs_D dim l1 l2 = ConvertibleLCSUs (DimFactorsOf dim) l1 l2

type family DefaultConvertibleLCSU_D (dim :: *) (l :: LCSU *) :: Constraint where ... Source #

Check if the DefaultLCSU can convert into the given one, at the given dimension.

Equations

 DefaultConvertibleLCSU_D dim l = (ValidDL (DimFactorsOf dim) DefaultLCSU, ConvertibleLCSUs (DimFactorsOf dim) DefaultLCSU l)

type family DefaultConvertibleLCSU_U (unit :: *) (l :: LCSU *) :: Constraint where ... Source #

Check if the DefaultLCSU can convert into the given one, at the given unit.

Equations

 DefaultConvertibleLCSU_U unit l = DefaultConvertibleLCSU_D (DimOfUnit unit) l

type family MultDimFactors (facts :: [Factor *]) where ... Source #

Extract a dimension specifier from a list of factors

Equations

 MultDimFactors '[] = Dimensionless MultDimFactors (F d z ': ds) = (d :^ z) :* MultDimFactors ds

type family MultUnitFactors (facts :: [Factor *]) where ... Source #

Extract a unit specifier from a list of factors

Equations

 MultUnitFactors '[] = Number MultUnitFactors (F unit z ': units) = (unit :^ z) :* MultUnitFactors units

type family UnitOfDimFactors (dims :: [Factor *]) (lcsu :: LCSU *) :: * where ... Source #

Extract a unit from a dimension factor list and an LCSU

Equations

 UnitOfDimFactors dims lcsu = MultUnitFactors (LookupList dims lcsu)

# Type-level integers

data Z Source #

The datatype for type-level integers.

Constructors

 Zero S Z P Z
Instances
 Source # Instance detailsDefined in Data.Metrology.Z Methods(==) :: Z -> Z -> Bool #(/=) :: Z -> Z -> Bool # SEq Z => SEq Z Source # Instance detailsDefined in Data.Metrology.Z Methods(%==) :: Sing a -> Sing b -> Sing (a == b) #(%/=) :: Sing a -> Sing b -> Sing (a /= b) # Source # Instance detailsDefined in Data.Metrology.Z Associated Typestype x == y :: Bool #type x /= y :: Bool # Source # Instance detailsDefined in Data.Metrology.Z Methods(%~) :: Sing a -> Sing b -> Decision (a :~: b) # Source # Instance detailsDefined in Data.Metrology.Z Associated Typestype Demote Z = (r :: Type) # MethodsfromSing :: Sing a -> Demote Z # Source # Instance detailsDefined in Data.Metrology.Z Methods SingI n => SingI (S n :: Z) Source # Instance detailsDefined in Data.Metrology.Z Methodssing :: Sing (S n) # SingI n => SingI (P n :: Z) Source # Instance detailsDefined in Data.Metrology.Z Methodssing :: Sing (P n) # Source # Instance detailsDefined in Data.Metrology.Z Methods Source # Instance detailsDefined in Data.Metrology.Z Methods Source # Instance detailsDefined in Data.Metrology.Z Methods Source # Instance detailsDefined in Data.Metrology.Z Methods Source # Instance detailsDefined in Data.Metrology.Z Methodssing :: Sing (TyCon1 S) # Source # Instance detailsDefined in Data.Metrology.Z Methodssing :: Sing (TyCon1 P) # data Sing (a :: Z) Source # Instance detailsDefined in Data.Metrology.Z data Sing (a :: Z) whereSZero :: forall (a :: Z). Sing ZeroSS :: forall (a :: Z) (n :: Z). Sing n -> Sing (S n)SP :: forall (a :: Z) (n :: Z). Sing n -> Sing (P n) type Demote Z Source # Instance detailsDefined in Data.Metrology.Z type Demote Z = Z type (x :: Z) /= (y :: Z) Source # Instance detailsDefined in Data.Metrology.Z type (x :: Z) /= (y :: Z) = Not (x == y) type (a :: Z) == (b :: Z) Source # Instance detailsDefined in Data.Metrology.Z type (a :: Z) == (b :: Z) type Apply PSym0 (t6989586621679083879 :: Z) Source # Instance detailsDefined in Data.Metrology.Z type Apply PSym0 (t6989586621679083879 :: Z) = P t6989586621679083879 type Apply SSym0 (t6989586621679083877 :: Z) Source # Instance detailsDefined in Data.Metrology.Z type Apply SSym0 (t6989586621679083877 :: Z) = S t6989586621679083877

type family Succ (z :: Z) :: Z where ... Source #

Equations

 Succ Zero = S Zero Succ (P z) = z Succ (S z) = S (S z)

type family Pred (z :: Z) :: Z where ... Source #

Subtract one from an integer

Equations

 Pred Zero = P Zero Pred (P z) = P (P z) Pred (S z) = z

type family (a :: Z) #+ (b :: Z) :: Z where ... infixl 6 Source #

Equations

 Zero #+ z = z (S z1) #+ (S z2) = S (S (z1 #+ z2)) (S z1) #+ Zero = S z1 (S z1) #+ (P z2) = z1 #+ z2 (P z1) #+ (S z2) = z1 #+ z2 (P z1) #+ Zero = P z1 (P z1) #+ (P z2) = P (P (z1 #+ z2))

type family (a :: Z) #- (b :: Z) :: Z where ... infixl 6 Source #

Subtract two integers

Equations

 z #- Zero = z (S z1) #- (S z2) = z1 #- z2 Zero #- (S z2) = P (Zero #- z2) (P z1) #- (S z2) = P (P (z1 #- z2)) (S z1) #- (P z2) = S (S (z1 #- z2)) Zero #- (P z2) = S (Zero #- z2) (P z1) #- (P z2) = z1 #- z2

type family (a :: Z) #* (b :: Z) :: Z where ... infixl 7 Source #

Multiply two integers

Equations

 Zero #* z = Zero (S z1) #* z2 = (z1 #* z2) #+ z2 (P z1) #* z2 = (z1 #* z2) #- z2

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

Divide two integers

Equations

 Zero #/ b = Zero a #/ (P b') = Negate (a #/ Negate (P b')) a #/ b = ZDiv b b a

type family Negate (z :: Z) :: Z where ... Source #

Negate an integer

Equations

 Negate Zero = Zero Negate (S z) = P (Negate z) Negate (P z) = S (Negate z)

## Synonyms for small numbers

type One = S Zero Source #

type Two = S One Source #

type Three = S Two Source #

type Five = S Four Source #

type MOne = P Zero Source #

type MTwo = P MOne Source #

## Term-level singletons

This is the singleton value representing Zero at the term level and at the type level, simultaneously. Used for raising units to powers.

sThree :: Sing (S (S (S Zero))) Source #

sFour :: Sing (S (S (S (S Zero)))) Source #

sFive :: Sing (S (S (S (S (S Zero))))) Source #

sMFour :: Sing (P (P (P (P Zero)))) Source #

sMFive :: Sing (P (P (P (P (P Zero))))) Source #

sSucc :: Sing z -> Sing (Succ z) Source #

Add one to a singleton Z.

sPred :: Sing z -> Sing (Pred z) Source #

Subtract one from a singleton Z.

sNegate :: Sing z -> Sing (Negate z) Source #

Negate a singleton Z.

## Deprecated synonyms for the ones above

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

pTwo :: Sing (S (S Zero)) Source #

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

pThree :: Sing (S (S (S Zero))) Source #

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

pFour :: Sing (S (S (S (S Zero)))) Source #

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

pFive :: Sing (S (S (S (S (S Zero))))) Source #

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

pMTwo :: Sing (P (P Zero)) Source #

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

pMThree :: Sing (P (P (P Zero))) Source #

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

pMFour :: Sing (P (P (P (P Zero)))) Source #

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

pMFive :: Sing (P (P (P (P (P Zero))))) Source #

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

pSucc :: Sing z -> Sing (Succ z) Source #

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

pPred :: Sing z -> Sing (Pred z) Source #

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

# Internal definitions

The following module is re-exported solely to prevent noise in error messages; we do not recommend trying to use these definitions in user code.