numtype-dk-0.5.0.3: Type-level integers, using TypeNats, Data Kinds, and Closed Type Families.

Copyright | Copyright (C) 2006-2015 Bjorn Buckwalter
License | BSD3
Maintainer | bjorn.buckwalter@gmail.com
Stability | Stable
Portability | GHC only
Safe Haskell | Safe-Inferred
Language | Haskell98

Extensions

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

Numeric.NumType.DK.Integers

Contents

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

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.

Synopsis

- data TypeInt
  - = Neg10Minus Nat
  - | Neg9
  - | Neg8
  - | Neg7
  - | Neg6
  - | Neg5
  - | Neg4
  - | Neg3
  - | Neg2
  - | Neg1
  - | Zero
  - | Pos1
  - | Pos2
  - | Pos3
  - | Pos4
  - | Pos5
  - | Pos6
  - | Pos7
  - | Pos8
  - | Pos9
  - | Pos10Plus Nat
- type family Pred (i :: TypeInt) :: TypeInt where ...
- type family Succ (i :: TypeInt) :: TypeInt where ...
- type family Negate (i :: TypeInt) :: TypeInt where ...
- type family Abs (i :: TypeInt) :: TypeInt where ...
- type family Signum (i :: TypeInt) :: TypeInt where ...
- type family (i :: TypeInt) + (i' :: TypeInt) :: TypeInt where ...
- type family (i :: TypeInt) - (i' :: TypeInt) :: TypeInt where ...
- type family (i :: TypeInt) * (i' :: TypeInt) :: TypeInt where ...
- type family (i :: TypeInt) / (i' :: TypeInt) :: TypeInt where ...
- type family (i :: TypeInt) ^ (i' :: TypeInt) :: TypeInt where ...
- pred :: forall (i :: TypeInt). Proxy i -> Proxy (Pred i)
- succ :: forall (i :: TypeInt). Proxy i -> Proxy (Succ i)
- negate :: forall (i :: TypeInt). Proxy i -> Proxy (Negate i)
- abs :: forall (i :: TypeInt). Proxy i -> Proxy (Abs i)
- signum :: forall (i :: TypeInt). Proxy i -> Proxy (Signum i)
- (+) :: forall (i :: TypeInt) (i' :: TypeInt). Proxy i -> Proxy i' -> Proxy (i + i')
- (-) :: forall (i :: TypeInt) (i' :: TypeInt). Proxy i -> Proxy i' -> Proxy (i - i')
- (*) :: forall (i :: TypeInt) (i' :: TypeInt). Proxy i -> Proxy i' -> Proxy (i * i')
- (/) :: forall (i :: TypeInt) (i' :: TypeInt). Proxy i -> Proxy i' -> Proxy (i / i')
- (^) :: forall (i :: TypeInt) (i' :: TypeInt). 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 :: TypeInt) where
  - toNum :: Num a => Proxy i -> a

# Type-Level Integers

data TypeInt Source #

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 ... 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) :: TypeInt where ... 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) :: 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 |

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

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

type family (i :: TypeInt) + (i' :: TypeInt) :: TypeInt where ... 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 :: TypeInt) - (i' :: TypeInt) :: TypeInt where ... infixl 6 Source #

TypeInt subtraction.

Equations

i - i' = i + Negate i' |

type family (i :: TypeInt) * (i' :: TypeInt) :: TypeInt where ... 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 :: TypeInt) / (i' :: TypeInt) :: TypeInt where ... infixl 7 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 |

type family (i :: TypeInt) ^ (i' :: TypeInt) :: TypeInt where ... 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

pred :: forall (i :: TypeInt). Proxy i -> Proxy (Pred i) Source #

succ :: forall (i :: TypeInt). Proxy i -> Proxy (Succ i) Source #

negate :: forall (i :: TypeInt). Proxy i -> Proxy (Negate i) Source #

abs :: forall (i :: TypeInt). Proxy i -> Proxy (Abs i) Source #

signum :: forall (i :: TypeInt). Proxy i -> Proxy (Signum i) Source #

(+) :: forall (i :: TypeInt) (i' :: TypeInt). Proxy i -> Proxy i' -> Proxy (i + i') infixl 6 Source #

(-) :: forall (i :: TypeInt) (i' :: TypeInt). Proxy i -> Proxy i' -> Proxy (i - i') infixl 6 Source #

(*) :: forall (i :: TypeInt) (i' :: TypeInt). Proxy i -> Proxy i' -> Proxy (i * i') infixl 7 Source #

(/) :: forall (i :: TypeInt) (i' :: TypeInt). Proxy i -> Proxy i' -> Proxy (i / i') infixl 7 Source #

(^) :: forall (i :: TypeInt) (i' :: TypeInt). Proxy i -> Proxy i' -> Proxy (i ^ i') infixr 8 Source #

# Convenience Synonyms for Proxies

zero :: Proxy 'Zero Source #

pos1 :: Proxy 'Pos1 Source #

pos2 :: Proxy 'Pos2 Source #

pos3 :: Proxy 'Pos3 Source #

pos4 :: Proxy 'Pos4 Source #

pos5 :: Proxy 'Pos5 Source #

pos6 :: Proxy 'Pos6 Source #

pos7 :: Proxy 'Pos7 Source #

pos8 :: Proxy 'Pos8 Source #

pos9 :: Proxy 'Pos9 Source #

neg1 :: Proxy 'Neg1 Source #

neg2 :: Proxy 'Neg2 Source #

neg3 :: Proxy 'Neg3 Source #

neg4 :: Proxy 'Neg4 Source #

neg5 :: Proxy 'Neg5 Source #

neg6 :: Proxy 'Neg6 Source #

neg7 :: Proxy 'Neg7 Source #

neg8 :: Proxy 'Neg8 Source #

neg9 :: Proxy 'Neg9 Source #

# Conversion from Types to Terms

class KnownTypeInt (i :: TypeInt) where Source #

Conversion to a `Num`.

Methods

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

#### Instances

Instances details

KnownTypeInt 'Neg1 Source # |
Instance details Defined in Numeric.NumType.DK.Integers Methods toNum :: Num a => Proxy 'Neg1 -> a Source #
KnownTypeInt 'Neg2 Source # |
Instance details Defined in Numeric.NumType.DK.Integers Methods toNum :: Num a => Proxy 'Neg2 -> a Source #
KnownTypeInt 'Neg3 Source # |
Instance details Defined in Numeric.NumType.DK.Integers Methods toNum :: Num a => Proxy 'Neg3 -> a Source #
KnownTypeInt 'Neg4 Source # |
Instance details Defined in Numeric.NumType.DK.Integers Methods toNum :: Num a => Proxy 'Neg4 -> a Source #
KnownTypeInt 'Neg5 Source # |
Instance details Defined in Numeric.NumType.DK.Integers Methods toNum :: Num a => Proxy 'Neg5 -> a Source #
KnownTypeInt 'Neg6 Source # |
Instance details Defined in Numeric.NumType.DK.Integers Methods toNum :: Num a => Proxy 'Neg6 -> a Source #
KnownTypeInt 'Neg7 Source # |
Instance details Defined in Numeric.NumType.DK.Integers Methods toNum :: Num a => Proxy 'Neg7 -> a Source #
KnownTypeInt 'Neg8 Source # |
Instance details Defined in Numeric.NumType.DK.Integers Methods toNum :: Num a => Proxy 'Neg8 -> a Source #
KnownTypeInt 'Neg9 Source # |
Instance details Defined in Numeric.NumType.DK.Integers Methods toNum :: Num a => Proxy 'Neg9 -> a Source #
KnownTypeInt 'Pos1 Source # |
Instance details Defined in Numeric.NumType.DK.Integers Methods toNum :: Num a => Proxy 'Pos1 -> a Source #
KnownTypeInt 'Pos2 Source # |
Instance details Defined in Numeric.NumType.DK.Integers Methods toNum :: Num a => Proxy 'Pos2 -> a Source #
KnownTypeInt 'Pos3 Source # |
Instance details Defined in Numeric.NumType.DK.Integers Methods toNum :: Num a => Proxy 'Pos3 -> a Source #
KnownTypeInt 'Pos4 Source # |
Instance details Defined in Numeric.NumType.DK.Integers Methods toNum :: Num a => Proxy 'Pos4 -> a Source #
KnownTypeInt 'Pos5 Source # |
Instance details Defined in Numeric.NumType.DK.Integers Methods toNum :: Num a => Proxy 'Pos5 -> a Source #
KnownTypeInt 'Pos6 Source # |
Instance details Defined in Numeric.NumType.DK.Integers Methods toNum :: Num a => Proxy 'Pos6 -> a Source #
KnownTypeInt 'Pos7 Source # |
Instance details Defined in Numeric.NumType.DK.Integers Methods toNum :: Num a => Proxy 'Pos7 -> a Source #
KnownTypeInt 'Pos8 Source # |
Instance details Defined in Numeric.NumType.DK.Integers Methods toNum :: Num a => Proxy 'Pos8 -> a Source #
KnownTypeInt 'Pos9 Source # |
Instance details Defined in Numeric.NumType.DK.Integers Methods toNum :: Num a => Proxy 'Pos9 -> a Source #
KnownTypeInt 'Zero Source # |
Instance details Defined in Numeric.NumType.DK.Integers Methods toNum :: Num a => Proxy 'Zero -> a Source #
KnownTypeInt (Succ ('Neg10Minus n)) => KnownTypeInt ('Neg10Minus n) Source # |
Instance details Defined in Numeric.NumType.DK.Integers Methods toNum :: Num a => Proxy ('Neg10Minus n) -> a Source #
KnownTypeInt (Pred ('Pos10Plus n)) => KnownTypeInt ('Pos10Plus n) Source # |
Instance details Defined in Numeric.NumType.DK.Integers Methods toNum :: Num a => Proxy ('Pos10Plus n) -> a Source #