numtype-dk-0.5.0.1: 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
LanguageHaskell98
Extensions
  • Cpp
  • UndecidableInstances
  • MonoLocalBinds
  • TypeFamilies
  • DataKinds
  • DeriveDataTypeable
  • AutoDeriveTypeable
  • TypeSynonymInstances
  • FlexibleInstances
  • KindSignatures
  • TypeOperators
  • ExplicitNamespaces

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.

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 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 Abs i :: TypeInt 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 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 + 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 6 Source

TypeInt subtraction.

Equations

i - i' = i + Negate 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

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

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 where Source

Conversion to a Num.

Methods

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

Instances