Modulenumtype-dk-0.5.0.3Haskell98

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.

1 type
1 class
29 values
Cpp
UndecidableInstances
MonoLocalBinds
TypeFamilies
DataKinds
DeriveDataTypeable
AutoDeriveTypeable
TypeSynonymInstances
FlexibleContexts
FlexibleInstances
KindSignatures
TypeOperators
ExplicitNamespaces

Packagenumtype-dk-0.5.0.3
Exports41
LanguageHaskell98
LicenceBSD-3-Clause
SourceIntegers.hs

Type-Level Integers

1 declaration

datadata 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

10 declarations

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

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

familytype 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

familytype 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

familytype 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

familytype family (+) (i :: TypeInt) (i' :: TypeInt) :: TypeInt where

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'

familytype family (-) (i :: TypeInt) (i' :: TypeInt) :: TypeInt where

TypeInt subtraction.

Equations

(-) i i' = i + Negate i'

familytype family (*) (i :: TypeInt) (i' :: TypeInt) :: TypeInt where

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

familytype family (/) (i :: TypeInt) (i' :: TypeInt) :: TypeInt where

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

familytype family (^) (i :: TypeInt) (i' :: TypeInt) :: TypeInt where

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

10 declarations

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

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

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

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

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

value(+) :: Proxy i -> Proxy i' -> Proxy (i + i')

value(-) :: Proxy i -> Proxy i' -> Proxy (i - i')

value(*) :: Proxy i -> Proxy i' -> Proxy (i * i')

value(/) :: Proxy i -> Proxy i' -> Proxy (i / i')

value(^) :: Proxy i -> Proxy i' -> Proxy (i ^ i')

Convenience Synonyms for Proxies

19 declarations

valuezero :: Proxy 'Zero

valuepos1 :: Proxy 'Pos1

valuepos2 :: Proxy 'Pos2

valuepos3 :: Proxy 'Pos3

valuepos4 :: Proxy 'Pos4

valuepos5 :: Proxy 'Pos5

valuepos6 :: Proxy 'Pos6

valuepos7 :: Proxy 'Pos7

valuepos8 :: Proxy 'Pos8

valuepos9 :: Proxy 'Pos9

valueneg1 :: Proxy 'Neg1

valueneg2 :: Proxy 'Neg2

valueneg3 :: Proxy 'Neg3

valueneg4 :: Proxy 'Neg4

valueneg5 :: Proxy 'Neg5

valueneg6 :: Proxy 'Neg6

valueneg7 :: Proxy 'Neg7

valueneg8 :: Proxy 'Neg8

valueneg9 :: Proxy 'Neg9

Conversion from Types to Terms

1 declaration

classclass KnownTypeInt (i :: TypeInt) where

Conversion to a Num.

Methods

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

Instances21KnownTypeInt, …

KnownTypeInt 'Neg1Defined in numtype-dk-0.5.0.3 · Numeric.NumType.DK.Integers
KnownTypeInt 'Neg2Defined in numtype-dk-0.5.0.3 · Numeric.NumType.DK.Integers
KnownTypeInt 'Neg3Defined in numtype-dk-0.5.0.3 · Numeric.NumType.DK.Integers
KnownTypeInt 'Neg4Defined in numtype-dk-0.5.0.3 · Numeric.NumType.DK.Integers
KnownTypeInt 'Neg5Defined in numtype-dk-0.5.0.3 · Numeric.NumType.DK.Integers
KnownTypeInt 'Neg6Defined in numtype-dk-0.5.0.3 · Numeric.NumType.DK.Integers
KnownTypeInt 'Neg7Defined in numtype-dk-0.5.0.3 · Numeric.NumType.DK.Integers
KnownTypeInt 'Neg8Defined in numtype-dk-0.5.0.3 · Numeric.NumType.DK.Integers
KnownTypeInt 'Neg9Defined in numtype-dk-0.5.0.3 · Numeric.NumType.DK.Integers
KnownTypeInt 'Pos1Defined in numtype-dk-0.5.0.3 · Numeric.NumType.DK.Integers
KnownTypeInt 'Pos2Defined in numtype-dk-0.5.0.3 · Numeric.NumType.DK.Integers
KnownTypeInt 'Pos3Defined in numtype-dk-0.5.0.3 · Numeric.NumType.DK.Integers
KnownTypeInt 'Pos4Defined in numtype-dk-0.5.0.3 · Numeric.NumType.DK.Integers
KnownTypeInt 'Pos5Defined in numtype-dk-0.5.0.3 · Numeric.NumType.DK.Integers
KnownTypeInt 'Pos6Defined in numtype-dk-0.5.0.3 · Numeric.NumType.DK.Integers
KnownTypeInt 'Pos7Defined in numtype-dk-0.5.0.3 · Numeric.NumType.DK.Integers
KnownTypeInt 'Pos8Defined in numtype-dk-0.5.0.3 · Numeric.NumType.DK.Integers
KnownTypeInt 'Pos9Defined in numtype-dk-0.5.0.3 · Numeric.NumType.DK.Integers
KnownTypeInt 'ZeroDefined in numtype-dk-0.5.0.3 · Numeric.NumType.DK.Integers
KnownTypeInt (Pred ('Pos10Plus n)) => KnownTypeInt ('Pos10Plus n)Defined in numtype-dk-0.5.0.3 · Numeric.NumType.DK.Integers
KnownTypeInt (Succ ('Neg10Minus n)) => KnownTypeInt ('Neg10Minus n)Defined in numtype-dk-0.5.0.3 · Numeric.NumType.DK.Integers