units-2.2: A domain-specific type system for dimensional analysis

Copyright(C) 2014 Richard Eisenberg
LicenseBSD-style (see LICENSE)
MaintainerRichard Eisenberg (eir@cis.upenn.edu)
Stabilityexperimental
Portabilitynon-portable
Safe HaskellNone
LanguageHaskell2010

Data.Metrology.Vector

Contents

Description

Exports combinators for building quantities out of vectors, from the vector-space library.

Synopsis

Term-level combinators

The term-level arithmetic operators are defined by applying vertical bar(s) to the sides the dimensioned quantities acts on.

Additive operations

zero :: AdditiveGroup n => Qu dimspec l n Source

The number 0, polymorphic in its dimension. Use of this will often require a type annotation.

(|+|) :: (d1 @~ d2, AdditiveGroup n) => Qu d1 l n -> Qu d2 l n -> Qu d1 l n infixl 6 Source

Add two compatible quantities

(|-|) :: (d1 @~ d2, AdditiveGroup n) => Qu d1 l n -> Qu d2 l n -> Qu d1 l n infixl 6 Source

Subtract two compatible quantities

qSum :: (Foldable f, AdditiveGroup n) => f (Qu d l n) -> Qu d l n Source

Take the sum of a list of quantities

qNegate :: AdditiveGroup n => Qu d l n -> Qu d l n Source

Negate a quantity

Multiplicative operations between non-vector quantities

(|*|) :: Num n => Qu a l n -> Qu b l n -> Qu (Normalize (a @+ b)) l n infixl 7 Source

Multiply two quantities

(|/|) :: Fractional n => Qu a l n -> Qu b l n -> Qu (Normalize (a @- b)) l n infixl 7 Source

Divide two quantities

(/|) :: Fractional n => n -> Qu b l n -> Qu (Normalize ([] @- b)) l n infixl 7 Source

Divide a scalar by a quantity

Multiplicative operations between a vector and a scalar

(*|) :: VectorSpace n => Scalar n -> Qu b l n -> Qu b l n infixl 7 Source

Multiply a quantity by a scalar from the left

(|*) :: VectorSpace n => Qu a l n -> Scalar n -> Qu a l n infixl 7 Source

Multiply a quantity by a scalar from the right

(|/) :: (VectorSpace n, Fractional (Scalar n)) => Qu a l n -> Scalar n -> Qu a l n infixl 7 Source

Divide a quantity by a scalar

Multiplicative operations on vectors

(|*^|) :: VectorSpace n => Qu d1 l (Scalar n) -> Qu d2 l n -> Qu (Normalize (d1 @+ d2)) l n infixl 7 Source

Multiply a scalar quantity by a vector quantity

(|^*|) :: VectorSpace n => Qu d1 l n -> Qu d2 l (Scalar n) -> Qu (Normalize (d1 @+ d2)) l n infixl 7 Source

Multiply a vector quantity by a scalar quantity

(|^/|) :: (VectorSpace n, Fractional (Scalar n)) => Qu d1 l n -> Qu d2 l (Scalar n) -> Qu (Normalize (d1 @- d2)) l n infixl 7 Source

Divide a vector quantity by a scalar quantity

(|.|) :: InnerSpace n => Qu d1 l n -> Qu d2 l n -> Qu (Normalize (d1 @+ d2)) l (Scalar n) infixl 7 Source

Take a inner (dot) product between two quantities.

Exponentiation

(|^) :: (NonNegative z, Num n) => Qu a l n -> Sing z -> Qu (a @* z) l n infixr 8 Source

Raise a quantity to a integer power, knowing at compile time that the integer is non-negative.

(|^^) :: Fractional n => Qu a l n -> Sing z -> Qu (a @* z) l n infixr 8 Source

Raise a quantity to a integer power known at compile time

qNthRoot :: ((Zero < z) ~ True, Floating n) => Sing z -> Qu a l n -> Qu (a @/ z) l n Source

Take the n'th root of a quantity, where n is known at compile time

