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.

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