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

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

Data.Metrology.Z

Contents

Description

This module defines a datatype and operations to represent type-level integers. Though it's defined as part of the units package, it may be useful beyond dimensional analysis. If you have a compelling non-units use of this package, please let me (Richard, eir at cis.upenn.edu) know.

Synopsis

The Z datatype

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 

data family Sing a

The singleton kind-indexed data family.

Instances

SDecide k (KProxy k) => TestEquality k (Sing k) 
data Sing Bool where 
data Sing Ordering where 
data Sing Nat where 
data Sing Symbol where 
data Sing () where 
data Sing Z where 
data Sing [a0] where 
data Sing (Maybe a0) where 
data Sing (TyFun k1 k2 -> *) = SLambda {} 
data Sing (Either a0 b0) where 
data Sing ((,) a0 b0) where 
data Sing ((,,) a0 b0 c0) where 
data Sing ((,,,) a0 b0 c0 d0) where 
data Sing ((,,,,) a0 b0 c0 d0 e0) where 
data Sing ((,,,,,) a0 b0 c0 d0 e0 f0) where 
data Sing ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) where 

type SZ z = Sing z Source

Defunctionalization symbols (these can be ignored)

data SSym0 l Source

Instances

type SSym1 t = S t Source

data PSym0 l Source

Instances

type PSym1 t = P t Source

Conversions

zToInt :: Z -> Int Source

Convert a Z to an Int

szToInt :: Sing (z :: Z) -> Int Source

Convert a singleton Z to an Int.

Type-level operations

Arithmetic

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 Negate z :: Z Source

Negate an integer

Equations

Negate Zero = Zero 
Negate (S z) = P (Negate z) 
Negate (P z) = S (Negate 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 

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.

Comparisons

type family a < b :: Bool Source

Less-than comparison

Equations

Zero < Zero = False 
Zero < (S n) = True 
Zero < (P n) = False 
(S n) < Zero = False 
(S n) < (S n') = n < n' 
(S n) < (P n') = False 
(P n) < Zero = True 
(P n) < (S n') = True 
(P n) < (P n') = n < n' 

type family NonNegative z :: Constraint Source

Check if a type-level integer is in fact a natural number

Equations

NonNegative Zero = () 
NonNegative (S z) = () 

Synonyms for certain 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

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

Deprecated synonyms

pZero :: Sing Z Zero Source

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

pOne :: Sing Z (S Zero) Source

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

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

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

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

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

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

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

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

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

pMOne :: Sing Z (P Zero) Source

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

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

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

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

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

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

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

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

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

pSucc :: Sing Z z -> Sing Z (Succ z) Source

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

pPred :: Sing Z z -> Sing Z (Pred z) Source

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.