Safe Haskell	None
Language	Haskell2010

Data.UnitsOfMeasure.Tutorial

Description

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

Synopsis

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,

>>> :kind One
One :: Unit

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

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

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

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

Declaring base and derived units

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

>>> unQuantity [u| 15 kg |]
15

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 ^: 3)

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