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

Language | Haskell2010 |

This module gives a brief introduction to the `uom-plugin`

library.

# Documentation

### Prerequisites

To use the `uom-plugin`

library, simply import Data.UnitsOfMeasure
and pass the option `-fplugin Data.UnitsOfMeasure.Plugin`

to GHC, for
example by adding the following above the module header of your source
files:

{-# OPTIONS_GHC -fplugin Data.UnitsOfMeasure.Plugin #-}

This will enable the typechecker plugin, which automatically solves equality constraints between units of measure. You will also need some language extensions:

{-# LANGUAGE DataKinds, QuasiQuotes, TypeOperators #-}

In order to declare new units, you will need:

{-# LANGUAGE TypeFamilies, UndecidableInstances #-}

### Interactive use

If experimenting with `uom-plugin`

in GHCi you will need to
activate the plugin with the command

`>>>`

`:seti -fplugin Data.UnitsOfMeasure.Plugin`

otherwise you will get mysterious unsolved constraint errors. You will probably also need the extensions:

`>>>`

`:seti -XDataKinds -XQuasiQuotes -XTypeOperators`

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

). For example,

`>>>`

One :: Unit`:kind One`

`>>>`

Base "m" /: Base "s" :: Unit`:kind Base "m" /: Base "s"`

The TH quasiquoter `u`

is provided to give a nice syntax for units
(see `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`

, for example

`>>>`

[u| m^2 |] :: Unit = Base "m" ^: 2`:kind! [u| m^2 |]`

`>>>`

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

### Declaring base and derived 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 as in a declaration context, it
creates new base or derived units. Alternatively,
`declareBaseUnit`

and `declareDerivedUnit`

can be used as top-level
TH declaration splices. For example:

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

is a numeric value annotated with its units.
Quantities can be created using the `u`

quasiquoter in an
expression, for example `[u| 5 m |]`

or `[u| 2.2 m/s^2 |]`

. The
syntax consists of an integer or decimal number, followed by a
unit.

The type of a quantity includes the underlying representation type and the unit, for example:

[u| 5 m |] :: Quantity Int (Base "m")

or using the `u`

quasiquoter in the type as well:

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

Numeric literals may be used to produce dimensionless quantities
(i.e. those with unit `One`

):

2 :: Quantity Int One

The underlying numeric value of a quantity may be extracted with
`unQuantity`

:

`>>>`

15`unQuantity [u| 15 kg |]`

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

`>>>`

Couldn't match type ‘Base "m"’ with ‘One’...`2 * [u| 5 m |]`

`>>>`

Couldn't match type ‘Base "m" /: Base "s"’ with ‘One’...`[u| 2 m/s |] + [u| 5 m/s |]`

Instead, Data.UnitsOfMeasure provides more general arithmetic
operators including (`+:`

), (`-:`

), (`*:`

) and (`/:`

). These may
be used to perform unit-safe arithmetic:

`>>>`

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

`>>>`

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

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

`>>>`

Couldn't match type ‘Base "s"’ with ‘Base "m"’...`[u| 3 m |] -: [u| 1 s |]`

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

`>>>`

cube :: Num a => Quantity a v -> Quantity a (v ^: 3)`:t cube`

`>>>`

`let f x y = (x *: y) +: (y *: x)`

`>>>`

f :: Num a => Quantity a v -> Quantity a u -> Quantity a (u *: v)`:t f`