Data.Metrology.Z

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.

Documentation

data Z

The datatype for type-level integers.

Constructors

Zero

S Z

P Z

Instances

Eq Z

SingI Z Zero

SEq 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)

data Sing Z where

• SZero :: (~) Z z Zero => Sing Z z
• SS :: (~) Z z (S n) => Sing Z n -> Sing Z z
• SP :: (~) Z z (P n) => Sing Z n -> Sing Z z

type (==) Z a0 b0 = Equals_1627415457 a0 b0

type DemoteRep Z (KProxy Z) = Z

type SZ z = Sing z

type family Equals_1627415457 a b :: Bool

Equations

Equals_1627415457 Zero Zero = True

Equals_1627415457 (S a) (S b) = (==) a b

Equals_1627415457 (P a) (P b) = (==) a b

Equals_1627415457 (a :: Z) (b :: Z) = False

zToInt :: Z -> Int

Convert a Z to an Int

type family Succ z :: Z

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

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

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

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

Multiply two integers

Equations

Zero #* z = Zero

(S z1) #* z2 = (z1 #* z2) #+ z2

(P z1) #* z2 = (z1 #* z2) #- z2

type family NegZ z :: Z

Negate an integer

Equations

NegZ Zero = Zero

NegZ (S z) = P (NegZ z)

NegZ (P z) = S (NegZ z)

type family a #/ b :: Z

Divide two integers

Equations

Zero #/ b = Zero

a #/ (P b') = NegZ (a #/ NegZ (P b'))

a #/ b = ZDiv b b a

type family ZDiv counter n z :: Z

Helper function for division

Equations

ZDiv One n (S z') = S (z' #/ n)

ZDiv One n (P z') = P (z' #/ n)

ZDiv (S count') n (S z') = ZDiv count' n z'

ZDiv (S count') n (P z') = ZDiv count' n z'

type family a < b :: Bool

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 One = S Zero

type Two = S One

type Three = S Two

type Four = S Three

type Five = S Four

type MOne = P Zero

type MTwo = P MOne

type MThree = P MTwo

type MFour = P MThree

type MFive = P MFour

pZero :: Sing Z Zero

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

pOne :: Sing Z (S Zero)

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

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

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

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

pMOne :: Sing Z (P Zero)

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

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

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

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

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

Add one to a singleton Z.

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

Subtract one from a singleton Z.

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

Convert a singleton Z to an Int.