Safe Haskell	Safe
Language	Haskell2010

Data.TypeNums.Arithmetic.Internal

Contents

Kind Results
Unary operations
- Rounding operations
Binary operations

Description

This module exposes the inner workings of type-level arithmetic for further extensions.

Synopsis

type family AddK k1 k2 where ...
type family SubK k1 k2 where ...
type family MulK k1 k2 where ...
type family IntDivK k where ...
type family ExpK k1 k2 where ...
type family NegK k where ...
type family Abs (x :: k) :: k where ...
type family Negate (x :: k) :: NegK k where ...
type family Recip (x :: k) :: Rat where ...
type family Simplify (x :: Rat) :: Rat where ...
type family Truncate (x :: k) :: TInt where ...
type family Floor (x :: k) :: TInt where ...
type family Ceiling (x :: k) :: TInt where ...
type family Add (x :: k1) (y :: k2) :: AddK k1 k2 where ...
type family Sub (x :: k1) (y :: k2) :: SubK k1 k2 where ...
type family Mul (x :: k1) (y :: k2) :: MulK k1 k2 where ...
type family RatDiv (x :: k1) (y :: k2) :: Rat where ...
type family DivMod (x :: k) (y :: Nat) :: (IntDivK k, IntDivK k) where ...
type family QuotRem (x :: k) (y :: Nat) :: (IntDivK k, IntDivK k) where ...
type family Div (x :: k) (y :: Nat) :: IntDivK k where ...
type family Mod (x :: k) (y :: Nat) :: IntDivK k where ...
type family Quot (x :: k) (y :: Nat) :: IntDivK k where ...
type family Rem (x :: k) (y :: Nat) :: IntDivK k where ...
type family GCD (x :: k1) (y :: k2) :: Nat where ...
type family LCM (x :: k1) (y :: k2) :: Nat where ...
type family Exp (x :: k1) (y :: k2) :: ExpK k1 k2 where ...
type family IntLog (n :: Nat) (x :: k) :: TInt where ...

Kind Results

type family AddK k1 k2 where ... Source #

The kind of the result of addition.

Since: 0.1.2

Equations

AddK Rat _ = Rat
AddK _ Rat = Rat
AddK Nat Nat = Nat
AddK Nat TInt = TInt
AddK TInt Nat = TInt
AddK TInt TInt = TInt

type family SubK k1 k2 where ... Source #

The kind of the result of subtraction.

Since: 0.1.2

Equations

SubK Rat _ = Rat
SubK _ Rat = Rat
SubK Nat Nat = Nat
SubK Nat TInt = TInt
SubK TInt Nat = TInt
SubK TInt TInt = TInt

type family MulK k1 k2 where ... Source #

The kind of the result of multiplication.

Since: 0.1.2

Equations

MulK k k = k
MulK Rat _ = Rat
MulK _ Rat = Rat
MulK Nat TInt = TInt
MulK TInt Nat = TInt

type family IntDivK k where ... Source #

The kind of the result of division by a natural number

Since: 0.1.4

Equations

IntDivK Nat = Nat
IntDivK TInt = TInt

type family ExpK k1 k2 where ... Source #

The kind of the result of type-level exponentiation

Equations

ExpK Nat Nat = Nat
ExpK TInt Nat = TInt
ExpK Rat Nat = Rat
ExpK _ TInt = Rat

type family NegK k where ... Source #

The kind of the result of negation

Since: 0.1.4

Equations

NegK Nat = TInt
NegK TInt = TInt
NegK Rat = Rat

Unary operations

type family Abs (x :: k) :: k where ... Source #

The absolute value of a type-level number

Since: 0.1.4

Equations

