-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | Units of measure as a GHC type-checker plugin -- -- The uom-plugin library adds support for units of measure as a -- GHC type-checker plugin. See Data.UnitsOfMeasure.Tutorial for -- an introduction to the library. @package uom-plugin @version 0.4.0.0 -- | This module defines the core types used in the uom-plugin -- library. Note that importing this module may allow you to violate -- invariants, so you should generally work with the safe interface in -- Data.UnitsOfMeasure instead. module Data.UnitsOfMeasure.Internal -- | (Kind) Units of measure data Unit -- | Dimensionless unit (identity element) type family One :: Unit -- | Base unit type family Base b -- | Multiplication for units of measure type family u *: v infixl 7 *: -- | Division for units of measure type family u /: v infixl 7 /: -- | Exponentiation (to a positive power) for units of measure; negative -- exponents are not yet supported (they require an Integer kind) type family u ^: n infixr 8 ^: -- | A Quantity a u is represented identically to a value of -- underlying numeric type a, but with units u. newtype Quantity a (u :: Unit) -- | Warning: the MkQuantity constructor allows module invariants to -- be violated, so use it with caution! MkQuantity :: a -> Quantity a (u :: Unit) -- | Extract the underlying value of a quantity unQuantity :: Quantity a u -> a -- | Zero is polymorphic in its units: this is required because the -- Num instance constrains the quantity to be dimensionless, so -- 0 :: Quantity a u is not well typed. zero :: Num a => Quantity a u -- | Construct a Quantity from a dimensionless value. Note that for -- numeric literals, the Num and Fractional instances allow -- them to be treated as quantities directly. mk :: a -> Quantity a One -- | Addition (+) of quantities requires the units to match. (+:) :: Num a => Quantity a u -> Quantity a u -> Quantity a u infixl 6 +: -- | Multiplication (*) of quantities multiplies the units. (*:) :: (Num a, w ~~ (u *: v)) => Quantity a u -> Quantity a v -> Quantity a w infixl 7 *: -- | Subtraction (-) of quantities requires the units to match. (-:) :: Num a => Quantity a u -> Quantity a u -> Quantity a u infixl 6 -: -- | Negation (negate) of quantities is polymorphic in the units. negate' :: Num a => Quantity a u -> Quantity a u -- | Absolute value (abs) of quantities is polymorphic in the units. abs' :: Num a => Quantity a u -> Quantity a u -- | The sign (signum) of a quantity gives a dimensionless result. signum' :: Num a => Quantity a u -> Quantity a One -- | Convert an Integer quantity into any Integral type -- (fromInteger). fromInteger' :: Integral a => Quantity Integer u -> Quantity a u -- | Division (/) of quantities divides the units. (/:) :: (Fractional a, w ~~ (u /: v)) => Quantity a u -> Quantity a v -> Quantity a w infixl 7 /: -- | Reciprocal (recip) of quantities reciprocates the units. recip' :: (Fractional a, w ~~ (One /: u)) => Quantity a u -> Quantity a w -- | Convert a Rational quantity into any Fractional type -- (fromRational). fromRational' :: Fractional a => Quantity Rational u -> Quantity a u -- | Convert any Real quantity into a Rational type -- (toRational). toRational' :: Real a => Quantity a u -> Quantity Rational u -- | Taking the square root (sqrt) of a quantity requires its units -- to be a square. Fractional units are not currently supported. sqrt' :: (Floating a, w ~~ (u ^: 2)) => Quantity a w -> Quantity a u -- | Syntactic representation of a unit as a pair of lists of base units, -- for example One is represented as [] :/ [] and -- Base "m" /: Base "s" ^: 2 is represented -- as ["m"] :/ ["s","s"]. data UnitSyntax s (:/) :: [s] -> [s] -> UnitSyntax s -- | Unpack a unit as a syntactic representation, where the order of units -- is deterministic. For example: -- --
--   Unpack One = [] :/ []
--   
-- --
--   Unpack (Base "s" *: Base "m") = ["m","s"] :/ []
--   
-- -- This does not break type soundness because Unpack will reduce -- only when the unit is entirely constant, and it does not allow the -- structure of the unit to be observed. The reduction behaviour is -- implemented by the plugin, because we cannot define it otherwise. type family Unpack u -- | Pack up a syntactic representation of a unit as a unit. For example: -- --
--   Pack ([] :/ []) = One
--   
-- --
--   Pack (["m"] :/ ["s","s"]) = Base "m" /: Base "s" ^: 2
--   
-- -- This is a perfectly ordinary closed type family. Pack is a left -- inverse of Unpack up to the equational theory of units, but it -- is not a right inverse (because there are multiple list -- representations of the same unit). type family Pack u -- | Take the product of a list of base units. type family Prod xs -- | This is a bit of a hack, honestly, but a good hack. Constraints u -- ~~ v are just like equalities u ~ v, except solving them -- will be delayed until the plugin. This may lead to better inferred -- types. type family u ~~ v infix 4 ~~ -- | This type family is used for translating unit names (as type-level -- strings) into units. It will be Base for base units or expand -- the definition for derived units. -- -- The instances displayed by Haddock are available only if -- Data.UnitsOfMeasure.Defs is imported. type family MkUnit s instance GHC.Show.Show s => GHC.Show.Show (Data.UnitsOfMeasure.Internal.UnitSyntax s) instance GHC.Classes.Eq s => GHC.Classes.Eq (Data.UnitsOfMeasure.Internal.UnitSyntax s) instance GHC.Enum.Bounded a => GHC.Enum.Bounded (Data.UnitsOfMeasure.Internal.Quantity a u) instance GHC.Classes.Eq a => GHC.Classes.Eq (Data.UnitsOfMeasure.Internal.Quantity a u) instance GHC.Classes.Ord a => GHC.Classes.Ord (Data.UnitsOfMeasure.Internal.Quantity a u) instance (GHC.Enum.Enum a, u GHC.Types.~ Data.UnitsOfMeasure.Internal.One) => GHC.Enum.Enum (Data.UnitsOfMeasure.Internal.Quantity a u) instance (GHC.Float.Floating a, u GHC.Types.~ Data.UnitsOfMeasure.Internal.One) => GHC.Float.Floating (Data.UnitsOfMeasure.Internal.Quantity a u) instance (GHC.Real.Fractional a, u GHC.Types.~ Data.UnitsOfMeasure.Internal.One) => GHC.Real.Fractional (Data.UnitsOfMeasure.Internal.Quantity a u) instance (GHC.Real.Integral a, u GHC.Types.~ Data.UnitsOfMeasure.Internal.One) => GHC.Real.Integral (Data.UnitsOfMeasure.Internal.Quantity a u) instance (GHC.Num.Num a, u GHC.Types.~ Data.UnitsOfMeasure.Internal.One) => GHC.Num.Num (Data.UnitsOfMeasure.Internal.Quantity a u) instance (GHC.Real.Real a, u GHC.Types.~ Data.UnitsOfMeasure.Internal.One) => GHC.Real.Real (Data.UnitsOfMeasure.Internal.Quantity a u) instance (GHC.Float.RealFloat a, u GHC.Types.~ Data.UnitsOfMeasure.Internal.One) => GHC.Float.RealFloat (Data.UnitsOfMeasure.Internal.Quantity a u) instance (GHC.Real.RealFrac a, u GHC.Types.~ Data.UnitsOfMeasure.Internal.One) => GHC.Real.RealFrac (Data.UnitsOfMeasure.Internal.Quantity a u) instance Foreign.Storable.Storable a => Foreign.Storable.Storable (Data.UnitsOfMeasure.Internal.Quantity a u) instance Control.DeepSeq.NFData a => Control.DeepSeq.NFData (Data.UnitsOfMeasure.Internal.Quantity a u) -- | This module defines singleton types for integers and concrete units. module Data.UnitsOfMeasure.Singleton -- | Singleton type for concrete units of measure represented as lists of -- base units data SUnit (u :: UnitSyntax Symbol) [SUnit] :: SList xs -> SList ys -> SUnit (xs :/ ys) -- | Extract the runtime syntactic representation from a singleton unit forgetSUnit :: SUnit u -> UnitSyntax String -- | A constraint KnownUnit u means that u must be -- a concrete unit that is statically known but passed at runtime class KnownUnit (u :: UnitSyntax Symbol) unitSing :: KnownUnit u => SUnit u -- | Extract the runtime syntactic representation of a KnownUnit unitVal :: forall proxy u. KnownUnit u => proxy u -> UnitSyntax String -- | Test whether two SUnits 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) -- | Singleton type for lists of base units data SList (xs :: [Symbol]) [SNil] :: SList '[] [SCons] :: KnownSymbol x => proxy x -> SList xs -> SList (x ': xs) -- | A constraint KnownList xs means that xs must -- be a list of base units that is statically known but passed at runtime class KnownList (xs :: [Symbol]) listSing :: KnownList xs => SList xs instance (Data.UnitsOfMeasure.Singleton.KnownList xs, Data.UnitsOfMeasure.Singleton.KnownList ys) => Data.UnitsOfMeasure.Singleton.KnownUnit (xs 'Data.UnitsOfMeasure.Internal.:/ ys) instance Data.UnitsOfMeasure.Singleton.KnownList '[] instance (GHC.TypeLits.KnownSymbol x, Data.UnitsOfMeasure.Singleton.KnownList xs) => Data.UnitsOfMeasure.Singleton.KnownList (x : xs) instance Data.Type.Equality.TestEquality Data.UnitsOfMeasure.Singleton.SUnit instance Data.Type.Equality.TestEquality Data.UnitsOfMeasure.Singleton.SList -- | Experimental support for showing units of measure in a pretty syntax. -- This requires the units to be fully determined. -- -- Apart from the definitions below, this module also exports a -- Show instance for Quantity a u, which is -- re-exported by Data.UnitsOfMeasure. module Data.UnitsOfMeasure.Show -- | Render a quantity nicely, followed by its units: -- --
--   >>> showQuantity (1 /: [u| 0.1 s / m kg |])
--   "10.0 kg m / s"
--   
showQuantity :: forall a u. (Show a, KnownUnit (Unpack u)) => Quantity a u -> String -- | Render a unit nicely: -- --
--   >>> showUnit (undefined :: proxy [u| 1 / s |])
--   "s^-1"
--   
showUnit :: forall proxy u. KnownUnit (Unpack u) => proxy u -> String instance (GHC.Show.Show a, Data.UnitsOfMeasure.Singleton.KnownUnit (Data.UnitsOfMeasure.Internal.Unpack u)) => GHC.Show.Show (Data.UnitsOfMeasure.Internal.Quantity a u) -- | Very very rough support for reading units of measure in the syntax -- used by Data.UnitsOfMeasure.Show. module Data.UnitsOfMeasure.Read -- | Parse a quantity along with its units. readQuantity :: Read a => String -> Either String (Some (QuantityWithUnit a)) -- | Parse a unit. readUnit :: String -> Either String (Some SUnit) -- | 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)) -- | An existential wrapper type: Some p is essentially -- exists x . p x. data Some p [Some] :: p x -> Some p -- | Represents a quantity whose units have a syntactic representation that -- is known statically and at runtime. data QuantityWithUnit a u [QuantityWithUnit] :: Quantity a (Pack u) -> SUnit u -> QuantityWithUnit a u instance (Data.UnitsOfMeasure.Singleton.KnownUnit (Data.UnitsOfMeasure.Internal.Unpack u), u GHC.Types.~ Data.UnitsOfMeasure.Internal.Pack (Data.UnitsOfMeasure.Internal.Unpack u), GHC.Read.Read a) => GHC.Read.Read (Data.UnitsOfMeasure.Internal.Quantity a u) -- | This module defines a typechecker plugin that solves equations -- involving units of measure. To use it, add -- --
--   {-# OPTIONS_GHC -fplugin Data.UnitsOfMeasure.Plugin #-}
--   
-- -- above the module header of your source files, or in the -- ghc-options field of your .cabal file. You do not -- need to import this module. module Data.UnitsOfMeasure.Plugin -- | The plugin that GHC will load when this module is used with the -- -fplugin option. plugin :: Plugin -- | Experimental support for conversions between units with the same -- dimension, for example feet and metres. This interface is not -- necessarily stable! -- -- Rather than defining dimensions explicitly, we pick a "canonical" base -- unit for each dimension, and record the conversion ratio between each -- base unit and the canonical base unit for its dimension. This means we -- can automatically calculate the conversion ratio between a unit and -- its canonical representation, and hence between any two units that -- share a dimension (i.e. have the same canonical representation). -- -- For example, to declare m as a canonical base unit, write: -- --
--   instance HasCanonicalBaseUnit "m"
--   
-- -- To declare ft as a derived unit, write: -- --
--   instance HasCanonicalBaseUnit "ft" where
--     type CanonicalBaseUnit "ft" = "m"
--     conversionBase _ = [u| 3.28 ft/m |]
--   
-- -- The above declarations can be written using the u declaration -- quasiquoter as [u| m, ft = 1 % 3.28 ft/m |], or -- generated automatically using declareConvertibleUnit. -- -- Now it is possible to convert between quantities whose units -- involve feet or metres. For example: -- --
--   >>> convert [u| 10m |] :: Quantity Double [u| ft |]
--   [u| 32.8 ft |]
--   
--   >>> convert [u| 3ft^2 |] :: Quantity Double [u| m^2 |]
--   [u| 0.27885187388459254 m^2 |]
--   
-- -- 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 -- | Automatically convert a quantity with units u so that its -- units are v, provided u and v have the same -- dimension. convert :: forall a u v. (Fractional a, Convertible u v) => Quantity a u -> Quantity a v -- | Calculate the conversion ratio between two units with the same -- dimension. The slightly unusual proxy arguments allow this to be -- called using quasiquoters to specify the units, for example -- ratio [u| ft |] [u| m |]. ratio :: forall a u v (proxy :: Unit -> Type) proxy'. (Fractional a, Convertible u v) => proxy' (proxy u) -> proxy' (proxy v) -> Quantity a (u /: v) -- | Class to capture the dimensions to which base units belong. For a -- canonical base unit, the class instance can be left empty. 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 :: 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 :: HasCanonicalBaseUnit b => proxy b -> Quantity Rational (Base b /: CanonicalBaseUnit b) -- | The conversion ratio between this base unit and its canonical base -- unit. If b is canonical then this ratio is 1. conversionBase :: (HasCanonicalBaseUnit b, Base b ~ CanonicalBaseUnit b) => proxy b -> Quantity Rational (Base b /: CanonicalBaseUnit b) -- | A unit is "good" if all its base units have been defined, and have -- associated canonical base units. type Good u = (u ~ Pack (Unpack u), KnownUnit (Unpack u), HasCanonical (Unpack u)) -- | This constraint will be satisfied if all the base units in a -- syntactically represented unit are in their canonical form. type family IsCanonical u -- | This constraint will be satisfied if all the base units in a -- syntactically represented unit have associated canonical -- representations. type family HasCanonical u -- | Two units are convertible if they are both Good and they have -- the same canonical units (and hence the same dimension). type Convertible u v = (Good u, Good v, ToCanonicalUnit u ~ ToCanonicalUnit v) -- | Converts a unit to the corresponding canonical representation. type ToCanonicalUnit u = ToCBU (Unpack u) -- | See Data.UnitsOfMeasure.Tutorial for how to use this module. module Data.UnitsOfMeasure -- | (Kind) Units of measure data Unit -- | Base unit type family Base b -- | Dimensionless unit (identity element) type family One :: Unit -- | Multiplication for units of measure type family u *: v infixl 7 *: -- | Division for units of measure type family u /: v infixl 7 /: -- | Exponentiation (to a positive power) for units of measure; negative -- exponents are not yet supported (they require an Integer kind) type family u ^: n infixr 8 ^: -- | A Quantity a u is represented identically to a value of -- underlying numeric type a, but with units u. data Quantity a (u :: Unit) -- | Extract the underlying value of a quantity unQuantity :: Quantity a u -> a -- | Zero is polymorphic in its units: this is required because the -- Num instance constrains the quantity to be dimensionless, so -- 0 :: Quantity a u is not well typed. zero :: Num a => Quantity a u -- | Construct a Quantity from a dimensionless value. Note that for -- numeric literals, the Num and Fractional instances allow -- them to be treated as quantities directly. mk :: a -> Quantity a One -- | Addition (+) of quantities requires the units to match. (+:) :: Num a => Quantity a u -> Quantity a u -> Quantity a u infixl 6 +: -- | Multiplication (*) of quantities multiplies the units. (*:) :: (Num a, w ~~ (u *: v)) => Quantity a u -> Quantity a v -> Quantity a w infixl 7 *: -- | Subtraction (-) of quantities requires the units to match. (-:) :: Num a => Quantity a u -> Quantity a u -> Quantity a u infixl 6 -: -- | Negation (negate) of quantities is polymorphic in the units. negate' :: Num a => Quantity a u -> Quantity a u -- | Absolute value (abs) of quantities is polymorphic in the units. abs' :: Num a => Quantity a u -> Quantity a u -- | The sign (signum) of a quantity gives a dimensionless result. signum' :: Num a => Quantity a u -> Quantity a One -- | Convert an Integer quantity into any Integral type -- (fromInteger). fromInteger' :: Integral a => Quantity Integer u -> Quantity a u -- | Division (/) of quantities divides the units. (/:) :: (Fractional a, w ~~ (u /: v)) => Quantity a u -> Quantity a v -> Quantity a w infixl 7 /: -- | Reciprocal (recip) of quantities reciprocates the units. recip' :: (Fractional a, w ~~ (One /: u)) => Quantity a u -> Quantity a w -- | Convert a Rational quantity into any Fractional type -- (fromRational). fromRational' :: Fractional a => Quantity Rational u -> Quantity a u -- | Convert any Real quantity into a Rational type -- (toRational). toRational' :: Real a => Quantity a u -> Quantity Rational u -- | Taking the square root (sqrt) of a quantity requires its units -- to be a square. Fractional units are not currently supported. sqrt' :: (Floating a, w ~~ (u ^: 2)) => Quantity a w -> Quantity a u -- | The u quasiquoter may be used to create units or quantities; -- its meaning depends on the context: -- -- u :: QuasiQuoter -- | Declare a canonical base unit of the given name, which must not -- contain any spaces, e.g. -- --
--   declareBaseUnit "m"
--   
-- -- produces -- --
--   type instance MkUnit "m" = Base "m"
--   instance HasCanonicalBaseUnit "m"
--   
-- -- This can also be written [u| m |]. declareBaseUnit :: String -> Q [Dec] -- | Declare a derived unit with the given name and definition, e.g. -- --
--   declareDerivedUnit "N" "kg m / s^2"
--   
-- -- produces -- --
--   type instance MkUnit "N" = Base "kg" *: Base "m" /: Base "s" ^: 2
--   
-- -- This can also be written [u| N = kg m / s^2 |]. declareDerivedUnit :: String -> String -> Q [Dec] -- | Declare a base unit of the given name, which is convertible to the -- canonical base unit, e.g. -- --
--   declareConvertibleUnit "kilobyte" 1024 "byte"
--   
-- -- produces -- --
--   type instance MkUnit "kilobyte" = Base "kilobyte"
--   instance HasCanonicalBaseUnit "kilobyte" where
--     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] -- | Automatically convert a quantity with units u so that its -- units are v, provided u and v have the same -- dimension. convert :: forall a u v. (Fractional a, Convertible u v) => Quantity a u -> Quantity a v -- | This type family is used for translating unit names (as type-level -- strings) into units. It will be Base for base units or expand -- the definition for derived units. -- -- The instances displayed by Haddock are available only if -- Data.UnitsOfMeasure.Defs is imported. type family MkUnit s -- | Pack up a syntactic representation of a unit as a unit. For example: -- --
--   Pack ([] :/ []) = One
--   
-- --
--   Pack (["m"] :/ ["s","s"]) = Base "m" /: Base "s" ^: 2
--   
-- -- This is a perfectly ordinary closed type family. Pack is a left -- inverse of Unpack up to the equational theory of units, but it -- is not a right inverse (because there are multiple list -- representations of the same unit). type family Pack u -- | Unpack a unit as a syntactic representation, where the order of units -- is deterministic. For example: -- --
--   Unpack One = [] :/ []
--   
-- --
--   Unpack (Base "s" *: Base "m") = ["m","s"] :/ []
--   
-- -- This does not break type soundness because Unpack will reduce -- only when the unit is entirely constant, and it does not allow the -- structure of the unit to be observed. The reduction behaviour is -- implemented by the plugin, because we cannot define it otherwise. type family Unpack u -- | A constraint KnownUnit u means that u must be -- a concrete unit that is statically known but passed at runtime class KnownUnit (u :: UnitSyntax Symbol) -- | This module gives a brief introduction to the uom-plugin -- library. module Data.UnitsOfMeasure.Tutorial -- | This module exports some example definitions of base and derived -- units, for demonstration purposes. In the future, this is likely to -- change or be moved to a separate package. module Data.UnitsOfMeasure.Defs -- | This type family is used for translating unit names (as type-level -- strings) into units. It will be Base for base units or expand -- the definition for derived units. -- -- The instances displayed by Haddock are available only if -- Data.UnitsOfMeasure.Defs is imported. type family MkUnit s instance Data.UnitsOfMeasure.Convert.HasCanonicalBaseUnit "m" instance Data.UnitsOfMeasure.Convert.HasCanonicalBaseUnit "kg" instance Data.UnitsOfMeasure.Convert.HasCanonicalBaseUnit "s" instance Data.UnitsOfMeasure.Convert.HasCanonicalBaseUnit "A" instance Data.UnitsOfMeasure.Convert.HasCanonicalBaseUnit "K" instance Data.UnitsOfMeasure.Convert.HasCanonicalBaseUnit "mol" instance Data.UnitsOfMeasure.Convert.HasCanonicalBaseUnit "cd" instance Data.UnitsOfMeasure.Convert.HasCanonicalBaseUnit "km" instance Data.UnitsOfMeasure.Convert.HasCanonicalBaseUnit "g" instance Data.UnitsOfMeasure.Convert.HasCanonicalBaseUnit "rad" instance Data.UnitsOfMeasure.Convert.HasCanonicalBaseUnit "sr" instance Data.UnitsOfMeasure.Convert.HasCanonicalBaseUnit "min" instance Data.UnitsOfMeasure.Convert.HasCanonicalBaseUnit "h" instance Data.UnitsOfMeasure.Convert.HasCanonicalBaseUnit "d" instance Data.UnitsOfMeasure.Convert.HasCanonicalBaseUnit "ha" instance Data.UnitsOfMeasure.Convert.HasCanonicalBaseUnit "l" instance Data.UnitsOfMeasure.Convert.HasCanonicalBaseUnit "t" instance Data.UnitsOfMeasure.Convert.HasCanonicalBaseUnit "au" instance Data.UnitsOfMeasure.Convert.HasCanonicalBaseUnit "ft" instance Data.UnitsOfMeasure.Convert.HasCanonicalBaseUnit "in" instance Data.UnitsOfMeasure.Convert.HasCanonicalBaseUnit "mi"