Data.UnitsOfMeasure

See Data.UnitsOfMeasure.Tutorial for how to use this module.

Type-level units of measure

data Unit

(Kind) Units of measure

type family Base b :: Unit

Base unit

type family One :: Unit

Dimensionless unit (identity element)

type family u *: v :: Unit infixl 7

Multiplication for units of measure

type family u /: v :: Unit infixl 7

Division for units of measure

type family u ^: n :: Unit infixr 8

Exponentiation (to a positive power) for units of measure; negative exponents are not yet supported (they require an Integer kind)

Equations

u ^: 0 = One

u ^: 1 = u

u ^: n = u *: (u ^: (n - 1))

Values indexed by their units

data Quantity a u

A Quantity a u is represented identically to a value of underlying numeric type a, but with units u.

Instances

Bounded a => Bounded (Quantity a u)

(Enum a, (~) Unit u One) => Enum (Quantity a u)

Eq a => Eq (Quantity a u)

(Floating a, (~) Unit u One) => Floating (Quantity a u)

(Fractional a, (~) Unit u One) => Fractional (Quantity a u)

(Integral a, (~) Unit u One) => Integral (Quantity a u)

(Num a, (~) Unit u One) => Num (Quantity a u)

Ord a => Ord (Quantity a u)

(Real a, (~) Unit u One) => Real (Quantity a u)

(RealFloat a, (~) Unit u One) => RealFloat (Quantity a u)

(RealFrac a, (~) Unit u One) => RealFrac (Quantity a u)

Storable a => Storable (Quantity a u)

NFData a => NFData (Quantity a u)

unQuantity :: Quantity a u -> a

Extract the underlying value of a quantity

zero :: Num a => Quantity a u

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.

mk :: a -> Quantity a One

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.

Unit-safe Num operations

(+:) :: Num a => Quantity a u -> Quantity a u -> Quantity a u infixl 6

Addition (+) of quantities requires the units to match.

(*:) :: (Num a, w ~~ (u *: v)) => Quantity a u -> Quantity a v -> Quantity a w infixl 7

Multiplication (*) of quantities multiplies the units.

(-:) :: Num a => Quantity a u -> Quantity a u -> Quantity a u infixl 6

Subtraction (-) of quantities requires the units to match.

negate' :: Num a => Quantity a u -> Quantity a u

Negation (negate) of quantities is polymorphic in the units.

abs' :: Num a => Quantity a u -> Quantity a u

Absolute value (abs) of quantities is polymorphic in the units.

signum' :: Num a => Quantity a u -> Quantity a One

The sign (signum) of a quantity gives a dimensionless result.

fromInteger' :: Integral a => Quantity Integer u -> Quantity a u

Convert an Integer quantity into any Integral type (fromInteger).

Unit-safe Fractional operations

(/:) :: (Fractional a, w ~~ (u /: v)) => Quantity a u -> Quantity a v -> Quantity a w infixl 7

Division (/) of quantities divides the units.

recip' :: (Fractional a, w ~~ (One /: u)) => Quantity a u -> Quantity a w

Reciprocal (recip) of quantities reciprocates the units.

fromRational' :: Fractional a => Quantity Rational u -> Quantity a u

Convert a Rational quantity into any Fractional type (fromRational).

Unit-safe Floating operations

sqrt' :: (Floating a, w ~~ (u ^: 2)) => Quantity a w -> Quantity a u

Taking the square root (sqrt) of a quantity requires its units to be a square. Fractional units are not currently supported.

TH constructor for quantities/units

u :: QuasiQuoter

The u quasiquoter may be used to create units or quantities; its meaning depends on the context:

• in a declaration context, it creates new base and derived units from a comma-separated list of names with optional definitions, for example [u|kg, m, s, N = kg * m/s^2|];
• in a type context, it parses a single unit and converts it into the corresponding type, so [u|m/s|] becomes the type Base "m" /: Base "s" of kind Unit;
• in an expression context, it can be used to create a Quantity corresponding to a numeric literal, for example [u|42 m|] is an expression of type Quantity Integer (Base "m"), [u|-2.2 m|] is an expression of type Quantity Double (Base "m"), and [u|m|] alone is a function of type a -> Quantity a (Base "m");
• in a pattern context, it can be used to match on a particular value of a quantity with an Integer or Rational representation type, for example f [u| 42 m |] = True is a (partial) function of type Quantity Integer [u|m|] -> Bool.

Declaring units

declareBaseUnit :: String -> Q [Dec]

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 |].

declareDerivedUnit :: String -> 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 |].

declareConvertibleUnit :: String -> Rational -> 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.

Automatic unit conversions

convert :: forall a u v. (Fractional a, Convertible u v) => Quantity a u -> Quantity a v

Automatically convert a quantity with units u so that its units are v, provided u and v have the same dimension.

Pay no attention to that man behind the curtain

type family MkUnit s :: Unit

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.

Instances

type MkUnit "A" = Base "A"

type MkUnit "C" = (*:) (MkUnit "s") (MkUnit "A")

type MkUnit "F" = (/:) (MkUnit "C") (MkUnit "V")

type MkUnit "Hz" = (/:) One ((^:) (MkUnit "s") 1)

type MkUnit "J" = (*:) (MkUnit "N") (MkUnit "m")

type MkUnit "K" = Base "K"

type MkUnit "N" = (/:) ((*:) (MkUnit "kg") (MkUnit "m")) ((^:) (MkUnit "s") 2)

type MkUnit "Pa" = (/:) (MkUnit "N") ((^:) (MkUnit "m") 2)

type MkUnit "V" = (/:) (MkUnit "W") (MkUnit "A")

type MkUnit "W" = (/:) (MkUnit "J") (MkUnit "s")

type MkUnit "au" = Base "au"

type MkUnit "cd" = Base "cd"

type MkUnit "d" = Base "d"

type MkUnit "ft" = Base "ft"

type MkUnit "g" = Base "g"

type MkUnit "h" = Base "h"

type MkUnit "ha" = Base "ha"

type MkUnit "in" = Base "in"

type MkUnit "kg" = Base "kg"

type MkUnit "km" = Base "km"

type MkUnit "l" = Base "l"

type MkUnit "m" = Base "m"

type MkUnit "mi" = Base "mi"

type MkUnit "min" = Base "min"

type MkUnit "mol" = Base "mol"

type MkUnit "mph" = (/:) (MkUnit "mi") (MkUnit "h")

type MkUnit "ohm" = (/:) (MkUnit "V") (MkUnit "A")

type MkUnit "rad" = Base "rad"

type MkUnit "s" = Base "s"

type MkUnit "sr" = Base "sr"

type MkUnit "t" = Base "t"

type family Pack u :: Unit

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).

Equations

Pack (xs :/ ys) = Prod xs /: Prod ys

type family Unpack u :: UnitSyntax Symbol

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.

class KnownUnit u

A constraint KnownUnit u means that u must be a concrete unit that is statically known but passed at runtime

Minimal complete definition

unitSing

Instances

(KnownList xs, KnownList ys) => KnownUnit ((:/) Symbol xs ys)