Abs (x :: Nat) = x
Abs ('Pos x) = 'Pos x
Abs ('Neg x) = 'Pos x
Abs (x :% y) = Simplify (Abs x :% y)

type family Negate (x :: k) :: NegK k where ... Source #

The result of negating a TInt

Since: 0.1.4

Equations

Negate (x :: Nat) = Negate ('Pos x)
Negate ('Pos 0) = 'Pos 0
Negate ('Neg 0) = 'Pos 0
Negate ('Pos x) = 'Neg x
Negate ('Neg x) = 'Pos x
Negate (x :% y) = Negate x :% y

type family Recip (x :: k) :: Rat where ... Source #

The reciprocal of a type-level number

Since: 0.1.4

Equations

Recip (x :: Nat) = 'Pos 1 :% x
Recip ('Pos x) = 'Pos 1 :% x
Recip ('Neg x) = 'Neg 1 :% x
Recip ('Pos x :% y) = 'Pos y :% x
Recip ('Neg x :% y) = 'Neg y :% x
Recip ((x :: Nat) :% y) = 'Pos y :% x

type family Simplify (x :: Rat) :: Rat where ... Source #

Reduce a type-level rational into its canonical form

Since: 0.1.4

Equations

Simplify ((x :: Nat) :% y) = Quot ('Pos x) (GCD x y) :% Quot y (GCD x y)
Simplify ((x :: TInt) :% y) = Quot x (GCD x y) :% Quot y (GCD x y)

Rounding operations

type family Truncate (x :: k) :: TInt where ... Source #

Round a type-level number towards zero

Since: 0.1.4

Equations

Truncate (x :: Nat) = 'Pos x
Truncate (x :: TInt) = x
Truncate (x :% 0) = TypeError ('Text "The denominator must not be 0")
Truncate ((x :: Nat) :% y) = 'Pos (Quot x y)
Truncate ((x :: TInt) :% y) = Quot x y

type family Floor (x :: k) :: TInt where ... Source #

Round a type-level number towards negative infinity

Since: 0.1.4

Equations

Floor (x :: Nat) = 'Pos x
Floor (x :: TInt) = x
Floor (x :% 0) = TypeError ('Text "The denominator must not be 0")
Floor ((x :: Nat) :% y) = 'Pos (Div x y)
Floor ((x :: TInt) :% y) = Div x y

type family Ceiling (x :: k) :: TInt where ... Source #

Round a type-level number towards positive infinity

Since: 0.1.4

Equations

Ceiling (x :: Nat) = 'Pos x
Ceiling (x :: TInt) = x
Ceiling (x :% 0) = TypeError ('Text "The denominator must not be 0")
Ceiling (x :% y) = Add 1 (Floor (Sub x 1 :% y))

Binary operations

type family Add (x :: k1) (y :: k2) :: AddK k1 k2 where ... Source #

The sum of two type-level numbers.

Since: 0.1.2

Equations

Add (x :: Nat) (y :: Nat) = x + y
Add ('Pos x) ('Pos y) = 'Pos (x + y)
Add ('Neg x) ('Pos y) = If (x <=? y) ('Pos (y - x)) ('Neg (x - y))
Add ('Pos x) ('Neg y) = If (y <=? x) ('Pos (x - y)) ('Neg (y - x))
Add ('Neg x) ('Neg y) = 'Neg (x + y)
Add ('Pos x) (y :: Nat) = 'Pos (x + y)
Add ('Neg x) (y :: Nat) = If (x <=? y) ('Pos (y - x)) ('Neg (x - y))
Add (x :: Nat) ('Pos y) = 'Pos (x + y)
Add (x :: Nat) ('Neg y) = If (y <=? x) ('Pos (x - y)) ('Neg (y - x))
Add (x :: Rat) (y :: Rat) = Simplify (AddRat x y)
Add (x :: Rat) y = Simplify (AddRat x (y :% 1))
Add x (y :: Rat) = Simplify (AddRat (x :% 1) y)

type family Sub (x :: k1) (y :: k2) :: SubK k1 k2 where ... Source #

The difference of two type-level numbers

For the difference of two naturals a and b, a-b is also a natural, so only exists for a >= b. @since 0.1.2

Equations

Sub (x :: Nat) (y :: Nat) = x - y
Sub ('Pos x) ('Pos y) = Add x ('Neg y)
Sub ('Neg x) ('Pos y) = Add ('Neg x) ('Neg y)
Sub ('Pos x) ('Neg y) = Add ('Pos x) ('Pos y)
Sub ('Neg x) ('Neg y) = Add ('Neg x) ('Pos y)
Sub ('Pos x) (y :: Nat) = Add ('Pos x) ('Neg y)
Sub ('Neg x) (y :: Nat) = Add ('Neg x) ('Neg y)
Sub (x :: Nat) ('Pos y) = Add x ('Neg y)
Sub (x :: Nat) ('Neg y) = Add x ('Pos y)
Sub (x :: Rat) (y :: Rat) = Simplify (SubRat x y)
Sub (x :: Rat) y = Simplify (SubRat x (y :% 1))
Sub x (y :: Rat) = Simplify (SubRat (x :% 1) y)

type family Mul (x :: k1) (y :: k2) :: MulK k1 k2 where ... Source #

The product of two type-level numbers

Since: 0.1.2

Equations

Mul (x :: Nat) (y :: Nat) = x * y
Mul ('Pos x) ('Pos y) = 'Pos (x * y)
Mul ('Neg x) ('Pos y) = 'Neg (x * y)
Mul ('Pos x) ('Neg y) = 'Neg (x * y)
Mul ('Neg x) ('Neg y) = 'Pos (x * y)
Mul ('Pos x) (y :: Nat) = 'Pos (x * y)
Mul ('Neg x) (y :: Nat) = 'Neg (x * y)
Mul (x :: Nat) ('Pos y) = 'Pos (x * y)
Mul (x :: Nat) ('Neg y) = 'Neg (x * y)
Mul (x :: Rat) (y :: Rat) = Simplify (MulRat x y)
Mul (x :: Rat) y = Simplify (MulRat x (y :% 1))
Mul x (y :: Rat) = Simplify (MulRat (x :% 1) y)

type family RatDiv (x :: k1) (y :: k2) :: Rat where ... Source #

The result of dividing two type-level numbers.

Since: 0.1.4

Equations

RatDiv (x :: Nat) (y :: Nat) = Simplify (x :% y)
RatDiv (x :: TInt) (y :: Nat) = Simplify (x :% y)
RatDiv (x :: Nat) ('Pos y) = Simplify (x :% y)
RatDiv (x :: Nat) ('Neg y) = Simplify ('Neg x :% y)
RatDiv (x :: TInt) ('Neg y) = Simplify (Negate x :% y)
RatDiv (x :: TInt) ('Pos y) = Simplify (x :% y)
RatDiv (x :: Rat) (y :: Rat) = Mul x (Recip y)
RatDiv x (y :: Rat) = Mul x (Recip y)
RatDiv (x :: Rat) y = Mul x (RatDiv 1 y)

type family DivMod (x :: k) (y :: Nat) :: (IntDivK k, IntDivK k) where ... Source #

The quotient and remainder of a type-level integer and a natural number. For a negative dividend, the remainder part is positive such that x = q*y + r @since 0.1.4

Equations

DivMod _ 0 = TypeError ('Text "Divisor must not be 0")
DivMod (x :: Nat) y = UnPos (DivModAux ('Pos x) y ('Pos 0))
DivMod ('Pos x) y = DivModAux ('Pos x) y ('Pos 0)
DivMod ('Neg x) y = DivModNegFixup (DivModAux ('Pos x) y ('Pos 0)) y

type family QuotRem (x :: k) (y :: Nat) :: (IntDivK k, IntDivK k) where ... Source #

The quotient and remainder of a type-level integer and a natural number. For a negative dividend, the remainder part is negative such that x = q*y + r @since 0.1.4

Equations

QuotRem ('Neg x) y = QuotRemFixup (DivMod ('Neg x) y) y
QuotRem x y = DivMod x y

type family Div (x :: k) (y :: Nat) :: IntDivK k where ... infixl 7 Source #

The quotient of a type-level integer and a natural number.

Since: 0.1.4

Equations

Div x y = Fst (DivMod x y)

type family Mod (x :: k) (y :: Nat) :: IntDivK k where ... infixl 7 Source #

The remainder of a type-level integer and a natural number For a negative number, behaves similarly to mod. @since 0.1.4

Equations

Mod x y = Snd (DivMod x y)

type family Quot (x :: k) (y :: Nat) :: IntDivK k where ... infixl 7 Source #

The integer part of the result of dividing an integer by a natural number

Since: 0.1.4

Equations

Quot x y = Fst (QuotRem x y)

type family Rem (x :: k) (y :: Nat) :: IntDivK k where ... infixl 7 Source #

The remainder of the result of dividing an integer by a natural number

Since: 0.1.4

Equations

Rem x y = Snd (QuotRem x y)

type family GCD (x :: k1) (y :: k2) :: Nat where ... Source #

The greatest common divisor of two type-level integers

Since: 0.1.4

Equations

GCD (x :: Nat) (y :: Nat) = GCDAux x y
GCD (x :: Nat) (y :: TInt) = GCDAux x (UnPos (Abs y))
GCD (x :: TInt) (y :: Nat) = GCDAux (UnPos (Abs x)) y
GCD (x :: TInt) (y :: TInt) = GCDAux (UnPos (Abs x)) (UnPos (Abs y))

type family LCM (x :: k1) (y :: k2) :: Nat where ... Source #

The least common multiple of two type-level integers

Since: 0.1.4

Equations

LCM (x :: Nat) (y :: Nat) = Mul (Div (Abs x) (GCD x y)) (Abs y)
LCM (x :: Nat) (y :: TInt) = UnPos (Mul (Div (Abs x) (GCD x y)) (Abs y))
LCM (x :: TInt) (y :: Nat) = UnPos (Mul (Div (Abs x) (GCD x y)) (Abs y))
LCM (x :: TInt) (y :: TInt) = UnPos (Mul (Div (Abs x) (GCD x y)) (Abs y))

type family Exp (x :: k1) (y :: k2) :: ExpK k1 k2 where ... Source #

Exponentiation of a type-level number by an integer

Since: 0.1.4

Equations

Exp (x :: Nat) (y :: Nat) = x ^ y
Exp ('Pos x) (y :: Nat) = 'Pos (x ^ y)
Exp ('Neg x) (y :: Nat) = ExpAux ('Pos 1) ('Neg x) y
Exp (x :: Rat) (y :: Nat) = Simplify (ExpAux (1 :% 1) x y)
Exp (x :: Rat) ('Pos y) = Simplify (ExpAux (1 :% 1) x y)
Exp (x :: Rat) ('Neg y) = Simplify (Recip (ExpAux (1 :% 1) x y))
Exp x ('Pos y) = Simplify (ExpAux (1 :% 1) (x :% 1) y)
Exp x ('Neg y) = Simplify (Recip (ExpAux (1 :% 1) (x :% 1) y))

type family IntLog (n :: Nat) (x :: k) :: TInt where ... Source #

The floor of the logarithm of a type-level number NB. unlike Log2, Log n 0 here is a type error.

Since: 0.1.4

Equations

IntLog 0 _ = TypeError ('Text "Invalid IntLog base: 0")
IntLog 1 _ = TypeError ('Text "Invalid IntLog base: 1")
IntLog _ 0 = TypeError ('Text "IntLog n 0 is infinite")
IntLog _ ('Pos 0) = TypeError ('Text "IntLog n 0 is infinite")
IntLog _ ('Neg 0) = TypeError ('Text "IntLog n 0 is infinite")
IntLog _ (0 :% _) = TypeError ('Text "IntLog n 0 is infinite")
IntLog _ (_ :% 0) = TypeError ('Text "IntLog parameter has zero denominator")
IntLog _ ('Neg _) = TypeError ('Text "IntLog of a negative does not exist")
IntLog n (x :: Nat) = IntLog n ('Pos x)
IntLog n ('Pos x) = IntLogAux n ('Pos x)
IntLog n (x :: Rat) = If (Floor x == 'Pos 0) (NegLogFudge n x (Negate (IntLogAux n (Floor (Recip x))))) (IntLog n (Floor x))