numtype-dk-0.5.0.3: Type-level integers, using TypeNats, Data Kinds, and Closed Type Families.
CopyrightCopyright (C) 2006-2015 Bjorn Buckwalter
LicenseBSD3
Maintainerbjorn.buckwalter@gmail.com
StabilityStable
PortabilityGHC only
Safe HaskellSafe-Inferred
LanguageHaskell98
Extensions
  • Cpp
  • UndecidableInstances
  • MonoLocalBinds
  • TypeFamilies
  • DataKinds
  • DeriveDataTypeable
  • AutoDeriveTypeable
  • TypeSynonymInstances
  • FlexibleContexts
  • FlexibleInstances
  • KindSignatures
  • TypeOperators
  • ExplicitNamespaces

Numeric.NumType.DK.Integers

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

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 :: Proxy i -> Proxy (Pred i) Source #

succ :: Proxy i -> Proxy (Succ i) Source #

negate :: Proxy i -> Proxy (Negate i) Source #

abs :: Proxy i -> Proxy (Abs i) Source #

signum :: Proxy i -> Proxy (Signum i) Source #

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

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

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

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

(^) :: 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 #