Safe Haskell | None |
---|---|
Language | Haskell2010 |
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.
- data Unit
- type family One :: Unit where ...
- type family Base (b :: Symbol) :: Unit where ...
- type family (u :: Unit) *: (v :: Unit) :: Unit where ...
- type family (u :: Unit) /: (v :: Unit) :: Unit where ...
- type family (u :: Unit) ^: (n :: Nat) :: Unit where ...
- newtype Quantity a (u :: Unit) = MkQuantity a
- unQuantity :: Quantity a u -> a
- zero :: Num a => Quantity a u
- mk :: a -> Quantity a One
- (+:) :: Num a => Quantity a u -> Quantity a u -> Quantity a u
- (*:) :: (Num a, w ~~ (u *: v)) => Quantity a u -> Quantity a v -> Quantity a w
- (-:) :: Num a => Quantity a u -> Quantity a u -> Quantity a u
- negate' :: Num a => Quantity a u -> Quantity a u
- abs' :: Num a => Quantity a u -> Quantity a u
- signum' :: Num a => Quantity a u -> Quantity a One
- fromInteger' :: Integral a => Quantity Integer u -> Quantity a u
- (/:) :: (Fractional a, w ~~ (u /: v)) => Quantity a u -> Quantity a v -> Quantity a w
- recip' :: (Fractional a, w ~~ (One /: u)) => Quantity a u -> Quantity a w
- fromRational' :: Fractional a => Quantity Rational u -> Quantity a u
- toRational' :: Real a => Quantity a u -> Quantity Rational u
- sqrt' :: (Floating a, w ~~ (u ^: 2)) => Quantity a w -> Quantity a u
- data UnitSyntax s = [s] :/ [s]
- type family Unpack (u :: Unit) :: UnitSyntax Symbol where ...
- type family Pack (u :: UnitSyntax Symbol) :: Unit where ...
- type family Prod (xs :: [Symbol]) :: Unit where ...
- type family (u :: Unit) ~~ (v :: Unit) :: Constraint where ...
- type family MkUnit (s :: Symbol) :: Unit
Type-level units of measure
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)
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
.
MkQuantity a | Warning: the |
Bounded a => Bounded (Quantity a u) Source # | |
(Enum a, (~) Unit u One) => Enum (Quantity a u) Source # | |
Eq a => Eq (Quantity a u) Source # | |
(Floating a, (~) Unit u One) => Floating (Quantity a u) Source # | |
(Fractional a, (~) Unit u One) => Fractional (Quantity a u) Source # | |
(Integral a, (~) Unit u One) => Integral (Quantity a u) Source # | |
(Num a, (~) Unit u One) => Num (Quantity a u) Source # | |
Ord a => Ord (Quantity a u) Source # | |
(Real a, (~) Unit u One) => Real (Quantity a u) Source # | |
(RealFloat a, (~) Unit u One) => RealFloat (Quantity a u) Source # | |
(RealFrac a, (~) Unit u One) => RealFrac (Quantity a u) Source # | |
Storable a => Storable (Quantity a u) Source # | |
NFData a => NFData (Quantity a u) Source # | |
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
:/
[]
is represented as Base
"m" /:
Base
"s" ^: 2["m"]
.:/
["s","s"]
[s] :/ [s] |
Eq s => Eq (UnitSyntax s) Source # | |
Show s => Show (UnitSyntax s) Source # | |
TestEquality (UnitSyntax Symbol) SUnit # | |
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).
type family Prod (xs :: [Symbol]) :: Unit where ... Source #
Take the product of a list of base units.
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.
type MkUnit "A" Source # | |
type MkUnit "C" Source # | |
type MkUnit "F" Source # | |
type MkUnit "Hz" Source # | |
type MkUnit "J" Source # | |
type MkUnit "K" Source # | |
type MkUnit "N" Source # | |
type MkUnit "Pa" Source # | |
type MkUnit "V" Source # | |
type MkUnit "W" Source # | |
type MkUnit "au" Source # | |
type MkUnit "cd" Source # | |
type MkUnit "d" Source # | |
type MkUnit "ft" Source # | |
type MkUnit "g" Source # | |
type MkUnit "h" Source # | |
type MkUnit "ha" Source # | |
type MkUnit "in" Source # | |
type MkUnit "kg" Source # | |
type MkUnit "km" Source # | |
type MkUnit "l" Source # | |
type MkUnit "m" Source # | |
type MkUnit "mi" Source # | |
type MkUnit "min" Source # | |
type MkUnit "mol" Source # | |
type MkUnit "mph" Source # | |
type MkUnit "ohm" Source # | |
type MkUnit "rad" Source # | |
type MkUnit "s" Source # | |
type MkUnit "sr" Source # | |
type MkUnit "t" Source # | |