Data.Metrology

The units package is a framework for strongly-typed dimensional analysis. This haddock documentation is generally not enough to be able to use this package effectively. Please see the readme at http://www.cis.upenn.edu/~eir/packages/units/README.html.

Some of the types below refer to declarations that are not exported and not documented here. This is because Haddock does not allow finely-tuned abstraction in documentation. (In particular, right-hand sides of type synonym declarations are always included.) If a symbol is not exported, you do not need to know anything about it to use this package.

Though it doesn't appear here, Scalar is an instance of Num, and generally has all the numeric instances that Double has.

Term-level combinators

The term-level arithmetic operators are defined by applying vertical bar(s) to the sides the dimensioned quantities acts on. See also Data.Metrology.AltOperators for an alternative system of operators.

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

Add two compatible quantities

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

Subtract two compatible quantities

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

Multiply two quantities

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

Divide two quantities

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

Multiply a quantity by a scalar from the left

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

Multiply a quantity by a scalar from the right

(/|) :: Fractional n => n -> Qu b l n -> Qu (NegList b) l n infixl 7

Divide a scalar by a quantity

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

Divide a quantity by a scalar

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

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

Raise a quantity to a integer power known at compile time

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

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

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

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

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

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

Check if two quantities are not equal

qApprox infix 4

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 the epsilon, they are considered equal.

qNapprox infix 4

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

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

Square a quantity

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

Cube a quantity

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

Take the square root of a quantity

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

Take the cubic root of a quantity

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

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

Nondimensional units, conversion between quantities and numeric values

unity :: Num n => Qu [] l n

The number 1, expressed as a unitless dimensioned quantity.

zero :: Num n => Qu dimspec l n

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

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

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

Dimension-keeping cast between different CSUs.

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

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

Infix synonym for numIn

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

Like '#', but uses a default LCSU. This operator is recommended for users who wish not to worry about LCSUs.

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

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

Infix synonym for quOf

(%%) :: (ValidDLU dim DefaultLCSU unit, Fractional n) => n -> unit -> Qu dim DefaultLCSU n infixr 9

Like %, but uses a default LCSU. This operator is recommended for users who wish not to worry about LCSUs.

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

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

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

Compute the argument in the DefaultLCSU, and present the result as lcsu-polymorphic dimension-polymorphic value.

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

A synonym of fromDefaultLCSU, for one of its dominant usecase is to inject constant quantities into dimension-polymorphic expressions.

Type-level unit combinators

data u1 :* u2 infixl 7

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)

(Dimension d1, Dimension d2) => Dimension ((:*) d1 d2)

(Unit u1, Unit u2) => Unit ((:*) u1 u2)

type DefaultUnitOfDim ((:*) d1 d2) = (:*) (DefaultUnitOfDim d1) (DefaultUnitOfDim d2)

type DimFactorsOf ((:*) d1 d2) = (@+) (DimFactorsOf d1) (DimFactorsOf d2)

type BaseUnit ((:*) u1 u2) = Canonical

type DimOfUnit ((:*) u1 u2) = (:*) (DimOfUnit u1) (DimOfUnit u2)

type UnitFactorsOf ((:*) u1 u2) = (@+) (UnitFactorsOf u1) (UnitFactorsOf u2)

data u1 :/ u2 infixl 7

Divide two units to get another unit

Constructors

u1 :/ u2 infixl 7

Instances

(Show u1, Show u2) => Show ((:/) u1 u2)

(Dimension d1, Dimension d2) => Dimension ((:/) d1 d2)

(Unit u1, Unit u2) => Unit ((:/) u1 u2)

type DefaultUnitOfDim ((:/) d1 d2) = (:/) (DefaultUnitOfDim d1) (DefaultUnitOfDim d2)

type DimFactorsOf ((:/) d1 d2) = (@-) (DimFactorsOf d1) (DimFactorsOf d2)

type BaseUnit ((:/) u1 u2) = Canonical

type DimOfUnit ((:/) u1 u2) = (:/) (DimOfUnit u1) (DimOfUnit u2)

type UnitFactorsOf ((:/) u1 u2) = (@-) (UnitFactorsOf u1) (UnitFactorsOf u2)

data unit :^ power infixr 8

Raise a unit to a power, known at compile time

