Numeric.NumType.DK.Integers

Summary

Type-level integers for GHC 7.8+.

We provide type level arithmetic operations. We also provide term-level arithmetic operations on proxys, and conversion from the type level to the term level.

Planned Obsolesence

We commit this package to hackage in sure and certain hope of the coming of glorious GHC integer type literals, when the sea shall give up her dead, and this package shall be rendered unto obsolescence.

Type-Level Integers

data TypeInt

Constructors

Neg10Minus Nat

Neg9

Neg8

Neg7

Neg6

Neg5

Neg4

Neg3

Neg2

Neg1

Zero

Pos1

Pos2

Pos3

Pos4

Pos5

Pos6

Pos7

Pos8

Pos9

Pos10Plus Nat

Type-level Arithmetic

type family Pred (i :: TypeInt) :: TypeInt where ...

Equations

Pred (Neg10Minus n) = Neg10Minus (NatSucc n)

Pred Neg9 = Neg10Minus Z

Pred Neg8 = Neg9

Pred Neg7 = Neg8

Pred Neg6 = Neg7

Pred Neg5 = Neg6

Pred Neg4 = Neg5

Pred Neg3 = Neg4

Pred Neg2 = Neg3

Pred Neg1 = Neg2

Pred Zero = Neg1

Pred Pos1 = Zero

Pred Pos2 = Pos1

Pred Pos3 = Pos2

Pred Pos4 = Pos3

Pred Pos5 = Pos4

Pred Pos6 = Pos5

Pred Pos7 = Pos6

Pred Pos8 = Pos7

Pred Pos9 = Pos8

Pred (Pos10Plus Z) = Pos9

Pred (Pos10Plus n) = Pos10Plus (NatPred n)

type family Succ (i :: TypeInt) :: TypeInt where ...

Equations

Succ (Neg10Minus Z) = Neg9

Succ (Neg10Minus n) = Neg10Minus (NatPred n)

Succ Neg9 = Neg8

Succ Neg8 = Neg7

Succ Neg7 = Neg6

Succ Neg6 = Neg5

Succ Neg5 = Neg4

Succ Neg4 = Neg3

Succ Neg3 = Neg2

Succ Neg2 = Neg1

Succ Neg1 = Zero

Succ Zero = Pos1

Succ Pos1 = Pos2

Succ Pos2 = Pos3

Succ Pos3 = Pos4

Succ Pos4 = Pos5

Succ Pos5 = Pos6

Succ Pos6 = Pos7

Succ Pos7 = Pos8

Succ Pos8 = Pos9

Succ Pos9 = Pos10Plus Z

Succ (Pos10Plus n) = Pos10Plus (NatSucc n)

type family Negate (i :: TypeInt) :: TypeInt where ...

TypeInt negation.

Equations

Negate (Neg10Minus n) = Pos10Plus n

Negate Neg9 = Pos9

Negate Neg8 = Pos8

Negate Neg7 = Pos7

Negate Neg6 = Pos6

Negate Neg5 = Pos5

Negate Neg4 = Pos4

Negate Neg3 = Pos3

Negate Neg2 = Pos2

Negate Neg1 = Pos1

Negate Zero = Zero

Negate Pos1 = Neg1

Negate Pos2 = Neg2

Negate Pos3 = Neg3

Negate Pos4 = Neg4

Negate Pos5 = Neg5

Negate Pos6 = Neg6

Negate Pos7 = Neg7

Negate Pos8 = Neg8

Negate Pos9 = Neg9

Negate (Pos10Plus n) = Neg10Minus n

type family Abs (i :: TypeInt) :: TypeInt where ...

Absolute value.

Equations

Abs (Neg10Minus n) = Pos10Plus n

Abs Neg9 = Pos9

Abs Neg8 = Pos8

Abs Neg7 = Pos7

Abs Neg6 = Pos6

Abs Neg5 = Pos5

Abs Neg4 = Pos4

Abs Neg3 = Pos3

