Data.Metrology.Internal

This file gathers and exports user-visible type-level definitions, to make error messages less cluttered. Non-expert users should never have to use the definitions exported from this module.

LCSU lookup

type family Lookup (dim :: *) (lcsu :: LCSU *) :: * where ...

Equations

Lookup dim (MkLCSU_ ('(dim, unit) ': rest)) = unit

Lookup dim (MkLCSU_ ('(other, u) ': rest)) = Lookup dim (MkLCSU_ rest)

Lookup dim DefaultLCSU = DefaultUnitOfDim dim

type family LookupList (keys :: [Factor *]) (map :: LCSU *) :: [Factor *] where ...

Equations

LookupList '[] lcsu = '[]

LookupList (F dim z ': rest) lcsu = F (Lookup dim lcsu) z ': LookupList rest lcsu

Validity checking

type family ConvertibleLCSUs (dfactors :: [Factor *]) (l1 :: LCSU *) (l2 :: LCSU *) :: Constraint where ...

Are two LCSUs inter-convertible at the given dimension?

Equations

ConvertibleLCSUs dfactors l1 l2 = (LookupList dfactors l1 *~ LookupList dfactors l2, ValidDL dfactors l1, ValidDL dfactors l2, UnitFactor (LookupList dfactors l1), UnitFactor (LookupList dfactors l2))

type family ValidDLU (dfactors :: [Factor *]) (lcsu :: LCSU *) (unit :: *) where ...

Check if a (dimension factors, LCSU, unit) triple are all valid to be used together.

Equations

ValidDLU dfactors lcsu unit = (dfactors ~ DimFactorsOf (DimOfUnit unit), UnitFactor (LookupList dfactors lcsu), Unit unit, UnitFactorsOf unit *~ LookupList dfactors lcsu)

type family ValidDL (dfactors :: [Factor *]) (lcsu :: LCSU *) :: Constraint where ...

Check if a (dimension factors, LCSU) pair are valid to be used together. This checks that each dimension maps to a unit of the correct dimension.

Equations

ValidDL dfactors lcsu = ValidDLU dfactors lcsu (UnitOfDimFactors dfactors lcsu)

type family (units1 :: [Factor *]) *~ (units2 :: [Factor *]) :: Constraint where ... infix 4

Check if two [Factor *]s, representing units, should be considered to be equal

Equations

units1 *~ units2 = CanonicalUnitsOfFactors units1 `SetEqual` CanonicalUnitsOfFactors units2

type family CanonicalUnitsOfFactors (fs :: [Factor *]) :: [*] where ...

Given a list of unit factors, extract out the canonical units they are based on.

Equations

CanonicalUnitsOfFactors '[] = '[]

CanonicalUnitsOfFactors (F u z ': fs) = CanonicalUnit u ': CanonicalUnitsOfFactors fs

Manipulating units

type family DimOfUnitIsConsistent unit :: Constraint where ...

Check to make sure that a unit has the same dimension as its base unit, if any.

Equations

DimOfUnitIsConsistent unit = (Dimension (DimOfUnit unit), If (BaseUnit unit == Canonical) (() :: Constraint) (DimOfUnit unit ~ DimOfUnit (BaseUnit unit)))

type family IsCanonical (unit :: *) where ...

Is this unit a canonical unit?

Equations

IsCanonical unit = BaseUnit unit == Canonical

type CanonicalUnit (unit :: *) = CanonicalUnit' (BaseUnit unit) unit

Get the canonical unit from a given unit. For example: CanonicalUnit Foot = Meter

type family CanonicalUnit' (base_unit :: *) (unit :: *) :: * where ...

Helper function in CanonicalUnit

Equations

CanonicalUnit' Canonical unit = unit

CanonicalUnit' base unit = CanonicalUnit' (BaseUnit base) base

type family BaseHasConvRatio unit where ...

Essentially, a constraint that checks if a conversion ratio can be calculated for a BaseUnit of a unit.

Equations

BaseHasConvRatio unit = HasConvRatio (IsCanonical unit) unit

class Units units => UnitFactor (units :: [Factor *])

Classifies well-formed list of unit factors, and permits calculating a conversion ratio for the purposes of LCSU conversions.

Minimal complete definition

canonicalConvRatioSpec

Instances

UnitFactor ('[] :: [Factor Type])

Defined in Data.Metrology.Units

Methods

canonicalConvRatioSpec :: Proxy '[] -> Rational

(UnitFactor rest, Unit unit, SingI n) => UnitFactor ('F unit n ': rest)

Defined in Data.Metrology.Units

Methods

canonicalConvRatioSpec :: Proxy ('F unit n ': rest) -> Rational

type family UnitFactorsOf unit :: [Factor *]

The internal list of canonical units corresponding to this unit. Overriding the default should not be necessary in user code.

Instances

type UnitFactorsOf Number

Defined in Data.Metrology.Units

type UnitFactorsOf Number = '[] :: [Factor Type]

type UnitFactorsOf (prefix :@ unit)

Defined in Data.Metrology.Combinators

type UnitFactorsOf (prefix :@ unit) = If (IsCanonical (prefix :@ unit)) '['F (prefix :@ unit) One] (UnitFactorsOf (BaseUnit (prefix :@ unit)))

type UnitFactorsOf (unit :^ power)

Defined in Data.Metrology.Combinators

type UnitFactorsOf (unit :^ power) = Normalize (UnitFactorsOf unit @* power)

type UnitFactorsOf (u1 :/ u2)

Defined in Data.Metrology.Combinators

type UnitFactorsOf (u1 :/ u2) = Normalize (UnitFactorsOf u1 @- UnitFactorsOf u2)

type UnitFactorsOf (u1 :* u2)

Defined in Data.Metrology.Combinators

type UnitFactorsOf (u1 :* u2) = Normalize (UnitFactorsOf u1 @+ UnitFactorsOf u2)

Maniuplating dimension specifications

data Factor star

This will only be used at the kind level. It holds a dimension or unit with its exponent.

Constructors

F star Z

Instances

UnitFactor ('[] :: [Factor Type])

Defined in Data.Metrology.Units

Methods

canonicalConvRatioSpec :: Proxy '[] -> Rational

Read n => Read (Qu ('[] :: [Factor Type]) l n)

Defined in Data.Metrology.Qu

Methods

readsPrec :: Int -> ReadS (Qu '[] l n)

readList :: ReadS [Qu '[] l n]

readPrec :: ReadPrec (Qu '[] l n)

readListPrec :: ReadPrec [Qu '[] l n]

Show n => Show (Qu ('[] :: [Factor Type]) l n)

Defined in Data.Metrology.Qu

Methods

showsPrec :: Int -> Qu '[] l n -> ShowS

show :: Qu '[] l n -> String

showList :: [Qu '[] l n] -> ShowS

(UnitFactor rest, Unit unit, SingI n) => UnitFactor ('F unit n ': rest)

Defined in Data.Metrology.Units

Methods

canonicalConvRatioSpec :: Proxy ('F unit n ': rest) -> Rational

type family (a :: Factor *) $= (b :: Factor *) :: Bool where ... infix 4

Do these Factors represent the same dimension?

Equations

(F n1 z1) $= (F n2 z2) = n1 == n2

a $= b = False

type family Extract (s :: Factor *) (lst :: [Factor *]) :: ([Factor *], Maybe (Factor *)) where ...

(Extract s lst) pulls the Factor that matches s out of lst, returning a diminished list and, possibly, the extracted Factor.

Extract A [A, B, C] ==> ([B, C], Just A
Extract F [A, B, C] ==> ([A, B, C], Nothing)

Equations

Extract s '[] = '('[], Nothing)

Extract s (h ': t) = If (s $= h) '(t, Just h) '(h ': Fst (Extract s t), Snd (Extract s t))

type family Reorder (a :: [Factor *]) (b :: [Factor *]) :: [Factor *] where ...

Reorders a to be the in the same order as b, putting entries not in b at the end

Reorder [A 1, B 2] [B 5, A 2] ==> [B 2, A 1]
Reorder [A 1, B 2, C 3] [C 2, A 8] ==> [C 3, A 1, B 2]
Reorder [A 1, B 2] [B 4, C 1, A 9] ==> [B 2, A 1]
Reorder x x ==> x
Reorder x [] ==> x
Reorder [] x ==> []

Equations

Reorder x x = x

Reorder '[] x = '[]

Reorder '[x] y = '[x]

Reorder x '[] = x

Reorder x (h ': t) = Reorder' (Extract h x) t

type family Reorder' (scrut :: ([Factor *], Maybe (Factor *))) (t :: [Factor *]) :: [Factor *] where ...

Helper function in Reorder

Equations

Reorder' '(lst, Nothing) t = Reorder lst t

Reorder' '(lst, Just elt) t = elt ': Reorder lst t

type family (a :: [Factor *]) @~ (b :: [Factor *]) :: Constraint where ... infix 4

Check if two [Factor *]s should be considered to be equal

Equations

a @~ b = Normalize (a @- b) ~ '[]

type family Normalize (d :: [Factor *]) :: [Factor *] where ...

Take a [Factor *] and remove any Factors with an exponent of 0

Equations

Normalize '[] = '[]

Normalize (F n Zero ': t) = Normalize t

Normalize (h ': t) = h ': Normalize t

type family (a :: [Factor *]) @@+ (b :: [Factor *]) :: [Factor *] where ... infixl 6

Adds corresponding exponents in two dimension, assuming the lists are ordered similarly.

Equations

'[] @@+ b = b

a @@+ '[] = a

(F name z1 ': t1) @@+ (F name z2 ': t2) = F name (z1 #+ z2) ': (t1 @@+ t2)

(h ': t) @@+ b = h ': (t @@+ b)

type family (a :: [Factor *]) @+ (b :: [Factor *]) :: [Factor *] where ... infixl 6

Adds corresponding exponents in two dimension, preserving order

Equations

a @+ b = a @@+ Reorder b a

type family (a :: [Factor *]) @@- (b :: [Factor *]) :: [Factor *] where ... infixl 6

Subtract exponents in two dimensions, assuming the lists are ordered similarly.

Equations

'[] @@- b = NegList b

a @@- '[] = a

(F name z1 ': t1) @@- (F name z2 ': t2) = F name (z1 #- z2) ': (t1 @@- t2)

(h ': t) @@- b = h ': (t @@- b)

type family (a :: [Factor *]) @- (b :: [Factor *]) :: [Factor *] where ... infixl 6

Subtract exponents in two dimensions

Equations

a @- a = '[]

a @- b = a @@- Reorder b a

type family NegDim (a :: Factor *) :: Factor * where ...

negate a single Factor

Equations

NegDim (F n z) = F n (Negate z)

type family NegList (a :: [Factor *]) :: [Factor *] where ...

negate a list of Factors

Equations

NegList '[] = '[]

NegList (h ': t) = NegDim h ': NegList t

type family (base :: [Factor *]) @* (power :: Z) :: [Factor *] where ... infixl 7

Multiplication of the exponents in a dimension by a scalar

Equations

'[] @* power = '[]

(F name num ': t) @* power = F name (num #* power) ': (t @* power)

type family (dims :: [Factor *]) @/ (z :: Z) :: [Factor *] where ... infixl 7

Division of the exponents in a dimension by a scalar

Equations

'[] @/ z = '[]

(F name num ': t) @/ z = F name (num #/ z) ': (t @/ z)

Set operations on lists

module Data.Metrology.Set

Dimensions

type family DimFactorsOf dim :: [Factor *]

Retrieve a list of Factors representing the given dimension. Overriding the default of this type family should not be necessary in user code.

Instances

type DimFactorsOf Dimensionless

Defined in Data.Metrology.Units

type DimFactorsOf Dimensionless = '[] :: [Factor Type]

type DimFactorsOf (dim :^ power)

Defined in Data.Metrology.Combinators

type DimFactorsOf (dim :^ power) = Normalize (DimFactorsOf dim @* power)

type DimFactorsOf (d1 :/ d2)

Defined in Data.Metrology.Combinators

type DimFactorsOf (d1 :/ d2) = Normalize (DimFactorsOf d1 @- DimFactorsOf d2)

type DimFactorsOf (d1 :* d2)

Defined in Data.Metrology.Combinators

type DimFactorsOf (d1 :* d2) = Normalize (DimFactorsOf d1 @+ DimFactorsOf d2)