| Copyright | Copyright (C) 2006-2015 Bjorn Buckwalter |
|---|---|
| License | BSD3 |
| Maintainer | bjorn.buckwalter@gmail.com |
| Stability | Stable |
| Portability | GHC only |
| Safe Haskell | Safe |
| Language | Haskell98 |
| Extensions |
|
Numeric.NumType.DK.Integers
Contents
Description
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.
- data TypeInt
- type family Pred i :: TypeInt
- type family Succ i :: TypeInt
- type family Negate i :: TypeInt
- type family Abs i :: TypeInt
- type family Signum i :: TypeInt
- type family i + i' :: TypeInt
- type family i - i' :: TypeInt
- type family i * i' :: TypeInt
- type family i / i' :: TypeInt
- type family i ^ i' :: TypeInt
- 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')
- (-) :: Proxy i -> Proxy i' -> Proxy (i - i')
- (*) :: Proxy i -> Proxy i' -> Proxy (i * i')
- (/) :: Proxy i -> Proxy i' -> Proxy (i / i')
- (^) :: Proxy i -> Proxy i' -> Proxy (i ^ i')
- 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
- class KnownTypeInt i where
Type-Level Integers
Type-level Arithmetic
type family Pred i :: TypeInt Source
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 Source
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 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 |
type family i + i' :: TypeInt infixl 6 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' |
type family i * i' :: TypeInt infixl 7 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') |
type family i / i' :: TypeInt infixl 7 Source
TypeInt division.
Equations
type family i ^ i' :: TypeInt infixr 8 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
Convenience Synonyms for Proxies
Conversion from Types to Terms
class KnownTypeInt i where Source
Conversion to a Num.
Instances