-- | This module gives a brief introduction to the @uom-plugin@ -- library. {-# OPTIONS_GHC -fno-warn-unused-imports #-} module Data.UnitsOfMeasure.Tutorial ( -- $tutorial ) where import Data.UnitsOfMeasure -- $tutorial -- -- === 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', ('Data.UnitsOfMeasure.Internal.*:'), -- ('Data.UnitsOfMeasure.Internal./:') and -- ('Data.UnitsOfMeasure.Internal.^:'). 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) -- -- -- == Further reading -- -- * <http://adam.gundry.co.uk/pub/typechecker-plugins/ Paper about uom-plugin> -- -- * <https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker Plugins on the GHC wiki>