qSq :: Num n => Qu a l n -> Qu (Normalize (a @+ a)) l n Source

Square a quantity

qCube :: Num n => Qu a l n -> Qu (Normalize (Normalize (a @+ a) @+ a)) l n Source

Cube a quantity

qSqrt :: Floating n => Qu a l n -> Qu (a @/ Two) l n Source

Take the square root of a quantity

qCubeRoot :: Floating n => Qu a l n -> Qu (a @/ Three) l n Source

Take the cubic root of a quantity

Other vector operations

qMagnitudeSq :: InnerSpace n => Qu d l n -> Qu (d @* Two) l (Scalar n) Source

Square the length of a vector.

qMagnitude :: (InnerSpace n, Floating (Scalar n)) => Qu d l n -> Qu d l (Scalar n) Source

Length of a vector.

qNormalized :: (InnerSpace n, Floating (Scalar n)) => Qu d l n -> Qu [] l n Source

Vector in same direction as given one but with length of one. If given the zero vector, then return it. The returned vector is dimensionless.

qProject :: (InnerSpace n, Floating (Scalar n)) => Qu d2 l n -> Qu d1 l n -> Qu d1 l n Source

qProject u v computes the projection of v onto u.

qCross2 :: HasCross2 n => Qu d l n -> Qu d l n Source

Cross product of 2D vectors.

qCross3 :: HasCross3 n => Qu d1 l n -> Qu d2 l n -> Qu (Normalize (d1 @+ d2)) l n Source

Cross product of 3D vectors.

Affine operations

newtype Point n Source

A Point n is an affine space built over n. Two Points cannot be added, but they can be subtracted to yield a difference of type n.

Constructors

Point n 

Instances

Bounded n => Bounded (Point n) 
Enum n => Enum (Point n) 
Eq n => Eq (Point n) 
Show n => Show (Point n) 
AdditiveGroup n => AffineSpace (Point n) 
type Diff (Point n) = n 

type family QPoint n Source

Make a point quantity from a non-point quantity.

Equations

QPoint (Qu d l n) = Qu d l (Point n) 

(|.-.|) :: (d1 @~ d2, AffineSpace n) => Qu d1 l n -> Qu d2 l n -> Qu d1 l (Diff n) infixl 6 Source

Subtract point quantities.

(|.+^|) :: (d1 @~ d2, AffineSpace n) => Qu d1 l n -> Qu d2 l (Diff n) -> Qu d1 l n infixl 6 Source

Add a point to a vector.

(|.-^|) :: (d1 @~ d2, AffineSpace n) => Qu d1 l n -> Qu d2 l (Diff n) -> Qu d1 l n infixl 6 Source

Subract a vector from a point.

qDistanceSq :: (d1 @~ d2, AffineSpace n, InnerSpace (Diff n)) => Qu d1 l n -> Qu d2 l n -> Qu (d1 @* Two) l (Scalar (Diff n)) Source

Square of the distance between two points.

qDistance :: (d1 @~ d2, AffineSpace n, InnerSpace (Diff n), Floating (Scalar (Diff n))) => Qu d1 l n -> Qu d2 l n -> Qu d1 l (Scalar (Diff n)) Source

Distance between two points.

Comparison

qCompare :: (d1 @~ d2, Ord n) => Qu d1 l n -> Qu d2 l n -> Ordering Source

Compare two quantities

(|<|) :: (d1 @~ d2, Ord n) => Qu d1 l n -> Qu d2 l n -> Bool infix 4 Source

Check if one quantity is less than a compatible one

(|>|) :: (d1 @~ d2, Ord n) => Qu d1 l n -> Qu d2 l n -> Bool infix 4 Source

Check if one quantity is greater than a compatible one

(|<=|) :: (d1 @~ d2, Ord n) => Qu d1 l n -> Qu d2 l n -> Bool infix 4 Source

Check if one quantity is less than or equal to a compatible one

(|>=|) :: (d1 @~ d2, Ord n) => Qu d1 l n -> Qu d2 l n -> Bool infix 4 Source

