uom-plugin-0.2.0.1: Units of measure as a GHC typechecker plugin

Data.UnitsOfMeasure.Internal

Description

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.

Synopsis

# Type-level units of measure

data Unit Source

(Kind) Units of measure

type family One :: Unit Source

Dimensionless unit (identity element)

type family Base b :: Unit Source

Base unit

type family u *: v :: Unit infixl 7 Source

Multiplication for units of measure

type family u /: v :: Unit infixl 7 Source

Division for units of measure

type family u ^: n :: Unit infixr 8 Source

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

newtype Quantity a u Source

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

Constructors

 MkQuantity a Warning: the `MkQuantity` constructor allows module invariants to be violated, so use it with caution!

Instances

 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.

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 Source

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

# Syntactic representation of units

data UnitSyntax s Source

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

Constructors

 [s] :/ [s]

Instances

 Eq s => Eq (UnitSyntax s) Source Show s => Show (UnitSyntax s) Source TestEquality (UnitSyntax Symbol) SUnit Source

type family Unpack u :: UnitSyntax Symbol 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.

type family Pack u :: Unit 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).

Equations

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

type family Prod xs :: Unit Source

Take the product of a list of base units.

Equations

 Prod [] = One Prod (x : xs) = Base x *: Prod xs

# Internal

type family u ~~ v :: Constraint infix 4 Source

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 MkUnit s :: 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.

Instances

 type MkUnit "A" = Base "A" Source type MkUnit "C" = (*:) (MkUnit "s") (MkUnit "A") Source type MkUnit "F" = (/:) (MkUnit "C") (MkUnit "V") Source type MkUnit "Hz" = (/:) One ((^:) (MkUnit "s") 1) Source type MkUnit "J" = (*:) (MkUnit "N") (MkUnit "m") Source type MkUnit "K" = Base "K" Source type MkUnit "N" = (/:) ((*:) (MkUnit "kg") (MkUnit "m")) ((^:) (MkUnit "s") 2) Source type MkUnit "Pa" = (/:) (MkUnit "N") ((^:) (MkUnit "m") 2) Source type MkUnit "V" = (/:) (MkUnit "W") (MkUnit "A") Source type MkUnit "W" = (/:) (MkUnit "J") (MkUnit "s") Source type MkUnit "au" = Base "au" Source type MkUnit "cd" = Base "cd" Source type MkUnit "d" = Base "d" Source type MkUnit "ft" = Base "ft" Source type MkUnit "g" = Base "g" Source type MkUnit "h" = Base "h" Source type MkUnit "ha" = Base "ha" Source type MkUnit "in" = Base "in" Source type MkUnit "kg" = Base "kg" Source type MkUnit "km" = Base "km" Source type MkUnit "l" = Base "l" Source type MkUnit "m" = Base "m" Source type MkUnit "mi" = Base "mi" Source type MkUnit "min" = Base "min" Source type MkUnit "mol" = Base "mol" Source type MkUnit "mph" = (/:) (MkUnit "mi") (MkUnit "h") Source type MkUnit "ohm" = (/:) (MkUnit "V") (MkUnit "A") Source type MkUnit "rad" = Base "rad" Source type MkUnit "s" = Base "s" Source type MkUnit "sr" = Base "sr" Source type MkUnit "t" = Base "t" Source