uom-plugin-0.3.0.0: Units of measure as a GHC typechecker plugin

Safe HaskellNone
LanguageHaskell2010

Data.UnitsOfMeasure.Internal

Contents

Description

This module defines the core types used in the uom-plugin library. Note that importing this module may allow you to violate invariants, so you should generally work with the safe interface in Data.UnitsOfMeasure instead.

Synopsis

Type-level units of measure

data Unit Source #

(Kind) Units of measure

type family One :: Unit where ... Source #

Dimensionless unit (identity element)

type family Base (b :: Symbol) :: Unit where ... Source #

Base unit

type family (u :: Unit) *: (v :: Unit) :: Unit where ... infixl 7 Source #

Multiplication for units of measure

type family (u :: Unit) /: (v :: Unit) :: Unit where ... infixl 7 Source #

Division for units of measure

type family (u :: Unit) ^: (n :: Nat) :: Unit where ... infixr 8 Source #

Exponentiation (to a positive power) for units of measure; negative exponents are not yet supported (they require an Integer kind)

Equations

u ^: 0 = One 
u ^: 1 = u 
u ^: n = u *: (u ^: (n - 1)) 

Values indexed by their units

newtype Quantity a (u :: Unit) Source #

A Quantity a u is represented identically to a value of underlying numeric type a, but with units u.

Constructors

MkQuantity a

Warning: the MkQuantity constructor allows module invariants to be violated, so use it with caution!

Instances

Bounded a => Bounded (Quantity a u) Source # 

Methods

minBound :: Quantity a u #

maxBound :: Quantity a u #

(Enum a, (~) Unit u One) => Enum (Quantity a u) Source # 

Methods

succ :: Quantity a u -> Quantity a u #

pred :: Quantity a u -> Quantity a u #

toEnum :: Int -> Quantity a u #

fromEnum :: Quantity a u -> Int #

enumFrom :: Quantity a u -> [Quantity a u] #

enumFromThen :: Quantity a u -> Quantity a u -> [Quantity a u] #

enumFromTo :: Quantity a u -> Quantity a u -> [Quantity a u] #

enumFromThenTo :: Quantity a u -> Quantity a u -> Quantity a u -> [Quantity a u] #

Eq a => Eq (Quantity a u) Source # 

Methods

(==) :: Quantity a u -> Quantity a u -> Bool #

(/=) :: Quantity a u -> Quantity a u -> Bool #

(Floating a, (~) Unit u One) => Floating (Quantity a u) Source # 

Methods

pi :: Quantity a u #

exp :: Quantity a u -> Quantity a u #

log :: Quantity a u -> Quantity a u #

sqrt :: Quantity a u -> Quantity a u #

(**) :: Quantity a u -> Quantity a u -> Quantity a u #

logBase :: Quantity a u -> Quantity a u -> Quantity a u #

sin :: Quantity a u -> Quantity a u #

cos :: Quantity a u -> Quantity a u #

tan :: Quantity a u -> Quantity a u #

asin :: Quantity a u -> Quantity a u #

acos :: Quantity a u -> Quantity a u #

atan :: Quantity a u -> Quantity a u #

sinh :: Quantity a u -> Quantity a u #

cosh :: Quantity a u -> Quantity a u #

tanh :: Quantity a u -> Quantity a u #

asinh :: Quantity a u -> Quantity a u #

acosh :: Quantity a u -> Quantity a u #

atanh :: Quantity a u -> Quantity a u #

log1p :: Quantity a u -> Quantity a u #

expm1 :: Quantity a u -> Quantity a u #

log1pexp :: Quantity a u -> Quantity a u #

log1mexp :: Quantity a u -> Quantity a u #

(Fractional a, (~) Unit u One) => Fractional (Quantity a u) Source # 

Methods

(/) :: Quantity a u -> Quantity a u -> Quantity a u #

recip :: Quantity a u -> Quantity a u #

fromRational :: Rational -> Quantity a u #

(Integral a, (~) Unit u One) => Integral (Quantity a u) Source # 

Methods

quot :: Quantity a u -> Quantity a u -> Quantity a u #

rem :: Quantity a u -> Quantity a u -> Quantity a u #

div :: Quantity a u -> Quantity a u -> Quantity a u #

mod :: Quantity a u -> Quantity a u -> Quantity a u #

quotRem :: Quantity a u -> Quantity a u -> (Quantity a u, Quantity a u) #

divMod :: Quantity a u -> Quantity a u -> (Quantity a u, Quantity a u) #

toInteger :: Quantity a u -> Integer #

(Num a, (~) Unit u One) => Num (Quantity a u) Source # 

Methods

(+) :: Quantity a u -> Quantity a u -> Quantity a u #

(-) :: Quantity a u -> Quantity a u -> Quantity a u #

(*) :: Quantity a u -> Quantity a u -> Quantity a u #

negate :: Quantity a u -> Quantity a u #

abs :: Quantity a u -> Quantity a u #

