dimensional-1.3: Statically checked physical dimensions, using Type Families and Data Kinds.

Copyright | Copyright (C) 2006-2018 Bjorn Buckwalter
License | BSD3
Maintainer | bjorn@buckwalter.se
Stability | Stable
Portability | GHC only
Safe Haskell | Safe
Language | Haskell2010

Extensions

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

Numeric.Units.Dimensional.Dimensions.TypeLevel

Contents

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

Description

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.

Synopsis

- data Dimension = Dim TypeInt TypeInt TypeInt TypeInt TypeInt TypeInt TypeInt
- type family (a :: Dimension) * (b :: Dimension) where ...
- type family (a :: Dimension) / (d :: Dimension) where ...
- type family (d :: Dimension) ^ (x :: TypeInt) where ...
- type Recip (d :: Dimension) = DOne / d
- type family NRoot (d :: Dimension) (x :: TypeInt) where ...
- type Sqrt d = NRoot d 'Pos2
- type Cbrt d = NRoot d 'Pos3
- type DOne = 'Dim 'Zero 'Zero 'Zero 'Zero 'Zero 'Zero 'Zero
- 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
- type KnownDimension (d :: Dimension) = HasDimension (Proxy d)

# Kind of Type-Level Dimensions

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

#### Instances

Instances details

(KnownTypeInt l, KnownTypeInt m, KnownTypeInt t, KnownTypeInt i, KnownTypeInt th, KnownTypeInt n, KnownTypeInt j) => HasDimension (Proxy ('Dim l m t i th n j)) Source # |
Instance details Defined in Numeric.Units.Dimensional.Dimensions.TypeLevel Methods dimension :: Proxy ('Dim l m t i th n j) -> Dimension' Source #
(KnownTypeInt l, KnownTypeInt m, KnownTypeInt t, KnownTypeInt i, KnownTypeInt th, KnownTypeInt n, KnownTypeInt j) => HasDynamicDimension (Proxy ('Dim l m t i th n j)) Source # |
Instance details Defined in Numeric.Units.Dimensional.Dimensions.TypeLevel Methods dynamicDimension :: Proxy ('Dim l m t i th n j) -> DynamicDimension Source #

# Dimension Arithmetic

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

Multiplication of dimensions corresponds to adding 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 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') |

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

Powers of dimensions corresponds 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 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.

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

Roots of dimensions corresponds 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 Source #

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

type Cbrt d = NRoot d 'Pos3 Source #

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 Source #

The type-level dimension of dimensionless values.

type DLength = 'Dim 'Pos1 'Zero 'Zero 'Zero 'Zero 'Zero 'Zero Source #

type DMass = 'Dim 'Zero 'Pos1 'Zero 'Zero 'Zero 'Zero 'Zero Source #

type DTime = 'Dim 'Zero 'Zero 'Pos1 'Zero 'Zero 'Zero 'Zero Source #

type DElectricCurrent = 'Dim 'Zero 'Zero 'Zero 'Pos1 'Zero 'Zero 'Zero Source #

type DThermodynamicTemperature = 'Dim 'Zero 'Zero 'Zero 'Zero 'Pos1 'Zero 'Zero Source #

type DAmountOfSubstance = 'Dim 'Zero 'Zero 'Zero 'Zero 'Zero 'Pos1 'Zero Source #

type DLuminousIntensity = 'Dim 'Zero 'Zero 'Zero 'Zero 'Zero 'Zero 'Pos1 Source #

# Conversion to Term Level

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