Summary

In this module we provide data types for performing arithmetic with physical quantities and units. Information about the physical dimensions of the quantities/units is embedded in their types and the validity of operations is verified by the type checker at compile time. The boxing and unboxing of numerical values as quantities is done by multiplication and division of units, of which an incomplete set is provided.

We limit ourselves to "Newtonian" physics. We do not attempt to accommodate relativistic physics in which e.g. addition of length and time would be valid.

As far as possible and/or practical the conventions and guidelines of NIST's "Guide for the Use of the International System of Units (SI)" [1] are followed. Occasionally we will reference specific sections from the guide and deviations will be explained.

Disclaimer

Merely an engineer, the author doubtlessly uses a language and notation that makes mathematicians and physicist cringe. He does not mind constructive criticism (or pull requests).

The sets of functions and units defined herein are incomplete and reflect only the author's needs to date. Again, patches are welcome.

Usage

Preliminaries

This module requires GHC 7.8 or later. We utilize Data Kinds, TypeNats, Closed Type Families, etc. Clients of the module are generally not required to use these extensions.

Clients probably will want to use the NegativeLiterals extension.

Examples

We have defined operators and units that allow us to define and work with physical quantities. A physical quantity is defined by multiplying a number with a unit (the type signature is optional).

v :: Velocity Prelude.Double
v = 90 *~ (kilo meter / hour)

It follows naturally that the numerical value of a quantity is obtained by division by a unit.

numval :: Prelude.Double
numval = v /~ (meter / second)

The notion of a quantity as the product of a numerical value and a unit is supported by 7.1 "Value and numerical value of a quantity" of [1]. While the above syntax is fairly natural it is unfortunate that it must violate a number of the guidelines in [1], in particular 9.3 "Spelling unit names with prefixes", 9.4 "Spelling unit names obtained by multiplication", 9.5 "Spelling unit names obtained by division".

As a more elaborate example of how to use the module we define a function for calculating the escape velocity of a celestial body [2].

escapeVelocity :: (Floating a) => Mass a -> Length a -> Velocity a
escapeVelocity m r = sqrt (two * g * m / r)
  where
      two = 2 *~ one
      g = 6.6720e-11 *~ (newton * meter ^ pos2 / kilo gram ^ pos2)

The following is an example GHC session where the above function is used to calculate the escape velocity of Earth in kilometer per second.

>>> :set +t
>>> let me = 5.9742e24 *~ kilo gram -- Mass of Earth.
me :: Quantity DMass GHC.Float.Double
>>> let re = 6372.792 *~ kilo meter -- Mean radius of Earth.
re :: Quantity DLength GHC.Float.Double
>>> let ve = escapeVelocity me re   -- Escape velocity of Earth.
ve :: Velocity GHC.Float.Double
>>> ve /~ (kilo meter / second)
11.184537332296259
it :: GHC.Float.Double

For completeness we should also show an example of the error messages we will get from GHC when performing invalid arithmetic. In the best case GHC will be able to use the type synonyms we have defined in its error messages.

>>> x = 1 *~ meter + 1 *~ second
Couldn't match type 'Numeric.NumType.DK.Integers.Zero
               with 'Numeric.NumType.DK.Integers.Pos1
  Expected type: Unit 'Metric DLength a
    Actual type: Unit 'Metric DTime a
  In the second argument of `(*~)', namely `second'
  In the second argument of `(+)', namely `1 *~ second'

In other cases the error messages aren't very friendly.

