Moduledimensional-1.6.2Haskell2010

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.

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

Contents

Kind of Type-Level Dimensions
Dimension Arithmetic
Synonyms for Base Dimensions
Conversion to Term Level

Synopsis

data Dimension
family *
family /
family ^
type Recip
family NRoot
type Sqrt
type Cbrt
type DOne
type DLength
type DMass
type DTime
type DElectricCurrent
type DThermodynamicTemperature
type DAmountOfSubstance
type DLuminousIntensity
type KnownDimension

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

Kind of Type-Level Dimensions

datadata Dimension

Source#

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.6.2 · 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.6.2 · Numeric.Units.Dimensional.Dimensions.TypeLevel

Dimension Arithmetic

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

Source#

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

Source#

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

Source#

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

Source#

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

Source#

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

Source#

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

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

Source#

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

Synonyms for Base Dimensions

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

Source#

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

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

Source#

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