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, rae at cs.brynmawr.edu) know.

The Z datatype

data Z

The datatype for type-level integers.

Constructors

Zero

S Z

P Z

Instances

Eq Z

Methods

(==) :: Z -> Z -> Bool

(/=) :: Z -> Z -> Bool

SEq Z

Methods

(%:==) :: Sing Z a -> Sing Z b -> Sing Bool ((Z :== a) b)

(%:/=) :: Sing Z a -> Sing Z b -> Sing Bool ((Z :/= a) b)

PEq Z

Associated Types

type (Z :== (x :: Z)) (y :: Z) :: Bool

type (Z :/= (x :: Z)) (y :: Z) :: Bool

SDecide Z

Methods

(%~) :: Sing Z a -> Sing Z b -> Decision ((Z :~: a) b)

SingKind Z

Associated Types

type Demote Z = (r :: *)

Methods

fromSing :: Sing Z a -> Demote Z

toSing :: Demote Z -> SomeSing Z

SingI Z Zero

Methods

sing :: Sing Zero a

SingI Z n => SingI Z (S n)

Methods

sing :: Sing (S n) a

SingI Z n => SingI Z (P n)

Methods

sing :: Sing (P n) a

SuppressUnusedWarnings (TyFun Z Z -> *) PSym0

Methods

suppressUnusedWarnings :: Proxy PSym0 t -> ()

SuppressUnusedWarnings (TyFun Z Z -> *) SSym0

Methods

suppressUnusedWarnings :: Proxy SSym0 t -> ()

data Sing Z

data Sing Z where

• SZero :: Sing Z z
• SS :: Sing Z z
• SP :: Sing Z z

type Demote Z

type Demote Z = Z

type (:/=) Z x y

type (:/=) Z x y = Not ((:==) Z x y)

type (:==) Z a b

type (:==) Z a b

type Apply Z Z PSym0 l

type Apply Z Z PSym0 l = P l

type Apply Z Z SSym0 l

type Apply Z Z SSym0 l = S l

data family Sing k (a :: k) :: *

The singleton kind-indexed data family.

Instances

data Sing Bool

data Sing Bool where

• SFalse :: Sing Bool z
• STrue :: Sing Bool z

data Sing Ordering

data Sing Ordering where

• SLT :: Sing Ordering z
• SEQ :: Sing Ordering z
• SGT :: Sing Ordering z

data Sing Nat

data Sing Nat where

• SNat :: Sing Nat n

data Sing Symbol

data Sing Symbol where

• SSym :: Sing Symbol n

data Sing ()

data Sing () where

• STuple0 :: Sing () z

data Sing Z

data Sing Z where

• SZero :: Sing Z z
• SS :: Sing Z z
• SP :: Sing Z z

data Sing [a]

data Sing [a] where

• SNil :: Sing [a] z
• SCons :: Sing [a] z

data Sing (Maybe a)

data Sing (Maybe a) where

• SNothing :: Sing (Maybe a) z
• SJust :: Sing (Maybe a) z

data Sing (NonEmpty a)

data Sing (NonEmpty a) where

• (:%|) :: Sing (NonEmpty a) z

data Sing (Either a b)

data Sing (Either a b) where

• SLeft :: Sing (Either a b) z
• SRight :: Sing (Either a b) z

data Sing (a, b)

data Sing (a, b) where

• STuple2 :: Sing (a, b) z

data Sing ((~>) k1 k2)

data Sing ((~>) k1 k2) = SLambda {

• applySing :: forall (t :: k1). Sing k1 t -> Sing k2 ((@@) k1 k2 f t)

}

data Sing (a, b, c)

data Sing (a, b, c) where

• STuple3 :: Sing (a, b, c) z

data Sing (a, b, c, d)

data Sing (a, b, c, d) where

• STuple4 :: Sing (a, b, c, d) z

data Sing (a, b, c, d, e)

data Sing (a, b, c, d, e) where

• STuple5 :: Sing (a, b, c, d, e) z

data Sing (a, b, c, d, e, f)

data Sing (a, b, c, d, e, f) where

• STuple6 :: Sing (a, b, c, d, e, f) z

data Sing (a, b, c, d, e, f, g)

data Sing (a, b, c, d, e, f, g) where

• STuple7 :: Sing (a, b, c, d, e, f, g) z

type SZ = (Sing :: Z -> Type)

Defunctionalization symbols (these can be ignored)

type ZeroSym0 = Zero

data SSym0 (l :: TyFun Z Z)

Instances

SuppressUnusedWarnings (TyFun Z Z -> *) SSym0

Methods

suppressUnusedWarnings :: Proxy SSym0 t -> ()

type Apply Z Z SSym0 l

type Apply Z Z SSym0 l = S l

type SSym1 (t :: Z) = S t

data PSym0 (l :: TyFun Z Z)

Instances

SuppressUnusedWarnings (TyFun Z Z -> *) PSym0

Methods

suppressUnusedWarnings :: Proxy PSym0 t -> ()

type Apply Z Z PSym0 l

type Apply Z Z PSym0 l = P l

type PSym1 (t :: Z) = P t

Conversions

zToInt :: Z -> Int

Convert a Z to an Int

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

Convert a singleton Z to an Int.

Type-level operations

Arithmetic

type family Succ (z :: Z) :: Z where ...

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) :: Z where ...

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) :: Z where ...

Negate an integer

Equations

Negate Zero = Zero

Negate (S z) = P (Negate z)

Negate (P z) = S (Negate z)

type family (a :: Z) #+ (b :: Z) :: Z where ... 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 :: Z) #- (b :: Z) :: Z where ... 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 :: Z) #* (b :: Z) :: Z where ... infixl 7

Multiply two integers

Equations

Zero #* z = Zero

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

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

type family (a :: Z) #/ (b :: Z) :: Z where ...

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)

Add one to a singleton Z.

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

Subtract one from a singleton Z.

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

Negate a singleton Z.

Comparisons

type family (a :: Z) < (b :: Z) :: Bool where ...

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 where ...

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

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

sZero :: 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.

sOne :: Sing Z (S Zero)

sTwo :: Sing Z (S (S Zero))

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

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

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

sMOne :: Sing Z (P Zero)

sMTwo :: Sing Z (P (P Zero))

sMThree :: Sing Z (P (P (P Zero)))

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

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

Deprecated synonyms

pZero :: Sing Z Zero

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)

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

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

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

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

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)

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

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

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

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

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)

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)

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