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

Instances

Typeable * TypeInt

Typeable TypeInt Pos9

Typeable TypeInt Pos8

Typeable TypeInt Pos7

Typeable TypeInt Pos6

Typeable TypeInt Pos5

Typeable TypeInt Pos4

Typeable TypeInt Pos3

Typeable TypeInt Pos2

Typeable TypeInt Pos1

Typeable TypeInt Zero

Typeable TypeInt Neg1

Typeable TypeInt Neg2

Typeable TypeInt Neg3

Typeable TypeInt Neg4

Typeable TypeInt Neg5

Typeable TypeInt Neg6

Typeable TypeInt Neg7

Typeable TypeInt Neg8

Typeable TypeInt Neg9

Typeable (TypeInt -> Constraint) KnownTypeInt

Type-level Arithmetic

type family Pred i :: TypeInt

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

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

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

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 + i' :: TypeInt 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 - i' :: TypeInt infixl 6

TypeInt subtraction.

Equations

i - i' = i + Negate i'

type family i * i' :: TypeInt 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 / i' :: TypeInt 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 ^ i' :: TypeInt 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 where

Conversion to a Num.

Methods

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

Instances

KnownTypeInt Pos9

KnownTypeInt Pos8

KnownTypeInt Pos7

KnownTypeInt Pos6

KnownTypeInt Pos5

KnownTypeInt Pos4

KnownTypeInt Pos3

KnownTypeInt Pos2

KnownTypeInt Pos1

KnownTypeInt Zero

KnownTypeInt Neg1

KnownTypeInt Neg2

KnownTypeInt Neg3

KnownTypeInt Neg4

KnownTypeInt Neg5

KnownTypeInt Neg6

KnownTypeInt Neg7

KnownTypeInt Neg8

KnownTypeInt Neg9

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

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

Typeable (TypeInt -> Constraint) KnownTypeInt