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

Type-level Arithmetic

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

abs :: Proxy i -> Proxy (Abs 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

Conversion from Types to Terms