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 _1 = Rat
AddK _1 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 _1 = Rat
SubK _1 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 _1 = Rat
MulK _1 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 _1 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 :: TInt) = 'Pos x
Abs ('Neg x :: TInt) = 'Pos x
Abs (x ':% y :: Rat) = 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 :: TInt) = 'Neg x
Negate ('Neg x :: TInt) = 'Pos x
Negate (x ':% y :: Rat) = 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 :: TInt) = 'Pos 1 ':% x
Recip ('Neg x :: TInt) = 'Neg 1 ':% x
Recip ('Pos x ':% y :: Rat) = 'Pos y ':% x
Recip ('Neg x ':% y :: Rat) = 'Neg y ':% x
Recip (x ':% y :: Rat) = '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 ':% y) = Quot ('Pos x) (GCD x y) ':% Quot y (GCD x y)
Simplify (x ':% 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 :: Rat) = TypeError ('Text "The denominator must not be 0") :: TInt
Truncate (x ':% y :: Rat) = 'Pos (Quot x y)
Truncate (x ':% y :: Rat) = 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 :: Rat) = TypeError ('Text "The denominator must not be 0") :: TInt
Floor (x ':% y :: Rat) = 'Pos (Div x y)
Floor (x ':% y :: Rat) = 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 :: Rat) = TypeError ('Text "The denominator must not be 0") :: TInt
Ceiling (x ':% y :: Rat) = 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 :: TInt) ('Pos y :: TInt) = 'Pos (x + y)
Add ('Neg x :: TInt) ('Pos y :: TInt) = If (x <=? y) ('Pos (y - x)) ('Neg (x - y))
Add ('Pos x :: TInt) ('Neg y :: TInt) = If (y <=? x) ('Pos (x - y)) ('Neg (y - x))
Add ('Neg x :: TInt) ('Neg y :: TInt) = 'Neg (x + y)
Add ('Pos x :: TInt) (y :: Nat) = 'Pos (x + y)
Add ('Neg x :: TInt) (y :: Nat) = If (x <=? y) ('Pos (y - x)) ('Neg (x - y))
Add (x :: Nat) ('Pos y :: TInt) = 'Pos (x + y)
Add (x :: Nat) ('Neg y :: TInt) = If (y <=? x) ('Pos (x - y)) ('Neg (y - x))
Add (x :: Rat) (y :: Rat) = Simplify (AddRat x y)
Add (x :: Rat) (y :: k) = Simplify (AddRat x (y ':% 1))
Add (x :: k) (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 :: TInt) ('Pos y :: TInt) = Add x ('Neg y)
Sub ('Neg x :: TInt) ('Pos y :: TInt) = Add ('Neg x) ('Neg y)
Sub ('Pos x :: TInt) ('Neg y :: TInt) = Add ('Pos x) ('Pos y)
Sub ('Neg x :: TInt) ('Neg y :: TInt) = Add ('Neg x) ('Pos y)
Sub ('Pos x :: TInt) (y :: Nat) = Add ('Pos x) ('Neg y)
Sub ('Neg x :: TInt) (y :: Nat) = Add ('Neg x) ('Neg y)
Sub (x :: Nat) ('Pos y :: TInt) = Add x ('Neg y)
Sub (x :: Nat) ('Neg y :: TInt) = Add x ('Pos y)
Sub (x :: Rat) (y :: Rat) = Simplify (SubRat x y)
Sub (x :: Rat) (y :: k) = Simplify (SubRat x (y ':% 1))
Sub (x :: k) (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 :: TInt) ('Pos y :: TInt) = 'Pos (x * y)
Mul ('Neg x :: TInt) ('Pos y :: TInt) = 'Neg (x * y)
Mul ('Pos x :: TInt) ('Neg y :: TInt) = 'Neg (x * y)
Mul ('Neg x :: TInt) ('Neg y :: TInt) = 'Pos (x * y)
Mul ('Pos x :: TInt) (y :: Nat) = 'Pos (x * y)
Mul ('Neg x :: TInt) (y :: Nat) = 'Neg (x * y)
Mul (x :: Nat) ('Pos y :: TInt) = 'Pos (x * y)
Mul (x :: Nat) ('Neg y :: TInt) = 'Neg (x * y)
Mul (x :: Rat) (y :: Rat) = Simplify (MulRat x y)
Mul (x :: Rat) (y :: k) = Simplify (MulRat x (y ':% 1))
Mul (x :: k) (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 :: TInt) = Simplify (x ':% y)
RatDiv (x :: Nat) ('Neg y :: TInt) = Simplify ('Neg x ':% y)
RatDiv (x :: TInt) ('Neg y :: TInt) = Simplify (Negate x ':% y)
RatDiv (x :: TInt) ('Pos y :: TInt) = Simplify (x ':% y)
RatDiv (x :: Rat) (y :: Rat) = Mul x (Recip y)
RatDiv (x :: k1) (y :: Rat) = Mul x (Recip y)
RatDiv (x :: Rat) (y :: k2) = 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 (_1 :: k) 0 = TypeError ('Text "Divisor must not be 0") :: (IntDivK k, IntDivK k)
DivMod (x :: Nat) y = UnPos (DivModAux ('Pos x) y ('Pos 0)) :: (Nat, Nat)
DivMod ('Pos x :: TInt) y = DivModAux ('Pos x) y ('Pos 0)
DivMod ('Neg x :: TInt) 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 :: TInt) y = QuotRemFixup (DivMod ('Neg x) y) y
QuotRem (x :: k) 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 :: k) 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 :: k) 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 :: k) 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 :: k) 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) :: Nat)
GCD (x :: TInt) (y :: Nat) = GCDAux (UnPos (Abs x) :: Nat) y
GCD (x :: TInt) (y :: TInt) = GCDAux (UnPos (Abs x) :: Nat) (UnPos (Abs y) :: Nat)

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)) :: Nat
LCM (x :: TInt) (y :: Nat) = UnPos (Mul (Div (Abs x) (GCD x y)) (Abs y)) :: Nat
LCM (x :: TInt) (y :: TInt) = UnPos (Mul (Div (Abs x) (GCD x y)) (Abs y)) :: Nat

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 :: TInt) (y :: Nat) = 'Pos (x ^ y)
Exp ('Neg x :: TInt) (y :: Nat) = ExpAux ('Pos 1) ('Neg x) y
Exp (x :: Rat) (y :: Nat) = Simplify (ExpAux (1 ':% 1) x y)
Exp (x :: Rat) ('Pos y :: TInt) = Simplify (ExpAux (1 ':% 1) x y)
Exp (x :: Rat) ('Neg y :: TInt) = Simplify (Recip (ExpAux (1 ':% 1) x y))
Exp (x :: k) ('Pos y :: TInt) = Simplify (ExpAux (1 ':% 1) (x ':% 1) y)
Exp (x :: k) ('Neg y :: TInt) = 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 (_1 :: k) = TypeError ('Text "Invalid IntLog base: 0") :: TInt
IntLog 1 (_1 :: k) = TypeError ('Text "Invalid IntLog base: 1") :: TInt
IntLog _1 0 = TypeError ('Text "IntLog n 0 is infinite") :: TInt
IntLog _1 ('Pos 0) = TypeError ('Text "IntLog n 0 is infinite") :: TInt
IntLog _1 ('Neg 0) = TypeError ('Text "IntLog n 0 is infinite") :: TInt
IntLog _1 (0 ':% _2 :: Rat) = TypeError ('Text "IntLog n 0 is infinite") :: TInt
IntLog _1 (_2 ':% 0 :: Rat) = TypeError ('Text "IntLog parameter has zero denominator") :: TInt
IntLog _1 ('Neg _2 :: TInt) = TypeError ('Text "IntLog of a negative does not exist") :: TInt
IntLog n (x :: Nat) = IntLog n ('Pos x)
IntLog n ('Pos x :: TInt) = 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))