Moduledimensional-1.5Haskell2010

Numeric.Units.Dimensional.Dimensions.TypeLevel

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

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

13 types
MonoLocalBinds
ScopedTypeVariables
TypeFamilies
ConstraintKinds
DataKinds
TypeSynonymInstances
FlexibleContexts
FlexibleInstances
KindSignatures
TypeOperators
ExplicitNamespaces
ExplicitForAll

Packagedimensional-1.5
Exports17
LanguageHaskell2010
LicenceBSD-3-Clause
SourceTypeLevel.hs

Kind of Type-Level Dimensions

1 declaration

datadata 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

Instances2HasDimension, HasDynamicDimension

(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 dimensional-1.5 · Numeric.Units.Dimensional.Dimensions.TypeLevel
(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 dimensional-1.5 · Numeric.Units.Dimensional.Dimensions.TypeLevel

Dimension Arithmetic

7 declarations

familytype family (*) (a :: Dimension) (b :: Dimension) :: Dimension where

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

familytype family (/) (a :: Dimension) (d :: Dimension) :: Dimension where

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

familytype family (^) (d :: Dimension) (x :: TypeInt) :: Dimension where

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)

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

familytype family NRoot (d :: Dimension) (x :: TypeInt) :: Dimension 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)

typetype Sqrt (d :: Dimension) = NRoot d 'Pos2

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

typetype Cbrt (d :: Dimension) = NRoot d 'Pos3

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

Synonyms for Base Dimensions

8 declarations

typetype DOne = 'Dim 'Zero 'Zero 'Zero 'Zero 'Zero 'Zero 'Zero

The type-level dimension of dimensionless values.

typetype DLength = 'Dim 'Pos1 'Zero 'Zero 'Zero 'Zero 'Zero 'Zero

typetype DMass = 'Dim 'Zero 'Pos1 'Zero 'Zero 'Zero 'Zero 'Zero

typetype DTime = 'Dim 'Zero 'Zero 'Pos1 'Zero 'Zero 'Zero 'Zero

typetype DElectricCurrent = 'Dim 'Zero 'Zero 'Zero 'Pos1 'Zero 'Zero 'Zero

typetype DThermodynamicTemperature = 'Dim 'Zero 'Zero 'Zero 'Zero 'Pos1 'Zero 'Zero

typetype DAmountOfSubstance = 'Dim 'Zero 'Zero 'Zero 'Zero 'Zero 'Pos1 'Zero

typetype DLuminousIntensity = 'Dim 'Zero 'Zero 'Zero 'Zero 'Zero 'Zero 'Pos1

Conversion to Term Level

1 declaration

typetype 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'.