units 1.1 → 2.0
raw patch · 29 files changed
+1633/−1468 lines, 29 filesdep +unitsdep ~basedep ~singletons
Dependencies added: units
Dependency ranges changed: base, singletons
Files
- Data/Dimensions.hs +0/−145
- Data/Dimensions/Dim.hs +0/−149
- Data/Dimensions/DimSpec.hs +0/−166
- Data/Dimensions/Poly.hs +0/−41
- Data/Dimensions/SI.hs +0/−29
- Data/Dimensions/SI/Prefixes.hs +0/−217
- Data/Dimensions/SI/Types.hs +0/−59
- Data/Dimensions/SI/Units.hs +0/−179
- Data/Dimensions/Show.hs +0/−73
- Data/Dimensions/UnitCombinators.hs +0/−72
- Data/Dimensions/Units.hs +0/−112
- Data/Dimensions/Unsafe.hs +0/−22
- Data/Dimensions/Z.hs +0/−148
- Data/Metrology.hs +266/−0
- Data/Metrology/Combinators.hs +97/−0
- Data/Metrology/Dimensions.hs +34/−0
- Data/Metrology/Factor.hs +168/−0
- Data/Metrology/Internal.hs +58/−0
- Data/Metrology/LCSU.hs +54/−0
- Data/Metrology/Quantity.hs +223/−0
- Data/Metrology/Set.hs +42/−0
- Data/Metrology/Show.hs +105/−0
- Data/Metrology/Units.hs +142/−0
- Data/Metrology/Unsafe.hs +23/−0
- Data/Metrology/Validity.hs +87/−0
- Data/Metrology/Z.hs +158/−0
- README.md +58/−36
- Test/Travel.hs +54/−0
- units.cabal +64/−20
− Data/Dimensions.hs
@@ -1,145 +0,0 @@-{- Data/Dimensions.hs-- The units Package- Copyright (c) 2013 Richard Eisenberg- eir@cis.upenn.edu-- This file gathers and exports all user-visible pieces of the units package.- It also defines the main creators and consumers of dimensioned objects.-- This package declares many closely-related types. The following naming- conventions should be helpful:-- Prefix Target type/kind- ------------------------- # Z- $ DimSpec *- @ [DimSpec *]- @@ [DimSpec *], where the arguments are ordered similarly- % Dim (at the type level)- . Dim (at the term level)- : units, at both type and term levels--}--{-# LANGUAGE ExplicitNamespaces, DataKinds, FlexibleInstances, TypeFamilies,- TypeOperators, ConstraintKinds #-}---------------------------------------------------------------------------------- |--- Module : Data.Dimensions--- Copyright : (C) 2013 Richard Eisenberg--- License : BSD-style (see LICENSE)--- Maintainer : Richard Eisenberg (eir@cis.upenn.edu)--- Stability : experimental--- Portability : non-portable------ The units package is a framework for strongly-typed dimensional analysis.--- This haddock documentation is generally /not/ enough to be able to use this--- package effectively. Please see the readme at--- <http://www.cis.upenn.edu/~eir/packages/units/README.html>.------ Some of the types below refer to declarations that are not exported and--- not documented here. This is because Haddock does not allow finely-tuned--- abstraction in documentation. (In particular, right-hand sides of type --- synonym declarations are always included.) If a symbol is not exported,--- you do /not/ need to know anything about it to use this package.------ Though it doesn't appear here, @Scalar@ is an instance of @Num@, and--- generally has all the numeric instances that @Double@ has.--------------------------------------------------------------------------------module Data.Dimensions (- -- * Term-level combinators- (.+), (.-), (.*), (./), (.^), (*.),- (.<), (.>), (.<=), (.>=), dimEq, dimNeq,- nthRoot, dimSqrt, dimCubeRoot,- unity, zero, dim,- dimIn, (#), dimOf, (%),-- -- * Type-level unit combinators- (:*)(..), (:/)(..), (:^)(..), (:@)(..),- UnitPrefix(..),-- -- * Type-level dimensioned-quantity combinators- type (%*), type (%/), type (%^),-- -- * Creating new units- Unit(type BaseUnit, conversionRatio), MkDim, MkGenDim, Canonical, -- -- * Scalars, the only built-in unit- Number(..), Scalar, scalar,-- -- * Type-level integers- Z(..), Succ, Pred, type (#+), type (#-), type (#*), type (#/), NegZ,-- -- ** Synonyms for small numbers- One, Two, Three, Four, Five, MOne, MTwo, MThree, MFour, MFive,-- -- ** Term-level singletons- pZero, pOne, pTwo, pThree, pFour, pFive,- pMOne, pMTwo, pMThree, pMFour, pMFive,- pSucc, pPred-- ) where--import Data.Dimensions.Z-import Data.Dimensions.Dim-import Data.Dimensions.DimSpec-import Data.Dimensions.Units-import Data.Dimensions.UnitCombinators---- | Extracts a @Double@ from a dimensioned quantity, expressed in--- the given unit. For example:------ > inMeters :: Length -> Double--- > inMeters x = dimIn x Meter-dimIn :: Unit unit => MkDim (CanonicalUnit unit) -> unit -> Double-dimIn (Dim val) u = val / canonicalConvRatio u--infix 5 #--- | Infix synonym for 'dimIn'-(#) :: Unit unit => MkDim (CanonicalUnit unit) -> unit -> Double-(#) = dimIn---- | Creates a dimensioned quantity in the given unit. For example:------ > height :: Length--- > height = dimOf 2.0 Meter-dimOf :: Unit unit => Double -> unit -> MkDim (CanonicalUnit unit)-dimOf d u = Dim (d * canonicalConvRatio u)--infix 9 %--- | Infix synonym for 'dimOf'-(%) :: Unit unit => Double -> unit -> MkDim (CanonicalUnit unit)-(%) = dimOf---- | The number 1, expressed as a unitless dimensioned quantity.-unity :: Num n => Dim n '[]-unity = Dim 1---- | The number 0, polymorphic in its dimension. Use of this will--- often require a type annotation.-zero :: Num n => Dim n dimspec-zero = Dim 0---- | Dimension-safe cast. See the README for more info.-dim :: (d @~ e) => Dim n d -> Dim n e-dim (Dim x) = Dim x------------------------------------------------------------------- "Number" unit ------------------------------------------------------------------------------------------------------------- | The unit for unitless dimensioned quantities-data Number = Number -- the unit for unadorned numbers-instance Unit Number where- type BaseUnit Number = Canonical- type DimSpecsOf Number = '[]---- | The type of unitless dimensioned quantities--- This is an instance of @Num@, though Haddock doesn't show it.-type Scalar = MkDim Number---- | Convert a raw number into a unitless dimensioned quantity-scalar :: n -> Dim n '[]-scalar = Dim
− Data/Dimensions/Dim.hs
@@ -1,149 +0,0 @@-{- Data/Dimensions.hs-- The units Package- Copyright (c) 2013 Richard Eisenberg- eir@cis.upenn.edu-- This file defines the Dim type and operations on that type.--}--{-# LANGUAGE TypeFamilies, TypeOperators, DataKinds, UndecidableInstances,- ConstraintKinds, StandaloneDeriving, GeneralizedNewtypeDeriving,- FlexibleInstances #-}--module Data.Dimensions.Dim where--import Data.Singletons ( Sing )-import Data.Dimensions.DimSpec-import Data.Dimensions.Z------------------------------------------------------------------- Internal ------------------------------------------------------------------------------------------------------------------ | Dim adds a dimensional annotation to its base type @n@. This is the--- representation for all dimensioned quantities.-newtype Dim (n :: *) (a :: [DimSpec *]) = Dim n------------------------------------------------------------------- User-facing -------------------------------------------------------------------------------------------------------------infixl 6 .+--- | Add two compatible dimensioned quantities-(.+) :: (d1 @~ d2, Num n) => Dim n d1 -> Dim n d2 -> Dim n d1-(Dim a) .+ (Dim b) = Dim (a + b)--infixl 6 .---- | Subtract two compatible dimensioned quantities-(.-) :: (d1 @~ d2, Num n) => Dim n d1 -> Dim n d2 -> Dim n d1-(Dim a) .- (Dim b) = Dim (a - b)--infixl 7 .*--- | Multiply two dimensioned quantities-(.*) :: Num n => Dim n a -> Dim n b -> Dim n (Normalize (a @+ b))-(Dim a) .* (Dim b) = Dim (a * b)--infixl 7 ./--- | Divide two dimensioned quantities-(./) :: Fractional n => Dim n a -> Dim n b -> Dim n (Normalize (a @- b))-(Dim a) ./ (Dim b) = Dim (a / b)--infixr 8 .^--- | Raise a dimensioned quantity to a power known at compile time-(.^) :: Fractional n => Dim n a -> Sing z -> Dim n (a @* z)-(Dim a) .^ sz = Dim (a ^^ szToInt sz)---- | Take the n'th root of a dimensioned quantity, where n is known at compile--- time-nthRoot :: ((Zero < z) ~ True, Floating n) => Sing z -> Dim n a -> Dim n (a @/ z)-nthRoot sz (Dim a) = Dim (a ** (1.0 / (fromIntegral $ szToInt sz)))--infix 4 .<--- | Check if one dimensioned quantity is less than a compatible one-(.<) :: (d1 @~ d2, Ord n) => Dim n d1 -> Dim n d2 -> Bool-(Dim a) .< (Dim b) = a < b--infix 4 .>--- | Check if one dimensioned quantity is greater than a compatible one-(.>) :: (d1 @~ d2, Ord n) => Dim n d1 -> Dim n d2 -> Bool-(Dim a) .> (Dim b) = a > b--infix 4 .<=--- | Check if one dimensioned quantity is less than or equal to a compatible one-(.<=) :: (d1 @~ d2, Ord n) => Dim n d1 -> Dim n d2 -> Bool-(Dim a) .<= (Dim b) = a <= b--infix 4 .>=--- | Check if one dimensioned quantity is greater than or equal to a compatible one-(.>=) :: (d1 @~ d2, Ord n) => Dim n d1 -> Dim n d2 -> Bool-(Dim a) .>= (Dim b) = a >= b---- | Compare two compatible dimensioned quantities for equality-dimEq :: (d0 @~ d1, d0 @~ d2, Num n, Ord n)- => Dim n d0 -- ^ If the difference between the next- -- two arguments are less than this - -- amount, they are considered equal- -> Dim n d1 -> Dim n d2 -> Bool-dimEq (Dim epsilon) (Dim a) (Dim b) = abs(a-b) < epsilon---- | Compare two compatible dimensioned quantities for inequality-dimNeq :: (d0 @~ d1, d0 @~ d2, Num n, Ord n)- => Dim n d0 -- ^ If the difference between the next- -- two arguments are less than this - -- amount, they are considered equal- -> Dim n d1 -> Dim n d2 -> Bool-dimNeq (Dim epsilon) (Dim a) (Dim b) = abs(a-b) >= epsilon---- | Square a dimensioned quantity-dimSqr :: Num n => Dim n a -> Dim n (Normalize (a @+ a))-dimSqr x = x .* x---- | Take the square root of a dimensioned quantity-dimSqrt :: Floating n => Dim n a -> Dim n (a @/ Two)-dimSqrt = nthRoot pTwo---- | Take the cube root of a dimensioned quantity-dimCubeRoot :: Floating n => Dim n a -> Dim n (a @/ Three)-dimCubeRoot = nthRoot pThree--infixl 7 *.--- | Multiply a dimensioned quantity by a scalar-(*.) :: Num n => n -> Dim n a -> Dim n a-a *. (Dim b) = Dim (a * b)------------------------------------------------------------------- Instances ---------------------------------------------------------------------------------------------------------------deriving instance Eq n => Eq (Dim n '[])-deriving instance Ord n => Ord (Dim n '[])-deriving instance Num n => Num (Dim n '[])-deriving instance Real n => Real (Dim n '[])-deriving instance Fractional n => Fractional (Dim n '[])-deriving instance Floating n => Floating (Dim n '[])-deriving instance RealFrac n => RealFrac (Dim n '[])-deriving instance RealFloat n => RealFloat (Dim n '[])------------------------------------------------------------------- Combinators -------------------------------------------------------------------------------------------------------------infixl 7 %*--- | Multiply two dimension types to produce a new one. For example:------ > type Velocity = Length %/ Time-type family (d1 :: *) %* (d2 :: *) :: *-type instance (Dim n d1) %* (Dim n d2) = Dim n (d1 @+ d2)--infixl 7 %/--- | Divide two dimension types to produce a new one-type family (d1 :: *) %/ (d2 :: *) :: *-type instance (Dim n d1) %/ (Dim n d2) = Dim n (d1 @- d2)--infixr 8 %^--- | Exponentiate a dimension type to an integer-type family (d :: *) %^ (z :: Z) :: *-type instance (Dim n d) %^ z = Dim n (d @* z)--
− Data/Dimensions/DimSpec.hs
@@ -1,166 +0,0 @@-{- Data/Dimensions/DimSpec.hs-- The units Package- Copyright (c) 2013 Richard Eisenberg- eir@cis.upenn.edu-- This file defines the DimSpec kind and operations over lists of DimSpecs--}--{-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, UndecidableInstances #-}--module Data.Dimensions.DimSpec where--import GHC.Exts (Constraint)-import Data.Dimensions.Z-import Data.Type.Equality-import Data.Type.Bool--import Data.Singletons.Tuple (Fst, Snd)---- | This will only be used at the kind level. It holds a dimension with its--- exponent.-data DimSpec star = D star Z---------------------------------------------------------------- Set-like operations ----------------------------------------------------------------------------------------------{--These functions are templates for type-level functions.-remove :: String -> [String] -> [String]-remove _ [] = []-remove s (h:t) = if s == h then t else h : remove s t--member :: String -> [String] -> Bool-member _ [] = False-member s (h:t) = s == h || member s t--extract :: String -> [String] -> ([String], Maybe String)-extract _ [] = ([], Nothing)-extract s (h:t) =- if s == h- then (t, Just s)- else let (resList, resVal) = extract s t in (h : resList, resVal)--reorder :: [String] -> [String] -> [String]-reorder x [] = x-reorder x (h:t) =- case extract h x of- (lst, Nothing) -> reorder lst t- (lst, Just elt) -> elt : (reorder lst t)--}--infix 4 $=--- | Do these DimSpecs represent the same dimension?-type family (a :: DimSpec *) $= (b :: DimSpec *) :: Bool where- (D n1 z1) $= (D n2 z2) = n1 == n2- a $= b = False---- | @(Extract s lst)@ pulls the DimSpec that matches s out of lst, returning a--- diminished list and, possibly, the extracted DimSpec.------ @--- Extract A [A, B, C] ==> ([B, C], Just A--- Extract D [A, B, C] ==> ([A, B, C], Nothing)--- @-type family Extract (s :: DimSpec *)- (lst :: [DimSpec *])- :: ([DimSpec *], Maybe (DimSpec *)) where- Extract s '[] = '( '[], Nothing )- Extract s (h ': t) =- If (s $= h)- '(t, Just h)- '(h ': Fst (Extract s t), Snd (Extract s t))---- kind DimAnnotation = [DimSpec *]--- a list of DimSpecs forms a full annotation of a quantity's dimension---- | 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 ==> []--- @-type family Reorder (a :: [DimSpec *]) (b :: [DimSpec *]) :: [DimSpec *] where- Reorder x x = x- Reorder x '[] = x- Reorder x (h ': t) = Reorder' (Extract h x) t---- | Helper function in 'Reorder'-type family Reorder' (scrut :: ([DimSpec *], Maybe (DimSpec *)))- (t :: [DimSpec *])- :: [DimSpec *] where- Reorder' '(lst, Nothing) t = Reorder lst t- Reorder' '(lst, Just elt) t = elt ': (Reorder lst t)--infix 4 @~--- | Check if two @[DimSpec *]@s should be considered to be equal-type family (a :: [DimSpec *]) @~ (b :: [DimSpec *]) :: Constraint where- a @~ b = (Normalize (Reorder a b) ~ Normalize b)---------------------------------------------------------------- Normalization ------------------------------------------------------------------------------------------------------- | Take a @[DimSpec *]@ and remove any @DimSpec@s with an exponent of 0-type family Normalize (d :: [DimSpec *]) :: [DimSpec *] where- Normalize '[] = '[]- Normalize ((D n Zero) ': t) = Normalize t- Normalize (h ': t) = h ': Normalize t---------------------------------------------------------------- Arithmetic --------------------------------------------------------------------------------------------------------infixl 6 @@+--- | Adds corresponding exponents in two dimension, assuming the lists are--- ordered similarly.-type family (a :: [DimSpec *]) @@+ (b :: [DimSpec *]) :: [DimSpec *] where- '[] @@+ b = b- a @@+ '[] = a- ((D name z1) ': t1) @@+ ((D name z2) ': t2) = (D name (z1 #+ z2)) ': (t1 @@+ t2)- a @@+ (h ': t) = h ': (a @@+ t)--infixl 6 @+--- | Adds corresponding exponents in two dimension-type family (a :: [DimSpec *]) @+ (b :: [DimSpec *]) :: [DimSpec *] where- a @+ b = (Reorder a b) @@+ b--infixl 6 @@---- | Subtract exponents in two dimensions, assuming the lists are ordered--- similarly.-type family (a :: [DimSpec *]) @@- (b :: [DimSpec *]) :: [DimSpec *] where- '[] @@- b = NegList b- a @@- '[] = a- ((D name z1) ': t1) @@- ((D name z2) ': t2) = (D name (z1 #- z2)) ': (t1 @@- t2)- a @@- (h ': t) = (NegDim h) ': (a @@- t)--infixl 6 @---- | Subtract exponents in two dimensions-type family (a :: [DimSpec *]) @- (b :: [DimSpec *]) :: [DimSpec *] where- a @- b = (Reorder a b) @@- b---- | negate a single @DimSpec@-type family NegDim (a :: DimSpec *) :: DimSpec * where- NegDim (D n z) = D n (NegZ z)---- | negate a list of @DimSpec@s-type family NegList (a :: [DimSpec *]) :: [DimSpec *] where- NegList '[] = '[]- NegList (h ': t) = (NegDim h ': (NegList t))--infixl 7 @*--- | Multiplication of the exponents in a dimension by a scalar-type family (base :: [DimSpec *]) @* (power :: Z) :: [DimSpec *] where- '[] @* power = '[]- ((D name num) ': t) @* power = (D name (num #* power)) ': (t @* power)--infixl 7 @/--- | Division of the exponents in a dimension by a scalar-type family (dims :: [DimSpec *]) @/ (z :: Z) :: [DimSpec *] where- '[] @/ z = '[]- ((D name num) ': t) @/ z = (D name (num #/ z)) ': (t @/ z)
− Data/Dimensions/Poly.hs
@@ -1,41 +0,0 @@-{-# LANGUAGE ExplicitNamespaces #-}---------------------------------------------------------------------------------- |--- Module : Data.Dimensions.Poly--- Copyright : (C) 2013 Richard Eisenberg--- License : BSD-style (see LICENSE)--- Maintainer : Richard Eisenberg (eir@cis.upenn.edu)--- Stability : experimental--- Portability : non-portable------ This module exports all of the definitions you need if you wish to--- write functions polymorphic over dimension specifications.------ Each dimensioned quantity is represented by a member of the type--- 'Dim', which is parameterized by a type-level list of 'DimSpec's.--- A 'DimSpec', in turn, is a unit type paired with its exponent,--- representented with a type-level 'Z'. The unit types should all be--- /canonical/ -- that is, the "base" unit of all compatible units. Thus,--- the type of velocity in the SI system would be--- @Dim '[D Meter One, D Second MOne]@.------ A technical detail: because 'DimSpec' is used only at the type level--- and needs to store types of kind @*@, it must be parameterized, as we--- can't specify @*@ in its declaration. (See \"The Right Kind of Generic--- Programming\", by José Pedro Magalhães, published at WGP'12, for more--- explanation.) So, we always work with @(DimSpec *)@s.-------------------------------------------------------------------------------module Data.Dimensions.Poly (- -- * The 'Dim' type- Dim,-- -- * Maniuplating dimension specifications- DimSpec(..), type ($=), Extract, Reorder, type (@~), Normalize,- type (@+), type (@-), NegDim, NegList, type (@*), type (@/)-- ) where--import Data.Dimensions.Dim-import Data.Dimensions.DimSpec
− Data/Dimensions/SI.hs
@@ -1,29 +0,0 @@-{-# LANGUAGE TypeFamilies, TypeOperators #-}---------------------------------------------------------------------------------- |--- Module : Data.Dimensions.SI--- Copyright : (C) 2013 Richard Eisenberg--- License : BSD-style (see LICENSE)--- Maintainer : Richard Eisenberg (eir@cis.upenn.edu)--- Stability : experimental--- Portability : non-portable------ This module exports unit, type, and prefix definitions according to the SI--- system of units. The definitions were taken from here:--- <http://www.bipm.org/en/si/>.------ There is one deviation from the definition at that site: To work better--- with prefixes, the unit of mass is 'Gram'.--------------------------------------------------------------------------------module Data.Dimensions.SI (- module Data.Dimensions.SI.Units,- module Data.Dimensions.SI.Types,- module Data.Dimensions.SI.Prefixes- ) where--import Data.Dimensions.SI.Units-import Data.Dimensions.SI.Types-import Data.Dimensions.SI.Prefixes-
− Data/Dimensions/SI/Prefixes.hs
@@ -1,217 +0,0 @@-{-# LANGUAGE TypeOperators #-}---------------------------------------------------------------------------------- |--- Module : Data.Dimensions.SI.Prefixes--- Copyright : (C) 2013 Richard Eisenberg--- License : BSD-style (see LICENSE)--- Maintainer : Richard Eisenberg (eir@cis.upenn.edu)--- Stability : experimental--- Portability : non-portable------ Defines prefixes from the SI standard at <http://www.bipm.org/en/si/>--------------------------------------------------------------------------------module Data.Dimensions.SI.Prefixes where--import Data.Dimensions---- | 10^1-data Deca = Deca-instance UnitPrefix Deca where- multiplier _ = 1e1-instance Show Deca where- show _ = "da"--deca :: unit -> Deca :@ unit-deca = (Deca :@)---- | 10^2-data Hecto = Hecto-instance UnitPrefix Hecto where- multiplier _ = 1e2-instance Show Hecto where- show _ = "h"--hecto :: unit -> Hecto :@ unit-hecto = (Hecto :@)---- | 10^3-data Kilo = Kilo-instance UnitPrefix Kilo where- multiplier _ = 1e3-instance Show Kilo where- show _ = "k"--kilo :: unit -> Kilo :@ unit-kilo = (Kilo :@)---- | 10^6-data Mega = Mega-instance UnitPrefix Mega where- multiplier _ = 1e6-instance Show Mega where- show _ = "M"--mega :: unit -> Mega :@ unit-mega = (Mega :@)---- | 10^9-data Giga = Giga-instance UnitPrefix Giga where- multiplier _ = 1e9-instance Show Giga where- show _ = "G"--giga :: unit -> Giga :@ unit-giga = (Giga :@)---- | 10^12-data Tera = Tera-instance UnitPrefix Tera where- multiplier _ = 1e12-instance Show Tera where- show _ = "T"--tera :: unit -> Tera :@ unit-tera = (Tera :@)---- | 10^15-data Peta = Peta-instance UnitPrefix Peta where- multiplier _ = 1e15-instance Show Peta where- show _ = "P"--peta :: unit -> Peta :@ unit-peta = (Peta :@)---- | 10^18-data Exa = Exa-instance UnitPrefix Exa where- multiplier _ = 1e18-instance Show Exa where- show _ = "E"--exa :: unit -> Exa :@ unit-exa = (Exa :@)---- | 10^21-data Zetta = Zetta-instance UnitPrefix Zetta where- multiplier _ = 1e21-instance Show Zetta where- show _ = "Z"--zetta :: unit -> Zetta :@ unit-zetta = (Zetta :@)---- | 10^24-data Yotta = Yotta-instance UnitPrefix Yotta where- multiplier _ = 1e24-instance Show Yotta where- show _ = "Y"--yotta :: unit -> Yotta :@ unit-yotta = (Yotta :@)---- | 10^-1-data Deci = Deci-instance UnitPrefix Deci where- multiplier _ = 1e-1-instance Show Deci where- show _ = "d"--deci :: unit -> Deci :@ unit-deci = (Deci :@)---- | 10^-2-data Centi = Centi-instance UnitPrefix Centi where- multiplier _ = 1e-2-instance Show Centi where- show _ = "c"--centi :: unit -> Centi :@ unit-centi = (Centi :@)---- | 10^-3-data Milli = Milli-instance UnitPrefix Milli where- multiplier _ = 1e-3-instance Show Milli where- show _ = "m"--milli :: unit -> Milli :@ unit-milli = (Milli :@)---- | 10^-6-data Micro = Micro-instance UnitPrefix Micro where- multiplier _ = 1e-6-instance Show Micro where- show _ = "μ"--micro :: unit -> Micro :@ unit-micro = (Micro :@)---- | 10^-9-data Nano = Nano-instance UnitPrefix Nano where- multiplier _ = 1e-9-instance Show Nano where- show _ = "n"--nano :: unit -> Nano :@ unit-nano = (Nano :@)---- | 10^-12-data Pico = Pico-instance UnitPrefix Pico where- multiplier _ = 1e-12-instance Show Pico where- show _ = "p"--pico :: unit -> Pico :@ unit-pico = (Pico :@)---- | 10^-15-data Femto = Femto-instance UnitPrefix Femto where- multiplier _ = 1e-15-instance Show Femto where- show _ = "f"--femto :: unit -> Femto :@ unit-femto = (Femto :@)---- | 10^-18-data Atto = Atto-instance UnitPrefix Atto where- multiplier _ = 1e-18-instance Show Atto where- show _ = "a"--atto :: unit -> Atto :@ unit-atto = (Atto :@)---- | 10^-21-data Zepto = Zepto-instance UnitPrefix Zepto where- multiplier _ = 1e-21-instance Show Zepto where- show _ = "z"--zepto :: unit -> Zepto :@ unit-zepto = (Zepto :@)---- | 10^-24-data Yocto = Yocto-instance UnitPrefix Yocto where- multiplier _ = 1e-24-instance Show Yocto where- show _ = "y"--yocto :: unit -> Yocto :@ unit-yocto = (Yocto :@)
− Data/Dimensions/SI/Types.hs
@@ -1,59 +0,0 @@-{-# LANGUAGE TypeOperators #-}---------------------------------------------------------------------------------- |--- Module : Data.Dimensions.SI.Types--- Copyright : (C) 2013 Richard Eisenberg--- License : BSD-style (see LICENSE)--- Maintainer : Richard Eisenberg (eir@cis.upenn.edu)--- Stability : experimental--- Portability : non-portable------ This module defines type synonyms for SI units.--------------------------------------------------------------------------------module Data.Dimensions.SI.Types where--import Data.Dimensions-import Data.Dimensions.SI.Units--type Length = MkDim Meter-type Mass = MkDim Gram-type Time = MkDim Second-type Current = MkDim Ampere-type Temperature = MkDim Kelvin-type Quantity = MkDim Mole-type Luminosity = MkDim Candela--type Area = Length %^ Two-type Volume = Length %^ Three-type Velocity = Length %/ Time-type Acceleration = Length %/ (Time %^ Two)-type Wavenumber = Length %^ MOne-type Density = Mass %/ Volume-type SurfaceDensity = Mass %/ Area-type SpecificVolume = Volume %/ Mass-type CurrentDensity = Current %/ Area-type MagneticStrength = Current %/ Length-type Concentration = Quantity %/ Volume-type Luminance = Luminosity %/ Area--type Frequency = MkDim Hertz-type Force = MkDim Newton-type Pressure = MkDim Pascal-type Energy = MkDim Joule-type Power = MkDim Watt-type Charge = MkDim Coulomb-type ElectricPotential = MkDim Volt-type Capacitance = MkDim Farad-type Resistance = MkDim Ohm-type Conductance = MkDim Siemens-type MagneticFlux = MkDim Weber-type MagneticFluxDensity = MkDim Tesla-type Inductance = MkDim Henry-type LuminousFlux = MkDim Lumen-type Illuminance = MkDim Lux-type Kerma = MkDim Gray-type CatalyticActivity = MkDim Katal--type Momentum = Mass %* Velocity
− Data/Dimensions/SI/Units.hs
@@ -1,179 +0,0 @@-{-# LANGUAGE TypeFamilies, TypeOperators #-}---------------------------------------------------------------------------------- |--- Module : Data.Dimensions.SI.Units--- Copyright : (C) 2013 Richard Eisenberg--- License : BSD-style (see LICENSE)--- Maintainer : Richard Eisenberg (eir@cis.upenn.edu)--- Stability : experimental--- Portability : non-portable------ This module exports unit definitions according to the SI system of units.--- The definitions were taken from here: <http://www.bipm.org/en/si/>.------ There is one deviation from the definition at that site: To work better--- with prefixes, the unit of mass is 'Gram'.--------------------------------------------------------------------------------module Data.Dimensions.SI.Units where--import Data.Dimensions--data Meter = Meter-instance Unit Meter where- type BaseUnit Meter = Canonical-instance Show Meter where- show _ = "m"--data Gram = Gram-instance Unit Gram where- type BaseUnit Gram = Canonical-instance Show Gram where- show _ = "g"--data Second = Second-instance Unit Second where- type BaseUnit Second = Canonical-instance Show Second where- show _ = "s"--data Ampere = Ampere-instance Unit Ampere where- type BaseUnit Ampere = Canonical-instance Show Ampere where- show _ = "A"--data Kelvin = Kelvin-instance Unit Kelvin where- type BaseUnit Kelvin = Canonical-instance Show Kelvin where- show _ = "K"--data Mole = Mole-instance Unit Mole where- type BaseUnit Mole = Canonical-instance Show Mole where- show _ = "mol"--data Candela = Candela-instance Unit Candela where- type BaseUnit Candela = Canonical-instance Show Candela where- show _ = "cd"--data Hertz = Hertz-instance Unit Hertz where- type BaseUnit Hertz = Number :/ Second-instance Show Hertz where- show _ = "Hz"--data Newton = Newton-instance Unit Newton where- type BaseUnit Newton = Meter :* Gram :/ (Second :^ Two)- conversionRatio _ = 1000-instance Show Newton where- show _ = "N"--data Pascal = Pascal-instance Unit Pascal where- type BaseUnit Pascal = Newton :/ (Meter :^ Two)-instance Show Pascal where- show _ = "Pa"--data Joule = Joule-instance Unit Joule where- type BaseUnit Joule = Newton :* Meter-instance Show Joule where- show _ = "J"--data Watt = Watt-instance Unit Watt where- type BaseUnit Watt = Joule :/ Second-instance Show Watt where- show _ = "W"--data Coulomb = Coulomb-instance Unit Coulomb where- type BaseUnit Coulomb = Second :* Ampere-instance Show Coulomb where- show _ = "C"--data Volt = Volt-instance Unit Volt where- type BaseUnit Volt = Watt :/ Ampere-instance Show Volt where- show _ = "V"--data Farad = Farad-instance Unit Farad where- type BaseUnit Farad = Coulomb :/ Volt-instance Show Farad where- show _ = "F"--data Ohm = Ohm-instance Unit Ohm where- type BaseUnit Ohm = Volt :/ Ampere-instance Show Ohm where- show _ = "Ω"--data Siemens = Siemens-instance Unit Siemens where- type BaseUnit Siemens = Ampere :/ Volt-instance Show Siemens where- show _ = "S"--data Weber = Weber-instance Unit Weber where- type BaseUnit Weber = Volt :* Second-instance Show Weber where- show _ = "Wb"--data Tesla = Tesla-instance Unit Tesla where- type BaseUnit Tesla = Weber :/ (Meter :^ Two)-instance Show Tesla where- show _ = "T"--data Henry = Henry-instance Unit Henry where- type BaseUnit Henry = Weber :/ Ampere-instance Show Henry where- show _ = "H"--data Lumen = Lumen-instance Unit Lumen where- type BaseUnit Lumen = Candela-instance Show Lumen where- show _ = "lm"--data Lux = Lux-instance Unit Lux where- type BaseUnit Lux = Lumen :/ (Meter :^ Two)-instance Show Lux where- show _ = "lx"--data Becquerel = Becquerel-instance Unit Becquerel where- type BaseUnit Becquerel = Number :/ Second-instance Show Becquerel where- show _ = "Bq"--data Gray = Gray-instance Unit Gray where- type BaseUnit Gray = (Meter :^ Two) :/ (Second :^ Two)-instance Show Gray where- show _ = "Gy"--data Sievert = Sievert-instance Unit Sievert where- type BaseUnit Sievert = (Meter :^ Two) :/ (Second :^ Two)-instance Show Sievert where- show _ = "Sv"--data Katal = Katal-instance Unit Katal where- type BaseUnit Katal = Mole :/ Second-instance Show Katal where- show _ = "kat"-
− Data/Dimensions/Show.hs
@@ -1,73 +0,0 @@-{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, FlexibleInstances,- ScopedTypeVariables #-}-{-# OPTIONS_GHC -fno-warn-orphans #-}---------------------------------------------------------------------------------- |--- Module : Data.Dimensions.Show--- Copyright : (C) 2013 Richard Eisenberg--- License : BSD-style (see LICENSE)--- Maintainer : Richard Eisenberg (eir@cis.upenn.edu)--- Stability : experimental--- Portability : non-portable------ This module defines only a 'Show' instance for dimensioned quantities.--- The Show instance prints out the number stored internally with its canonical--- units.--------------------------------------------------------------------------------module Data.Dimensions.Show () where--import Data.Proxy (Proxy(..))-import Data.List-import Data.Singletons (Sing, sing, SingI)--import Data.Dimensions.DimSpec-import Data.Dimensions.Dim-import Data.Dimensions.Z--class ShowDimSpec (dims :: [DimSpec *]) where- showDims :: Proxy dims -> ([String], [String])--instance ShowDimSpec '[] where- showDims _ = ([], [])--instance (ShowDimSpec rest, Show unit, SingI z)- => ShowDimSpec (D unit z ': rest) where- showDims _ =- let (nums, denoms) = showDims (Proxy :: Proxy rest)- baseStr = show (undefined :: unit)- power = szToInt (sing :: Sing z)- abs_power = abs power- str = if abs_power == 1- then baseStr- else baseStr ++ "^" ++ (show abs_power) in- case compare power 0 of- LT -> (nums, str : denoms)- EQ -> (nums, denoms)- GT -> (str : nums, denoms)--showDimSpec :: ShowDimSpec dimspec => Proxy dimspec -> String-showDimSpec p- = let (nums, denoms) = mapPair (build_string . sort) $ showDims p in- case (length nums, length denoms) of- (0, 0) -> ""- (_, 0) -> " " ++ nums- (0, _) -> " 1/" ++ denoms- (_, _) -> " " ++ nums ++ "/" ++ denoms- where- mapPair :: (a -> b) -> (a, a) -> (b, b)- mapPair f (x, y) = (f x, f y)-- build_string :: [String] -> String- build_string [] = ""- build_string [s] = s- build_string s = "(" ++ build_string_helper s ++ ")"-- build_string_helper :: [String] -> String- build_string_helper [] = ""- build_string_helper [s] = s- build_string_helper (h:t) = h ++ " * " ++ build_string_helper t--instance (ShowDimSpec dims, Show n) => Show (Dim n dims) where- show (Dim d) = (show d ++ showDimSpec (Proxy :: Proxy dims))
− Data/Dimensions/UnitCombinators.hs
@@ -1,72 +0,0 @@-{- Data/Dimensions/UnitCombinators.hs-- The units Package- Copyright (c) 2013 Richard Eisenberg- eir@cis.upenn.edu-- This file defines combinators to build more complex units from simpler ones.--}--{-# LANGUAGE TypeOperators, TypeFamilies, UndecidableInstances,- ScopedTypeVariables, DataKinds, FlexibleInstances #-}--module Data.Dimensions.UnitCombinators where--import Data.Singletons ( Sing, SingI, sing )--import Data.Dimensions.Units-import Data.Dimensions.DimSpec-import Data.Dimensions.Z--infixl 7 :*--- | Multiply two units to get another unit.--- For example: @type MetersSquared = Meter :* Meter@-data u1 :* u2 = u1 :* u2--instance (Unit u1, Unit u2) => Unit (u1 :* u2) where-- -- we override the default conversion lookup behavior- type BaseUnit (u1 :* u2) = Canonical- conversionRatio _ = undefined -- this should never be called-- type DimSpecsOf (u1 :* u2) = (DimSpecsOf u1) @+ (DimSpecsOf u2)- canonicalConvRatio _ = canonicalConvRatio (undefined :: u1) *- canonicalConvRatio (undefined :: u2)--infixl 7 :/--- | Divide two units to get another unit-data u1 :/ u2 = u1 :/ u2--instance (Unit u1, Unit u2) => Unit (u1 :/ u2) where- type BaseUnit (u1 :/ u2) = Canonical- conversionRatio _ = undefined -- this should never be called- type DimSpecsOf (u1 :/ u2) = (DimSpecsOf u1) @- (DimSpecsOf u2)- canonicalConvRatio _ = canonicalConvRatio (undefined :: u1) /- canonicalConvRatio (undefined :: u2)--infixr 8 :^--- | Raise a unit to a power, known at compile time-data unit :^ (power :: Z) = unit :^ Sing power--instance (Unit unit, SingI power) => Unit (unit :^ power) where- type BaseUnit (unit :^ power) = Canonical- conversionRatio _ = undefined-- type DimSpecsOf (unit :^ power) = (DimSpecsOf unit) @* power- canonicalConvRatio _ = canonicalConvRatio (undefined :: unit) ^^ (szToInt (sing :: Sing power))--infixr 9 :@--- | Multiply a conversion ratio by some constant. Used for defining prefixes.-data prefix :@ unit = prefix :@ unit---- | A class for user-defined prefixes-class UnitPrefix prefix where- -- | This should return the desired multiplier for the prefix being defined.- -- This function must /not/ inspect its argument.- multiplier :: prefix -> Double--instance ( CheckCanonical unit ~ False- , Unit unit- , UnitPrefix prefix ) => Unit (prefix :@ unit) where- type BaseUnit (prefix :@ unit) = unit- conversionRatio _ = multiplier (undefined :: prefix)
− Data/Dimensions/Units.hs
@@ -1,112 +0,0 @@-{- Data/Dimensions/Units.hs-- The units Package- Copyright (c) 2013 Richard Eisenberg- eir@cis.upenn.edu-- This file defines the class Unit, which is needed for- user-defined units.--}--{-# LANGUAGE TypeFamilies, DataKinds, DefaultSignatures, MultiParamTypeClasses,- ConstraintKinds, UndecidableInstances, FlexibleContexts,- FlexibleInstances, ScopedTypeVariables #-}--module Data.Dimensions.Units where--import Data.Dimensions.Z-import Data.Dimensions.DimSpec-import Data.Dimensions.Dim-import Data.Type.Bool---- | Dummy type use just to label canonical units. It does /not/ have a--- 'Unit' instance.-data Canonical---- | Class of units. Make an instance of this class to define a new unit.-class Unit unit where- -- | The base unit of this unit: what this unit is defined in terms of.- -- For units that are not defined in terms of anything else, the base unit- -- should be 'Canonical'.- type BaseUnit unit :: *-- -- | The conversion ratio /from/ the base unit /to/ this unit.- -- If left out, a conversion ratio of 1 is assumed.- --- -- For example:- --- -- > instance Unit Foot where- -- > type BaseUnit Foot = Meter- -- > conversionRatio _ = 0.3048- --- -- Implementations should /never/ examine their argument!- conversionRatio :: unit -> Double-- -- | The internal list of dimensions for a dimensioned quantity built from- -- this unit.- type DimSpecsOf unit :: [DimSpec *]- type DimSpecsOf unit = If (IsCanonical unit)- '[D unit One]- (DimSpecsOf (BaseUnit unit))-- -- if unspecified, assume a conversion ratio of 1- conversionRatio _ = 1-- -- | Compute the conversion from the underlying canonical unit to- -- this one. A default is provided that multiplies together the ratios- -- of all units between this one and the canonical one.- canonicalConvRatio :: unit -> Double- default canonicalConvRatio :: BaseHasConvRatio unit => unit -> Double- canonicalConvRatio u = conversionRatio u * baseUnitRatio u---- Abbreviation for creating a Dim (defined here to avoid a module cycle)---- | Make a dimensioned quantity type capable of storing a value of a given--- unit. This uses a 'Double' for storage of the value. For example:------ > type Length = MkDim Meter-type MkDim unit = Dim Double (DimSpecsOf unit)---- | Make a dimensioned quantity with a custom numerical type.-type MkGenDim n unit = Dim n (DimSpecsOf unit)---- | Is this unit a canonical unit?-type IsCanonical (unit :: *) = CheckCanonical (BaseUnit unit)---- | Is the argument the special datatype 'Canonical'?-type family CheckCanonical (base_unit :: *) :: Bool where- CheckCanonical Canonical = True- CheckCanonical unit = False--{- I want to say this. But type families are *eager* so I have to write- it another way.-type family CanonicalUnit (unit :: *) where- CanonicalUnit unit- = If (IsCanonical unit) unit (CanonicalUnit (BaseUnit unit))--}---- | Get the canonical unit from a given unit.--- For example: @CanonicalUnit Foot = Meter@-type CanonicalUnit (unit :: *) = CanonicalUnit' (BaseUnit unit) unit---- | Helper function in 'CanonicalUnit'-type family CanonicalUnit' (base_unit :: *) (unit :: *) :: * where- CanonicalUnit' Canonical unit = unit- CanonicalUnit' base unit = CanonicalUnit' (BaseUnit base) base---- | Essentially, a constraint that checks if a conversion ratio can be--- calculated for a @BaseUnit@ of a unit.-type BaseHasConvRatio unit = HasConvRatio (IsCanonical unit) unit---- | This is like 'Unit', but deals with 'Canonical'. It is necessary--- to be able to define 'canonicalConvRatio' in the right way.-class is_canonical ~ IsCanonical unit- => HasConvRatio (is_canonical :: Bool) (unit :: *) where- baseUnitRatio :: unit -> Double-instance True ~ IsCanonical canonical_unit- => HasConvRatio True canonical_unit where- baseUnitRatio _ = 1-instance ( False ~ IsCanonical noncanonical_unit- , Unit (BaseUnit noncanonical_unit) )- => HasConvRatio False noncanonical_unit where- baseUnitRatio _ = canonicalConvRatio (undefined :: BaseUnit noncanonical_unit)
− Data/Dimensions/Unsafe.hs
@@ -1,22 +0,0 @@-{-# LANGUAGE ExplicitNamespaces #-}---------------------------------------------------------------------------------- |--- Module : Data.Dimensions.Unsafe--- Copyright : (C) 2013 Richard Eisenberg--- License : BSD-style (see LICENSE)--- Maintainer : Richard Eisenberg (eir@cis.upenn.edu)--- Stability : experimental--- Portability : non-portable------ This module exports the constructor of the 'Dim' type. This allows you--- to write dimension-unsafe code. Use at your peril.--------------------------------------------------------------------------------module Data.Dimensions.Unsafe (- -- * The 'Dim' type- Dim(..),- ) where--import Data.Dimensions.Dim-
− Data/Dimensions/Z.hs
@@ -1,148 +0,0 @@-{- Data/Dimensions/Z.hs- - The units Package- Copyright (c) 2013 Richard Eisenberg- eir@cis.upenn.edu-- This file contains a definition of integers at the type-level, in terms- of a promoted datatype 'Z'.--}--{-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, UndecidableInstances,- GADTs, PolyKinds, TemplateHaskell, ScopedTypeVariables,- EmptyCase #-}-{-# OPTIONS_GHC -fno-warn-missing-signatures #-}---- | This module defines a datatype and operations to represent type-level--- integers. Though it's defined as part of the units package, it may be--- useful beyond dimensional analysis. If you have a compelling non-units--- use of this package, please let me (Richard, @eir@ at @cis.upenn.edu@)--- know.--module Data.Dimensions.Z where--import Data.Singletons.TH---- | The datatype for type-level integers.-$(singletons [d| data Z = Zero | S Z | P Z deriving Eq |])---- | Convert a 'Z' to an 'Int'-zToInt :: Z -> Int-zToInt Zero = 0-zToInt (S z) = zToInt z + 1-zToInt (P z) = zToInt z - 1---- | Add one to an integer-type family Succ (z :: Z) :: Z where- Succ Zero = S Zero- Succ (P z) = z- Succ (S z) = S (S z)---- | Subtract one from an integer-type family Pred (z :: Z) :: Z where- Pred Zero = P Zero- Pred (P z) = P (P z)- Pred (S z) = z--infixl 6 #+--- | Add two integers-type family (a :: Z) #+ (b :: Z) :: Z where- Zero #+ z = z- (S z1) #+ (S z2) = S (S (z1 #+ z2))- (S z1) #+ Zero = S z1- (S z1) #+ (P z2) = z1 #+ z2- (P z1) #+ (S z2) = z1 #+ z2- (P z1) #+ Zero = P z1- (P z1) #+ (P z2) = P (P (z1 #+ z2))--infixl 6 #---- | Subtract two integers-type family (a :: Z) #- (b :: Z) :: Z where- z #- Zero = z- (S z1) #- (S z2) = z1 #- z2- Zero #- (S z2) = P (Zero #- z2)- (P z1) #- (S z2) = P (P (z1 #- z2))- (S z1) #- (P z2) = S (S (z1 #- z2))- Zero #- (P z2) = S (Zero #- z2)- (P z1) #- (P z2) = z1 #- z2--infixl 7 #*--- | Multiply two integers-type family (a :: Z) #* (b :: Z) :: Z where- Zero #* z = Zero- (S z1) #* z2 = (z1 #* z2) #+ z2- (P z1) #* z2 = (z1 #* z2) #- z2---- | Negate an integer-type family NegZ (z :: Z) :: Z where- NegZ Zero = Zero- NegZ (S z) = P (NegZ z)- NegZ (P z) = S (NegZ z)---- | Divide two integers-type family (a :: Z) #/ (b :: Z) :: Z where- Zero #/ b = Zero- a #/ (P b') = NegZ (a #/ (NegZ (P b')))- a #/ b = ZDiv b b a---- | Helper function for division-type family ZDiv (counter :: Z) (n :: Z) (z :: Z) :: Z where- ZDiv One n (S z') = S (z' #/ n)- ZDiv One n (P z') = P (z' #/ n)- ZDiv (S count') n (S z') = ZDiv count' n z'- ZDiv (S count') n (P z') = ZDiv count' n z'---- | Less-than comparison-type family (a :: Z) < (b :: Z) :: Bool where- Zero < Zero = False- Zero < (S n) = True- Zero < (P n) = False- (S n) < Zero = False- (S n) < (S n') = n < n'- (S n) < (P n') = False- (P n) < Zero = True- (P n) < (S n') = True- (P n) < (P n') = n < n'--type One = S Zero-type Two = S One-type Three = S Two-type Four = S Three-type Five = S Four--type MOne = P Zero-type MTwo = P MOne-type MThree = P MTwo-type MFour = P MThree-type MFive = P MFour---- | This is the singleton value representing @Zero@ at the term level and--- at the type level, simultaneously. Used for raising units to powers.-pZero = SZero-pOne = SS pZero-pTwo = SS pOne-pThree = SS pTwo-pFour = SS pThree-pFive = SS pFour--pMOne = SP pZero-pMTwo = SP pMOne-pMThree = SP pMTwo-pMFour = SP pMThree-pMFive = SP pMFour---- | Add one to a singleton @Z@.-pSucc :: Sing z -> Sing (Succ z)-pSucc SZero = pOne-pSucc (SS z') = SS (SS z')-pSucc (SP z') = z'---- | Subtract one from a singleton @Z@.-pPred :: Sing z -> Sing (Pred z)-pPred SZero = pMOne-pPred (SS z') = z'-pPred (SP z') = SP (SP z')---- | Convert a singleton @Z@ to an @Int@.-szToInt :: Sing (z :: Z) -> Int-szToInt = zToInt . fromSing
+ Data/Metrology.hs view
@@ -0,0 +1,266 @@+{- Data/Metrology.hs++ The units Package+ Copyright (c) 2013 Richard Eisenberg+ eir@cis.upenn.edu++ This file gathers and exports all user-visible pieces of the units package.+ It also defines the main creators and consumers of dimensioned objects.++ This package declares many closely-related types. The following naming+ conventions should be helpful:++ Prefix Target type/kind+ ------------------------+ # Z+ $ Factor *+ @ [Factor *]+ @@ [Factor *], where the arguments are ordered similarly+ % Qu (at the type level)+ | Qu (at the term level)+ : units & dimensions, at both type and term levels+-}++{-# LANGUAGE ExplicitNamespaces, DataKinds, FlexibleInstances, TypeFamilies,+ TypeOperators, ConstraintKinds, ScopedTypeVariables,+ FlexibleContexts #-}++-----------------------------------------------------------------------------+-- |+-- Module : Data.Metrology+-- Copyright : (C) 2013 Richard Eisenberg+-- License : BSD-style (see LICENSE)+-- Maintainer : Richard Eisenberg (eir@cis.upenn.edu)+-- Stability : experimental+-- Portability : non-portable+--+-- The units package is a framework for strongly-typed dimensional analysis.+-- This haddock documentation is generally /not/ enough to be able to use this+-- package effectively. Please see the readme at+-- <http://www.cis.upenn.edu/~eir/packages/units/README.html>.+--+-- Some of the types below refer to declarations that are not exported and+-- not documented here. This is because Haddock does not allow finely-tuned+-- abstraction in documentation. (In particular, right-hand sides of type +-- synonym declarations are always included.) If a symbol is not exported,+-- you do /not/ need to know anything about it to use this package.+--+-- Though it doesn't appear here, @Scalar@ is an instance of @Num@, and+-- generally has all the numeric instances that @Double@ has.+-----------------------------------------------------------------------------++module Data.Metrology (+ -- * Term-level combinators++ -- | The term-level arithmetic operators are defined by+ -- applying vertical bar(s) to the sides the dimensioned + -- quantities acts on. + -- See also "Data.Metrology.AltOperators" for an alternative system of operators.+ (|+|), (|-|), + (|*|), (|/|), (*|), (|*), (/|), (|/), + (|^), (|^^),+ (|<|), (|>|), (|<=|), (|>=|), (|==|), (|/=|),+ qApprox, qNapprox, + qSq, qCube, qSqrt, qCubeRoot, nthRoot, ++ -- * Nondimensional units, conversion between quantities and numeric values+ unity, zero, redim, convert,+ numIn, (#), (##), quOf, (%), (%%), defaultLCSU, fromDefaultLCSU,+ constant,++ -- * Type-level unit combinators+ (:*)(..), (:/)(..), (:^)(..), (:@)(..),+ UnitPrefix(..),++ -- * Type-level quantity combinators+ type (%*), type (%/), type (%^),++ -- * Creating quantity types+ Qu, MkQu_D, MkQu_DLN, MkQu_U, MkQu_ULN, ++ -- * Creating new dimensions+ Dimension,++ -- * Creating new units+ Unit(type BaseUnit, type DimOfUnit, conversionRatio), + Canonical,++ -- * Scalars, the only built-in unit+ Dimensionless(..), Number(..), Scalar, scalar,++ -- * LCSUs (locally coherent system of units)+ MkLCSU, LCSU(DefaultLCSU), DefaultUnitOfDim,++ -- * Validity checks and assertions+ CompatibleUnit, CompatibleDim, ConvertibleLCSUs_D,+ DefaultConvertibleLCSU_D, DefaultConvertibleLCSU_U,++ -- * Type-level integers+ Z(..), Succ, Pred, type (#+), type (#-), type (#*), type (#/), NegZ,++ -- ** Synonyms for small numbers+ One, Two, Three, Four, Five, MOne, MTwo, MThree, MFour, MFive,++ -- ** Term-level singletons+ pZero, pOne, pTwo, pThree, pFour, pFive,+ pMOne, pMTwo, pMThree, pMFour, pMFive,+ pSucc, pPred,++ -- * Internal definitions+ -- | The following module is re-exported solely to prevent noise in error messages;+ -- we do not recommend trying to use these definitions in user code.+ module Data.Metrology.Internal++ ) where++import Data.Metrology.Z+import Data.Metrology.Quantity+import Data.Metrology.Dimensions+import Data.Metrology.Factor+import Data.Metrology.Units+import Data.Metrology.Combinators+import Data.Metrology.LCSU+import Data.Metrology.Validity+import Data.Metrology.Internal+import Data.Proxy++-- | Extracts a numerical value from a dimensioned quantity, expressed in+-- the given unit. For example:+--+-- > inMeters :: Length -> Double+-- > inMeters x = numIn x Meter+--+-- or+--+-- > inMeters x = x # Meter +numIn :: forall unit dim lcsu n.+ ( ValidDLU dim lcsu unit+ , Fractional n )+ => Qu dim lcsu n -> unit -> n+numIn (Qu val) u+ = val * fromRational+ (canonicalConvRatioSpec (Proxy :: Proxy (LookupList dim lcsu))+ / canonicalConvRatio u)++infix 5 #+-- | Infix synonym for 'numIn'+(#) :: ( ValidDLU dim lcsu unit+ , Fractional n )+ => Qu dim lcsu n -> unit -> n+(#) = numIn++infix 5 ##+-- | Like '#', but uses a default LCSU. This operator is recommended+-- for users who wish not to worry about LCSUs.+(##) :: ( ValidDLU dim DefaultLCSU unit+ , Fractional n )+ => Qu dim DefaultLCSU n -> unit -> n+(##) = numIn++-- | Creates a dimensioned quantity in the given unit. For example:+--+-- > height :: Length+-- > height = quOf 2.0 Meter+--+-- or+--+-- > height = 2.0 % Meter+quOf :: forall unit dim lcsu n.+ ( ValidDLU dim lcsu unit+ , Fractional n )+ => n -> unit -> Qu dim lcsu n+quOf d u+ = Qu (d * fromRational+ (canonicalConvRatio u+ / canonicalConvRatioSpec (Proxy :: Proxy (LookupList dim lcsu))))++infixr 9 %+-- | Infix synonym for 'quOf'+(%) :: ( ValidDLU dim lcsu unit+ , Fractional n )+ => n -> unit -> Qu dim lcsu n+(%) = quOf++infixr 9 %%+-- | Like '%', but uses a default LCSU. This operator is recommended+-- for users who wish not to worry about LCSUs.+(%%) :: ( ValidDLU dim DefaultLCSU unit+ , Fractional n )+ => n -> unit -> Qu dim DefaultLCSU n+(%%) = quOf++-- | Use this to choose a default LCSU for a dimensioned quantity.+-- The default LCSU uses the 'DefaultUnitOfDim' representation for each+-- dimension.+defaultLCSU :: Qu dim DefaultLCSU n -> Qu dim DefaultLCSU n+defaultLCSU = id++-- | The number 1, expressed as a unitless dimensioned quantity.+unity :: Num n => Qu '[] l n+unity = Qu 1++-- | The number 0, polymorphic in its dimension. Use of this will+-- often require a type annotation.+zero :: Num n => Qu dimspec l n+zero = Qu 0++-- | Cast between equivalent dimension within the same CSU.+-- for example [kg m s] and [s m kg]. See the README for more info.+redim :: (d @~ e) => Qu d l n -> Qu e l n+redim (Qu x) = Qu x++-- | Dimension-keeping cast between different CSUs.+convert :: forall d l1 l2 n. + ( ConvertibleLCSUs d l1 l2+ , Fractional n ) + => Qu d l1 n -> Qu d l2 n+convert (Qu x) = Qu $ x * fromRational (+ canonicalConvRatioSpec (Proxy :: Proxy (LookupList d l1))+ / canonicalConvRatioSpec (Proxy :: Proxy (LookupList d l2)))+++-- | Compute the argument in the DefaultLCSU, and present the result+-- as lcsu-polymorphic dimension-polymorphic value.+fromDefaultLCSU :: ( d @~ e+ , ConvertibleLCSUs e DefaultLCSU l+ , Fractional n )+ => Qu d DefaultLCSU n -> Qu e l n+fromDefaultLCSU = convert . redim+++-- | A synonym of 'fromDefaultLCSU', for one of its dominant usecase+-- is to inject constant quantities into dimension-polymorphic+-- expressions.+constant :: ( d @~ e+ , ConvertibleLCSUs e DefaultLCSU l+ , Fractional n )+ => Qu d DefaultLCSU n -> Qu e l n+constant = fromDefaultLCSU++-------------------------------------------------------------+--- "Number" unit -------------------------------------------+-------------------------------------------------------------++-- | The dimension for the dimensionless quantities.+-- It is also called "quantities of dimension one", but+-- @One@ is confusing with the type-level integer One.+data Dimensionless = Dimensionless+instance Dimension Dimensionless where+ type DimFactorsOf Dimensionless = '[]+type instance DefaultUnitOfDim Dimensionless = Number++-- | The unit for unitless dimensioned quantities+data Number = Number -- the unit for unadorned numbers+instance Unit Number where+ type BaseUnit Number = Canonical+ type DimOfUnit Number = Dimensionless+ type UnitFactorsOf Number = '[]++-- | The type of unitless dimensioned quantities.+-- This is an instance of @Num@, though Haddock doesn't show it.+-- This uses a @Double@ internally and uses a default LCSU.+type Scalar = MkQu_U Number++-- | Convert a raw number into a unitless dimensioned quantity+scalar :: n -> Qu '[] l n+scalar = Qu
+ Data/Metrology/Combinators.hs view
@@ -0,0 +1,97 @@+{- Data/Metrology/Combinators.hs++ The units Package+ Copyright (c) 2013 Richard Eisenberg+ eir@cis.upenn.edu++ This file defines combinators to build more complex units and dimensions from simpler ones.+-}++{-# LANGUAGE TypeOperators, TypeFamilies, UndecidableInstances, + ScopedTypeVariables, DataKinds, FlexibleInstances,+ ConstraintKinds #-}++module Data.Metrology.Combinators where++import Data.Singletons ( Sing, SingI, sing )++import Data.Metrology.Dimensions+import Data.Metrology.Units+import Data.Metrology.Factor+import Data.Metrology.Z+import Data.Type.Equality+import Data.Metrology.LCSU++infixl 7 :*+-- | Multiply two units to get another unit.+-- For example: @type MetersSquared = Meter :* Meter@+data u1 :* u2 = u1 :* u2++instance (Dimension d1, Dimension d2) => Dimension (d1 :* d2) where+ type DimFactorsOf (d1 :* d2) = (DimFactorsOf d1) @+ (DimFactorsOf d2)++instance (Unit u1, Unit u2) => Unit (u1 :* u2) where++ -- we override the default conversion lookup behavior+ type BaseUnit (u1 :* u2) = Canonical+ type DimOfUnit (u1 :* u2) = DimOfUnit u1 :* DimOfUnit u2+ conversionRatio _ = undefined -- this should never be called++ type UnitFactorsOf (u1 :* u2) = (UnitFactorsOf u1) @+ (UnitFactorsOf u2)+ canonicalConvRatio _ = canonicalConvRatio (undefined :: u1) *+ canonicalConvRatio (undefined :: u2)++type instance DefaultUnitOfDim (d1 :* d2) =+ DefaultUnitOfDim d1 :* DefaultUnitOfDim d2++infixl 7 :/+-- | Divide two units to get another unit+data u1 :/ u2 = u1 :/ u2++instance (Dimension d1, Dimension d2) => Dimension (d1 :/ d2) where+ type DimFactorsOf (d1 :/ d2) = (DimFactorsOf d1) @- (DimFactorsOf d2)++instance (Unit u1, Unit u2) => Unit (u1 :/ u2) where+ type BaseUnit (u1 :/ u2) = Canonical+ type DimOfUnit (u1 :/ u2) = DimOfUnit u1 :/ DimOfUnit u2+ conversionRatio _ = undefined -- this should never be called+ type UnitFactorsOf (u1 :/ u2) = (UnitFactorsOf u1) @- (UnitFactorsOf u2)+ canonicalConvRatio _ = canonicalConvRatio (undefined :: u1) /+ canonicalConvRatio (undefined :: u2)++type instance DefaultUnitOfDim (d1 :/ d2) =+ DefaultUnitOfDim d1 :/ DefaultUnitOfDim d2+ +infixr 8 :^+-- | Raise a unit to a power, known at compile time+data unit :^ (power :: Z) = unit :^ Sing power++instance Dimension dim => Dimension (dim :^ power) where+ type DimFactorsOf (dim :^ power) = (DimFactorsOf dim) @* power++instance (Unit unit, SingI power) => Unit (unit :^ power) where+ type BaseUnit (unit :^ power) = Canonical+ type DimOfUnit (unit :^ power) = DimOfUnit unit :^ power+ conversionRatio _ = undefined++ type UnitFactorsOf (unit :^ power) = (UnitFactorsOf unit) @* power+ canonicalConvRatio _ = canonicalConvRatio (undefined :: unit) ^^ (szToInt (sing :: Sing power))++type instance DefaultUnitOfDim (d :^ z) = DefaultUnitOfDim d :^ z++infixr 9 :@+-- | Multiply a conversion ratio by some constant. Used for defining prefixes.+data prefix :@ unit = prefix :@ unit++-- | A class for user-defined prefixes+class UnitPrefix prefix where+ -- | This should return the desired multiplier for the prefix being defined.+ -- This function must /not/ inspect its argument.+ multiplier :: Fractional f => prefix -> f++instance ( (unit == Canonical) ~ False+ , Unit unit+ , UnitPrefix prefix ) => Unit (prefix :@ unit) where+ type BaseUnit (prefix :@ unit) = unit+ conversionRatio _ = multiplier (undefined :: prefix)+
+ Data/Metrology/Dimensions.hs view
@@ -0,0 +1,34 @@+{- Data/Metrology/Units.hs++ The units Package+ Copyright (c) 2013 Richard Eisenberg+ eir@cis.upenn.edu++ This file defines the class Dimension, which is needed for+ defining dimensions.+-}++{-# LANGUAGE TypeFamilies, DataKinds, DefaultSignatures, MultiParamTypeClasses,+ ConstraintKinds, UndecidableInstances, FlexibleContexts,+ FlexibleInstances, ScopedTypeVariables, TypeOperators #-}++module Data.Metrology.Dimensions where++import Data.Metrology.Z+import Data.Metrology.Factor+import Data.Metrology.LCSU+import Data.Type.Bool+import Data.Type.Equality+import Data.Proxy+import Data.Singletons+import GHC.Exts+++-- | This class is used to mark abstract dimensions, such as @Length@, or+-- @Mass@.+class Dimension dim where+ -- | Retrieve a list of @Factor@s representing the given dimension. Overriding+ -- the default of this type family should not be necessary in user code.+ type DimFactorsOf dim :: [Factor *]+ type DimFactorsOf dim = '[F dim One]+
+ Data/Metrology/Factor.hs view
@@ -0,0 +1,168 @@+{- Data/Metrology.Factor.hs++ The units Package+ Copyright (c) 2013 Richard Eisenberg+ eir@cis.upenn.edu++ This file defines the Factor kind and operations over lists of Factors.++ Factors represents dimensions and units raised to a power of integers, and the lists of Factors represents monomials of dimensions and units.+-}++{-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, UndecidableInstances #-}++module Data.Metrology.Factor where++import GHC.Exts (Constraint)+import Data.Metrology.Z+import Data.Type.Equality+import Data.Type.Bool++import Data.Singletons.Tuple (Fst, Snd)++-- | This will only be used at the kind level. It holds a dimension or unit+-- with its exponent.+data Factor star = F star Z++----------------------------------------------------------+--- Set-like operations ----------------------------------+----------------------------------------------------------+{-+These functions are templates for type-level functions.+remove :: String -> [String] -> [String]+remove _ [] = []+remove s (h:t) = if s == h then t else h : remove s t++member :: String -> [String] -> Bool+member _ [] = False+member s (h:t) = s == h || member s t++extract :: String -> [String] -> ([String], Maybe String)+extract _ [] = ([], Nothing)+extract s (h:t) =+ if s == h+ then (t, Just s)+ else let (resList, resVal) = extract s t in (h : resList, resVal)++reorder :: [String] -> [String] -> [String]+reorder x [] = x+reorder x (h:t) =+ case extract h x of+ (lst, Nothing) -> reorder lst t+ (lst, Just elt) -> elt : (reorder lst t)+-}++infix 4 $=+-- | Do these Factors represent the same dimension?+type family (a :: Factor *) $= (b :: Factor *) :: Bool where+ (F n1 z1) $= (F n2 z2) = n1 == n2+ a $= b = False++-- | @(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)+-- @+type family Extract (s :: Factor *)+ (lst :: [Factor *])+ :: ([Factor *], Maybe (Factor *)) where+ Extract s '[] = '( '[], Nothing )+ Extract s (h ': t) =+ If (s $= h)+ '(t, Just h)+ '(h ': Fst (Extract s t), Snd (Extract s t))++-- kind DimAnnotation = [Factor *]+-- a list of Factors forms a full annotation of a quantity's dimension++-- | 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 ==> []+-- @+type family Reorder (a :: [Factor *]) (b :: [Factor *]) :: [Factor *] where+ Reorder x x = x+ Reorder x '[] = x+ Reorder x (h ': t) = Reorder' (Extract h x) t++-- | Helper function in 'Reorder'+type family Reorder' (scrut :: ([Factor *], Maybe (Factor *)))+ (t :: [Factor *])+ :: [Factor *] where+ Reorder' '(lst, Nothing) t = Reorder lst t+ Reorder' '(lst, Just elt) t = elt ': (Reorder lst t)++infix 4 @~+-- | Check if two @[Factor *]@s should be considered to be equal+type family (a :: [Factor *]) @~ (b :: [Factor *]) :: Constraint where+ a @~ b = (Normalize (Reorder a b) ~ Normalize b)++----------------------------------------------------------+--- Normalization ----------------------------------------+----------------------------------------------------------++-- | Take a @[Factor *]@ and remove any @Factor@s with an exponent of 0+type family Normalize (d :: [Factor *]) :: [Factor *] where+ Normalize '[] = '[]+ Normalize ((F n Zero) ': t) = Normalize t+ Normalize (h ': t) = h ': Normalize t++----------------------------------------------------------+--- Arithmetic -------------------------------------------+----------------------------------------------------------++infixl 6 @@++-- | Adds corresponding exponents in two dimension, assuming the lists are+-- ordered similarly.+type family (a :: [Factor *]) @@+ (b :: [Factor *]) :: [Factor *] where+ '[] @@+ b = b+ a @@+ '[] = a+ ((F name z1) ': t1) @@+ ((F name z2) ': t2) = (F name (z1 #+ z2)) ': (t1 @@+ t2)+ a @@+ (h ': t) = h ': (a @@+ t)++infixl 6 @++-- | Adds corresponding exponents in two dimension+type family (a :: [Factor *]) @+ (b :: [Factor *]) :: [Factor *] where+ a @+ b = (Reorder a b) @@+ b++infixl 6 @@-+-- | Subtract exponents in two dimensions, assuming the lists are ordered+-- similarly.+type family (a :: [Factor *]) @@- (b :: [Factor *]) :: [Factor *] where+ '[] @@- b = NegList b+ a @@- '[] = a+ ((F name z1) ': t1) @@- ((F name z2) ': t2) = (F name (z1 #- z2)) ': (t1 @@- t2)+ a @@- (h ': t) = (NegDim h) ': (a @@- t)++infixl 6 @-+-- | Subtract exponents in two dimensions+type family (a :: [Factor *]) @- (b :: [Factor *]) :: [Factor *] where+ a @- b = (Reorder a b) @@- b++-- | negate a single @Factor@+type family NegDim (a :: Factor *) :: Factor * where+ NegDim (F n z) = F n (NegZ z)++-- | negate a list of @Factor@s+type family NegList (a :: [Factor *]) :: [Factor *] where+ NegList '[] = '[]+ NegList (h ': t) = (NegDim h ': (NegList t))++infixl 7 @*+-- | Multiplication of the exponents in a dimension by a scalar+type family (base :: [Factor *]) @* (power :: Z) :: [Factor *] where+ '[] @* power = '[]+ ((F name num) ': t) @* power = (F name (num #* power)) ': (t @* power)++infixl 7 @/+-- | Division of the exponents in a dimension by a scalar+type family (dims :: [Factor *]) @/ (z :: Z) :: [Factor *] where+ '[] @/ z = '[]+ ((F name num) ': t) @/ z = (F name (num #/ z)) ': (t @/ z)
+ Data/Metrology/Internal.hs view
@@ -0,0 +1,58 @@+{- Data/Metrology/Internal.hs++ The units Package+ Copyright (c) 2013 Richard Eisenberg+ eir@cis.upenn.edu++ 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.+-}++-----------------------------------------------------------------------------+-- |+-- Module : Data.Metrology.Internal+-- Copyright : (C) 2013 Richard Eisenberg+-- License : BSD-style (see LICENSE)+-- Maintainer : Richard Eisenberg (eir@cis.upenn.edu)+-- Stability : experimental+-- Portability : non-portable+--+-- 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.+--+-----------------------------------------------------------------------------++{-# LANGUAGE ExplicitNamespaces #-}++module Data.Metrology.Internal (+ -- * LCSU lookup+ Lookup, LookupList,++ -- * Validity checking+ ConvertibleLCSUs, ValidDLU, ValidDL, type (*~), CanonicalUnitsOfFactors,++ -- * Manipulating units+ DimOfUnitIsConsistent, IsCanonical,+ CanonicalUnit, CanonicalUnit', BaseHasConvRatio,+ UnitFactor, UnitFactorsOf,++ -- * Maniuplating dimension specifications+ module Data.Metrology.Factor,++ -- * Set operations on lists+ module Data.Metrology.Set,++ -- * Dimensions+ DimFactorsOf+ ) where++import Data.Metrology.LCSU+import Data.Metrology.Validity+import Data.Metrology.Units+import Data.Metrology.Factor+import Data.Metrology.Set+import Data.Metrology.Dimensions++
+ Data/Metrology/LCSU.hs view
@@ -0,0 +1,54 @@+{- Data/Metrology/LCSU.hs++ The units Package+ Copyright (c) 2013 Richard Eisenberg+ eir@cis.upenn.edu++ Defines a locally coherent system of units (LCSUs),+ implemented as an association list.+ An LCSU is a from base dimensions to units, thus + defining a uniquely mapping units for any dimensions.+-}++{-# LANGUAGE DataKinds, PolyKinds, TypeFamilies, TypeOperators, UndecidableInstances #-}++module Data.Metrology.LCSU (+ LCSU(DefaultLCSU), DefaultUnitOfDim,+ Lookup, LookupList, MkLCSU+ ) where++import Data.Metrology.Factor+import Data.Metrology.Z++import Data.Singletons.Maybe++data LCSU star = MkLCSU_ [(star, star)]+ | DefaultLCSU++type family Lookup (dim :: *) (lcsu :: LCSU *) :: * where+ 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+ LookupList '[] lcsu = '[]+ LookupList (F dim z ': rest) lcsu+ = F (Lookup dim lcsu) z ': LookupList rest lcsu++-- | Assign a default unit for a dimension. Necessary only when using+-- default LCSUs.+type family DefaultUnitOfDim (dim :: *) :: *++-- use type family to prevent pattern-matching++-- | Make a local consistent set of units. The argument is a type-level+-- list of tuple types, to be interpreted as an association list from+-- dimensions to units. For example:+--+-- > type MyLCSU = MkLCSU '[(Length, Foot), (Mass, Gram), (Time, Year)]+type family MkLCSU pairs where -- uses unpromoted tuples to make it easier for users+ MkLCSU pairs = MkLCSU_ (UsePromotedTuples pairs)++type family UsePromotedTuples pairs where+ UsePromotedTuples '[] = '[]+ UsePromotedTuples ((dim, unit) ': rest) = ('(dim, unit) ': UsePromotedTuples rest)
+ Data/Metrology/Quantity.hs view
@@ -0,0 +1,223 @@+{- Data/Metrology.Quantity.hs++ The units Package+ Copyright (c) 2013 Richard Eisenberg+ eir@cis.upenn.edu++ This file defines the 'Qu' type that represents quantity+ (a number paired with its measurement reference).+ This file also defines operations on 'Qu' types.+-}++{-# LANGUAGE TypeFamilies, TypeOperators, DataKinds, UndecidableInstances,+ ConstraintKinds, StandaloneDeriving, GeneralizedNewtypeDeriving,+ FlexibleInstances, RoleAnnotations #-}++module Data.Metrology.Quantity where++import Data.Singletons ( Sing )+import Data.Metrology.Dimensions+import Data.Metrology.Factor+import Data.Metrology.Units+import Data.Metrology.Z+import Data.Metrology.LCSU++-------------------------------------------------------------+--- Internal ------------------------------------------------+-------------------------------------------------------------++-- | 'Qu' adds a dimensional annotation to its numerical value type+-- @n@. This is the representation for all quantities.+newtype Qu (a :: [Factor *]) (lcsu :: LCSU *) (n :: *) = Qu n+type role Qu nominal nominal representational++-------------------------------------------------------------+--- User-facing ---------------------------------------------+-------------------------------------------------------------++-- Abbreviation for creating a Qu (defined here to avoid a module cycle)++-- | Make a quantity type capable of storing a value of a given+-- unit. This uses a 'Double' for storage of the value. For example:+--+-- > data LengthDim = LengthDim+-- > instance Dimension LengthDim+-- > data Meter = Meter+-- > instance Unit Meter where+-- > type BaseUnit Meter = Canonical+-- > type DimOfUnit Meter = LengthDim+-- > type instance DefaultUnitOfDim LengthDim = Meter+-- > type Length = MkQu_D LengthDim+--+-- Note that the dimension /must/ have an instance for the type family+-- 'DefaultUnitOfDim' for this to work.+type MkQu_D dim = Qu (DimFactorsOf dim) DefaultLCSU Double++-- | Make a quantity type with a custom numerical type and LCSU.+type MkQu_DLN dim = Qu (DimFactorsOf dim)++-- | Make a quantity type with a given unit. It will be stored as a 'Double'.+-- Note that the corresponding dimension /must/ have an appropriate instance+-- for 'DefaultUnitOfDim' for this to work.+type MkQu_U unit = Qu (DimFactorsOf (DimOfUnit unit)) DefaultLCSU Double++-- | Make a quantity type with a unit and LCSU with custom numerical type.+-- The quantity will have the dimension corresponding to the unit.+type MkQu_ULN unit = Qu (DimFactorsOf (DimOfUnit unit))+++infixl 6 |+|+-- | Add two compatible quantities+(|+|) :: (d1 @~ d2, Num n) => Qu d1 l n -> Qu d2 l n -> Qu d1 l n+(Qu a) |+| (Qu b) = Qu (a + b)++infixl 6 |-|+-- | Subtract two compatible quantities+(|-|) :: (d1 @~ d2, Num n) => Qu d1 l n -> Qu d2 l n -> Qu d1 l n+(Qu a) |-| (Qu b) = Qu (a - b)++infixl 7 |*|+-- | Multiply two quantities+(|*|) :: Num n => Qu a l n -> Qu b l n -> Qu (Normalize (a @+ b)) l n+(Qu a) |*| (Qu b) = Qu (a * b)++infixl 7 |/|+-- | Divide two quantities+(|/|) :: Fractional n => Qu a l n -> Qu b l n -> Qu (Normalize (a @- b)) l n+(Qu a) |/| (Qu b) = Qu (a / b)++infixl 7 *| , |* , /| , |/+-- | Multiply a quantity by a scalar from the left+(*|) :: Num n => n -> Qu b l n -> Qu b l n+a *| (Qu b) = Qu (a * b)++-- | Multiply a quantity by a scalar from the right+(|*) :: Num n => Qu a l n -> n -> Qu a l n+(Qu a) |* b = Qu (a * b)++-- | Divide a scalar by a quantity+(/|) :: Fractional n => n -> Qu b l n -> Qu (NegList b) l n+a /| (Qu b) = Qu (a / b)++-- | Divide a quantity by a scalar+(|/) :: Fractional n => Qu a l n -> n -> Qu a l n+(Qu a) |/ b = Qu (a / b)++infixr 8 |^+-- | Raise a quantity to a integer power, knowing at compile time that the integer is non-negative.+(|^) :: Fractional n => Qu a l n -> Sing z -> Qu (a @* z) l n -- TODO: type level proof here+(Qu a) |^ sz = Qu (a ^ szToInt sz)++infixr 8 |^^+-- | Raise a quantity to a integer power known at compile time+(|^^) :: Fractional n => Qu a l n -> Sing z -> Qu (a @* z) l n+(Qu a) |^^ sz = Qu (a ^^ szToInt sz)++-- | Take the n'th root of a quantity, where n is known at compile+-- time+nthRoot :: ((Zero < z) ~ True, Floating n)+ => Sing z -> Qu a l n -> Qu (a @/ z) l n+nthRoot sz (Qu a) = Qu (a ** (1.0 / (fromIntegral $ szToInt sz)))++infix 4 |<|+-- | Check if one quantity is less than a compatible one+(|<|) :: (d1 @~ d2, Ord n) => Qu d1 l n -> Qu d2 l n -> Bool+(Qu a) |<| (Qu b) = a < b++infix 4 |>|+-- | Check if one quantity is greater than a compatible one+(|>|) :: (d1 @~ d2, Ord n) => Qu d1 l n -> Qu d2 l n -> Bool+(Qu a) |>| (Qu b) = a > b++infix 4 |<=|+-- | Check if one quantity is less than or equal to a compatible one+(|<=|) :: (d1 @~ d2, Ord n) => Qu d1 l n -> Qu d2 l n -> Bool+(Qu a) |<=| (Qu b) = a <= b++infix 4 |>=|+-- | Check if one quantity is greater than or equal to a compatible one+(|>=|) :: (d1 @~ d2, Ord n) => Qu d1 l n -> Qu d2 l n -> Bool+(Qu a) |>=| (Qu b) = a >= b++infix 4 |==|+-- | Check if two quantities are equal (uses the equality of the underlying numerical type)+(|==|) :: (d1 @~ d2, Eq n) => Qu d1 l n -> Qu d2 l n -> Bool+(Qu a) |==| (Qu b) = a == b++infix 4 |/=|+-- | Check if two quantities are not equal+(|/=|) :: (d1 @~ d2, Eq n) => Qu d1 l n -> Qu d2 l n -> Bool+(Qu a) |/=| (Qu b) = a /= b++infix 4 `qApprox` , `qNapprox`+-- | Compare two compatible quantities for approximate equality. If+-- the difference between the left hand side and the right hand side+-- arguments are less than the /epsilon/, they are considered equal.+qApprox :: (d0 @~ d1, d0 @~ d2, Num n, Ord n)+ => Qu d0 l n -- ^ /epsilon/+ -> Qu d1 l n -- ^ left hand side+ -> Qu d2 l n -- ^ right hand side+ -> Bool +qApprox (Qu epsilon) (Qu a) (Qu b) = abs(a-b) < epsilon++-- | Compare two compatible quantities for approixmate inequality. +-- @qNapprox e a b = not $ qApprox e a b@+qNapprox :: (d0 @~ d1, d0 @~ d2, Num n, Ord n)+ => Qu d0 l n -- ^ /epsilon/ + -> Qu d1 l n -- ^ left hand side + -> Qu d2 l n -- ^ right hand side+ -> Bool+qNapprox (Qu epsilon) (Qu a) (Qu b) = abs(a-b) >= epsilon++-- | Square a quantity+qSq :: Num n => Qu a l n -> Qu (Normalize (a @+ a)) l n+qSq x = x |*| x++-- | Cube a quantity+qCube :: Num n => Qu a l n -> Qu (Normalize (Normalize (a @+ a) @+ a)) l n+qCube x = x |*| x |*| x++-- | Take the square root of a quantity+qSqrt :: Floating n => Qu a l n -> Qu (a @/ Two) l n+qSqrt = nthRoot pTwo++-- | Take the cubic root of a quantity+qCubeRoot :: Floating n => Qu a l n -> Qu (a @/ Three) l n+qCubeRoot = nthRoot pThree+++-------------------------------------------------------------+--- Instances for dimensionless quantities ------------------+-------------------------------------------------------------++deriving instance Eq n => Eq (Qu '[] l n)+deriving instance Ord n => Ord (Qu '[] l n)+deriving instance Num n => Num (Qu '[] l n)+deriving instance Real n => Real (Qu '[] l n)+deriving instance Fractional n => Fractional (Qu '[] l n)+deriving instance Floating n => Floating (Qu '[] l n)+deriving instance RealFrac n => RealFrac (Qu '[] l n)+deriving instance RealFloat n => RealFloat (Qu '[] l n)++-------------------------------------------------------------+--- Combinators ---------------------------------------------+-------------------------------------------------------------++infixl 7 %*+-- | Multiply two quantity types to produce a new one. For example:+--+-- > type Velocity = Length %/ Time+type family (d1 :: *) %* (d2 :: *) :: *+type instance (Qu d1 l n) %* (Qu d2 l n) = Qu (d1 @+ d2) l n++infixl 7 %/+-- | Divide two quantity types to produce a new one+type family (d1 :: *) %/ (d2 :: *) :: *+type instance (Qu d1 l n) %/ (Qu d2 l n) = Qu (d1 @- d2) l n++infixr 8 %^+-- | Exponentiate a quantity type to an integer+type family (d :: *) %^ (z :: Z) :: *+type instance (Qu d l n) %^ z = Qu (d @* z) l n++
+ Data/Metrology/Set.hs view
@@ -0,0 +1,42 @@+{- Data/Metrology/Set.hs++ The units Package+ Copyright (c) 2013 Richard Eisenberg+ eir@cis.upenn.edu++ Defines set-like operations on type-level lists.+-}++-----------------------------------------------------------------------------+-- |+-- Module : Data.Metrology.Set+-- Copyright : (C) 2013 Richard Eisenberg+-- License : BSD-style (see LICENSE)+-- Maintainer : Richard Eisenberg (eir@cis.upenn.edu)+-- Stability : experimental+-- Portability : non-portable+--+-- This module defines a few set-like operations on type-level lists. It+-- may be applicable beyond the units package.+-----------------------------------------------------------------------------++{-# LANGUAGE DataKinds, PolyKinds, TypeFamilies, TypeOperators,+ UndecidableInstances #-}++module Data.Metrology.Set where++import GHC.Exts ( Constraint )++-- | Are two lists equal, when considered as sets?+type family SetEqual (as :: [k]) (bs :: [k]) :: Constraint where+ SetEqual as bs = (Subset as bs, Subset bs as)++-- | Is one list a subset of the other?+type family Subset (as :: [k]) (bs :: [k]) :: Constraint where+ Subset '[] bs = (() :: Constraint)+ Subset (a ': as) bs = (a `Elem` bs, as `Subset` bs)++-- | Is an element contained in a list?+type family Elem (a :: k) (bs :: [k]) :: Constraint where+ Elem a (a ': bs) = (() :: Constraint)+ Elem a (b ': bs) = a `Elem` bs
+ Data/Metrology/Show.hs view
@@ -0,0 +1,105 @@+{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, FlexibleInstances,+ ScopedTypeVariables, FlexibleContexts, ConstraintKinds #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}++-----------------------------------------------------------------------------+-- |+-- Module : Data.Metrology.Show+-- Copyright : (C) 2013 Richard Eisenberg+-- License : BSD-style (see LICENSE)+-- Maintainer : Richard Eisenberg (eir@cis.upenn.edu)+-- Stability : experimental+-- Portability : non-portable+--+-- This module defines 'Show' instance for quantities. The show instance+-- prints out the number stored internally with its canonical units. To print+-- out quantities with specific units use the function `showIn`.+-----------------------------------------------------------------------------++module Data.Metrology.Show (showIn) where++import Data.Proxy (Proxy(..))+import Data.List+import Data.Singletons (Sing, sing, SingI)++import Data.Metrology.Factor+import Data.Metrology.Quantity+import Data.Metrology.Z+import Data.Metrology.LCSU+import Data.Metrology.Combinators+import Data.Metrology.Units+import Data.Metrology++class ShowUnitFactor (dims :: [Factor *]) where+ showDims :: Bool -- take absolute value of exponents?+ -> Proxy dims -> ([String], [String])++instance ShowUnitFactor '[] where+ showDims _ _ = ([], [])++instance (ShowUnitFactor rest, Show unit, SingI z)+ => ShowUnitFactor (F unit z ': rest) where+ showDims take_abs _ =+ let (nums, denoms) = showDims take_abs (Proxy :: Proxy rest)+ baseStr = show (undefined :: unit)+ power = szToInt (sing :: Sing z)+ abs_power = if take_abs then abs power else power+ str = if abs_power == 1+ then baseStr+ else baseStr ++ "^" ++ (show abs_power) in+ case compare power 0 of+ LT -> (nums, str : denoms)+ EQ -> (nums, denoms)+ GT -> (str : nums, denoms)++showFactor :: ShowUnitFactor dimspec => Proxy dimspec -> String+showFactor p+ = let (nums, denoms) = mapPair (build_string . sort) $ showDims True p in+ case (length nums, length denoms) of+ (0, 0) -> ""+ (_, 0) -> " " ++ nums+ (0, _) -> build_string (snd (showDims False p))+ (_, _) -> " " ++ nums ++ "/" ++ denoms+ where+ mapPair :: (a -> b) -> (a, a) -> (b, b)+ mapPair f (x, y) = (f x, f y)++ build_string :: [String] -> String+ build_string [] = ""+ build_string [s] = s+ build_string s = "(" ++ build_string_helper s ++ ")"++ build_string_helper :: [String] -> String+ build_string_helper [] = ""+ build_string_helper [s] = s+ build_string_helper (h:t) = h ++ " * " ++ build_string_helper t++-- enable showing of compound units:+instance (Show u1, Show u2) => Show (u1 :* u2) where+ show _ = show (undefined :: u1) ++ " " ++ show (undefined :: u2)++instance (Show u1, Show u2) => Show (u1 :/ u2) where+ show _ = show (undefined :: u1) ++ "/" ++ show (undefined :: u2)++instance (Show u1, SingI power) => Show (u1 :^ (power :: Z)) where+ show _ = show (undefined :: u1) ++ "^" ++ show (szToInt (sing :: Sing power))++-- enable showing of units with prefixes:+instance (Show prefix, Show unit) => Show (prefix :@ unit) where+ show _ = show (undefined :: prefix) ++ show (undefined :: unit)++instance (ShowUnitFactor (LookupList dims lcsu), Show n)+ => Show (Qu dims lcsu n) where+ show (Qu d) = show d +++ (' ' : showFactor (Proxy :: Proxy (LookupList dims lcsu)))++infix 1 `showIn`++-- | Show a dimensioned quantity in a given unit. (The default @Show@+-- instance always uses canonical units.)+showIn :: ( ValidDLU dim lcsu unit+ , Fractional n+ , Show unit+ , Show n )+ => Qu dim lcsu n -> unit -> String+showIn x u = show (x # u) ++ " " ++ show u
+ Data/Metrology/Units.hs view
@@ -0,0 +1,142 @@+{- Data/Metrology/Units.hs++ The units Package+ Copyright (c) 2013 Richard Eisenberg+ eir@cis.upenn.edu++ This file defines the class Unit, which is needed for+ user-defined units.+-}++{-# LANGUAGE TypeFamilies, DataKinds, DefaultSignatures, MultiParamTypeClasses,+ ConstraintKinds, UndecidableInstances, FlexibleContexts,+ FlexibleInstances, ScopedTypeVariables, TypeOperators, PolyKinds #-}++module Data.Metrology.Units where++import Data.Metrology.Z+import Data.Metrology.Factor+import Data.Metrology.Dimensions+import Data.Metrology.LCSU+import Data.Type.Bool+import Data.Type.Equality+import Data.Proxy+import Data.Singletons+import GHC.Exts++-----------------------------------------------------------------------+-- Main Unit definitions (rather user-facing)+-----------------------------------------------------------------------++-- | Dummy type use just to label canonical units. It does /not/ have a+-- 'Unit' instance.+data Canonical++class DimOfUnitIsConsistent unit => Unit unit where+ -- | The base unit of this unit: what this unit is defined in terms of.+ -- For units that are not defined in terms of anything else, the base unit+ -- should be 'Canonical'.+ type BaseUnit unit :: *++ -- | The dimension that this unit is associated with. This needs to be+ -- defined only for canonical units; other units are necessarily of the+ -- same dimension as their base.+ type DimOfUnit unit :: *+ type DimOfUnit unit = DimOfUnit (BaseUnit unit)++ -- | The conversion ratio /from/ the base unit /to/ this unit.+ -- If left out, a conversion ratio of 1 is assumed.+ --+ -- For example:+ --+ -- > instance Unit Foot where+ -- > type BaseUnit Foot = Meter+ -- > conversionRatio _ = 0.3048+ --+ -- Implementations should /never/ examine their argument!+ conversionRatio :: unit -> Rational+ conversionRatio _ = 1 -- if unspecified, assume a conversion ratio of 1++ -- | The internal list of canonical units corresponding to this unit.+ -- Overriding the default should not be necessary in user code.+ type UnitFactorsOf unit :: [Factor *]+ type UnitFactorsOf unit = If (IsCanonical unit)+ '[F unit One]+ (UnitFactorsOf (BaseUnit unit))++ -- | Compute the conversion from the underlying canonical unit to+ -- this one. A default is provided that multiplies together the ratios+ -- of all units between this one and the canonical one.+ canonicalConvRatio :: unit -> Rational+ default canonicalConvRatio :: BaseHasConvRatio unit => unit -> Rational+ canonicalConvRatio u = conversionRatio u * baseUnitRatio u++-- | Check to make sure that a unit has the same dimension as its base unit,+-- if any.+type family DimOfUnitIsConsistent unit :: Constraint where+ DimOfUnitIsConsistent unit = ( Dimension (DimOfUnit unit)+ , If (BaseUnit unit == Canonical)+ (() :: Constraint)+ (DimOfUnit unit ~ DimOfUnit (BaseUnit unit)) )+ -- This definition does not use || so that we get better error messages.++-----------------------------------------------------------------------+-- Internal implementation details+-----------------------------------------------------------------------++-- | Is this unit a canonical unit?+type family IsCanonical (unit :: *) where+ IsCanonical unit = (BaseUnit unit == Canonical)+ -- this is a type family because of GHC #8978++{- I want to say this. But type families are *eager* so I have to write+ it another way.+type family CanonicalUnit (unit :: *) where+ CanonicalUnit unit+ = If (IsCanonical unit) unit (CanonicalUnit (BaseUnit unit))+-}++-- | Get the canonical unit from a given unit.+-- For example: @CanonicalUnit Foot = Meter@+type CanonicalUnit (unit :: *) = CanonicalUnit' (BaseUnit unit) unit++-- | Helper function in 'CanonicalUnit'+type family CanonicalUnit' (base_unit :: *) (unit :: *) :: * where+ CanonicalUnit' Canonical unit = unit+ CanonicalUnit' base unit = CanonicalUnit' (BaseUnit base) base++-- | Essentially, a constraint that checks if a conversion ratio can be+-- calculated for a @BaseUnit@ of a unit.+type family BaseHasConvRatio unit where+ BaseHasConvRatio unit = HasConvRatio (IsCanonical unit) unit+ -- this is a type family because of GHC #8978++-- | This is like 'Unit', but deals with 'Canonical'. It is necessary+-- to be able to define 'canonicalConvRatio' in the right way.+class is_canonical ~ IsCanonical unit+ => HasConvRatio (is_canonical :: Bool) (unit :: *) where+ baseUnitRatio :: unit -> Rational+instance True ~ IsCanonical canonical_unit+ => HasConvRatio True canonical_unit where+ baseUnitRatio _ = 1+instance ( False ~ IsCanonical noncanonical_unit+ , Unit (BaseUnit noncanonical_unit) )+ => HasConvRatio False noncanonical_unit where+ baseUnitRatio _ = canonicalConvRatio (undefined :: BaseUnit noncanonical_unit)++-----------------------------------------------------------------------+-- Conversion ratios for lists of units+-----------------------------------------------------------------------++-- | Classifies well-formed list of unit factors, and permits calculating a+-- conversion ratio for the purposes of LCSU conversions.+class UnitFactor (units :: [Factor *]) where+ canonicalConvRatioSpec :: Proxy units -> Rational++instance UnitFactor '[] where+ canonicalConvRatioSpec _ = 1++instance (UnitFactor rest, Unit unit, SingI n) => UnitFactor (F unit n ': rest) where+ canonicalConvRatioSpec _ =+ (canonicalConvRatio (undefined :: unit) ^^ szToInt (sing :: Sing n)) *+ canonicalConvRatioSpec (Proxy :: Proxy rest)
+ Data/Metrology/Unsafe.hs view
@@ -0,0 +1,23 @@+{-# LANGUAGE Unsafe #-}++-----------------------------------------------------------------------------+-- |+-- Module : Data.Metrology.Unsafe+-- Copyright : (C) 2013 Richard Eisenberg+-- License : BSD-style (see LICENSE)+-- Maintainer : Richard Eisenberg (eir@cis.upenn.edu)+-- Stability : experimental+-- Portability : non-portable+--+-- This module exports the constructor of the 'Qu' type. This allows you+-- to write code that takes creates and reads quantities at will, +-- which may lead to dimension unsafety. Use at your peril.+-----------------------------------------------------------------------------++module Data.Metrology.Unsafe (+ -- * The 'Dim' type+ Qu(..),+ ) where++import Data.Metrology.Quantity+
+ Data/Metrology/Validity.hs view
@@ -0,0 +1,87 @@+{- Data/Metrology/Validity.hs++ The units Package+ Copyright (c) 2013 Richard Eisenberg+ eir@cis.upenn.edu++ This file defines validity checks on dimension, unit, and LCSU definitions.+-}++{-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, PolyKinds,+ UndecidableInstances #-}++module Data.Metrology.Validity where++import Data.Metrology.LCSU+import Data.Metrology.Factor+import Data.Metrology.Dimensions+import Data.Metrology.Units+import Data.Metrology.Set+import GHC.Exts ( Constraint )++-- | Check if a (dimension factors, LCSU, unit) triple are all valid to be used together.+type family ValidDLU (dfactors :: [Factor *]) (lcsu :: LCSU *) (unit :: *) where+ ValidDLU dfactors lcsu unit =+ ( dfactors ~ DimFactorsOf (DimOfUnit unit)+ , UnitFactor (LookupList dfactors lcsu)+ , Unit unit+ , UnitFactorsOf unit *~ LookupList dfactors lcsu )++-- | 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.+type family ValidDL (dfactors :: [Factor *]) (lcsu :: LCSU *) :: Constraint where+ ValidDL '[] lcsu = (() :: Constraint)+ ValidDL (F d z ': rest) lcsu = (DimOfUnit (Lookup d lcsu) ~ d, ValidDL rest lcsu)++-- | Are two LCSUs inter-convertible at the given dimension?+type family ConvertibleLCSUs (dfactors :: [Factor *])+ (l1 :: LCSU *) (l2 :: LCSU *) :: Constraint where+ ConvertibleLCSUs dfactors l1 l2 =+ ( LookupList dfactors l1 *~ LookupList dfactors l2+ , ValidDL dfactors l1+ , ValidDL dfactors l2+ , UnitFactor (LookupList dfactors l1)+ , UnitFactor (LookupList dfactors l2) )++-- | Like 'ConvertibleLCSUs', but takes a dimension, not a dimension factors.+type family ConvertibleLCSUs_D (dim :: *) (l1 :: LCSU *) (l2 :: LCSU *) :: Constraint where+ ConvertibleLCSUs_D dim l1 l2 = ConvertibleLCSUs (DimFactorsOf dim) l1 l2++infix 4 *~+-- | Check if two @[Factor *]@s, representing /units/, should be+-- considered to be equal+type family (units1 :: [Factor *]) *~ (units2 :: [Factor *]) :: Constraint where+ units1 *~ units2 =+ CanonicalUnitsOfFactors units1 `SetEqual` CanonicalUnitsOfFactors units2++-- | Given a list of unit factors, extract out the canonical units they are based+-- on.+type family CanonicalUnitsOfFactors (fs :: [Factor *]) :: [*] where+ CanonicalUnitsOfFactors '[] = '[]+ CanonicalUnitsOfFactors (F u z ': fs) = (CanonicalUnit u) ': CanonicalUnitsOfFactors fs+ +-- | Check if an LCSU has consistent entries for the given unit. i.e. can the lcsu+-- describe the unit?+type family CompatibleUnit (lcsu :: LCSU *) (unit :: *) :: Constraint where+ CompatibleUnit lcsu unit+ = ( ValidDLU (DimFactorsOf (DimOfUnit unit)) lcsu unit+ , UnitFactor (LookupList (DimFactorsOf (DimOfUnit unit)) lcsu) )++-- | Check if an LCSU can express the given dimension+type family CompatibleDim (lcsu :: LCSU *) (dim :: *) :: Constraint where+ CompatibleDim lcsu dim+ = ( UnitFactor (LookupList (DimFactorsOf dim) lcsu)+ , DimOfUnit (Lookup dim lcsu) ~ dim )++-- | Check if the 'DefaultLCSU' can convert into the given one, at the given+-- dimension.+type family DefaultConvertibleLCSU_D (dim :: *) (l :: LCSU *) :: Constraint where+ DefaultConvertibleLCSU_D dim l =+ ( ValidDL (DimFactorsOf dim) DefaultLCSU+ , ConvertibleLCSUs (DimFactorsOf dim) DefaultLCSU l )++-- | Check if the 'DefaultLCSU' can convert into the given one, at the given+-- unit.+type family DefaultConvertibleLCSU_U (unit :: *) (l :: LCSU *) :: Constraint where+ DefaultConvertibleLCSU_U unit l =+ DefaultConvertibleLCSU_D (DimOfUnit unit) l
+ Data/Metrology/Z.hs view
@@ -0,0 +1,158 @@+{- Data/Metrology/Z.hs+ + The units Package+ Copyright (c) 2013 Richard Eisenberg+ eir@cis.upenn.edu++ This file contains a definition of integers at the type-level, in terms+ of a promoted datatype 'Z'.+-}++{-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, UndecidableInstances,+ GADTs, PolyKinds, TemplateHaskell, ScopedTypeVariables,+ EmptyCase #-}+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}++-----------------------------------------------------------------------------+-- |+-- Module : Data.Metrology.Z+-- Copyright : (C) 2013 Richard Eisenberg+-- License : BSD-style (see LICENSE)+-- Maintainer : Richard Eisenberg (eir@cis.upenn.edu)+-- Stability : experimental+-- Portability : non-portable+--+-- This module defines a datatype and operations to represent type-level+-- integers. Though it's defined as part of the units package, it may be+-- useful beyond dimensional analysis. If you have a compelling non-units+-- use of this package, please let me (Richard, @eir@ at @cis.upenn.edu@)+-- know.+-----------------------------------------------------------------------------++module Data.Metrology.Z where++import Data.Singletons.TH++-- | The datatype for type-level integers.+$(singletons [d| data Z = Zero | S Z | P Z deriving Eq |])++-- | Convert a 'Z' to an 'Int'+zToInt :: Z -> Int+zToInt Zero = 0+zToInt (S z) = zToInt z + 1+zToInt (P z) = zToInt z - 1++-- | Add one to an integer+type family Succ (z :: Z) :: Z where+ Succ Zero = S Zero+ Succ (P z) = z+ Succ (S z) = S (S z)++-- | Subtract one from an integer+type family Pred (z :: Z) :: Z where+ Pred Zero = P Zero+ Pred (P z) = P (P z)+ Pred (S z) = z++infixl 6 #++-- | Add two integers+type family (a :: Z) #+ (b :: Z) :: Z where+ Zero #+ z = z+ (S z1) #+ (S z2) = S (S (z1 #+ z2))+ (S z1) #+ Zero = S z1+ (S z1) #+ (P z2) = z1 #+ z2+ (P z1) #+ (S z2) = z1 #+ z2+ (P z1) #+ Zero = P z1+ (P z1) #+ (P z2) = P (P (z1 #+ z2))++infixl 6 #-+-- | Subtract two integers+type family (a :: Z) #- (b :: Z) :: Z where+ z #- Zero = z+ (S z1) #- (S z2) = z1 #- z2+ Zero #- (S z2) = P (Zero #- z2)+ (P z1) #- (S z2) = P (P (z1 #- z2))+ (S z1) #- (P z2) = S (S (z1 #- z2))+ Zero #- (P z2) = S (Zero #- z2)+ (P z1) #- (P z2) = z1 #- z2++infixl 7 #*+-- | Multiply two integers+type family (a :: Z) #* (b :: Z) :: Z where+ Zero #* z = Zero+ (S z1) #* z2 = (z1 #* z2) #+ z2+ (P z1) #* z2 = (z1 #* z2) #- z2++-- | Negate an integer+type family NegZ (z :: Z) :: Z where+ NegZ Zero = Zero+ NegZ (S z) = P (NegZ z)+ NegZ (P z) = S (NegZ z)++-- | Divide two integers+type family (a :: Z) #/ (b :: Z) :: Z where+ Zero #/ b = Zero+ a #/ (P b') = NegZ (a #/ (NegZ (P b')))+ a #/ b = ZDiv b b a++-- | Helper function for division+type family ZDiv (counter :: Z) (n :: Z) (z :: Z) :: Z where+ ZDiv One n (S z') = S (z' #/ n)+ ZDiv One n (P z') = P (z' #/ n)+ ZDiv (S count') n (S z') = ZDiv count' n z'+ ZDiv (S count') n (P z') = ZDiv count' n z'++-- | Less-than comparison+type family (a :: Z) < (b :: Z) :: Bool where+ Zero < Zero = False+ Zero < (S n) = True+ Zero < (P n) = False+ (S n) < Zero = False+ (S n) < (S n') = n < n'+ (S n) < (P n') = False+ (P n) < Zero = True+ (P n) < (S n') = True+ (P n) < (P n') = n < n'++type One = S Zero+type Two = S One+type Three = S Two+type Four = S Three+type Five = S Four++type MOne = P Zero+type MTwo = P MOne+type MThree = P MTwo+type MFour = P MThree+type MFive = P MFour++-- | This is the singleton value representing @Zero@ at the term level and+-- at the type level, simultaneously. Used for raising units to powers.+pZero = SZero+pOne = SS pZero+pTwo = SS pOne+pThree = SS pTwo+pFour = SS pThree+pFive = SS pFour++pMOne = SP pZero+pMTwo = SP pMOne+pMThree = SP pMTwo+pMFour = SP pMThree+pMFive = SP pMFour++-- | Add one to a singleton @Z@.+pSucc :: Sing z -> Sing (Succ z)+pSucc SZero = pOne+pSucc (SS z') = SS (SS z')+pSucc (SP z') = z'++-- | Subtract one from a singleton @Z@.+pPred :: Sing z -> Sing (Pred z)+pPred SZero = pMOne+pPred (SS z') = z'+pPred (SP z') = SP (SP z')++-- | Convert a singleton @Z@ to an @Int@.+szToInt :: Sing (z :: Z) -> Int+szToInt = zToInt . fromSing
README.md view
@@ -4,11 +4,36 @@ The _units_ package provides a mechanism for compile-time dimensional analysis in Haskell programs. It defines an embedded type system based on units-of-measure. The units defined are fully extensible, and need not relate-to physical properties. In fact, the core package defines only one built-in-unit: Scalar. The package supports defining multiple inter-convertible units,-such as Meter and Foot. When extracting a number from a dimensioned quantity,-the desired unit must be specified, and the value is converted into that unit.+to physical properties. As a matter of convenience only, the core package+defines the dimensions and units for the international system (SI), and you+can find many additional units and dimensions in package _units-extra_. +The package supports defining multiple inter-convertible units, such+as `Meter` and `Foot`. When extracting a numerical value from a quantity,+the desired unit must be specified, and the value is converted into+that unit.++The laws of nature have dimensions, and they hold true regardless of the units+used. For example, the gravitational force between two bodies is+`(gravitational constant) * (mass 1) * (mass 2) / (distance between body 1 and+2)^2`, regardless of whether the distance is given in meters or feet+or centimeters. In other words, every law of nature is unit-polymorphic.++The _units_ package supports unit-polymorphic programs through the coherent+system of units (CSU) mechanism. A CSU is essentially a mapping from+dimensions (such as length or mass) to the units (such as meters or+kilograms). All dimensioned quantities (generally just called quantities) are+expressed using the `Qu` type. The `Qu` type constructor takes a (perhaps+compound) dimension, a CSU and a numerical value type as arguments.+Internally, the quantity is stored as a number in the units as specified in+the CSU -- this may matter if you are worried about rounding errors.+In the sequence of computations that works within one CSU,+there is no unit conversion. Unit conversions are needed only when+putting values in and out of quantities, or converting between two different+CSUs.+++ User contributions ------------------ @@ -29,58 +54,55 @@ dependents, but it probably won't be very useful to you. I hope that this list grows over time. - - __`Data.Dimensions`__+ - __`Data.Metrology`__ This is the main exported module. It exports all the necessary functionality for you to build your own set of units and operate with them. All modules implicitly depend on this one. - - __`Data.Dimensions.Poly`__-- This module exports some more definitions that may be useful when writing- functions polymorphic over the choice of dimension. These functions are- sometimes challenging (or perhaps impossible) to write, as the system is- designed more with _monomorphic_ use than polymorphic use.-- - __`Data.Dimensions.Unsafe`__+ - __`Data.Metrology.Unsafe`__ This module exports the constructor for the central datatype that stores- dimensioned quantities. With this constructor, you can arbitrarily change+ quantities. With this constructor, you can arbitrarily change units! Use at your peril. - - __`Data.Dimensions.Show`__+ - __`Data.Metrology.Show`__ - This module defines a `Show` instance for dimensioned quantities, printing+ This module defines a `Show` instance for quantities, printing out the number stored along with its canonical dimension. This behavior may not be the best for every setting, so it is exported separately. - - __`Data.Dimensions.SI`__+ - __`Data.Metrology.SI`__ This module exports unit definitions for the [SI][] system of units, re-exporting the three modules below. [SI]: http://en.wikipedia.org/wiki/International_System_of_Units - - __`Data.Dimensions.SI.Units`__+ - __`Data.Metrology.SI.Units`__ This module exports only the SI units, such as `Meter` and `Ampere`. - - __`Data.Dimensions.SI.Types`__+ - __`Data.Metrology.SI.Types`__ - This module exports several useful types for use with the SI.Units module,- which it depends on. For example, `Length` is the type of dimensioned- quantities made with `Meter`s.+ This module exports pre-defined unit type synonyms for SI dimensions,+ convenient for use with the SI.Units module.+ For example, `Length` is the type of+ quantities with unit `Meter`s and with numerical type `Double`. - - __`Data.Dimensions.SI.Prefixes`__+ - __`Data.Metrology.SI.Prefixes`__ This module exports the SI prefixes. Note that this does *not* depend on any of the other SI modules -- you can use these prefixes with any system of units. + Examples ======== +**NOTE: THIS IS OUT OF DATE.**+ Unit definitions ---------------- @@ -99,8 +121,8 @@ instance Show Foot where show _ = "ft" - type Length = MkDim Meter -- we will manipulate Lengths- type Length' = MkDim Foot -- this is the *same* as Length+ type Length = MkQu Meter -- we will manipulate Lengths+ type Length' = MkQu Foot -- this is the *same* as Length extend :: Length -> Length -- a function over lengths extend x = dim $ x .+ (1 % Meter) -- more on this later@@ -128,14 +150,14 @@ it _must not_ inspect that parameter. Internally, it will be passed `undefined` quite often. -The `MkDim` type synonym makes a dimensioned quantity for a given unit. Note-that `Length` and `Length'` are _the same type_. The `MkDim` machinery notices+The `MkQu` type synonym makes a quantity for a given unit. Note+that `Length` and `Length'` are _the same type_. The `MkQu` machinery notices that these two are inter-convertible and will produce the same dimensioned quantity. Note that, as you can see in the function examples at the end, it is necessary-to specify the choice of unit when creating a dimensioned quantity or-extracting from a dimensioned quantity. Thus, other than thinking about the+to specify the choice of unit when creating a quantity or+extracting from a quantity. Thus, other than thinking about the vagaries of floating point wibbles and the `Show` instance, it is _completely irrelevant_ which unit is canonical. The type `Length` defined here could be used equally well in a program that deals exclusively in feet as it could in a@@ -187,30 +209,30 @@ instance Show Second where show _ = "s" - type Time = MkDim Second+ type Time = MkQu Second Units can be multiplied and divided with the operators `:*` and `:/`, at either the term or type level. For example: type MetersPerSecond = Meter :/ Second- type Velocity1 = MkDim MetersPerSecond+ type Velocity1 = MkQu MetersPerSecond speed :: Velocity1 speed = 20 % (Meter :/ Second) The _units_ package also provides combinators "%*" and "%/" to combine the-types of dimensioned quantities.+types of quantities. type Velocity2 = Length %/ Time -- same type as Velocity1 There are also exponentiation combinators `:^` (for units) and `%^` (for-dimensioned quantities) to raise to a power. To represent the power, the+quantities) to raise to a power. To represent the power, the _units_ package exports `Zero`, positive numbers `One` through `Five`, and negative numbers `MOne` through `MFive`. At the term level, precede the number with a `p` (mnemonic: "power"). For example: type MetersSquared = Meter :^ Two- type Area1 = MkDim MetersSquared+ type Area1 = MkQu MetersSquared type Area2 = Length %^ Two -- same type as Area1 roomSize :: Area1@@ -225,14 +247,14 @@ Dimension-safe cast ------------------- -The haddock documentation shows the term-level dimensioned quantity+The haddock documentation shows the term-level quantity combinators. The only one deserving special mention is `dim`, the dimension-safe cast operator. Expressions written with the _units_ package can have their types inferred. This works just fine in practice, but the types are terrible, unfortunately. Much better is to use top-level annotations (using abbreviations like `Length` and `Time`) for your functions. However, it may happen that the inferred type of your expression and the given type of your-function may not exactly match up. This is because dimensioned quantities have+function may not exactly match up. This is because quantities have a looser notion of type equality than Haskell does. For example, "meter * second" should be the same as "second * meter", even though these are in different order. The `dim` function checks (at compile time) to make sure its
+ Test/Travel.hs view
@@ -0,0 +1,54 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE TypeOperators #-}++module Main where++import Data.Metrology+import Data.Metrology.SI.Poly+import Data.Metrology.Imperial.Types (Imperial)+import Data.Metrology.Imperial.Units+import Data.Metrology.Show+import qualified Data.Metrology.SI.Dims as D++type PerArea lcsu n = MkQu_DLN (D.Area :^ MOne) lcsu n++fromGLtoED :: MkQu_DLN D.Length Imperial Float+fromGLtoED = 46.5 % Mile++fuelEfficiency :: PerArea Imperial Float+fuelEfficiency = 40 % (Mile :/ Gallon)++gasolineDensity :: MkQu_DLN D.Density Imperial Float+gasolineDensity = 7.29 % (Pound :/ Gallon)++gasolineWeight :: (Fractional f) + => MkQu_DLN D.Length su f -> PerArea su f -> MkQu_DLN D.Density su f -> MkQu_DLN D.Mass su f+gasolineWeight len0 ef0 den0 = len0 |/| ef0 |*| den0+++main :: IO ()+main = do+ putStrLn $ fromGLtoED `showIn` Mile+ putStrLn $ fuelEfficiency `showIn` Mile :/ Gallon+ putStrLn $ gasolineDensity `showIn` Pound :/ Gallon+ putStrLn $ show $ gasolineWeight fromGLtoED fuelEfficiency gasolineDensity ++ putStrLn ""+ putStrLn $ fromGLtoED `showIn` (kilo Meter)+ putStrLn $ fuelEfficiency `showIn` kilo Meter :/ Liter+ putStrLn $ gasolineDensity `showIn` kilo Gram :/ Liter+ putStrLn $ show $ (gasolineWeight + (convert fromGLtoED) (convert fuelEfficiency) (convert gasolineDensity) :: MkQu_DLN D.Mass SI Float)++{---- Execution result ---+46.5 mi+39.999996 mi/gal+7.29 lb/gal+8.474626 lb++74.834496 km+14.160248 km/l+0.7273698 kg/l+3.8440251 kg+-}
units.cabal view
@@ -1,11 +1,11 @@ name: units-version: 1.1+version: 2.0 cabal-version: >= 1.10 synopsis: A domain-specific type system for dimensional analysis homepage: http://www.cis.upenn.edu/~eir/packages/units category: Math author: Richard Eisenberg <eir@cis.upenn.edu>-maintainer: Richard Eisenberg <eir@cis.upenn.edu>+maintainer: Richard Eisenberg <eir@cis.upenn.edu>, Takayuki Muranushi <muranushi@gmail.com> bug-reports: https://github.com/goldfirere/units/issues stability: experimental extra-source-files: README.md, CHANGES.md@@ -13,31 +13,75 @@ license-file: LICENSE build-type: Simple description:- The units package provides a mechanism for compile-time dimensional analysis- in Haskell programs. It defines an embedded type system based on- units-of-measure. The units defined are fully extensible, and need not relate- to physical properties. In fact, the core package defines only one built-in- unit: Scalar. The package supports defining multiple inter-convertible units,- such as Meter and Foot. When extracting a number from a dimensioned quantity,- the desired unit must be specified, and the value is converted into that unit. - The Haddock documentation is insufficient for using the units package. Please- see the README file, available from the package home page.+ The units package provides a mechanism for compile-time+ dimensional analysis in Haskell programs. It defines an embedded+ type system based on units-of-measure. The units defined are fully+ extensible, and need not relate to physical properties. + The package supports defining multiple inter-convertible units,+ such as Meter and Foot. When extracting a number from a+ dimensioned quantity, the desired unit must be specified, and the+ value is converted into that unit.++ If you are looking for specific systems of units (such as SI),+ please see the `units-defs` package.++ The Haddock documentation is insufficient for using the units+ package. Please see the README file, available from the package+ home page.+ source-repository this type: git location: https://github.com/goldfirere/units.git- tag: v1.1+ tag: v2.0 library build-depends: base >= 4.7 && < 5,- singletons >= 0.9- exposed-modules: Data.Dimensions, Data.Dimensions.Show,- Data.Dimensions.Poly, Data.Dimensions.Unsafe,- Data.Dimensions.SI, Data.Dimensions.SI.Prefixes,- Data.Dimensions.SI.Types, Data.Dimensions.SI.Units- other-modules: Data.Dimensions.Dim, Data.Dimensions.DimSpec,- Data.Dimensions.Units, Data.Dimensions.UnitCombinators,- Data.Dimensions.Z+ singletons >= 0.9 && < 1+ exposed-modules: + Data.Metrology, + Data.Metrology.Internal,+ Data.Metrology.Show,+ Data.Metrology.Unsafe,+ Data.Metrology.Z,+ Data.Metrology.Set++ other-modules: + Data.Metrology.Factor,+ Data.Metrology.LCSU,+ Data.Metrology.Quantity, + Data.Metrology.Dimensions,+ Data.Metrology.Units,+ Data.Metrology.Combinators,+ Data.Metrology.Validity++ -- cabal now recommends that TH be explicitly listed in cabal files+ default-extensions: TemplateHaskell+ default-language: Haskell2010+++-- Here are some test scripts for `units`. Since `units` is a+-- type-level library and mainly works at compile time, we're just+-- testing if these programs compiles and runs properlly.+-- +-- !IMPORTANT! You need to type+--+-- > make prepare-test+--+-- once, to bring the specific unit definitions from `units-defs`+-- into scope to run the tests.++Test-Suite travel+ Type: exitcode-stdio-1.0+ Hs-Source-Dirs: Test+ Ghc-Options: -Wall+ Main-Is: Travel.hs+ Other-Modules: + + Build-Depends: + base+ , units+ default-language: Haskell2010