Check if one quantity is greater than or equal to a compatible one

(|==|) :: (d1 @~ d2, Eq n) => Qu d1 l n -> Qu d2 l n -> Bool infix 4 Source

Check if two quantities are equal (uses the equality of the underlying numerical type)

(|/=|) :: (d1 @~ d2, Eq n) => Qu d1 l n -> Qu d2 l n -> Bool infix 4 Source

Check if two quantities are not equal

qApprox infix 4 Source

Arguments

:: (d0 @~ d1, d0 @~ d2, Num n, Ord n) 
=> Qu d0 l n

epsilon

-> Qu d1 l n

left hand side

-> Qu d2 l n

right hand side

-> Bool 

Compare two compatible quantities for approximate equality. If the difference between the left hand side and the right hand side arguments are less than or equal to the epsilon, they are considered equal.

qNapprox infix 4 Source

Arguments

:: (d0 @~ d1, d0 @~ d2, Num n, Ord n) 
=> Qu d0 l n

epsilon

-> Qu d1 l n

left hand side

-> Qu d2 l n

right hand side

-> Bool 

Compare two compatible quantities for approixmate inequality. qNapprox e a b = not $ qApprox e a b

Nondimensional units, conversion between quantities and numeric values

numIn :: forall unit dim lcsu n. (ValidDLU dim lcsu unit, VectorSpace n, Fractional (Scalar n)) => Qu dim lcsu n -> unit -> n Source

Extracts a numerical value from a dimensioned quantity, expressed in the given unit. For example:

inMeters :: Length -> Double
inMeters x = numIn x Meter

or

inMeters x = x # Meter   

