This module gives a brief introduction to the uom-plugin library.

The uom-plugin adds support for type safe units of measure. Its typechecker plugin automatically solves equality constraints between units of measure.

To use the uom-plugin library, import Data.UnitsOfMeasure after making GHC aware of the plugin and enabling language extensions.

>>> {-# OPTIONS_GHC -fplugin Data.UnitsOfMeasure.Plugin #-}
>>> {-# LANGUAGE DataKinds, QuasiQuotes, TypeOperators #-}
>>> import Data.UnitsOfMeasure

In a module that imports the library but has not enabled the plugin or enabled the required extensions you will likely get mysterious unsolved constraint errors when working with units. It is only with the plugin enabled that GHC can solve these.

To start experimenting with uom-plugin in GHCi you will need to do the equivalent setup.

>>> :seti -fplugin Data.UnitsOfMeasure.Plugin -XDataKinds -XQuasiQuotes -XTypeOperators
>>> import Data.UnitsOfMeasure

Units of measure, such as kilograms or metres per second, are represented by the abstract kind Unit. They can be built out of One, Base, (*:), (/:) and (^:). Base units are represented as type-level strings (with kind Symbol).

>>> :kind One
One :: Unit
>>> :kind Base "m" /: Base "s"
Base "m" /: Base "s" :: Unit

The template Haskell quasiquoter u gives a nice syntax for units (see module Text.Parse.Units from the units-parser package for details of the syntax). When used in a type, the quasiquoter produces an expression of kind Unit.

>>> :kind! [u| m^2 |]
[u| m^2 |] :: Unit
= Base "m" *: Base "m"
>>> :kind! [u| kg m/s |]
[u| kg m/s |] :: Unit
= (Base "kg" *: Base "m") /: Base "s"

Base and derived units need to be declared before use, otherwise you will get unsolved constraints like KnownUnit (Unpack (MkUnit "m")). When the TH quasiquoter u is used in a declaration context, it creates new base or derived units. Alternatively, declareBaseUnit and declareDerivedUnit can be used as top-level TH declaration splices. Where declaring new units, you will also need a couple more extensions.

>>> {-# LANGUAGE TypeFamilies, UndecidableInstances #-}

declareBaseUnit "m"
declareDerivedUnit "N" "kg m / s^2"
[u| kg, s |]

Note that these lines must appear in a module, not GHCi. For experimenting interactively, Data.UnitsOfMeasure.Defs provides definitions of common units, but is subject to change.

A numeric value a annotated with units u is a Quantity a u. Without using the internal MkQuantity constructor, we can use literals, multiplication by 1 and unit attaching functions to create quantities.

For literal quantities use the u quasiquoter, putting the number before the unit. The most general polymorphic type will be inferred.

>>> :type [u| 1 m |]
[u| 1 m |] :: Num a => Quantity a (Base "m")
>>> :type [u| 1.0 m |]
[u| 1.0 m |] :: Fractional a => Quantity a (Base "m")
>>> :type [u| 1 % 1 m |]
[u| 1 % 1 m |] :: Fractional a => Quantity a (Base "m")

Adding a full or partial type signature can make the underlying representational type more concrete.

>>> :seti -XPartialTypeSignatures -fno-warn-partial-type-signatures

>>> :type [u| 1 m |] :: _ Int _
[u| 1 m |] :: _ Int _ :: Quantity Int (Base "m")
>>> :type [u| 1 m |] :: _ Double _
[u| 1 m |] :: _ Double _ :: Quantity Double (Base "m")
>>> :type [u| 1 m |] :: _ Rational _
[u| 1 m |] :: _ Rational _ :: Quantity Rational (Base "m")

Note how the u quasiquoter can be used for the units in the type too. This is redundant repetition with a literal but is useful when adding type signatures elsewhere.

>>> [u| 1.1 m / s |] :: Quantity Double [u| m / s |]
[u| 1.1 m / s |]

The units parser handles various number formats.

>>> [u| 0o1327 Hz |]
[u| 727 s^-1 |]
>>> [u| 0x2d7 Hz |]
[u| 727 s^-1 |]
>>> [u| 325e-2 in |]
[u| 3.25 in |]
>>> [u| 36E+2 s |]
[u| 3600.0 s |]
>>> [u| 14.67e1 mi |]
[u| 146.7 mi |]

Without putting the numeric value in a quotation and without templating altogether we can create dimensionless units, those with units of One.

>>> 1 :: Quantity Int One
[u| 1 |]
>>> [u| 1 |]
[u| 1 |]
>>> :type [u| 1 |]
[u| 1 |] :: Num a => Quantity a One
>>> :type 1 :: Quantity _ [u| 1 |]
1 :: Quantity _ [u| 1 |] :: Num w => Quantity w One
>>> :type 1.0 :: Quantity _ One
1.0 :: Quantity _ One :: Fractional w => Quantity w One

Quoted rationals are fine but type annotating them as dimensionless quantities will not work.

>>> :type [u| 1 % 1 |]
[u| 1 % 1 |] :: Fractional a => Quantity a One
>>> import Data.Ratio ((%))
>>> :type (1 % 1) :: Quantity _ One

...
...Couldn't match expected type...Quantity w1 One...
...with actual type...GHC.Real.Ratio...
...

Things get a little weird when not being explicit about Quantity.

>>> :type 1 :: _ _ [u| 1 |]
1 :: _ _ [u| 1 |]
  :: ...
     Num (w1 w2 One) =>
     w1 w2 One
>>> :type 1 :: _ _ One
1 :: _ _ One
  :: ...
     Num (w1 w2 One) =>
     w1 w2 One
>>> :type 1.0 :: _ _ One
1.0 :: _ _ One
  :: ...
     Fractional (w1 w2 One) =>
     w1 w2 One

The product of a numeric value and one of a unit will attach those units to the value.

>>> [u| 1 m s^-2 |] *: 9.8
[u| 9.8 m / s^2 |]
>>> 9.8 *: [u| 1 m s^-2 |]
[u| 9.8 m / s^2 |]

The same trick works with dimensionless values.

>>> [u| 1 m s^-2 |] *: [u| 9.8 |]
[u| 9.8 m / s^2 |]
>>> [u| 9.8 |] *: [u| 1 m s^-2 |]
[u| 9.8 m / s^2 |]

Quoted units without a value specialise to functions we can use to attach units to unitless numeric values.

>>> [u| m / s^2 |] 9.8
[u| 9.8 m / s^2 |]
>>> [u| m s^-2 |] 9.8
[u| 9.8 m / s^2 |]
>>> [u| m / s / s |] 9.8
[u| 9.8 m / s^2 |]
>>> [u| s^-2 m |] 9.8
[u| 9.8 m / s^2 |]

Composition of these functions doesn't work as expected. It doesn't apply composed units to the numeric value.

>>> [u| m |] $ [u| s^-2 |] 9.8
[u| [u| 9.8 s^-2 |] m |]
>>> [u| s^-2 |] $ [u| m |] 9.8
[u| [u| 9.8 m |] s^-2 |]
>>> [u| m |] . [u| s^-2 |] $ 9.8
[u| [u| 9.8 s^-2 |] m |]
>>> [u| s^-2 |] . [u| m |] $ 9.8
[u| [u| 9.8 m |] s^-2 |]
>>> [u| m |] [u| 9.8 s^-2 |]
[u| [u| 9.8 s^-2 |] m |]
>>> [u| s^-2 |] [u| 9.8 m |]
[u| [u| 9.8 m |] s^-2 |]
>>> [u| m |] . [u| s^-1 |] . [u| s^-1 |] $ 9.8
[u| [u| [u| 9.8 s^-1 |] s^-1 |] m |]

The underlying numeric value of a quantity may be extracted with unQuantity, detaching the units:

>>> unQuantity [u| 15 kg |]
15
>>> unQuantity [u| 9.8 m / s^2 |]
9.8
>>> unQuantity <$> [[u| 1 kg |], [u| 2 kg |]]
[1,2]
>>> unQuantity . [u| kg |] <$> [1,2]
[1,2]
>>> :type unQuantity . [u| kg |]
unQuantity . [u| kg |] :: c -> c

The usual arithmetic operators from Num and related typeclasses are restricted to operating on dimensionless quantities. Thus using them directly on quantities with units will result in errors:

>>> 2 * [u| 5 m |]

...
... Couldn't match type...Base "m"...with...One...
...

>>> [u| 2 m/s |] + [u| 5 m/s |]

...
... Couldn't match type...Base "m" /: Base "s"...with...One...
...

Instead, Data.UnitsOfMeasure provides more general arithmetic operators including (+:), (-:), (*:) and (/:). These may be used to perform unit-safe arithmetic:

>>> 2 *: [u| 5 m |]
[u| 10 m |]

>>> [u| 2 m / s |] +: [u| 5 m / s |]
[u| 7 m / s |]

However, unit errors will be detected by the type system:

>>> [u| 3 m |] -: [u| 1 s |]

...
... Couldn't match type...Base "s"
... with...Base "m"...
...

It is easy to work with arbitrary units (type variables of kind Unit) rather than particular choices of unit. The typechecker plugin ensures that type inference is well-behaved and automatically solves equations between units (e.g. making unit multiplication commutative):

>>> let cube x = x *: x *: x
>>> :t cube
cube :: Num a => Quantity a v -> Quantity a (v *: (v *: v))

>>> let f x y = (x *: y) +: (y *: x)
>>> :t f
f :: Num a => Quantity a v -> Quantity a u -> Quantity a (u *: v)

• Paper about uom-plugin
• Plugins on the GHC wiki