numtype-1.0: Type-level (low cardinality) integers.

PortabilityGHC only?
StabilityStable
Maintainerbjorn.buckwalter@gmail.com

Numeric.NumType

Description

Please refer to the literate Haskell code for documentation of both API and implementation.

Documentation

class NumTypeI n => NumType n Source

Instances

NumTypeI n => NumType n 

class PosTypeI n => PosType n Source

Instances

PosTypeI n => PosType n 

class NegTypeI n => NegType n Source

Instances

NegTypeI n => NegType n 

class NonZeroI n => NonZero n Source

Instances

NonZeroI n => NonZero n 

class (NumTypeI a, NumTypeI b) => Succ a b | a -> b, b -> aSource

Instances

Succ Zero (Pos Zero) 
Succ (Neg Zero) Zero 
NegTypeI a => Succ (Neg (Neg a)) (Neg a) 
PosTypeI a => Succ (Pos a) (Pos (Pos a)) 

class (NumTypeI a, NumTypeI b) => Negate a b | a -> b, b -> aSource

Instances

Negate Zero Zero 
(NegTypeI a, PosTypeI b, Negate a b) => Negate (Neg a) (Pos b) 
(PosTypeI a, NegTypeI b, Negate a b) => Negate (Pos a) (Neg b) 

class (Add a b c, Sub c b a) => Sum a b c | a b -> c, a c -> b, b c -> aSource

Instances

(Add a b c, Sub c b a) => Sum a b c 

class (NumTypeI a, NonZeroI b, NumTypeI c) => Div a b c | a b -> c, c b -> aSource

Instances

NonZeroI n => Div Zero n Zero 
(NegTypeI n, Negate n p', Div (Pos p') (Pos p) (Pos p''), Negate (Pos p'') (Neg n'')) => Div (Neg n) (Pos p) (Neg n'') 
(NegTypeI n, NegTypeI n', Negate n p, Negate n' p', Div (Pos p) (Pos p') (Pos p'')) => Div (Neg n) (Neg n') (Pos p'') 
(NegTypeI n, Negate n p', Div (Pos p) (Pos p') (Pos p''), Negate (Pos p'') (Neg n'')) => Div (Pos p) (Neg n) (Neg n'') 
(Sum n' (Pos n'') (Pos n), Div n'' (Pos n') n''', PosTypeI n''') => Div (Pos n) (Pos n') (Pos n''') 

class (NumTypeI a, NumTypeI b, NumTypeI c) => Mul a b c | a b -> cSource

Instances

NumTypeI n => Mul n Zero Zero 
(NegTypeI n, Div c (Neg n) a) => Mul a (Neg n) c 
(PosTypeI p, Div c (Pos p) a) => Mul a (Pos p) c 

toNum :: (NumTypeI n, Num a) => n -> aSource

incr :: Succ a b => a -> bSource

decr :: Succ a b => b -> aSource

negate :: Negate a b => a -> bSource

(+) :: Sum a b c => a -> b -> cSource

(-) :: Sum a b c => c -> b -> aSource

(*) :: Mul a b c => a -> b -> cSource

(/) :: Div a b c => a -> b -> cSource

data Zero Source

Instances

Show Zero 
NegTypeI Zero 
PosTypeI Zero 
NumTypeI Zero 
Negate Zero Zero 
NumTypeI n => Mul n Zero Zero 
NonZeroI n => Div Zero n Zero 
NumType a => Sub a Zero a 
NumTypeI a => Add Zero a a 
Succ Zero (Pos Zero) 
Succ (Neg Zero) Zero 

data Pos n Source

Instances

Succ Zero (Pos Zero) 
(PosTypeI p, Div c (Pos p) a) => Mul a (Pos p) c 
(Succ a' a, PosTypeI b, Sub a' b c) => Sub a (Pos b) c 
PosTypeI n => Show (Pos n) 
PosTypeI n => NonZeroI (Pos n) 
PosTypeI n => PosTypeI (Pos n) 
PosTypeI n => NumTypeI (Pos n) 
(PosTypeI a, Succ b c, Add a c d) => Add (Pos a) b d 
PosTypeI a => Succ (Pos a) (Pos (Pos a)) 
(NegTypeI a, PosTypeI b, Negate a b) => Negate (Neg a) (Pos b) 
(PosTypeI a, NegTypeI b, Negate a b) => Negate (Pos a) (Neg b) 
(NegTypeI n, Negate n p', Div (Pos p') (Pos p) (Pos p''), Negate (Pos p'') (Neg n'')) => Div (Neg n) (Pos p) (Neg n'') 
(NegTypeI n, NegTypeI n', Negate n p, Negate n' p', Div (Pos p) (Pos p') (Pos p'')) => Div (Neg n) (Neg n') (Pos p'') 
(NegTypeI n, Negate n p', Div (Pos p) (Pos p') (Pos p''), Negate (Pos p'') (Neg n'')) => Div (Pos p) (Neg n) (Neg n'') 
(Sum n' (Pos n'') (Pos n), Div n'' (Pos n') n''', PosTypeI n''') => Div (Pos n) (Pos n') (Pos n''') 

data Neg n Source

Instances

(NegTypeI n, Div c (Neg n) a) => Mul a (Neg n) c 
(Succ a a', NegTypeI b, Sub a' b c) => Sub a (Neg b) c 
NegTypeI n => Show (Neg n) 
NegTypeI n => NonZeroI (Neg n) 
NegTypeI n => NegTypeI (Neg n) 
NegTypeI n => NumTypeI (Neg n) 
Succ (Neg Zero) Zero 
(NegTypeI a, Succ c b, Add a c d) => Add (Neg a) b d 
NegTypeI a => Succ (Neg (Neg a)) (Neg a) 
(NegTypeI a, PosTypeI b, Negate a b) => Negate (Neg a) (Pos b) 
(PosTypeI a, NegTypeI b, Negate a b) => Negate (Pos a) (Neg b) 
(NegTypeI n, Negate n p', Div (Pos p') (Pos p) (Pos p''), Negate (Pos p'') (Neg n'')) => Div (Neg n) (Pos p) (Neg n'') 
(NegTypeI n, NegTypeI n', Negate n p, Negate n' p', Div (Pos p) (Pos p') (Pos p'')) => Div (Neg n) (Neg n') (Pos p'') 
(NegTypeI n, Negate n p', Div (Pos p) (Pos p') (Pos p''), Negate (Pos p'') (Neg n'')) => Div (Pos p) (Neg n) (Neg n'')