(#) :: (ValidDLU dim lcsu unit, VectorSpace n, Fractional (Scalar n)) => Qu dim lcsu n -> unit -> n infix 5 Source

Infix synonym for numIn

quOf :: forall unit dim lcsu n. (ValidDLU dim lcsu unit, VectorSpace n, Fractional (Scalar n)) => n -> unit -> Qu dim lcsu n Source

Creates a dimensioned quantity in the given unit. For example:

height :: Length
height = quOf 2.0 Meter

or

height = 2.0 % Meter

(%) :: (ValidDLU dim lcsu unit, VectorSpace n, Fractional (Scalar n)) => n -> unit -> Qu dim lcsu n infixr 9 Source

Infix synonym for quOf

showIn :: (ValidDLU dim lcsu unit, VectorSpace n, Fractional (Scalar n), Show unit, Show n) => Qu dim lcsu n -> unit -> String infix 1 Source

Show a dimensioned quantity in a given unit. (The default Show instance always uses units as specified in the LCSU.)

unity :: Num n => Qu [] l n Source

The number 1, expressed as a unitless dimensioned quantity.

redim :: d @~ e => Qu d l n -> Qu e l n Source

Cast between equivalent dimension within the same CSU. for example [kg m s] and [s m kg]. See the README for more info.

convert :: forall d l1 l2 n. (ConvertibleLCSUs d l1 l2, VectorSpace n, Fractional (Scalar n)) => Qu d l1 n -> Qu d l2 n Source

Dimension-keeping cast between different CSUs.

defaultLCSU :: Qu dim DefaultLCSU n -> Qu dim DefaultLCSU n Source

Use this to choose a default LCSU for a dimensioned quantity. The default LCSU uses the DefaultUnitOfDim representation for each dimension.

constant :: (d @~ e, ConvertibleLCSUs e DefaultLCSU l, VectorSpace n, Fractional (Scalar n)) => Qu d DefaultLCSU n -> Qu e l n Source

Compute the argument in the DefaultLCSU, and present the result as lcsu-polymorphic dimension-polymorphic value. Named constant because one of its dominant usecase is to inject constant quantities into dimension-polymorphic expressions.

Type-level unit combinators

data u1 :* u2 infixl 7 Source

Multiply two units to get another unit. For example: type MetersSquared = Meter :* Meter

Constructors

u1 :* u2 infixl 7 

Instances

(Show u1, Show u2) => Show ((:*) u1 u2) 
(Dimension d1, Dimension d2) => Dimension ((:*) d1 d2) 
(Unit u1, Unit u2) => Unit ((:*) u1 u2) 
type DefaultUnitOfDim ((:*) d1 d2) = (:*) (DefaultUnitOfDim d1) (DefaultUnitOfDim d2) 
type DimFactorsOf ((:*) d1 d2) = Normalize ((@+) (DimFactorsOf d1) (DimFactorsOf d2)) 
type BaseUnit ((:*) u1 u2) = Canonical 
type DimOfUnit ((:*) u1 u2) = (:*) (DimOfUnit u1) (DimOfUnit u2) 
type UnitFactorsOf ((:*) u1 u2) = Normalize ((@+) (UnitFactorsOf u1) (UnitFactorsOf u2)) 

data u1 :/ u2 infixl 7 Source

Divide two units to get another unit

Constructors

u1 :/ u2 infixl 7 

Instances

(Show u1, Show u2) => Show ((:/) u1 u2) 
(Dimension d1, Dimension d2) => Dimension ((:/) d1 d2) 
(Unit u1, Unit u2) => Unit ((:/) u1 u2) 
type DefaultUnitOfDim ((:/) d1 d2) = (:/) (DefaultUnitOfDim d1) (DefaultUnitOfDim d2) 
type DimFactorsOf ((:/) d1 d2) = Normalize ((@-) (DimFactorsOf d1) (DimFactorsOf d2)) 
type BaseUnit ((:/) u1 u2) = Canonical 
type DimOfUnit ((:/) u1 u2) = (:/) (DimOfUnit u1) (DimOfUnit u2) 
type UnitFactorsOf ((:/) u1 u2) = Normalize ((@-) (UnitFactorsOf u1) (UnitFactorsOf u2)) 

data unit :^ power infixr 8 Source

Raise a unit to a power, known at compile time

Constructors

unit :^ (Sing power) infixr 8 

Instances

(Show u1, SingI Z power) => Show ((:^) u1 power) 
Dimension dim => Dimension ((:^) dim power) 
(Unit unit, SingI Z power) => Unit ((:^) unit power) 
type DefaultUnitOfDim ((:^) d z) = (:^) (DefaultUnitOfDim d) z 
type DimFactorsOf ((:^) dim power) = Normalize ((@*) (DimFactorsOf dim) power) 
type BaseUnit ((:^) unit power) = Canonical 
type DimOfUnit ((:^) unit power) = (:^) (DimOfUnit unit) power 
type UnitFactorsOf ((:^) unit power) = Normalize ((@*) (UnitFactorsOf unit) power) 

data prefix :@ unit infixr 9 Source

Multiply a conversion ratio by some constant. Used for defining prefixes.

Constructors

prefix :@ unit infixr 9 

Instances

(Show prefix, Show unit) => Show ((:@) prefix unit) 
((~) Bool ((==) * unit Canonical) False, Unit unit, UnitPrefix prefix) => Unit ((:@) prefix unit) 
type BaseUnit ((:@) prefix unit) = unit 
type DimOfUnit ((:@) prefix unit) = DimOfUnit (BaseUnit ((:@) prefix unit)) 
type UnitFactorsOf ((:@) prefix unit) = If [Factor *] (IsCanonical ((:@) prefix unit)) ((:) (Factor *) (F * ((:@) prefix unit) One) ([] (Factor *))) (UnitFactorsOf (BaseUnit ((:@) prefix unit))) 

class UnitPrefix prefix where Source

A class for user-defined prefixes

Methods

multiplier :: Fractional f => prefix -> f Source

This should return the desired multiplier for the prefix being defined. This function must not inspect its argument.

Type-level quantity combinators

type family d1 %* d2 :: * infixl 7 Source

Multiply two quantity types to produce a new one. For example:

type Velocity = Length %/ Time

Instances

type (Qu d1 l n) %* (Qu d2 l n) = Qu ((@+) d1 d2) l n 

type family d1 %/ d2 :: * infixl 7 Source

Divide two quantity types to produce a new one

Instances

type (Qu d1 l n) %/ (Qu d2 l n) = Qu ((@-) d1 d2) l n 

type family d %^ z :: * infixr 8 Source

Exponentiate a quantity type to an integer

Instances

type (Qu d l n) %^ z = Qu ((@*) d z) l n 

Creating quantity types

data Qu a lcsu n Source

Qu adds a dimensional annotation to its numerical value type n. This is the representation for all quantities.

Instances

Eq n => Eq (Qu d l n) 
((~) [Factor *] d ([] (Factor *)), Floating n) => Floating (Qu d l n) 
((~) [Factor *] d ([] (Factor *)), Fractional n) => Fractional (Qu d l n) 
((~) [Factor *] d ([] (Factor *)), Num n) => Num (Qu d l n) 
Ord n => Ord (Qu d l n) 
((~) [Factor *] d ([] (Factor *)), Real n) => Real (Qu d l n) 
((~) [Factor *] d ([] (Factor *)), RealFloat n) => RealFloat (Qu d l n) 
((~) [Factor *] d ([] (Factor *)), RealFrac n) => RealFrac (Qu d l n) 
(ShowUnitFactor (LookupList dims lcsu), Show n) => Show (Qu dims lcsu n) 
ValidDL d l => Quantity (Qu d l n) 
type QuantityUnit (Qu d l n) = UnitOfDimFactors d l 
type QuantityLCSU (Qu d l n) = l 
type QuantityRep (Qu d l n) = n 
type (Qu d l n) %^ z = Qu ((@*) d z) l n 
type (Qu d1 l n) %/ (Qu d2 l n) = Qu ((@-) d1 d2) l n 
type (Qu d1 l n) %* (Qu d2 l n) = Qu ((@+) d1 d2) l n 

type MkQu_D dim = Qu (DimFactorsOf dim) DefaultLCSU Double Source

Make a quantity type capable of storing a value of a given unit. This uses a Double for storage of the value. For example:

data LengthDim = LengthDim
instance Dimension LengthDim
data Meter = Meter
instance Unit Meter where
  type BaseUnit Meter = Canonical
  type DimOfUnit Meter = LengthDim
type instance DefaultUnitOfDim LengthDim = Meter
type Length = MkQu_D LengthDim

Note that the dimension must have an instance for the type family DefaultUnitOfDim for this to work.

type MkQu_DLN dim = Qu (DimFactorsOf dim) Source

Make a quantity type with a custom numerical type and LCSU.

type MkQu_U unit = Qu (DimFactorsOf (DimOfUnit unit)) DefaultLCSU Double Source

Make a quantity type with a given unit. It will be stored as a Double. Note that the corresponding dimension must have an appropriate instance for DefaultUnitOfDim for this to work.

type MkQu_ULN unit = Qu (DimFactorsOf (DimOfUnit unit)) Source

Make a quantity type with a unit and LCSU with custom numerical type. The quantity will have the dimension corresponding to the unit.

Creating new dimensions

class Dimension dim Source

This class is used to mark abstract dimensions, such as Length, or Mass.

Associated Types

type DimFactorsOf dim :: [Factor *] Source

Retrieve a list of Factors representing the given dimension. Overriding the default of this type family should not be necessary in user code.

Instances

Dimension Dimensionless 
Dimension dim => Dimension ((:^) dim power) 
(Dimension d1, Dimension d2) => Dimension ((:/) d1 d2) 
(Dimension d1, Dimension d2) => Dimension ((:*) d1 d2) 

Creating new units

class DimOfUnitIsConsistent unit => Unit unit where Source

Minimal complete definition

Nothing

Associated Types

type BaseUnit unit :: * Source

The base unit of this unit: what this unit is defined in terms of. For units that are not defined in terms of anything else, the base unit should be Canonical.

type DimOfUnit unit :: * Source

The dimension that this unit is associated with. This needs to be defined only for canonical units; other units are necessarily of the same dimension as their base.

type UnitFactorsOf unit :: [Factor *] Source

The internal list of canonical units corresponding to this unit. Overriding the default should not be necessary in user code.

Methods

conversionRatio :: unit -> Rational Source

The conversion ratio from the base unit to this unit. If left out, a conversion ratio of 1 is assumed.

For example:

instance Unit Foot where
  type BaseUnit Foot = Meter
  conversionRatio _ = 0.3048

Implementations should never examine their argument!

Instances

Unit Number 
((~) Bool ((==) * unit Canonical) False, Unit unit, UnitPrefix prefix) => Unit ((:@) prefix unit) 
(Unit unit, SingI Z power) => Unit ((:^) unit power) 
(Unit u1, Unit u2) => Unit ((:/) u1 u2) 
(Unit u1, Unit u2) => Unit ((:*) u1 u2) 

data Canonical Source

Dummy type use just to label canonical units. It does not have a Unit instance.

Numbers, the only built-in unit

data Dimensionless Source

The dimension for the dimensionless quantities. It is also called "quantities of dimension one", but One is confusing with the type-level integer One.

Constructors

Dimensionless 

data Number Source

The unit for unitless dimensioned quantities

Constructors

Number 

type Count = MkQu_ULN Number Source

The type of unitless dimensioned quantities. This is an instance of Num, though Haddock doesn't show it. This is parameterized by an LCSU and a number representation.

quantity :: n -> Qu [] l n Source

Convert a raw number into a unitless dimensioned quantity

LCSUs (locally coherent system of units)

type family MkLCSU pairs Source

Make a local consistent set of units. The argument is a type-level list of tuple types, to be interpreted as an association list from dimensions to units. For example:

type MyLCSU = MkLCSU '[(Length, Foot), (Mass, Gram), (Time, Year)]

Equations

MkLCSU pairs = MkLCSU_ (UsePromotedTuples pairs) 

data LCSU star Source

Constructors

DefaultLCSU 

type family DefaultUnitOfDim dim :: * Source

Assign a default unit for a dimension. Necessary only when using default LCSUs.

Validity checks and assertions

type family CompatibleUnit lcsu unit :: Constraint Source

Check if an LCSU has consistent entries for the given unit. i.e. can the lcsu describe the unit?

Equations

CompatibleUnit lcsu unit = (ValidDLU (DimFactorsOf (DimOfUnit unit)) lcsu unit, UnitFactor (LookupList (DimFactorsOf (DimOfUnit unit)) lcsu)) 

type family CompatibleDim lcsu dim :: Constraint Source

Check if an LCSU can express the given dimension

Equations

CompatibleDim lcsu dim = (UnitFactor (LookupList (DimFactorsOf dim) lcsu), DimOfUnit (Lookup dim lcsu) ~ dim) 

type family ConvertibleLCSUs_D dim l1 l2 :: Constraint Source

Like ConvertibleLCSUs, but takes a dimension, not a dimension factors.

Equations

ConvertibleLCSUs_D dim l1 l2 = ConvertibleLCSUs (DimFactorsOf dim) l1 l2 

type family DefaultConvertibleLCSU_D dim l :: Constraint Source

Check if the DefaultLCSU can convert into the given one, at the given dimension.

type family DefaultConvertibleLCSU_U unit l :: Constraint Source

Check if the DefaultLCSU can convert into the given one, at the given unit.

type family MultDimFactors facts Source

Extract a dimension specifier from a list of factors

Equations

MultDimFactors [] = Dimensionless 
MultDimFactors (F d z : ds) = (d :^ z) :* MultDimFactors ds 

type family MultUnitFactors facts Source

Extract a unit specifier from a list of factors

Equations

MultUnitFactors [] = Number 
MultUnitFactors (F unit z : units) = (unit :^ z) :* MultUnitFactors units 

type family UnitOfDimFactors dims lcsu :: * Source

Extract a unit from a dimension factor list and an LCSU

Equations

UnitOfDimFactors dims lcsu = MultUnitFactors (LookupList dims lcsu) 

Type-level integers

data Z Source

The datatype for type-level integers.

Constructors

Zero 
S Z 
P Z 

Instances

Eq Z 
SingI Z Zero 
SEq Z (KProxy Z) 
PEq Z (KProxy Z) 
SDecide Z (KProxy Z) 
SingI Z n0 => SingI Z (P n) 
SingI Z n0 => SingI Z (S n) 
SingKind Z (KProxy Z) 
SuppressUnusedWarnings (TyFun Z Z -> *) PSym0 
SuppressUnusedWarnings (TyFun Z Z -> *) SSym0 
data Sing Z where 
type (:==) Z a0 b0 
type Apply Z Z PSym0 l0 = PSym1 l0 
type Apply Z Z SSym0 l0 = SSym1 l0 
type DemoteRep Z (KProxy Z) = Z 

type family Succ z :: Z Source

Add one to an integer

Equations

Succ Zero = S Zero 
Succ (P z) = z 
Succ (S z) = S (S z) 

type family Pred z :: Z Source

Subtract one from an integer

Equations

Pred Zero = P Zero 
Pred (P z) = P (P z) 
Pred (S z) = z 

type family a #+ b :: Z infixl 6 Source

Add two integers

Equations

Zero #+ z = z 
(S z1) #+ (S z2) = S (S (z1 #+ z2)) 
(S z1) #+ Zero = S z1 
(S z1) #+ (P z2) = z1 #+ z2 
(P z1) #+ (S z2) = z1 #+ z2 
(P z1) #+ Zero = P z1 
(P z1) #+ (P z2) = P (P (z1 #+ z2)) 

type family a #- b :: Z infixl 6 Source

Subtract two integers

Equations

z #- Zero = z 
(S z1) #- (S z2) = z1 #- z2 
Zero #- (S z2) = P (Zero #- z2) 
(P z1) #- (S z2) = P (P (z1 #- z2)) 
(S z1) #- (P z2) = S (S (z1 #- z2)) 
Zero #- (P z2) = S (Zero #- z2) 
(P z1) #- (P z2) = z1 #- z2 

type family a #* b :: Z infixl 7 Source

Multiply two integers

Equations

Zero #* z = Zero 
(S z1) #* z2 = (z1 #* z2) #+ z2 
(P z1) #* z2 = (z1 #* z2) #- z2 

type family a #/ b :: Z Source

Divide two integers

Equations

Zero #/ b = Zero 
a #/ (P b') = Negate (a #/ Negate (P b')) 
a #/ b = ZDiv b b a 

type family Negate z :: Z Source

Negate an integer

Equations

Negate Zero = Zero 
Negate (S z) = P (Negate z) 
Negate (P z) = S (Negate z) 

Synonyms for small numbers

type One = S Zero Source

type Two = S One Source

type Three = S Two Source

type Five = S Four Source

type MOne = P Zero Source

type MTwo = P MOne Source

Term-level singletons

sZero :: Sing Z Zero Source

This is the singleton value representing Zero at the term level and at the type level, simultaneously. Used for raising units to powers.

sThree :: Sing Z (S (S (S Zero))) Source

sFour :: Sing Z (S (S (S (S Zero)))) Source

sFive :: Sing Z (S (S (S (S (S Zero))))) Source

sMFour :: Sing Z (P (P (P (P Zero)))) Source

sMFive :: Sing Z (P (P (P (P (P Zero))))) Source

sSucc :: Sing z -> Sing (Succ z) Source

Add one to a singleton Z.

sPred :: Sing z -> Sing (Pred z) Source

Subtract one from a singleton Z.

sNegate :: Sing z -> Sing (Negate z) Source

Negate a singleton Z.

Internal definitions

The following module is re-exported solely to prevent noise in error messages; we do not recommend trying to use these definitions in user code.