units (empty) → 1.0.0
raw patch · 17 files changed
+1759/−0 lines, 17 filesdep +basesetup-changed
Dependencies added: base
Files
- CHANGES.md +4/−0
- LICENSE +27/−0
- README.md +251/−0
- Setup.hs +2/−0
- src/Data/Dimensions.hs +140/−0
- src/Data/Dimensions/Dim.hs +148/−0
- src/Data/Dimensions/DimSpec.hs +192/−0
- src/Data/Dimensions/Internal.hs +38/−0
- src/Data/Dimensions/SI.hs +180/−0
- src/Data/Dimensions/SI/Prefixes.hs +217/−0
- src/Data/Dimensions/SI/Types.hs +56/−0
- src/Data/Dimensions/Show.hs +71/−0
- src/Data/Dimensions/TypePrelude.hs +45/−0
- src/Data/Dimensions/UnitCombinators.hs +72/−0
- src/Data/Dimensions/Units.hs +108/−0
- src/Data/Dimensions/Z.hs +165/−0
- units.cabal +43/−0
+ CHANGES.md view
@@ -0,0 +1,4 @@+Version 1.0+===========++ * First release
+ LICENSE view
@@ -0,0 +1,27 @@+Copyright (c) 2013, Richard Eisenberg+All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++1. Redistributions of source code must retain the above copyright notice, this+list of conditions and the following disclaimer.++2. Redistributions in binary form must reproduce the above copyright notice,+this list of conditions and the following disclaimer in the documentation+and/or other materials provided with the distribution.++3. Neither the name of the author nor the names of its contributors may be+used to endorse or promote products derived from this software without+specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"+AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR+SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER+CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,+OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,251 @@+units+=====++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.++Limitations:+- The _units_ package does not easily allow users to write code polymorphic+ in the chosen units. For example, a `sum` function that adds together a+ homogeneous list of dimensioned quantities is not straightforward. The+ package exports its internals to allow clients to try to get these working,+ but it is generally hard to do. However, monomorphic functions are easy.++- The _units_ package is not generalized over number representation: it forces+ client code to use `Double`. It wouldn't be hard to generalize, though, but+ it would add a fair amount of extra cruft here and there. Shout (to+ `eir@cis.upenn.edu`) if this is important to you.++User contributions+------------------++It is easy to imagine any number of built-in facilities that would go well+with this package (sets of definitions of units for various systems, vector+operations, a suite of polymorphic functions that are commonly needed but hard+to define, etc.). Yet, I (Richard) don't have the time to imagine or write all+of these. If you write code that is sufficiently general and might want to be+included with this package (but you don't necessarily want to create your own+new package), please write me!++Modules+-------++The _units_ package exports several modules. For any given project, you will+include some set of these modules. There are dependency relationships+between them. Of course, you're welcome to `import` a module without its+dependents, but it probably won't be very useful to you. I hope that this list+grows over time.++ - __`Data.Dimensions`__++ 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.Show`__++ This module defines a `Show` instance for dimensioned 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`__++ This module exports unit definitions for the [SI][] system of units.++[SI]: http://en.wikipedia.org/wiki/International_System_of_Units++ - __`Data.Dimensions.SI.Prefixes`__++ This module exports the SI prefixes. Note that this does *not* depend+ on `Data.Dimensions.SI` -- you can use these prefixes with any system of+ units.++ - __`Data.Dimensions.SI.Types`__++ This module exports several useful types for use with the SI package,+ which it depends on. For example, `Length` is the type of dimensioned+ quantities made with `Meter`s.++Examples+========++Unit definitions+----------------++Here is how to define two inter-convertible units:++ data Meter = Meter -- each unit is a datatype that acts as its own proxy+ instance Unit Meter where -- declare Meter as a Unit+ type BaseUnit Meter = Canonical -- Meters are "canonical"+ instance Show Meter where -- Show instances are optional but useful+ show _ = "m" -- do *not* examine the argument!++ data Foot = Foot+ instance Unit Foot where+ type BaseUnit Foot = Meter -- Foot is defined in terms of Meter+ conversionRatio _ = 0.3048 -- do *not* examine the argument!+ instance Show Foot where+ show _ = "ft"++ type Length = MkDim Meter -- we will manipulate Lengths+ type Length' = MkDim Foot -- this is the *same* as Length++ extend :: Length -> Length -- a function over lengths+ extend x = dim $ x .+ (1 % Meter) -- more on this later++ inMeters :: Length -> Double -- extract the # of meters+ inMeters = (# Meter) -- more on this later++Let's pick this apart. The `data Meter = Meter` declaration creates both the+type `Meter` and a term-level proxy for it. It would be possible to get away+without the proxies and lots of type annotations, but who would want to?+Then, we define an instance of `Unit` to make `Meter` into a proper unit.+The `Unit` class is primarily responsible for handling unit conversions.+In the case of `Meter`, we define that as the _canonical_ unit of length, meaning+that all lengths will internally be stored in meters. It also means that we+don't need to define a conversion ratio for meters.++We also include a `Show` instance for `Meter` so that lengths can be printed+easily. If you don't need to `show` your lengths, there is no need for this+instance.++When defining `Foot`, we say that its `BaseUnit` is `Meter`, meaning that+`Foot` is inter-convertible with `Meter`. We also must define the conversion+ratio, which is the number of meters in a foot. Note that the+`conversionRatio` method must take a parameter to fix its type parameter, but+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+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+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+program with meters.++As a tangential note: I have experimented both with definitions like `data+Meter = Meter` and `data Meter = Meters` (note the `s` at the end). The second+often flows more nicely in code, but the annoyance of having to remember+whether I was at the type level or the term level led me to use the former in+my work.++Prefixes+--------++Here is how to define the "kilo" prefix:++ data Kilo = Kilo+ instance UnitPrefix Kilo where+ multiplier _ = 1000++ kilo :: unit -> Kilo :@ unit+ kilo = (Kilo :@)++We define a prefix in much the same way as an ordinary unit, with a datatype+and a constructor to serve as a proxy. Instead of the `Unit` class, though,+we use the `UnitPrefix` class, which contains a `multiplier` method. As with+other methods, this may *not* inspect its argument.++Due to the way units are encoded, it is necessary to explicitly apply prefixes+with the `:@` combinator (available at both the type and term level). It is often+convenient to then define a function like `kilo` to make the code flow more+naturally:++ longWayAway :: Length+ longWayAway = 150 % kilo Meter++ longWayAwayInMeters :: Double+ longWayAwayInMeters = longWayAway # Meter -- 150000.0++Unit combinators+----------------++There are several ways of combining units to create other units. Let's also+have a unit of time:++ data Second = Second+ instance Unit Second where+ type BaseUnit Second = Canonical+ instance Show Second where+ show _ = "s"++ type Time = MkDim 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++ speed :: Velocity1+ speed = 20 % (Meter :/ Second)++The _units_ package also provides combinators "%*" and "%/" to combine the+types of dimensioned 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+_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 Area2 = Length %^ Two -- same type as Area1++ roomSize :: Area1+ roomSize = 100 % (Meter :^ pTwo)++ roomSize' :: Area1+ roomSize' = 100 % (Meter :* Meter)+ +These operations have no defined inverses, though I don't think they would be+hard to define. Shout if you need that functionality.++Note that addition and subtraction on units does not make physical sense, so+those operations are not provided.++Dimension-safe cast+-------------------++The haddock documentation shows the term-level dimensioned 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+a looser notion of type equality than Haskell does. For example, "meter *+second" should be the same as "second * meter", even those these are in+different order. The `dim` function checks (at compile time) to make sure its+input type and output type represent the same underlying dimension and then+performs a cast from one to the other. When providing type annotations, it is+good practice to start your function with a `dim $` to prevent the possibility+of type errors. For example, say we redefine velocity a different way:++ type Velocity3 = Scalar %/ Time %* Length+ addVels :: Velocity1 -> Velocity1 -> Velocity3+ addVels v1 v2 = dim $ v1 .+ v2++This is a bit contrived, but it demonstrates the point. Without the `dim`, the+`addVels` function would not type-check. Because `dim` needs to know its+_result_ type to type-check, it should only be used at the top level, such as+here, where there is a type annotation to guide it.++Note that `dim` is _always_ dimension-safe -- it will not convert a time to a+length!+
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ src/Data/Dimensions.hs view
@@ -0,0 +1,140 @@+{- 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 #-}++{-| 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+ <https://github.com/goldfirere/units/blob/master/README.md>.++ 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.++ The type @Dim@, which is not exported, is the type used internally to+ represent dimensioned quantities.++ 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, 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 :: Dim '[]+unity = Dim 1++-- | The number 0, expressed as a polymorphic dimensioned quantity.+-- The polymorphism allows it to be added to any dimensioned quantity+-- without fuss.+zero :: Dim '[DAny]+zero = Dim 0++-- | Dimension-safe cast. See the README for more info.+dim :: (d @~ e) => Dim d -> Dim 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 Double into a unitless dimensioned quantity+scalar :: Double -> Dim '[]+scalar = Dim
+ src/Data/Dimensions/Dim.hs view
@@ -0,0 +1,148 @@+{- 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 GHC.TypeLits ( Sing )++import Data.Dimensions.DimSpec+import Data.Dimensions.Z++-------------------------------------------------------------+--- Internal ------------------------------------------------+-------------------------------------------------------------++-- | Dim adds a dimensional annotation to a Double. This is the+-- representation for all dimensioned quantities.+newtype Dim (a :: [DimSpec *]) = Dim Double++-------------------------------------------------------------+--- User-facing ---------------------------------------------+-------------------------------------------------------------++infixl 6 .++-- | Add two compatible dimensioned quantities+(.+) :: (d1 @~ d2) => Dim d1 -> Dim d2 -> Dim (ChooseFrom d1 d2)+(Dim a) .+ (Dim b) = Dim (a + b)++infixl 6 .-+-- | Subtract two compatible dimensioned quantities+(.-) :: (d1 @~ d2) => Dim d1 -> Dim d2 -> Dim (ChooseFrom d1 d2)+(Dim a) .- (Dim b) = Dim (a - b)++infixl 7 .*+-- | Multiply two dimensioned quantities+(.*) :: Dim a -> Dim b -> Dim (Normalize (a @+ b))+(Dim a) .* (Dim b) = Dim (a * b)++infixl 7 ./+-- | Divide two dimensioned quantities+(./) :: Dim a -> Dim b -> Dim (Normalize (a @- b))+(Dim a) ./ (Dim b) = Dim (a / b)++infixr 8 .^+-- | Raise a dimensioned quantity to a power known at compile time+(.^) :: Dim a -> Sing z -> Dim (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 => Sing z -> Dim a -> Dim (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) => Dim d1 -> Dim d2 -> Bool+(Dim a) .< (Dim b) = a < b++infix 4 .>+-- | Check if one dimensioned quantity is greater than a compatible one+(.>) :: (d1 @~ d2) => Dim d1 -> Dim 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) => Dim d1 -> Dim 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) => Dim d1 -> Dim d2 -> Bool+(Dim a) .>= (Dim b) = a >= b++-- | Compare two compatible dimensioned quantities for equality+dimEq :: (d0 @~ d1, d0 @~ d2) => Dim d0 -- ^ If the difference between the next+ -- two arguments are less than this + -- amount, they are considered equal+ -> Dim d1 -> Dim 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) => Dim d0 -- ^ If the difference between the next+ -- two arguments are less than this + -- amount, they are considered equal+ -> Dim d1 -> Dim d2 -> Bool+dimNeq (Dim epsilon) (Dim a) (Dim b) = abs(a-b) >= epsilon++-- | Square a dimensioned quantity+dimSqr :: Dim a -> Dim (Normalize (a @+ a))+dimSqr x = x .* x++-- | Take the square root of a dimensioned quantity+dimSqrt :: Dim a -> Dim (a @/ Two)+dimSqrt = nthRoot pTwo++-- | Take the cube root of a dimensioned quantity+dimCubeRoot :: Dim a -> Dim (a @/ Three)+dimCubeRoot = nthRoot pThree++infixl 7 *.+-- | Multiply a dimensioned quantity by a scalar @Double@+(*.) :: Double -> Dim a -> Dim a+a *. (Dim b) = Dim (a * b)++-------------------------------------------------------------+--- Instances -----------------------------------------------+-------------------------------------------------------------++deriving instance Eq (Dim '[])+deriving instance Ord (Dim '[])+deriving instance Num (Dim '[])+deriving instance Real (Dim '[])+deriving instance Fractional (Dim '[])+deriving instance Floating (Dim '[])+deriving instance RealFrac (Dim '[])+deriving instance RealFloat (Dim '[])++-------------------------------------------------------------+--- 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 d1) %* (Dim d2) = Dim (d1 @+ d2)++infixl 7 %/+-- | Divide two dimension types to produce a new one+type family (d1 :: *) %/ (d2 :: *) :: *+type instance (Dim d1) %/ (Dim d2) = Dim (d1 @- d2)++infixr 8 %^+-- | Exponentiate a dimension type to an integer+type family (d :: *) %^ (z :: Z) :: *+type instance (Dim d) %^ z = Dim (d @* z)++
+ src/Data/Dimensions/DimSpec.hs view
@@ -0,0 +1,192 @@+{- 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.TypePrelude+import Data.Dimensions.Z++-- | This will only be used at the kind level.+-- It either holds a dimension with its exponent, or the special constant DAny,+-- which can be any combination of dimensions at any exponents. It is used to+-- represent multiplying by 0 somewhere.+data DimSpec star = D star Z | DAny++----------------------------------------------------------+--- 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+ DAny $= DAny = True+ 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+ 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)++-- | Check if a @[DimSpec *]@ has a 'DAny' inside it+type family HasAny (lst :: [DimSpec *]) :: Bool where+ HasAny '[] = False+ HasAny (DAny ': t) = True+ HasAny (h ': t) = HasAny t++infix 4 @~+-- | Check if two @[DimSpec *]@s should be considered to be equal+type family (a :: [DimSpec *]) @~ (b :: [DimSpec *]) :: Constraint where+ a @~ b = If (HasAny a :||: HasAny b)+ (() :: Constraint)+ (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++-- | If a @[DimSpec *]@ has a 'DAny', collapse the whole list to one 'DAny'.+-- Otherwise, normalize the list by removing exponents of 0.+type family Normalize (d :: [DimSpec *]) :: [DimSpec *] where+ Normalize d = If (HasAny d) '[DAny] (Normalize' d)++-- | Given two @[DimSpec *]@s, return the one that lacks a 'DAny', if there is one.+type family ChooseFrom (d1 :: [DimSpec *]) (d2 :: [DimSpec *]) :: [DimSpec *] where+ ChooseFrom d d = Normalize d+ ChooseFrom '[DAny] d2 = Normalize d2 -- common cases+ ChooseFrom d1 '[DAny] = Normalize d1+ ChooseFrom d1 d2 = Normalize (If (HasAny d1) d2 d1)++----------------------------------------------------------+--- 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+ (DAny ': t1) @@+ b = '[DAny]+ a @@+ (DAny ': t2) = '[DAny]+ ((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+ (DAny ': t1) @@- b = '[DAny]+ a @@- (DAny ': t2) = '[DAny]+ ((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)+ NegDim DAny = DAny++-- | 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)+ (DAny ': t) @* power = DAny ': (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)+ (DAny ': t) @/ z = DAny ': (t @/ z)
+ src/Data/Dimensions/Internal.hs view
@@ -0,0 +1,38 @@+{- Data/Dimensions/Internal.hs++ The units Package+ Copyright (c) 2013 Richard Eisenberg+ eir@cis.upenn.edu+-}++{-# LANGUAGE ExplicitNamespaces #-}++{-| This module gathers and exports all parts of the units package that might+ be useful, even when going past the abstraction layer of the package.++ With the exports from this module, it is possible to perform unsafe+ operations that do not respect the rules of dimensional analysis. Use with+ caution.++ Additionally, no attempt will be made to keep the exports of this module+ backward compatible.+-}++module Data.Dimensions.Internal (+ -- * The @Dim@ type+ Dim(..),++ -- * Manipulating dimension specifications+ DimSpec(..), type ($=), Extract, Reorder, HasAny, type (@~),+ Normalize, ChooseFrom,++ type (@+), type (@-), NegDim, NegList, type (@*), type (@/),++ -- * Generally-useful type operations+ Fst, Snd, If, (:&&:), (:||:), (:=:)++ ) where++import Data.Dimensions.Dim+import Data.Dimensions.TypePrelude+import Data.Dimensions.DimSpec
+ src/Data/Dimensions/SI.hs view
@@ -0,0 +1,180 @@+{- Data/Dimensions/SI.hs++ The units Package+ Copyright (c) 2013 Richard Eisenberg+ eir@cis.upenn.edu++ This module defines the units from the SI system, as put forth here:+ http://www.bipm.org/en/si/+-}++{-# LANGUAGE TypeFamilies, TypeOperators #-}++{-| 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 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"+
+ src/Data/Dimensions/SI/Prefixes.hs view
@@ -0,0 +1,217 @@+{- Data/Dimensions/SI/Prefixes.hs++ The units Package+ Copyright (c) 2013 Richard Eisenberg+ eir@cis.upenn.edu++ This module defines the prefixes from the SI system, as put forth here:+ http://www.bipm.org/en/si/+-}++{-# LANGUAGE TypeOperators #-}++-- | 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 :@)
+ src/Data/Dimensions/SI/Types.hs view
@@ -0,0 +1,56 @@+{- Data/Dimensions/SI/Types.hs++ The units Package+ Copyright (c) 2013 Richard Eisenberg+ eir@cis.upenn.edu+-}++{-# LANGUAGE TypeOperators #-}++-- | This module defines type synonyms for SI units.++module Data.Dimensions.SI.Types where++import Data.Dimensions+import Data.Dimensions.SI++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
+ src/Data/Dimensions/Show.hs view
@@ -0,0 +1,71 @@+{- Data/Dimensions/Show.hs++ The units Package+ Copyright (c) 2013 Richard Eisenberg+ eir@cis.upenn.edu++ This file defines Show instances for dimensioned quantities.+-}++{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, FlexibleInstances,+ ScopedTypeVariables #-}++-- | 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.Typeable (Proxy(..))+import Data.List+import GHC.TypeLits (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 (Dim dims) where+ show (Dim d) = (show d ++ showDimSpec (Proxy :: Proxy dims))
+ src/Data/Dimensions/TypePrelude.hs view
@@ -0,0 +1,45 @@+{- Data/Dimensions/TypePrelude.hs++ The units Package+ Copyright (c) 2013 Richard Eisenberg+ eir@cis.upenn.edu++ Type-level prelude-like operations.+ + Note to self: Consider using the type-prelude package instead.+-}++{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, TypeOperators #-}++module Data.Dimensions.TypePrelude where++-- | Extract the first element of a pair+type family Fst (x :: (a,b)) :: a+type instance Fst '(a,b) = a++-- | Extract the second element of a pair+type family Snd (x :: (a,b)) :: b+type instance Snd '(a,b) = b++-- | Type-level conditional+type family If (switch :: Bool) (true :: k) (false :: k) :: k where+ If True t f = t+ If False t f = f++infixr 3 :&&:+-- | Type-level "and"+type family (a :: Bool) :&&: (b :: Bool) :: Bool where+ False :&&: a = False+ True :&&: a = a++infixr 2 :||:+-- | Type-level "or"+type family (a :: Bool) :||: (b :: Bool) :: Bool where+ False :||: a = a+ True :||: a = True++infix 4 :=:+-- | Type-level equality over @*@.+type family (a :: *) :=: (b :: *) :: Bool where+ (a :: *) :=: (a :: *) = True+ (a :: *) :=: (b :: *) = False
+ src/Data/Dimensions/UnitCombinators.hs view
@@ -0,0 +1,72 @@+{- 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 GHC.TypeLits ( 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))++infix 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)
+ src/Data/Dimensions/Units.hs view
@@ -0,0 +1,108 @@+{- 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.Dimensions.TypePrelude++-- | 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 capable of storing a value of a given unit.+-- For example:+--+-- > type Length = MkDim Meter+type MkDim unit = Dim (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)
+ src/Data/Dimensions/Z.hs view
@@ -0,0 +1,165 @@+{- 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 #-}++-- | This module defines a datatype and operations to represent type-level+-- integers. Though it's defined as part of the unitss 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 GHC.TypeLits ( Sing, SingI(..), SingE(..), KindIs(..) )++-- | The datatype for type-level integers.+data Z = Zero | S Z | P Z++-- | 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++---- Singleton for Z+data instance Sing (z :: Z) where+ SZero :: Sing Zero+ SS :: Sing z -> Sing (S z)+ SP :: Sing z -> Sing (P z)++instance SingI Zero where+ sing = SZero+instance SingI z => SingI (S z) where+ sing = SS sing+instance SingI z => SingI (P z) where+ sing = SP sing++instance SingE (KindParam :: KindIs Z) where+ type DemoteRep (KindParam :: KindIs Z) = Z+ fromSing SZero = Zero+ fromSing (SS z) = S (fromSing z)+ fromSing (SP z) = P (fromSing z)++-- | 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
+ units.cabal view
@@ -0,0 +1,43 @@+name: units+version: 1.0.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>+bug-reports: https://github.com/goldfirere/units/issues+stability: experimental+extra-source-files: README.md, CHANGES.md+license: BSD3+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.++source-repository this+ type: git+ location: https://github.com/goldfirere/units.git+ tag: v1.0.0++library+ build-depends: + base >= 4 && < 5+ exposed-modules: Data.Dimensions, Data.Dimensions.Show,+ Data.Dimensions.Internal,+ Data.Dimensions.SI, Data.Dimensions.SI.Prefixes,+ Data.Dimensions.SI.Types+ other-modules: Data.Dimensions.Dim, Data.Dimensions.DimSpec,+ Data.Dimensions.Units, Data.Dimensions.UnitCombinators,+ Data.Dimensions.TypePrelude, Data.Dimensions.Z+ hs-source-dirs: src+ default-language: Haskell2010