Numeric.Units.Dimensional.Dimensions.TypeLevel

This module defines type-level physical dimensions expressed in terms of the SI base dimensions using NumType for type-level integers.

Type-level arithmetic, synonyms for the base dimensions, and conversion to the term-level are included.

Kind of Type-Level Dimensions

data Dimension

Represents a physical dimension in the basis of the 7 SI base dimensions, where the respective dimensions are represented by type variables using the following convention:

• l: Length
• m: Mass
• t: Time
• i: Electric current
• th: Thermodynamic temperature
• n: Amount of substance
• j: Luminous intensity

For the equivalent term-level representation, see Dimension'

Constructors

Dim TypeInt TypeInt TypeInt TypeInt TypeInt TypeInt TypeInt

Instances

(KnownTypeInt l, KnownTypeInt m, KnownTypeInt t, KnownTypeInt i, KnownTypeInt th, KnownTypeInt n, KnownTypeInt j) => HasDimension (Proxy ('Dim l m t i th n j))

Defined in Numeric.Units.Dimensional.Dimensions.TypeLevel

Methods

dimension :: Proxy ('Dim l m t i th n j) -> Dimension'

(KnownTypeInt l, KnownTypeInt m, KnownTypeInt t, KnownTypeInt i, KnownTypeInt th, KnownTypeInt n, KnownTypeInt j) => HasDynamicDimension (Proxy ('Dim l m t i th n j))

Defined in Numeric.Units.Dimensional.Dimensions.TypeLevel

Methods

dynamicDimension :: Proxy ('Dim l m t i th n j) -> DynamicDimension

Dimension Arithmetic

type family (a :: Dimension) * (b :: Dimension) where ... infixl 7

Multiplication of dimensions corresponds to addition of the base dimensions' exponents.

Equations

DOne * d = d

d * DOne = d

('Dim l m t i th n j) * ('Dim l' m' t' i' th' n' j') = 'Dim (l + l') (m + m') (t + t') (i + i') (th + th') (n + n') (j + j')

type family (a :: Dimension) / (d :: Dimension) where ... infixl 7

Division of dimensions corresponds to subtraction of the base dimensions' exponents.

Equations

d / DOne = d

d / d = DOne

('Dim l m t i th n j) / ('Dim l' m' t' i' th' n' j') = 'Dim (l - l') (m - m') (t - t') (i - i') (th - th') (n - n') (j - j')

type family (d :: Dimension) ^ (x :: TypeInt) where ... infixr 8

Powers of dimensions correspond to multiplication of the base dimensions' exponents by the exponent.

We limit ourselves to integer powers of Dimensionals as fractional powers make little physical sense.

Equations

DOne ^ x = DOne

d ^ 'Zero = DOne

d ^ 'Pos1 = d

('Dim l m t i th n j) ^ x = 'Dim (l * x) (m * x) (t * x) (i * x) (th * x) (n * x) (j * x)

type Recip (d :: Dimension) = DOne / d

The reciprocal of a dimension is defined as the result of dividing DOne by it, or of negating each of the base dimensions' exponents.

type family NRoot (d :: Dimension) (x :: TypeInt) where ...

Roots of dimensions correspond to division of the base dimensions' exponents by the order of the root.

Equations

NRoot DOne x = DOne

NRoot d 'Pos1 = d

NRoot ('Dim l m t i th n j) x = 'Dim (l / x) (m / x) (t / x) (i / x) (th / x) (n / x) (j / x)

type Sqrt d = NRoot d 'Pos2

Square root is a special case of NRoot with order 2.

type Cbrt d = NRoot d 'Pos3

Cube root is a special case of NRoot with order 3.

Synonyms for Base Dimensions

type DOne = 'Dim 'Zero 'Zero 'Zero 'Zero 'Zero 'Zero 'Zero

The type-level dimension of dimensionless values.

type DLength = 'Dim 'Pos1 'Zero 'Zero 'Zero 'Zero 'Zero 'Zero

type DMass = 'Dim 'Zero 'Pos1 'Zero 'Zero 'Zero 'Zero 'Zero

type DTime = 'Dim 'Zero 'Zero 'Pos1 'Zero 'Zero 'Zero 'Zero

type DElectricCurrent = 'Dim 'Zero 'Zero 'Zero 'Pos1 'Zero 'Zero 'Zero

type DThermodynamicTemperature = 'Dim 'Zero 'Zero 'Zero 'Zero 'Pos1 'Zero 'Zero

type DAmountOfSubstance = 'Dim 'Zero 'Zero 'Zero 'Zero 'Zero 'Pos1 'Zero

type DLuminousIntensity = 'Dim 'Zero 'Zero 'Zero 'Zero 'Zero 'Zero 'Pos1

Conversion to Term Level

type KnownDimension (d :: Dimension) = HasDimension (Proxy d)

A KnownDimension is one for which we can construct a term-level representation. Each validly constructed type of kind Dimension has a KnownDimension instance.

While KnownDimension is a constraint synonym, the presence of KnownDimension d in a context allows use of dimension :: Proxy d -> Dimension'.