units-2.2: A domain-specific type system for dimensional analysis

Copyright(C) 2013 Richard Eisenberg
LicenseBSD-style (see LICENSE)
MaintainerRichard Eisenberg (eir@cis.upenn.edu)
Stabilityexperimental
Portabilitynon-portable
Safe HaskellNone
LanguageHaskell2010

Data.Metrology.Internal

Contents

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 :: * 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 map :: [Factor *] Source

Equations

LookupList [] lcsu = [] 
LookupList (F dim z : rest) lcsu = F (Lookup dim lcsu) z : LookupList rest lcsu 

Validity checking

type family ConvertibleLCSUs dfactors l1 l2 :: Constraint 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 lcsu unit 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 lcsu :: Constraint 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 *~ units2 :: Constraint 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 :: [*] Source

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 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 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 :: * Source

Helper function in CanonicalUnit

Equations

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

type family BaseHasConvRatio unit 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 UnitFactor units 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

UnitFactor ([] (Factor *)) 
(UnitFactor rest, Unit unit, SingI Z n) => UnitFactor ((:) (Factor *) (F * unit n) rest) 

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

UnitFactor ([] (Factor *)) 
(UnitFactor rest, Unit unit, SingI Z n) => UnitFactor ((:) (Factor *) (F * unit n) rest) 

type family a $= b :: Bool 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 lst :: ([Factor *], Maybe (Factor *)) 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 b :: [Factor *] 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 t :: [Factor *] 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 @~ b :: Constraint 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 *] 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 @@+ b :: [Factor *] 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 @+ b :: [Factor *] infixl 6 Source

Adds corresponding exponents in two dimension, preserving order

Equations

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

type family a @@- b :: [Factor *] 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 @- b :: [Factor *] infixl 6 Source

Subtract exponents in two dimensions

Equations

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

type family NegDim a :: Factor * Source

negate a single Factor

Equations

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

type family NegList a :: [Factor *] Source

negate a list of Factors

Equations

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

type family base @* power :: [Factor *] 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 @/ z :: [Factor *] 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

module Data.Metrology.Set

Dimensions