>>> x = 1 *~ meter / (1 *~ second) + 1 *~ kilo gram
Couldn't match type 'Numeric.NumType.DK.Integers.Zero
               with 'Numeric.NumType.DK.Integers.Neg1
  Expected type: Quantity DMass a
    Actual type: Dimensional
                   ('Numeric.Units.Dimensional.Variants.DQuantity
                    Numeric.Units.Dimensional.Variants.* 'Numeric.Units.Dimensional.Variants.DQuantity)
                   (DLength / DTime)
                   a
  In the first argument of `(+)', namely `1 *~ meter / (1 *~ second)'
  In the expression: 1 *~ meter / (1 *~ second) + 1 *~ kilo gram
  In an equation for `x':
      x = 1 *~ meter / (1 *~ second) + 1 *~ kilo gram

It is the author's experience that the usefullness of the compiler error messages is more often than not limited to pinpointing the location of errors.

Notes

Future work

While there is an insane amount of units in use around the world it is reasonable to provide at least all SI units. Units outside of SI will most likely be added on an as-needed basis.

There are also plenty of elementary functions to add. The Floating class can be used as reference.

Additional physics models could be implemented. See [3] for ideas.

Related work

Henning Thielemann numeric prelude has a physical units library, however, checking of dimensions is dynamic rather than static. Aaron Denney has created a toy example of statically checked physical dimensions covering only length and time. HaskellWiki has pointers [4] to these.

Also see Samuel Hoffstaetter's blog post [5] which uses techniques similar to this library.

Libraries with similar functionality exist for other programming languages and may serve as inspiration. The author has found the Java library JScience [6] and the Fortress programming language [7] particularly noteworthy.

References

1. http://physics.nist.gov/Pubs/SP811/
2. http://en.wikipedia.org/wiki/Escape_velocity
3. http://jscience.org/api/org/jscience/physics/models/package-summary.html
4. http://www.haskell.org/haskellwiki/Physical_units
5. http://liftm.wordpress.com/2007/06/03/scientificdimension-type-arithmetic-and-physical-units-in-haskell/
6. http://jscience.org/
7. http://research.sun.com/projects/plrg/fortress.pdf

Our primary objective is to define a data type that can be used to represent (while still differentiating between) units and quantities. There are two reasons for consolidating units and quantities in one data type. The first being to allow code reuse as they are largely subject to the same operations. The second being that it allows reuse of operators (and functions) between the two without resorting to occasionally cumbersome type classes.

The relationship between (the value of) a Quantity, its numerical value and its Unit is described in 7.1 "Value and numerical value of a quantity" of [1]. In short a Quantity is the product of a number and a Unit. We define the *~ operator as a convenient way to declare quantities as such a product.

The phantom type variable d encompasses the physical dimension of a Dimensional. As detailed in [5] there are seven base dimensions, which can be combined in integer powers to a given physical dimension. We represent physical dimensions as the powers of the seven base dimensions that make up the given dimension. The powers are represented using NumTypes. For convenience we collect all seven base dimensions in a data kind Dimension.

We could have chosen to provide type variables for the seven base dimensions in Dimensional instead of creating a new data kind Dimension. However, that would have made any type signatures involving Dimensional very cumbersome. By encompassing the physical dimension in a single type variable we can "hide" the cumbersome type arithmetic behind convenient type classes as will be seen later.

When performing arithmetic on units and quantities the arithmetics must be applied to both the numerical values of the Dimensionals but also to their physical dimensions. The type level arithmetic on physical dimensions is governed by closed type families expressed as type operators.

We could provide the Mul and Div classes with full functional dependencies but that would be of limited utility as there is no limited use for "backwards" type inference. Efforts are underway to develop a type-checker plugin that does enable these scenarios, e.g. for linear algebra.

To facilitate parsing and pretty-printing functions that may wish to operate on term-level representations of dimension, we provide a means for converting from type-level dimensions to term-level dimensions.

Here we define operators and functions to make working with homogenuous lists of dimensionals more convenient.

We define two convenience operators for applying units to all elements of a functor (e.g. a list).

Using our Dimension data kind we define some type synonyms for convenience. We start with the base dimensions, others can be found in Numeric.Units.Dimensional.Quantities.

Using the above type synonyms we can define type synonyms for quantities of particular physical dimensions.

Again we limit ourselves to the base dimensions, others can be found in Numeric.Units.Dimensional.Quantities.

For convenience we define some constants for small integer values that often show up in formulae. We also throw in pi and tau for good measure.

We intentionally decline to provide a Functor instance for Dimensional because its use breaks the abstraction of physical dimensions.

If you feel your work requires this instance, it is provided as an orphan in Numeric.Units.Dimensional.Functor.