signum :: Quantity a u -> Quantity a u #

fromInteger :: Integer -> Quantity a u #

Ord a => Ord (Quantity a u) Source # 

Methods

compare :: Quantity a u -> Quantity a u -> Ordering #

(<) :: Quantity a u -> Quantity a u -> Bool #

(<=) :: Quantity a u -> Quantity a u -> Bool #

(>) :: Quantity a u -> Quantity a u -> Bool #

(>=) :: Quantity a u -> Quantity a u -> Bool #

max :: Quantity a u -> Quantity a u -> Quantity a u #

min :: Quantity a u -> Quantity a u -> Quantity a u #

(Real a, (~) Unit u One) => Real (Quantity a u) Source # 

Methods

toRational :: Quantity a u -> Rational #

(RealFloat a, (~) Unit u One) => RealFloat (Quantity a u) Source # 
(RealFrac a, (~) Unit u One) => RealFrac (Quantity a u) Source # 

Methods

properFraction :: Integral b => Quantity a u -> (b, Quantity a u) #

truncate :: Integral b => Quantity a u -> b #

round :: Integral b => Quantity a u -> b #

ceiling :: Integral b => Quantity a u -> b #

floor :: Integral b => Quantity a u -> b #

Storable a => Storable (Quantity a u) Source # 

Methods

sizeOf :: Quantity a u -> Int #

alignment :: Quantity a u -> Int #

peekElemOff :: Ptr (Quantity a u) -> Int -> IO (Quantity a u) #

pokeElemOff :: Ptr (Quantity a u) -> Int -> Quantity a u -> IO () #

peekByteOff :: Ptr b -> Int -> IO (Quantity a u) #

pokeByteOff :: Ptr b -> Int -> Quantity a u -> IO () #

peek :: Ptr (Quantity a u) -> IO (Quantity a u) #

poke :: Ptr (Quantity a u) -> Quantity a u -> IO () #

NFData a => NFData (Quantity a u) Source # 

Methods

rnf :: Quantity a u -> () #

unQuantity :: Quantity a u -> a Source #

Extract the underlying value of a quantity

zero :: Num a => Quantity a u Source #

Zero is polymorphic in its units: this is required because the Num instance constrains the quantity to be dimensionless, so 0 :: Quantity a u is not well typed.

mk :: a -> Quantity a One Source #

Construct a Quantity from a dimensionless value. Note that for numeric literals, the Num and Fractional instances allow them to be treated as quantities directly.

Unit-safe Num operations

(+:) :: Num a => Quantity a u -> Quantity a u -> Quantity a u infixl 6 Source #

Addition (+) of quantities requires the units to match.

(*:) :: (Num a, w ~~ (u *: v)) => Quantity a u -> Quantity a v -> Quantity a w infixl 7 Source #

Multiplication (*) of quantities multiplies the units.

(-:) :: Num a => Quantity a u -> Quantity a u -> Quantity a u infixl 6 Source #

Subtraction (-) of quantities requires the units to match.

negate' :: Num a => Quantity a u -> Quantity a u Source #

Negation (negate) of quantities is polymorphic in the units.

abs' :: Num a => Quantity a u -> Quantity a u Source #

Absolute value (abs) of quantities is polymorphic in the units.

signum' :: Num a => Quantity a u -> Quantity a One Source #

The sign (signum) of a quantity gives a dimensionless result.

fromInteger' :: Integral a => Quantity Integer u -> Quantity a u Source #

Convert an Integer quantity into any Integral type (fromInteger).

Unit-safe Fractional operations

(/:) :: (Fractional a, w ~~ (u /: v)) => Quantity a u -> Quantity a v -> Quantity a w infixl 7 Source #

Division (/) of quantities divides the units.

recip' :: (Fractional a, w ~~ (One /: u)) => Quantity a u -> Quantity a w Source #

Reciprocal (recip) of quantities reciprocates the units.

fromRational' :: Fractional a => Quantity Rational u -> Quantity a u Source #

Convert a Rational quantity into any Fractional type (fromRational).

Unit-safe Real operations

toRational' :: Real a => Quantity a u -> Quantity Rational u Source #

Convert any Real quantity into a Rational type (toRational).

Unit-safe Floating operations

sqrt' :: (Floating a, w ~~ (u ^: 2)) => Quantity a w -> Quantity a u Source #

Taking the square root (sqrt) of a quantity requires its units to be a square. Fractional units are not currently supported.

Syntactic representation of units

data UnitSyntax s Source #

Syntactic representation of a unit as a pair of lists of base units, for example One is represented as [] :/ [] and Base "m" /: Base "s" ^: 2 is represented as ["m"] :/ ["s","s"].

Constructors

[s] :/ [s] 

Instances

Eq s => Eq (UnitSyntax s) Source # 

Methods

(==) :: UnitSyntax s -> UnitSyntax s -> Bool #

(/=) :: UnitSyntax s -> UnitSyntax s -> Bool #

