Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
This module gives a brief introduction to the uom-plugin
library.
Synopsis
Introduction
The uom-plugin
adds support for type safe units of measure. Its
typechecker plugin automatically solves equality constraints between units
of measure.
Setup
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.
Interactive Setup
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
The Unit
Kind
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"
Declaring Units
Base and derived units need to be declared before use, otherwise you will
get unsolved constraints like
. When
the TH quasiquoter KnownUnit
(Unpack
(MkUnit
"m"))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.
Creating Quantities
A numeric value a
annotated with units u
is a
. Without using the internal Quantity
a
u
constructor, we can use
literals, multiplication by 1 and unit attaching functions to create
quantities.MkQuantity
Literals
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 |]
Dimensionless Literals
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
Multiplication by 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 |]
Attaching Units
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 |]
Detaching Units
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
Operations on Quantities
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"... ...
Unit Polymorphism
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)