Abs Neg2 = Pos2

Abs Neg1 = Pos1

Abs i = i

type family Signum (i :: TypeInt) :: TypeInt where ...

Signum.

Equations

Signum (Neg10Minus n) = Neg1

Signum Neg9 = Neg1

Signum Neg8 = Neg1

Signum Neg7 = Neg1

Signum Neg6 = Neg1

Signum Neg5 = Neg1

Signum Neg4 = Neg1

Signum Neg3 = Neg1

Signum Neg2 = Neg1

Signum Neg1 = Neg1

Signum Zero = Zero

Signum i = Pos1

type family (i :: TypeInt) + (i' :: TypeInt) :: TypeInt where ... infixl 6

TypeInt addition.

Equations

Zero + i = i

i + (Neg10Minus n) = Pred i + Succ (Neg10Minus n)

i + Neg9 = Pred i + Neg8

i + Neg8 = Pred i + Neg7

i + Neg7 = Pred i + Neg6

i + Neg6 = Pred i + Neg5

i + Neg5 = Pred i + Neg4

i + Neg4 = Pred i + Neg3

i + Neg3 = Pred i + Neg2

i + Neg2 = Pred i + Neg1

i + Neg1 = Pred i

i + Zero = i

i + i' = Succ i + Pred i'

type family (i :: TypeInt) - (i' :: TypeInt) :: TypeInt where ... infixl 6

TypeInt subtraction.

Equations

i - i' = i + Negate i'

type family (i :: TypeInt) * (i' :: TypeInt) :: TypeInt where ... infixl 7

TypeInt multiplication.

Equations

Zero * i = Zero

i * Zero = Zero

i * Pos1 = i

i * Pos2 = i + i

i * Pos3 = (i + i) + i

i * Pos4 = ((i + i) + i) + i

i * Pos5 = (((i + i) + i) + i) + i

i * Pos6 = ((((i + i) + i) + i) + i) + i

i * Pos7 = (((((i + i) + i) + i) + i) + i) + i

i * Pos8 = ((((((i + i) + i) + i) + i) + i) + i) + i

i * Pos9 = (((((((i + i) + i) + i) + i) + i) + i) + i) + i

i * (Pos10Plus n) = i + (i * Pred (Pos10Plus n))

i * i' = Negate (i * Negate i')

type family (i :: TypeInt) / (i' :: TypeInt) :: TypeInt where ... infixl 7

TypeInt division.

Equations

i / Pos1 = i

i / Neg1 = Negate i

Zero / (Neg10Minus n) = Zero

Zero / Neg9 = Zero

Zero / Neg8 = Zero

Zero / Neg7 = Zero

Zero / Neg6 = Zero

Zero / Neg5 = Zero

Zero / Neg4 = Zero

Zero / Neg3 = Zero

Zero / Neg2 = Zero

Zero / Pos2 = Zero

Zero / Pos3 = Zero

Zero / Pos4 = Zero

Zero / Pos5 = Zero

Zero / Pos6 = Zero

Zero / Pos7 = Zero

Zero / Pos8 = Zero

Zero / Pos9 = Zero

Zero / (Pos10Plus n) = Zero

Neg2 / Neg2 = Pos1

Neg3 / Neg3 = Pos1

Neg4 / Neg4 = Pos1

Neg5 / Neg5 = Pos1

Neg6 / Neg6 = Pos1

Neg7 / Neg7 = Pos1

Neg8 / Neg8 = Pos1

Neg9 / Neg9 = Pos1

(Neg10Minus n) / (Neg10Minus n) = Pos1

Neg2 / Pos2 = Neg1

Neg3 / Pos3 = Neg1

Neg4 / Pos4 = Neg1

Neg5 / Pos5 = Neg1

Neg6 / Pos6 = Neg1

Neg7 / Pos7 = Neg1

Neg8 / Pos8 = Neg1

Neg9 / Pos9 = Neg1

(Neg10Minus n) / (Pos10Plus n) = Neg1

Pos2 / Neg2 = Neg1

Pos3 / Neg3 = Neg1

Pos4 / Neg4 = Neg1

Pos5 / Neg5 = Neg1

Pos6 / Neg6 = Neg1

Pos7 / Neg7 = Neg1

Pos8 / Neg8 = Neg1

Pos9 / Neg9 = Neg1

(Pos10Plus n) / (Neg10Minus n) = Neg1

Pos2 / Pos2 = Pos1

Pos3 / Pos3 = Pos1

Pos4 / Pos4 = Pos1

Pos5 / Pos5 = Pos1

Pos6 / Pos6 = Pos1

Pos7 / Pos7 = Pos1

Pos8 / Pos8 = Pos1

Pos9 / Pos9 = Pos1

(Pos10Plus n) / (Pos10Plus n) = Pos1

Neg4 / Neg2 = Pos2

Neg6 / Neg2 = Pos3

Neg8 / Neg2 = Pos4

Neg6 / Neg3 = Pos2

Neg9 / Neg3 = Pos3

Neg8 / Neg4 = Pos2

(Neg10Minus n) / i = ((Neg10Minus n + Abs i) / i) - Signum i

Neg4 / Pos2 = Neg2

Neg6 / Pos2 = Neg3

Neg8 / Pos2 = Neg4

Neg6 / Pos3 = Neg2

Neg9 / Pos3 = Neg3

Neg8 / Pos4 = Neg2

Pos4 / Neg2 = Neg2

Pos6 / Neg2 = Neg3

Pos8 / Neg2 = Neg4

Pos6 / Neg3 = Neg2

Pos9 / Neg3 = Neg3

Pos8 / Neg4 = Neg2

Pos4 / Pos2 = Pos2

Pos6 / Pos2 = Pos3

Pos8 / Pos2 = Pos4

Pos6 / Pos3 = Pos2

Pos9 / Pos3 = Pos3

Pos8 / Pos4 = Pos2

(Pos10Plus n) / i = ((Pos10Plus n - Abs i) / i) + Signum i

type family (i :: TypeInt) ^ (i' :: TypeInt) :: TypeInt where ... infixr 8

TypeInt exponentiation.

Equations

i ^ Zero = Pos1

i ^ Pos1 = i

i ^ Pos2 = i * i

i ^ Pos3 = (i * i) * i

i ^ Pos4 = ((i * i) * i) * i

i ^ Pos5 = (((i * i) * i) * i) * i

i ^ Pos6 = ((((i * i) * i) * i) * i) * i

i ^ Pos7 = (((((i * i) * i) * i) * i) * i) * i

i ^ Pos8 = ((((((i * i) * i) * i) * i) * i) * i) * i

i ^ Pos9 = (((((((i * i) * i) * i) * i) * i) * i) * i) * i

i ^ (Pos10Plus n) = i * (i ^ Pred (Pos10Plus n))

Arithmetic on Proxies

pred :: Proxy i -> Proxy (Pred i)

succ :: Proxy i -> Proxy (Succ i)

negate :: Proxy i -> Proxy (Negate i)

abs :: Proxy i -> Proxy (Abs i)

signum :: Proxy i -> Proxy (Signum i)

(+) :: Proxy i -> Proxy i' -> Proxy (i + i') infixl 6

(-) :: Proxy i -> Proxy i' -> Proxy (i - i') infixl 6

(*) :: Proxy i -> Proxy i' -> Proxy (i * i') infixl 7

(/) :: Proxy i -> Proxy i' -> Proxy (i / i') infixl 7