Constructors

unit :^ (Sing power) infixr 8

Instances

(Show u1, SingI Z power) => Show ((:^) u1 power)

Dimension dim => Dimension ((:^) dim power)

(Unit unit, SingI Z power) => Unit ((:^) unit power)

type DefaultUnitOfDim ((:^) d z) = (:^) (DefaultUnitOfDim d) z

type DimFactorsOf ((:^) dim power) = (@*) (DimFactorsOf dim) power

type BaseUnit ((:^) unit power) = Canonical

type DimOfUnit ((:^) unit power) = (:^) (DimOfUnit unit) power

type UnitFactorsOf ((:^) unit power) = (@*) (UnitFactorsOf unit) power

data prefix :@ unit infixr 9

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

Constructors

prefix :@ unit infixr 9

Instances

(Show prefix, Show unit) => Show ((:@) prefix unit)

((~) Bool ((==) * unit Canonical) False, Unit unit, UnitPrefix prefix) => Unit ((:@) prefix unit)

type BaseUnit ((:@) prefix unit) = unit

type DimOfUnit ((:@) prefix unit) = DimOfUnit (BaseUnit ((:@) prefix unit))

type UnitFactorsOf ((:@) prefix unit) = If [Factor *] (IsCanonical ((:@) prefix unit)) ((:) (Factor *) (F * ((:@) prefix unit) One) ([] (Factor *))) (UnitFactorsOf (BaseUnit ((:@) prefix unit)))

class UnitPrefix prefix where

A class for user-defined prefixes

Methods

multiplier :: Fractional f => prefix -> f

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

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) = Qu ((@+) d1 d2) l n

type family d1 %/ d2 :: * infixl 7

Divide two quantity types to produce a new one

Instances

type (Qu d1 l n) %/ (Qu d2 l n) = Qu ((@-) d1 d2) l n

type family d %^ z :: * infixr 8

Exponentiate a quantity type to an integer

Instances

type (Qu d l n) %^ z = Qu ((@*) d z) l n

Creating quantity types

data Qu a lcsu n

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

Instances

Eq n => Eq (Qu ([] (Factor *)) l n)

Floating n => Floating (Qu ([] (Factor *)) l n)

Fractional n => Fractional (Qu ([] (Factor *)) l n)

Num n => Num (Qu ([] (Factor *)) l n)

Ord n => Ord (Qu ([] (Factor *)) l n)

Real n => Real (Qu ([] (Factor *)) l n)

RealFloat n => RealFloat (Qu ([] (Factor *)) l n)

RealFrac n => RealFrac (Qu ([] (Factor *)) l n)

(ShowUnitFactor (LookupList dims lcsu), Show n) => Show (Qu dims lcsu n)

type (Qu d l n) %^ z = Qu ((@*) d z) l n

type (Qu d1 l n) %/ (Qu d2 l n) = Qu ((@-) d1 d2) l n

type (Qu d1 l n) %* (Qu d2 l n) = Qu ((@+) d1 d2) l n

type MkQu_D dim = Qu (DimFactorsOf dim) DefaultLCSU Double

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)

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

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

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

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

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

Associated Types

type DimFactorsOf dim :: [Factor *]

Retrieve a list of Factors representing the given dimension. Overriding the default of this type family should not be necessary in user code.

Instances

Dimension Dimensionless

Dimension dim => Dimension ((:^) dim power)

(Dimension d1, Dimension d2) => Dimension ((:/) d1 d2)

(Dimension d1, Dimension d2) => Dimension ((:*) d1 d2)

Creating new units

class DimOfUnitIsConsistent unit => Unit unit where

Minimal complete definition

Nothing

Associated Types

type BaseUnit unit :: *

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

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.

type UnitFactorsOf unit :: [Factor *]

The internal list of canonical units corresponding to this unit. Overriding the default should not be necessary in user code.

Methods

conversionRatio :: unit -> Rational

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

Unit Number

((~) Bool ((==) * unit Canonical) False, Unit unit, UnitPrefix prefix) => Unit ((:@) prefix unit)

(Unit unit, SingI Z power) => Unit ((:^) unit power)

(Unit u1, Unit u2) => Unit ((:/) u1 u2)

(Unit u1, Unit u2) => Unit ((:*) u1 u2)