Show s => Show (UnitSyntax s) Source # 
TestEquality (UnitSyntax Symbol) SUnit # 

Methods

testEquality :: f a -> f b -> Maybe ((SUnit :~: a) b) #

type family Unpack (u :: Unit) :: UnitSyntax Symbol where ... Source #

Unpack a unit as a syntactic representation, where the order of units is deterministic. For example:

 Unpack One = [] :/ []
 Unpack (Base "s" *: Base "m") = ["m","s"] :/ []

This does not break type soundness because Unpack will reduce only when the unit is entirely constant, and it does not allow the structure of the unit to be observed. The reduction behaviour is implemented by the plugin, because we cannot define it otherwise.

type family Pack (u :: UnitSyntax Symbol) :: Unit where ... Source #

Pack up a syntactic representation of a unit as a unit. For example:

 Pack ([] :/ []) = One
 Pack (["m"] :/ ["s","s"]) = Base "m" /: Base "s" ^: 2

This is a perfectly ordinary closed type family. Pack is a left inverse of Unpack up to the equational theory of units, but it is not a right inverse (because there are multiple list representations of the same unit).

Equations

Pack (xs :/ ys) = Prod xs /: Prod ys 

type family Prod (xs :: [Symbol]) :: Unit where ... Source #

Take the product of a list of base units.

Equations

Prod '[] = One 
Prod (x ': xs) = Base x *: Prod xs 

Internal

type family (u :: Unit) ~~ (v :: Unit) :: Constraint where ... infix 4 Source #

This is a bit of a hack, honestly, but a good hack. Constraints u ~~ v are just like equalities u ~ v, except solving them will be delayed until the plugin. This may lead to better inferred types.

type family MkUnit (s :: Symbol) :: Unit Source #

This type family is used for translating unit names (as type-level strings) into units. It will be Base for base units or expand the definition for derived units.

The instances displayed by Haddock are available only if Data.UnitsOfMeasure.Defs is imported.

Instances

type MkUnit "A" Source # 
type MkUnit "A" = Base "A"
type MkUnit "C" Source # 
type MkUnit "C" = (*:) (MkUnit "s") (MkUnit "A")
type MkUnit "F" Source # 
type MkUnit "F" = (/:) (MkUnit "C") (MkUnit "V")
type MkUnit "Hz" Source # 
type MkUnit "Hz" = (/:) One ((^:) (MkUnit "s") 1)
type MkUnit "J" Source # 
type MkUnit "J" = (*:) (MkUnit "N") (MkUnit "m")
type MkUnit "K" Source # 
type MkUnit "K" = Base "K"
type MkUnit "N" Source # 
type MkUnit "N" = (/:) ((*:) (MkUnit "kg") (MkUnit "m")) ((^:) (MkUnit "s") 2)
type MkUnit "Pa" Source # 
type MkUnit "Pa" = (/:) (MkUnit "N") ((^:) (MkUnit "m") 2)
type MkUnit "V" Source # 
type MkUnit "V" = (/:) (MkUnit "W") (MkUnit "A")
type MkUnit "W" Source # 
type MkUnit "W" = (/:) (MkUnit "J") (MkUnit "s")
type MkUnit "au" Source # 
type MkUnit "au" = Base "au"
type MkUnit "cd" Source # 
type MkUnit "cd" = Base "cd"
type MkUnit "d" Source # 
type MkUnit "d" = Base "d"
type MkUnit "ft" Source # 
type MkUnit "ft" = Base "ft"
type MkUnit "g" Source # 
type MkUnit "g" = Base "g"
type MkUnit "h" Source # 
type MkUnit "h" = Base "h"
type MkUnit "ha" Source # 
type MkUnit "ha" = Base "ha"
type MkUnit "in" Source # 
type MkUnit "in" = Base "in"
type MkUnit "kg" Source # 
type MkUnit "kg" = Base "kg"
type MkUnit "km" Source # 
type MkUnit "km" = Base "km"
type MkUnit "l" Source # 
type MkUnit "l" = Base "l"
type MkUnit "m" Source # 
type MkUnit "m" = Base "m"
type MkUnit "mi" Source # 
type MkUnit "mi" = Base "mi"
type MkUnit "min" Source # 
type MkUnit "min" = Base "min"
type MkUnit "mol" Source # 
type MkUnit "mol" = Base "mol"
type MkUnit "mph" Source # 
type MkUnit "mph" = (/:) (MkUnit "mi") (MkUnit "h")
type MkUnit "ohm" Source # 
type MkUnit "ohm" = (/:) (MkUnit "V") (MkUnit "A")
type MkUnit "rad" Source # 
type MkUnit "rad" = Base "rad"
type MkUnit "s" Source # 
type MkUnit "s" = Base "s"
type MkUnit "sr" Source # 
type MkUnit "sr" = Base "sr"
type MkUnit "t" Source # 
type MkUnit "t" = Base "t"