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

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