data Canonical

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

Scalars, the only built-in unit

data Dimensionless

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

Dimension Dimensionless

type DefaultUnitOfDim Dimensionless = Number

type DimFactorsOf Dimensionless = [] (Factor *)

data Number

The unit for unitless dimensioned quantities

Constructors

Number

Instances

Unit Number

type BaseUnit Number = Canonical

type DimOfUnit Number = Dimensionless

type UnitFactorsOf Number = [] (Factor *)

type Scalar = MkQu_U Number

The type of unitless dimensioned quantities. This is an instance of Num, though Haddock doesn't show it. This uses a Double internally and uses a default LCSU.

scalar :: n -> Qu [] l n

Convert a raw number into a unitless dimensioned quantity

LCSUs (locally coherent system of units)

type family MkLCSU pairs

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

Constructors

DefaultLCSU

type family DefaultUnitOfDim dim :: *

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

Instances

type DefaultUnitOfDim Dimensionless = Number

type DefaultUnitOfDim ((:^) d z) = (:^) (DefaultUnitOfDim d) z

type DefaultUnitOfDim ((:/) d1 d2) = (:/) (DefaultUnitOfDim d1) (DefaultUnitOfDim d2)

type DefaultUnitOfDim ((:*) d1 d2) = (:*) (DefaultUnitOfDim d1) (DefaultUnitOfDim d2)

Validity checks and assertions

type family CompatibleUnit lcsu unit :: Constraint

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 dim :: Constraint

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 l2 :: Constraint

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

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

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

data Z

The datatype for type-level integers.

Constructors

Zero

S Z

P Z

Instances

Eq Z

SingI Z Zero

SEq Z (KProxy Z)

SDecide Z (KProxy Z)

SingI Z n0 => SingI Z (P n)

SingI Z n0 => SingI Z (S n)

SingKind Z (KProxy Z)

data Sing Z where

• SZero :: (~) Z z Zero => Sing Z z
• SS :: (~) Z z (S n) => Sing Z n -> Sing Z z
• SP :: (~) Z z (P n) => Sing Z n -> Sing Z z

type (==) Z a0 b0 = Equals_1627415457 a0 b0

type DemoteRep Z (KProxy Z) = Z

type family Succ z :: Z

Add one to an integer

Equations

Succ Zero = S Zero

Succ (P z) = z

Succ (S z) = S (S z)

type family Pred z :: Z

Subtract one from an integer

Equations

Pred Zero = P Zero

Pred (P z) = P (P z)

Pred (S z) = z

type family a #+ b :: Z infixl 6

Add two integers

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 #- b :: Z infixl 6

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 #* b :: Z infixl 7

Multiply two integers

Equations

Zero #* z = Zero

(S z1) #* z2 = (z1 #* z2) #+ z2

(P z1) #* z2 = (z1 #* z2) #- z2

type family a #/ b :: Z

Divide two integers

Equations

Zero #/ b = Zero

a #/ (P b') = NegZ (a #/ NegZ (P b'))

a #/ b = ZDiv b b a

type family NegZ z :: Z

Negate an integer

Equations

NegZ Zero = Zero

NegZ (S z) = P (NegZ z)

NegZ (P z) = S (NegZ z)

Synonyms for small numbers

type One = S Zero

type Two = S One

type Three = S Two

type Four = S Three

type Five = S Four

type MOne = P Zero

type MTwo = P MOne

type MThree = P MTwo

type MFour = P MThree

type MFive = P MFour

Term-level singletons

pZero :: Sing Z Zero

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

pOne :: Sing Z (S Zero)

pTwo :: Sing Z (S (S Zero))

pThree :: Sing Z (S (S (S Zero)))

pFour :: Sing Z (S (S (S (S Zero))))

pFive :: Sing Z (S (S (S (S (S Zero)))))

pMOne :: Sing Z (P Zero)

pMTwo :: Sing Z (P (P Zero))

pMThree :: Sing Z (P (P (P Zero)))

pMFour :: Sing Z (P (P (P (P Zero))))

pMFive :: Sing Z (P (P (P (P (P Zero)))))

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

Add one to a singleton Z.

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

Subtract one from a singleton Z.

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.

module Data.Metrology.Internal