units-2.4.1.4: A domain-specific type system for dimensional analysis
Copyright(C) 2013 Richard Eisenberg
LicenseBSD-style (see LICENSE)
MaintainerRichard Eisenberg (rae@cs.brynmawr.edu)
Stabilityexperimental
Portabilitynon-portable
Safe HaskellNone
LanguageHaskell2010

Data.Metrology.Internal

Description

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.

Synopsis

LCSU lookup

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

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

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

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

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

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

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

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

Manipulating units

type family DimOfUnitIsConsistent unit :: Constraint where ... Source #

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

Is this unit a canonical unit?

Equations

IsCanonical unit = BaseUnit unit == Canonical 

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

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

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

Helper function in CanonicalUnit

Equations

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

type family BaseHasConvRatio unit where ... Source #

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 *]) Source #

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

Minimal complete definition

canonicalConvRatioSpec

Instances

Instances details
UnitFactor ('[] :: [Factor Type]) Source # 
Instance details

Defined in Data.Metrology.Units

(UnitFactor rest, Unit unit, SingI n) => UnitFactor ('F unit n ': rest) Source # 
Instance details

Defined in Data.Metrology.Units

Methods

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

type family UnitFactorsOf unit :: [Factor *] Source #

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

Instances

Instances details
type UnitFactorsOf Number Source # 
Instance details

Defined in Data.Metrology.Units

type UnitFactorsOf (prefix :@ unit) Source # 
Instance details

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) Source # 
Instance details

Defined in Data.Metrology.Combinators

type UnitFactorsOf (unit :^ power) = Normalize (UnitFactorsOf unit @* power)
type UnitFactorsOf (u1 :/ u2) Source # 
Instance details

Defined in Data.Metrology.Combinators

type UnitFactorsOf (u1 :* u2) Source # 
Instance details

Defined in Data.Metrology.Combinators

Maniuplating dimension specifications

data Factor star Source #

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

Constructors

F star Z 

Instances

Instances details
UnitFactor ('[] :: [Factor Type]) Source # 
Instance details

Defined in Data.Metrology.Units

Read n => Read (Qu ('[] :: [Factor Type]) l n) Source # 
Instance details

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) Source # 
Instance details

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) Source # 
Instance details

Defined in Data.Metrology.Units

Methods

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

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

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

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

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

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

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

Equations

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

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

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

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

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

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

Subtract exponents in two dimensions

Equations

a @- a = '[] 
a @- b = a @@- Reorder b a 

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

negate a single Factor

Equations

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

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

negate a list of Factors

Equations

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

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

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

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

Dimensions

type family DimFactorsOf dim :: [Factor *] Source #

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

Instances

Instances details
type DimFactorsOf Dimensionless Source # 
Instance details

Defined in Data.Metrology.Units

type DimFactorsOf (dim :^ power) Source # 
Instance details

Defined in Data.Metrology.Combinators

type DimFactorsOf (dim :^ power) = Normalize (DimFactorsOf dim @* power)
type DimFactorsOf (d1 :/ d2) Source # 
Instance details

Defined in Data.Metrology.Combinators

type DimFactorsOf (d1 :* d2) Source # 
Instance details

Defined in Data.Metrology.Combinators