(^) :: Proxy i -> Proxy i' -> Proxy (i ^ i') infixr 8

Convenience Synonyms for Proxies

zero :: Proxy Zero

pos1 :: Proxy Pos1

pos2 :: Proxy Pos2

pos3 :: Proxy Pos3

pos4 :: Proxy Pos4

pos5 :: Proxy Pos5

pos6 :: Proxy Pos6

pos7 :: Proxy Pos7

pos8 :: Proxy Pos8

pos9 :: Proxy Pos9

neg1 :: Proxy Neg1

neg2 :: Proxy Neg2

neg3 :: Proxy Neg3

neg4 :: Proxy Neg4

neg5 :: Proxy Neg5

neg6 :: Proxy Neg6

neg7 :: Proxy Neg7

neg8 :: Proxy Neg8

neg9 :: Proxy Neg9

Conversion from Types to Terms

class KnownTypeInt (i :: TypeInt) where

Conversion to a Num.

Minimal complete definition

toNum

Methods

toNum :: Num a => Proxy i -> a

Instances

KnownTypeInt Neg9

Defined in Numeric.NumType.DK.Integers

Methods

toNum :: Num a => Proxy Neg9 -> a

KnownTypeInt Neg8

Defined in Numeric.NumType.DK.Integers

Methods

