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	Cpp UndecidableInstances MonoLocalBinds TypeFamilies DataKinds DeriveDataTypeable AutoDeriveTypeable TypeSynonymInstances 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

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

Conversion to a Num.

Minimal complete definition

toNum

Methods

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

Instances

KnownTypeInt Neg9 Source #
Methods toNum :: Num a => Proxy TypeInt Neg9 -> a Source #
KnownTypeInt Neg8 Source #
Methods toNum :: Num a => Proxy TypeInt Neg8 -> a Source #
KnownTypeInt Neg7 Source #
Methods toNum :: Num a => Proxy TypeInt Neg7 -> a Source #
KnownTypeInt Neg6 Source #
Methods toNum :: Num a => Proxy TypeInt Neg6 -> a Source #
KnownTypeInt Neg5 Source #
Methods toNum :: Num a => Proxy TypeInt Neg5 -> a Source #
KnownTypeInt Neg4 Source #
Methods toNum :: Num a => Proxy TypeInt Neg4 -> a Source #
KnownTypeInt Neg3 Source #
Methods toNum :: Num a => Proxy TypeInt Neg3 -> a Source #
KnownTypeInt Neg2 Source #
Methods toNum :: Num a => Proxy TypeInt Neg2 -> a Source #
KnownTypeInt Neg1 Source #
Methods toNum :: Num a => Proxy TypeInt Neg1 -> a Source #
KnownTypeInt Zero Source #
Methods toNum :: Num a => Proxy TypeInt Zero -> a Source #
KnownTypeInt Pos1 Source #
Methods toNum :: Num a => Proxy TypeInt Pos1 -> a Source #
KnownTypeInt Pos2 Source #
Methods toNum :: Num a => Proxy TypeInt Pos2 -> a Source #
KnownTypeInt Pos3 Source #
Methods toNum :: Num a => Proxy TypeInt Pos3 -> a Source #
KnownTypeInt Pos4 Source #
Methods toNum :: Num a => Proxy TypeInt Pos4 -> a Source #
KnownTypeInt Pos5 Source #
Methods toNum :: Num a => Proxy TypeInt Pos5 -> a Source #
KnownTypeInt Pos6 Source #
Methods toNum :: Num a => Proxy TypeInt Pos6 -> a Source #
KnownTypeInt Pos7 Source #
Methods toNum :: Num a => Proxy TypeInt Pos7 -> a Source #
KnownTypeInt Pos8 Source #
Methods toNum :: Num a => Proxy TypeInt Pos8 -> a Source #
KnownTypeInt Pos9 Source #
Methods toNum :: Num a => Proxy TypeInt Pos9 -> a Source #
KnownTypeInt (Succ (Neg10Minus n)) => KnownTypeInt (Neg10Minus n) Source #
Methods toNum :: Num a => Proxy TypeInt (Neg10Minus n) -> a Source #
KnownTypeInt (Pred (Pos10Plus n)) => KnownTypeInt (Pos10Plus n) Source #
Methods toNum :: Num a => Proxy TypeInt (Pos10Plus n) -> a Source #