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.

Cpp
UndecidableInstances
MonoLocalBinds
TypeFamilies
DataKinds
DeriveDataTypeable
AutoDeriveTypeable
TypeSynonymInstances
FlexibleContexts
FlexibleInstances
KindSignatures
TypeOperators
ExplicitNamespaces

Contents

Type-Level Integers
Type-level Arithmetic
Arithmetic on Proxies
Convenience Synonyms for Proxies
Conversion from Types to Terms

Synopsis

data TypeInt
family Pred
family Succ
family Negate
family Abs
family Signum
family +
family -
family *
family /
family ^
value pred
value succ
value negate
value abs
value signum
value +
value -
value *
value /
value ^
value zero
value pos1
value pos2
value pos3
value pos4
value pos5
value pos6
value pos7
value pos8
value pos9
value neg1
value neg2
value neg3
value neg4
value neg5
value neg6
value neg7
value neg8
value neg9
class KnownTypeInt

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

Type-Level Integers

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

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

Source#

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

Source#

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

Source#

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

Source#

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

Source#

TypeInt subtraction.

Equations

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

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

Source#

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

Source#

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

Source#

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

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

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

classclass KnownTypeInt (i :: TypeInt) where

Source#

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