diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,9 +1,20 @@ +Version 1.1 +----------- + +* Added dependency on the singletons library + +* Brought up to date with changes for GHC 7.8 + +* Generalized numerical representation + +* Improved Haddock headers + Version 1.0.1 -============= +------------- * Fixed dependency on base to force compilation with GHC >= 7.7 Version 1.0 -=========== +----------- * First release diff --git a/Data/Dimensions.hs b/Data/Dimensions.hs new file mode 100644 --- /dev/null +++ b/Data/Dimensions.hs @@ -0,0 +1,145 @@ +{- 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 +-- . +-- +-- 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 diff --git a/Data/Dimensions/Dim.hs b/Data/Dimensions/Dim.hs new file mode 100644 --- /dev/null +++ b/Data/Dimensions/Dim.hs @@ -0,0 +1,149 @@ +{- 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) + + diff --git a/Data/Dimensions/DimSpec.hs b/Data/Dimensions/DimSpec.hs new file mode 100644 --- /dev/null +++ b/Data/Dimensions/DimSpec.hs @@ -0,0 +1,166 @@ +{- 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) diff --git a/Data/Dimensions/Poly.hs b/Data/Dimensions/Poly.hs new file mode 100644 --- /dev/null +++ b/Data/Dimensions/Poly.hs @@ -0,0 +1,41 @@ +{-# 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 diff --git a/Data/Dimensions/SI.hs b/Data/Dimensions/SI.hs new file mode 100644 --- /dev/null +++ b/Data/Dimensions/SI.hs @@ -0,0 +1,29 @@ +{-# 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: +-- . +-- +-- 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 + diff --git a/Data/Dimensions/SI/Prefixes.hs b/Data/Dimensions/SI/Prefixes.hs new file mode 100644 --- /dev/null +++ b/Data/Dimensions/SI/Prefixes.hs @@ -0,0 +1,217 @@ +{-# 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 +----------------------------------------------------------------------------- + +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 :@) diff --git a/Data/Dimensions/SI/Types.hs b/Data/Dimensions/SI/Types.hs new file mode 100644 --- /dev/null +++ b/Data/Dimensions/SI/Types.hs @@ -0,0 +1,59 @@ +{-# 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 diff --git a/Data/Dimensions/SI/Units.hs b/Data/Dimensions/SI/Units.hs new file mode 100644 --- /dev/null +++ b/Data/Dimensions/SI/Units.hs @@ -0,0 +1,179 @@ +{-# 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: . +-- +-- 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" + diff --git a/Data/Dimensions/Show.hs b/Data/Dimensions/Show.hs new file mode 100644 --- /dev/null +++ b/Data/Dimensions/Show.hs @@ -0,0 +1,73 @@ +{-# 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)) diff --git a/Data/Dimensions/UnitCombinators.hs b/Data/Dimensions/UnitCombinators.hs new file mode 100644 --- /dev/null +++ b/Data/Dimensions/UnitCombinators.hs @@ -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 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) diff --git a/Data/Dimensions/Units.hs b/Data/Dimensions/Units.hs new file mode 100644 --- /dev/null +++ b/Data/Dimensions/Units.hs @@ -0,0 +1,112 @@ +{- 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) diff --git a/Data/Dimensions/Unsafe.hs b/Data/Dimensions/Unsafe.hs new file mode 100644 --- /dev/null +++ b/Data/Dimensions/Unsafe.hs @@ -0,0 +1,22 @@ +{-# 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 + diff --git a/Data/Dimensions/Z.hs b/Data/Dimensions/Z.hs new file mode 100644 --- /dev/null +++ b/Data/Dimensions/Z.hs @@ -0,0 +1,148 @@ +{- 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 diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -9,18 +9,6 @@ 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 ------------------ @@ -47,6 +35,19 @@ 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`__ + + This module exports the constructor for the central datatype that stores + dimensioned quantities. With this constructor, you can arbitrarily change + units! Use at your peril. + - __`Data.Dimensions.Show`__ This module defines a `Show` instance for dimensioned quantities, printing @@ -55,22 +56,28 @@ - __`Data.Dimensions.SI`__ - This module exports unit definitions for the [SI][] system of units. + 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.Prefixes`__ + + - __`Data.Dimensions.SI.Units`__ - 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. + This module exports only the SI units, such as `Meter` and `Ampere`. - __`Data.Dimensions.SI.Types`__ - This module exports several useful types for use with the SI package, + 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. + - __`Data.Dimensions.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 ======== @@ -212,9 +219,6 @@ 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. @@ -230,12 +234,13 @@ 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 +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 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: +performs a cast from one to the other. This cast is completely free at +runtime. 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 diff --git a/src/Data/Dimensions.hs b/src/Data/Dimensions.hs deleted file mode 100644 --- a/src/Data/Dimensions.hs +++ /dev/null @@ -1,140 +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 #-} - -{-| 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 - . - - 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 diff --git a/src/Data/Dimensions/Dim.hs b/src/Data/Dimensions/Dim.hs deleted file mode 100644 --- a/src/Data/Dimensions/Dim.hs +++ /dev/null @@ -1,148 +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 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) - - diff --git a/src/Data/Dimensions/DimSpec.hs b/src/Data/Dimensions/DimSpec.hs deleted file mode 100644 --- a/src/Data/Dimensions/DimSpec.hs +++ /dev/null @@ -1,192 +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.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) diff --git a/src/Data/Dimensions/Internal.hs b/src/Data/Dimensions/Internal.hs deleted file mode 100644 --- a/src/Data/Dimensions/Internal.hs +++ /dev/null @@ -1,38 +0,0 @@ -{- 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 diff --git a/src/Data/Dimensions/SI.hs b/src/Data/Dimensions/SI.hs deleted file mode 100644 --- a/src/Data/Dimensions/SI.hs +++ /dev/null @@ -1,180 +0,0 @@ -{- 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: . - - 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" - diff --git a/src/Data/Dimensions/SI/Prefixes.hs b/src/Data/Dimensions/SI/Prefixes.hs deleted file mode 100644 --- a/src/Data/Dimensions/SI/Prefixes.hs +++ /dev/null @@ -1,217 +0,0 @@ -{- 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 - -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 :@) diff --git a/src/Data/Dimensions/SI/Types.hs b/src/Data/Dimensions/SI/Types.hs deleted file mode 100644 --- a/src/Data/Dimensions/SI/Types.hs +++ /dev/null @@ -1,56 +0,0 @@ -{- 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 diff --git a/src/Data/Dimensions/Show.hs b/src/Data/Dimensions/Show.hs deleted file mode 100644 --- a/src/Data/Dimensions/Show.hs +++ /dev/null @@ -1,71 +0,0 @@ -{- 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)) diff --git a/src/Data/Dimensions/TypePrelude.hs b/src/Data/Dimensions/TypePrelude.hs deleted file mode 100644 --- a/src/Data/Dimensions/TypePrelude.hs +++ /dev/null @@ -1,45 +0,0 @@ -{- 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 diff --git a/src/Data/Dimensions/UnitCombinators.hs b/src/Data/Dimensions/UnitCombinators.hs deleted file mode 100644 --- a/src/Data/Dimensions/UnitCombinators.hs +++ /dev/null @@ -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 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) diff --git a/src/Data/Dimensions/Units.hs b/src/Data/Dimensions/Units.hs deleted file mode 100644 --- a/src/Data/Dimensions/Units.hs +++ /dev/null @@ -1,108 +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.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) diff --git a/src/Data/Dimensions/Z.hs b/src/Data/Dimensions/Z.hs deleted file mode 100644 --- a/src/Data/Dimensions/Z.hs +++ /dev/null @@ -1,165 +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 #-} - --- | 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 diff --git a/units.cabal b/units.cabal --- a/units.cabal +++ b/units.cabal @@ -1,5 +1,5 @@ name: units -version: 1.0.1 +version: 1.1 cabal-version: >= 1.10 synopsis: A domain-specific type system for dimensional analysis homepage: http://www.cis.upenn.edu/~eir/packages/units @@ -27,17 +27,17 @@ source-repository this type: git location: https://github.com/goldfirere/units.git - tag: v1.0.1 + tag: v1.1 library build-depends: - base >= 4.7 && < 5 + base >= 4.7 && < 5, + singletons >= 0.9 exposed-modules: Data.Dimensions, Data.Dimensions.Show, - Data.Dimensions.Internal, + Data.Dimensions.Poly, Data.Dimensions.Unsafe, Data.Dimensions.SI, Data.Dimensions.SI.Prefixes, - Data.Dimensions.SI.Types + Data.Dimensions.SI.Types, Data.Dimensions.SI.Units other-modules: Data.Dimensions.Dim, Data.Dimensions.DimSpec, Data.Dimensions.Units, Data.Dimensions.UnitCombinators, - Data.Dimensions.TypePrelude, Data.Dimensions.Z - hs-source-dirs: src + Data.Dimensions.Z default-language: Haskell2010