toNum :: Num a => Proxy Neg8 -> a

KnownTypeInt Neg7

Defined in Numeric.NumType.DK.Integers

Methods

toNum :: Num a => Proxy Neg7 -> a

KnownTypeInt Neg6

Defined in Numeric.NumType.DK.Integers

Methods

toNum :: Num a => Proxy Neg6 -> a

KnownTypeInt Neg5

Defined in Numeric.NumType.DK.Integers

Methods

toNum :: Num a => Proxy Neg5 -> a

KnownTypeInt Neg4

Defined in Numeric.NumType.DK.Integers

Methods

toNum :: Num a => Proxy Neg4 -> a

KnownTypeInt Neg3

Defined in Numeric.NumType.DK.Integers

Methods

toNum :: Num a => Proxy Neg3 -> a

KnownTypeInt Neg2

Defined in Numeric.NumType.DK.Integers

Methods

toNum :: Num a => Proxy Neg2 -> a

KnownTypeInt Neg1

Defined in Numeric.NumType.DK.Integers

Methods

toNum :: Num a => Proxy Neg1 -> a

KnownTypeInt Zero

Defined in Numeric.NumType.DK.Integers

Methods

toNum :: Num a => Proxy Zero -> a

KnownTypeInt Pos1

Defined in Numeric.NumType.DK.Integers

Methods

toNum :: Num a => Proxy Pos1 -> a

KnownTypeInt Pos2

Defined in Numeric.NumType.DK.Integers

Methods

toNum :: Num a => Proxy Pos2 -> a

KnownTypeInt Pos3

Defined in Numeric.NumType.DK.Integers

Methods

toNum :: Num a => Proxy Pos3 -> a

KnownTypeInt Pos4

Defined in Numeric.NumType.DK.Integers

Methods

toNum :: Num a => Proxy Pos4 -> a

KnownTypeInt Pos5

Defined in Numeric.NumType.DK.Integers

Methods

toNum :: Num a => Proxy Pos5 -> a

KnownTypeInt Pos6

Defined in Numeric.NumType.DK.Integers

Methods

toNum :: Num a => Proxy Pos6 -> a

KnownTypeInt Pos7

Defined in Numeric.NumType.DK.Integers

Methods

toNum :: Num a => Proxy Pos7 -> a

KnownTypeInt Pos8

Defined in Numeric.NumType.DK.Integers

Methods

toNum :: Num a => Proxy Pos8 -> a

KnownTypeInt Pos9

Defined in Numeric.NumType.DK.Integers

Methods

toNum :: Num a => Proxy Pos9 -> a

KnownTypeInt (Succ (Neg10Minus n)) => KnownTypeInt (Neg10Minus n)

Defined in Numeric.NumType.DK.Integers

Methods

toNum :: Num a => Proxy (Neg10Minus n) -> a

KnownTypeInt (Pred (Pos10Plus n)) => KnownTypeInt (Pos10Plus n)

Defined in Numeric.NumType.DK.Integers

Methods

toNum :: Num a => Proxy (Pos10Plus n) -> a