diff --git a/changelog b/changelog new file mode 100644 --- /dev/null +++ b/changelog @@ -0,0 +1,14 @@ +-*-change-log-*- + +0.2.0.0 Adam Gundry December 2015 + * Add Data.UnitsOfMeasure.Read module and a Read instance for Quantity + * Make it possible to declare derived compound units + * Define litres, hectares, radians and steradians + * Prevent cyclic definitions of convertible units + +0.1.1.0 Adam Gundry November 2015 + * Add more conversion ratios (thanks to Joe Hermaszewski) + * Add Storable and NFData instances for Quantity (thanks to Marcin Mrotek) + +0.1.0.0 Adam Gundry August 2015 + * First public release diff --git a/src/Data/UnitsOfMeasure.hs b/src/Data/UnitsOfMeasure.hs --- a/src/Data/UnitsOfMeasure.hs +++ b/src/Data/UnitsOfMeasure.hs @@ -65,6 +65,7 @@ import Data.UnitsOfMeasure.Convert import Data.UnitsOfMeasure.Internal +import Data.UnitsOfMeasure.Read () import Data.UnitsOfMeasure.Show () import Data.UnitsOfMeasure.Singleton import Data.UnitsOfMeasure.TH diff --git a/src/Data/UnitsOfMeasure/Convert.hs b/src/Data/UnitsOfMeasure/Convert.hs --- a/src/Data/UnitsOfMeasure/Convert.hs +++ b/src/Data/UnitsOfMeasure/Convert.hs @@ -8,6 +8,7 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -fplugin Data.UnitsOfMeasure.Plugin #-} @@ -48,16 +49,21 @@ -- You are likely to get unpleasant compiler error messages if you -- attempt to convert without the units being fully determined by type -- inference, or if the units do not have the same dimension. +-- +-- If you wish to define a dimensionless unit that requires explicit +-- conversion to @1@, such as radians, write @['u'| rad = 1 1 |]@. +-- The syntax @['u'| dimensionless = 1 |]@ defines @dimensionless@ as +-- a unit synonym for @1@ that does not require conversion. module Data.UnitsOfMeasure.Convert ( convert , ratio , HasCanonicalBaseUnit(..) -- * Constraints , Good + , IsCanonical , HasCanonical , Convertible , ToCanonicalUnit - , MapCBU ) where import Data.UnitsOfMeasure.Internal @@ -69,28 +75,28 @@ -- | Class to capture the dimensions to which base units belong. For -- a canonical base unit, the class instance can be left empty. -class (CanonicalBaseUnit (CanonicalBaseUnit b) ~ CanonicalBaseUnit b) +class IsCanonical (Unpack (CanonicalBaseUnit b)) => HasCanonicalBaseUnit (b :: Symbol) where -- | The canonical base unit for this base unit. If @b@ is -- canonical, then @'CanonicalBaseUnit' b = b@. Otherwise, -- @'CanonicalBaseUnit' b@ must itself be canonical. - type CanonicalBaseUnit b :: Symbol - type CanonicalBaseUnit b = b + type CanonicalBaseUnit b :: Unit + type CanonicalBaseUnit b = Base b -- | The conversion ratio between this base unit and its canonical -- base unit. If @b@ is canonical then this ratio is @1@. - conversionBase :: proxy b -> Quantity Rational (Base b /: Base (CanonicalBaseUnit b)) - default conversionBase :: (b ~ CanonicalBaseUnit b) => proxy b -> Quantity Rational (Base b /: Base b) + conversionBase :: proxy b -> Quantity Rational (Base b /: CanonicalBaseUnit b) + default conversionBase :: (Base b ~ CanonicalBaseUnit b) => proxy b -> Quantity Rational (Base b /: Base b) conversionBase _ = 1 -- | Convert a unit into its canonical representation, where units are -- represented syntactically. -type family MapCBU (u :: UnitSyntax Symbol) :: UnitSyntax Symbol where - MapCBU (xs :/ ys) = ListMapCBU xs :/ ListMapCBU ys +type family ToCBU (u :: UnitSyntax Symbol) :: Unit where + ToCBU (xs :/ ys) = ListToCBU xs /: ListToCBU ys -type family ListMapCBU (xs :: [Symbol]) :: [Symbol] where - ListMapCBU '[] = '[] - ListMapCBU (x ': xs) = CanonicalBaseUnit x ': ListMapCBU xs +type family ListToCBU (xs :: [Symbol]) :: Unit where + ListToCBU '[] = One + ListToCBU (x ': xs) = CanonicalBaseUnit x *: ListToCBU xs -- | This constraint will be satisfied if all the base units in a -- syntactically represented unit have associated canonical @@ -102,15 +108,24 @@ AllHasCanonical '[] = () AllHasCanonical (x ': xs) = (HasCanonicalBaseUnit x, AllHasCanonical xs) +-- | This constraint will be satisfied if all the base units in a +-- syntactically represented unit are in their canonical form. +type family IsCanonical (u :: UnitSyntax Symbol) :: Constraint where + IsCanonical (xs :/ ys) = (AllIsCanonical xs, AllIsCanonical ys) +type family AllIsCanonical (xs :: [Symbol]) :: Constraint where + AllIsCanonical '[] = () + AllIsCanonical (x ': xs) = (CanonicalBaseUnit x ~ Base x, AllIsCanonical xs) + + conversionRatio :: forall proxy u . Good u - => proxy u -> Quantity Rational (u /: Pack (MapCBU (Unpack u))) + => proxy u -> Quantity Rational (u /: ToCBU (Unpack u)) conversionRatio _ = help (unitSing :: SUnit (Unpack u)) -help :: forall u . HasCanonical u => SUnit u -> Quantity Rational (Pack u /: Pack (MapCBU u)) +help :: forall u . HasCanonical u => SUnit u -> Quantity Rational (Pack u /: ToCBU u) help (SUnit xs ys) = help' xs /: help' ys -help' :: forall xs . AllHasCanonical xs => SList xs -> Quantity Rational (Prod xs /: Prod (ListMapCBU xs)) +help' :: forall xs . AllHasCanonical xs => SList xs -> Quantity Rational (Prod xs /: ListToCBU xs) help' SNil = 1 help' (SCons p xs) = conversionBase p *: help' xs @@ -124,7 +139,7 @@ type Convertible u v = (Good u, Good v, ToCanonicalUnit u ~ ToCanonicalUnit v) -- | Converts a unit to the corresponding canonical representation. -type ToCanonicalUnit u = Pack (MapCBU (Unpack u)) +type ToCanonicalUnit u = ToCBU (Unpack u) -- | Automatically convert a quantity with units @u@ so that its units -- are @v@, provided @u@ and @v@ have the same dimension. diff --git a/src/Data/UnitsOfMeasure/Defs.hs b/src/Data/UnitsOfMeasure/Defs.hs --- a/src/Data/UnitsOfMeasure/Defs.hs +++ b/src/Data/UnitsOfMeasure/Defs.hs @@ -36,15 +36,18 @@ , ohm = V / A |] +-- SI derived units that require explicit conversion +[u| rad = 1 1 + , sr = 1 1 + |] + -- Non-SI units accepted for use with them -- http://www.bipm.org/en/publications/si-brochure/chapter4.html --- hectares and liters are unable to be defined at the moment due to --- https://github.com/adamgundry/uom-plugin/issues/4 [u| min = 60 s , h = 3600 s , d = 86400 s - , ha - , l + , ha = 10000 m^2 + , l = 0.001 m^3 , t = 1000 kg , au = 149597870700 m |] diff --git a/src/Data/UnitsOfMeasure/Internal.hs b/src/Data/UnitsOfMeasure/Internal.hs --- a/src/Data/UnitsOfMeasure/Internal.hs +++ b/src/Data/UnitsOfMeasure/Internal.hs @@ -198,6 +198,7 @@ -- units, for example 'One' is represented as @[] ':/' []@ and -- @'Base' "m" '/:' 'Base' "s" ^: 2@ is represented as @["m"] ':/' ["s","s"]@. data UnitSyntax s = [s] :/ [s] + deriving (Eq, Show) -- | Pack up a syntactic representation of a unit as a unit. For example: -- diff --git a/src/Data/UnitsOfMeasure/Read.hs b/src/Data/UnitsOfMeasure/Read.hs new file mode 100644 --- /dev/null +++ b/src/Data/UnitsOfMeasure/Read.hs @@ -0,0 +1,94 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PartialTypeSignatures #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# OPTIONS_GHC -fno-warn-partial-type-signatures #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} + +-- | Very very rough support for reading units of measure in the +-- syntax used by "Data.UnitsOfMeasure.Show". +module Data.UnitsOfMeasure.Read + ( readQuantity + , readUnit + , readWithUnit + , Some(..) + , QuantityWithUnit(..) + ) where + +import Control.Monad (join) +import GHC.TypeLits +import Data.List (genericReplicate) +import Data.Proxy +import Data.Type.Equality ((:~:)(..)) +import Text.Parse.Units (parseUnit, universalSymbolTable, UnitExp(..)) + +import Data.UnitsOfMeasure.Internal +import Data.UnitsOfMeasure.Singleton + +-- | Represents a quantity whose units have a syntactic representation +-- that is known statically and at runtime. +data QuantityWithUnit a u where + QuantityWithUnit :: Quantity a (Pack u) -> SUnit u -> QuantityWithUnit a u + +-- | An existential wrapper type: @'Some' p@ is essentially @exists x . p x@. +data Some p where + Some :: p x -> Some p + +instance (KnownUnit (Unpack u), u ~ Pack (Unpack u), Read a) => Read (Quantity a u) where + readsPrec i (' ':s) = readsPrec i s + readsPrec _ ('[':'u':'|':s) + | (t, '|':']':r) <- break (== '|') s + , Right v <- readWithUnit (Proxy :: Proxy (Unpack u)) t = [(v, r)] + readsPrec _ _ = [] + +-- | Parse a quantity and check that it has the expected units. +readWithUnit :: forall proxy a u . (Read a, KnownUnit u) + => proxy u -> String -> Either String (Quantity a (Pack u)) +readWithUnit _ s = do + Some (QuantityWithUnit (q :: Quantity a _) v) <- readQuantity s + case testEquivalentSUnit (unitSing :: SUnit u) v of + Just Refl -> Right q + Nothing -> Left ("wrong units: got " ++ show (forgetSUnit v)) + +-- | Parse a quantity along with its units. +readQuantity :: Read a => String -> Either String (Some (QuantityWithUnit a)) +readQuantity s = case reads s of + [(n, s')] -> do Some u <- readUnit s' + return $ Some (QuantityWithUnit (MkQuantity n) u) + _ -> Left "reads: no parse" + +-- | Parse a unit. +readUnit :: String -> Either String (Some SUnit) +readUnit s = expToSomeUnit <$> parseUnit universalSymbolTable s + +expToSomeUnit :: UnitExp () String -> Some SUnit +expToSomeUnit = unitSyntaxToSomeUnit . expToUnitSyntax + +unitSyntaxToSomeUnit :: UnitSyntax String -> Some SUnit +unitSyntaxToSomeUnit (xs :/ ys) = case (someListVal xs, someListVal ys) of + (Some xs', Some ys') -> Some (SUnit xs' ys') + +someListVal :: [String] -> Some SList +someListVal [] = Some SNil +someListVal (x:xs) = case (someSymbolVal x, someListVal xs) of + (SomeSymbol x', Some xs') -> Some (SCons x' xs') + +expToUnitSyntax :: UnitExp () String -> UnitSyntax String +expToUnitSyntax Unity = [] :/ [] +expToUnitSyntax (Unit _ s) = [s] :/ [] +expToUnitSyntax (u `Mult` v) = (u_xs ++ v_xs) :/ (u_ys ++ v_ys) + where + u_xs :/ u_ys = expToUnitSyntax u + v_xs :/ v_ys = expToUnitSyntax v +expToUnitSyntax (u `Div` v) = (u_xs ++ v_ys) :/ (u_ys ++ v_xs) + where + u_xs :/ u_ys = expToUnitSyntax u + v_xs :/ v_ys = expToUnitSyntax v +expToUnitSyntax (u `Pow` n) + | n >= 0 = join (genericReplicate n u_xs) :/ join (genericReplicate n u_ys) + | otherwise = join (genericReplicate (negate n) u_ys) :/ join (genericReplicate (negate n) u_xs) + where + u_xs :/ u_ys = expToUnitSyntax u diff --git a/src/Data/UnitsOfMeasure/Singleton.hs b/src/Data/UnitsOfMeasure/Singleton.hs --- a/src/Data/UnitsOfMeasure/Singleton.hs +++ b/src/Data/UnitsOfMeasure/Singleton.hs @@ -26,6 +26,7 @@ , forgetSUnit , KnownUnit(..) , unitVal + , testEquivalentSUnit -- * Singletons for lists , SList(..) @@ -33,6 +34,10 @@ ) where import GHC.TypeLits +import Data.List (foldl') +import qualified Data.Map as Map +import Data.Type.Equality +import Unsafe.Coerce import Data.UnitsOfMeasure.Internal @@ -46,6 +51,43 @@ data SList (xs :: [Symbol]) where SNil :: SList '[] SCons :: KnownSymbol x => proxy x -> SList xs -> SList (x ': xs) + +instance TestEquality SUnit where + testEquality (SUnit xs ys) (SUnit xs' ys') = case (testEquality xs xs', testEquality ys ys') of + (Just Refl, Just Refl) -> Just Refl + _ -> Nothing + +instance TestEquality SList where + testEquality SNil SNil = Just Refl + testEquality (SCons px xs) (SCons py ys) + | Just Refl <- testEqualitySymbol px py + , Just Refl <- testEquality xs ys = Just Refl + testEquality _ _ = Nothing + +-- | Annoyingly, base doesn't appear to export enough stuff to make it +-- possible to write a @TestEquality SSymbol@ instance, so we cheat. +testEqualitySymbol :: forall proxy proxy' x y . (KnownSymbol x, KnownSymbol y) + => proxy x -> proxy' y -> Maybe (x :~: y) +testEqualitySymbol px py + | symbolVal px == symbolVal py = Just (unsafeCoerce Refl) + | otherwise = Nothing + +-- | Test whether two 'SUnit's represent the same units, up to the +-- equivalence relation. TODO: this currently uses 'unsafeCoerce', +-- but in principle it should be possible to avoid it. +testEquivalentSUnit :: SUnit u -> SUnit v -> Maybe (Pack u :~: Pack v) +testEquivalentSUnit su sv + | normaliseUnitSyntax (forgetSUnit su) == normaliseUnitSyntax (forgetSUnit sv) = Just (unsafeCoerce Refl) + | otherwise = Nothing + +-- | Calculate a normal form of a syntactic unit: a map from base unit +-- names to non-zero integers. +normaliseUnitSyntax :: UnitSyntax String -> Map.Map String Integer +normaliseUnitSyntax (xs :/ ys) = + Map.filter (/= 0) + (foldl' (\ m x -> Map.insertWith (-) x 1 m) + (foldl' (\ m x -> Map.insertWith (+) x 1 m) Map.empty xs) ys) + -- | Extract the runtime syntactic representation from a singleton unit forgetSUnit :: SUnit u -> UnitSyntax String diff --git a/src/Data/UnitsOfMeasure/TH.hs b/src/Data/UnitsOfMeasure/TH.hs --- a/src/Data/UnitsOfMeasure/TH.hs +++ b/src/Data/UnitsOfMeasure/TH.hs @@ -108,7 +108,7 @@ data UnitDecl = BaseUnit | DefinedUnit (UnitExp () String) - | ConversionUnit Rational String + | ConversionUnit Rational (UnitExp () String) -- | Parse a comma-separated list of unit declarations, for example: -- @@ -127,12 +127,14 @@ go' u (',':xs) = ((u, BaseUnit) :) <$> go xs go' u ('=':xs) = let (d, ys) = break (== ',') xs in case readNumber d of - Just (ei, s) -> case parseUnit universalSymbolTable s of - Right (Unit _ e :: UnitExp () String) -> ((u, ConversionUnit (either fromInteger id ei) e) :) <$> go ys - _ -> Nothing - _ -> case parseUnit universalSymbolTable d of - Right e -> ((u, DefinedUnit e) :) <$> go ys - Left _ -> Nothing + Just (ei, s) + | not (all isSpace s) -- parse "x = 1" as DefinedUnit, not ConversionUnit + -> case parseUnit universalSymbolTable s of + Right e -> ((u, ConversionUnit (either fromInteger id ei) e) :) <$> go ys + _ -> Nothing + _ -> case parseUnit universalSymbolTable d of + Right e -> ((u, DefinedUnit e) :) <$> go ys + Left _ -> Nothing go' _ _ = Nothing -- | Given a unit name and an optional definition, create an @@ -143,9 +145,11 @@ instance HasCanonicalBaseUnit $(litT (strTyLit s)) |] DefinedUnit u -> [d| type instance MkUnit $(litT (strTyLit s)) = $(reifyUnit u) |] - ConversionUnit r t -> [d| type instance MkUnit $(litT (strTyLit s)) = Base $(litT (strTyLit s)) + ConversionUnit _ (Unit Nothing s') | s == s' + -> reportError ("cannot define cyclic convertible unit: " ++ s) >> return [] + ConversionUnit r u -> [d| type instance MkUnit $(litT (strTyLit s)) = Base $(litT (strTyLit s)) instance HasCanonicalBaseUnit $(litT (strTyLit s)) where - type CanonicalBaseUnit $(litT (strTyLit s)) = $(litT (strTyLit t)) + type CanonicalBaseUnit $(litT (strTyLit s)) = $(reifyUnit u) conversionBase _ = MkQuantity $(litE (rationalL (recip r))) |] @@ -187,13 +191,15 @@ -- -- > type instance MkUnit "kilobyte" = Base "kilobyte" -- > instance HasCanonicalBaseUnit "kilobyte" where --- > type CanonicalBaseUnit "kilobyte" = "byte" +-- > type CanonicalBaseUnit "kilobyte" = Base "byte" -- > conversionBase _ = [u| 1 % 1024 kilobyte/byte |] -- -- This can also be written @['u'| kilobyte = 1024 byte |]@. -- See "Data.UnitsOfMeasure.Convert" for more information about conversions. declareConvertibleUnit :: String -> Rational -> String -> Q [Dec] -declareConvertibleUnit derived r base = declareUnit derived (ConversionUnit r base) +declareConvertibleUnit derived r base = case parseUnit universalSymbolTable base of + Right e -> declareUnit derived (ConversionUnit r e) + Left _ -> reportError ("unable to parse convertible unit: " ++ base) >> return [] -- | Read either an integer or a rational from a string, if possible, diff --git a/tests/Tests.hs b/tests/Tests.hs --- a/tests/Tests.hs +++ b/tests/Tests.hs @@ -29,6 +29,7 @@ declareBaseUnit "byte" declareDerivedUnit "bps" "byte / s" declareConvertibleUnit "kilobyte" 1024 "byte" +declareConvertibleUnit "squiggle" 2 "m/s" -- Some basic examples @@ -58,7 +59,13 @@ foo' :: Num a => Quantity a u -> Quantity a v -> Quantity a (u *: v) foo' = foo +-- thanks to expipiplus1, https://github.com/adamgundry/uom-plugin/issues/14 +angularSpeed :: Quantity Rational [u|rad/s|] +angularSpeed = convert x + where x :: Quantity Rational [u|s^-1|] + x = undefined + -- Check that the abelian group laws hold associativity :: Quantity a (u *: (v *: w)) -> Quantity a ((u *: v) *: w) @@ -130,6 +137,17 @@ pow = id +-- This declares a synonym for One +[u| dimensionless = 1 |] +dimensionless :: Quantity a [u|dimensionless|] -> Quantity a [u|1|] +dimensionless = id + +-- This declares a dimensionless unit that requires explicit conversion +[u| dime = 1 1 |] +dime :: Fractional a => Quantity a [u|dime|] -> Quantity a [u|1|] +dime = convert + + -- Runtime testsuite main :: IO () @@ -164,6 +182,14 @@ [ testCase "10m in ft" $ convert [u| 10m |] @?= [u| 32.8 ft |] , testCase "5 km^2 in m^2" $ convert [u| 5km^2 |] @?= [u| 5000000 m m |] , testCase "ratio" $ show (ratio [u| ft |] [u| m |]) @?= "[u| 3.28 ft / m |]" + , testCase "100l in m^3" $ convert [u| 100l |] @?= [u| 0.1 m^3 |] + , testCase "1l/m in m^2" $ convert [u| 1l/m |] @?= [u| 0.001 m^2 |] + , testCase "1l/m in m^2" $ convert [u| 1l/m |] @?= [u| 0.001 m^2 |] + , testCase "5l in ft^3" $ convert [u| 5l |] @?= [u| 0.17643776 ft^3 |] + , testCase "2000000l^2 in ft^3 m^3" $ convert [u| 2000000l^2 |] @?= [u| 70.575104 ft^3 m^3 |] + , testCase "42 rad/s in s^-1" $ convert [u| 42 rad/s |] @?= [u| 42 s^-1 |] + , testCase "2.4 l/h in m" $ convert [u| 2.4 l/ha |] @?= [u| 2.4e-7 m |] + , testCase "1 m^4 in l m" $ convert [u| 1 m^4 |] @?= [u| 1000 l m |] ] , testGroup "errors" [ testCase "s/m ~ m/s" $ mismatch1 `throws` mismatch1_errors @@ -171,6 +197,16 @@ , testCase "a ~ a => a ~ kg" $ given1 undefined `throws` given1_errors , testCase "a ~ b => a ~ kg" $ given2 undefined `throws` given2_errors , testCase "a^2 ~ b^3 => a ~ s" $ given3 undefined `throws` given3_errors + ] + , testGroup "read . show" + [ testCase "3 m" $ read (show [u| 3 m |]) @?= [u| 3 m |] + , testCase "1.2 m/s" $ read (show [u| 1.2 m/s |]) @?= [u| 1.2 m/s |] + , testCase "0" $ read (show [u| 1 |]) @?= [u| 1 |] + ] + , testGroup "read normalisation" + [ testCase "1 m/m" $ read "[u| 1 m/m |]" @?= [u| 1 |] + , testCase "-0.3 m s^-1" $ read "[u| -0.3 m s^-1 |]" @?= [u| -0.3 m/s |] + , testCase "42 s m s" $ read "[u| 42 s m s |]" @?= [u| 42 m s^2 |] ] ] diff --git a/uom-plugin.cabal b/uom-plugin.cabal --- a/uom-plugin.cabal +++ b/uom-plugin.cabal @@ -1,5 +1,5 @@ name: uom-plugin -version: 0.1.1.0 +version: 0.2.0.0 synopsis: Units of measure as a GHC typechecker plugin category: Type System description: A prototype typechecker plugin for GHC with support for units of measure @@ -20,6 +20,8 @@ is available in GHC 7.10 and later. See "Data.UnitsOfMeasure.Tutorial" for an introduction to the library. +extra-source-files: changelog + source-repository head type: git location: https://github.com/adamgundry/uom-plugin.git @@ -30,6 +32,7 @@ Data.UnitsOfMeasure.Defs, Data.UnitsOfMeasure.Internal, Data.UnitsOfMeasure.Plugin, + Data.UnitsOfMeasure.Read, Data.UnitsOfMeasure.Show, Data.UnitsOfMeasure.Singleton, Data.UnitsOfMeasure.Tutorial @@ -56,7 +59,7 @@ other-modules: ErrorTests other-extensions: TemplateHaskell build-depends: base, uom-plugin, - tasty >=0.10 && <0.11, tasty-hunit >=0.9 && <0.10 + tasty >=0.10 && <0.12, tasty-hunit >=0.9 && <0.10 hs-source-dirs: tests default-language: Haskell2010 ghc-options: -O0