Safe Haskell | None |
---|---|

Language | Haskell2010 |

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

- data Unit
- type family Base (b :: Symbol) :: Unit where ...
- type family One :: Unit where ...
- type family (u :: Unit) *: (v :: Unit) :: Unit where ...
- type family (u :: Unit) /: (v :: Unit) :: Unit where ...
- type family (u :: Unit) ^: (n :: Nat) :: Unit where ...
- data Quantity a (u :: Unit)
- unQuantity :: Quantity a u -> a
- zero :: Num a => Quantity a u
- mk :: a -> Quantity a One
- (+:) :: Num a => Quantity a u -> Quantity a u -> Quantity a u
- (*:) :: (Num a, w ~~ (u *: v)) => Quantity a u -> Quantity a v -> Quantity a w
- (-:) :: Num a => Quantity a u -> Quantity a u -> Quantity a u
- negate' :: Num a => Quantity a u -> Quantity a u
- abs' :: Num a => Quantity a u -> Quantity a u
- signum' :: Num a => Quantity a u -> Quantity a One
- fromInteger' :: Integral a => Quantity Integer u -> Quantity a u
- (/:) :: (Fractional a, w ~~ (u /: v)) => Quantity a u -> Quantity a v -> Quantity a w
- recip' :: (Fractional a, w ~~ (One /: u)) => Quantity a u -> Quantity a w
- fromRational' :: Fractional a => Quantity Rational u -> Quantity a u
- toRational' :: Real a => Quantity a u -> Quantity Rational u
- sqrt' :: (Floating a, w ~~ (u ^: 2)) => Quantity a w -> Quantity a u
- u :: QuasiQuoter
- declareBaseUnit :: String -> Q [Dec]
- declareDerivedUnit :: String -> String -> Q [Dec]
- declareConvertibleUnit :: String -> Rational -> String -> Q [Dec]
- convert :: forall a u v. (Fractional a, Convertible u v) => Quantity a u -> Quantity a v
- type family MkUnit (s :: Symbol) :: Unit
- type family Pack (u :: UnitSyntax Symbol) :: Unit where ...
- type family Unpack (u :: Unit) :: UnitSyntax Symbol where ...
- class KnownUnit (u :: UnitSyntax Symbol)

# Type-level units of measure

type family (u :: Unit) *: (v :: Unit) :: Unit where ... infixl 7 Source #

Multiplication for units of measure

type family (u :: Unit) /: (v :: Unit) :: Unit where ... infixl 7 Source #

Division for units of measure

type family (u :: Unit) ^: (n :: Nat) :: Unit where ... infixr 8 Source #

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

# Values indexed by their units

data Quantity a (u :: Unit) Source #

A `Quantity a u`

is represented identically to a value of
underlying numeric type `a`

, but with units `u`

.

Bounded a => Bounded (Quantity a u) Source # | |

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

Eq a => Eq (Quantity a u) Source # | |

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

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

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

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

Ord a => Ord (Quantity a u) Source # | |

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

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

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

Storable a => Storable (Quantity a u) Source # | |

NFData a => NFData (Quantity a u) Source # | |

unQuantity :: Quantity a u -> a Source #

Extract the underlying value of a quantity

zero :: Num a => Quantity a u Source #

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 Source #

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 Source #

Addition (`+`

) of quantities requires the units to match.

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

Multiplication (`*`

) of quantities multiplies the units.

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

Subtraction (`-`

) of quantities requires the units to match.

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

Negation (`negate`

) of quantities is polymorphic in the units.

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

Absolute value (`abs`

) of quantities is polymorphic in the units.

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

The sign (`signum`

) of a quantity gives a dimensionless result.

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

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 Source #

Division (`/`

) of quantities divides the units.

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

Reciprocal (`recip`

) of quantities reciprocates the units.

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

Convert a `Rational`

quantity into any `Fractional`

type (`fromRational`

).

# Unit-safe `Real`

operations

toRational' :: Real a => Quantity a u -> Quantity Rational u Source #

Convert any `Real`

quantity into a `Rational`

type (`toRational`

).

# Unit-safe `Floating`

operations

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

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 Source #

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
`[`

becomes the type`u`

|m/s|]

of kind`Base`

"m" /:`Base`

"s"`Unit`

; - in an expression context, it can be used to create a
`Quantity`

corresponding to a numeric literal, for example`[`

is an expression of type`u`

|42 m|]

,`Quantity`

`Integer`

(`Base`

"m")`[`

is an expression of type`u`

|-2.2 m|]

, and`Quantity`

`Double`

(`Base`

"m")`[`

alone is a function of type`u`

|m|]`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 [`

is a (partial) function of type`u`

| 42 m |] =`True`

.`Quantity`

`Integer`

[u|m|] -> Bool

# Declaring units

declareBaseUnit :: String -> Q [Dec] Source #

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] Source #

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] Source #

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 `[`

.
See Data.UnitsOfMeasure.Convert for more information about conversions.`u`

| kilobyte = 1024 byte |]

# Automatic unit conversions

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

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 :: Symbol) :: Unit Source #

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 MkUnit "A" Source # | |

type MkUnit "C" Source # | |

type MkUnit "F" Source # | |

type MkUnit "Hz" Source # | |

type MkUnit "J" Source # | |

type MkUnit "K" Source # | |

type MkUnit "N" Source # | |

type MkUnit "Pa" Source # | |

type MkUnit "V" Source # | |

type MkUnit "W" Source # | |

type MkUnit "au" Source # | |

type MkUnit "cd" Source # | |

type MkUnit "d" Source # | |

type MkUnit "ft" Source # | |

type MkUnit "g" Source # | |

type MkUnit "h" Source # | |

type MkUnit "ha" Source # | |

type MkUnit "in" Source # | |

type MkUnit "kg" Source # | |

type MkUnit "km" Source # | |

type MkUnit "l" Source # | |

type MkUnit "m" Source # | |

type MkUnit "mi" Source # | |

type MkUnit "min" Source # | |

type MkUnit "mol" Source # | |

type MkUnit "mph" Source # | |

type MkUnit "ohm" Source # | |

type MkUnit "rad" Source # | |

type MkUnit "s" Source # | |

type MkUnit "sr" Source # | |

type MkUnit "t" Source # | |

type family Pack (u :: UnitSyntax Symbol) :: Unit where ... Source #

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 Unpack (u :: Unit) :: UnitSyntax Symbol where ... Source #

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.