Data.TypeNums.Arithmetic.Internal

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

Kind Results

type family AddK k1 k2 where ...

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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