Data.TypeNums.Arithmetic.Internal

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

Documentation

type family AddK k1 k2 where ...

The kind of the result of addition.

Since: typenums-0.1.2

Equations

AddK Nat Nat = Nat

AddK Nat Rat = Rat

AddK Nat TInt = TInt

AddK Rat Nat = Rat

AddK Rat Rat = Rat

AddK Rat TInt = Rat

AddK TInt Nat = TInt

AddK TInt Rat = Rat

AddK TInt TInt = TInt

type family SubK k1 k2 where ...

The kind of the result of subtraction.

Since: typenums-0.1.2

Equations

SubK Nat Nat = Nat

SubK Nat Rat = Rat

SubK Nat TInt = TInt

SubK Rat Nat = Rat

SubK Rat Rat = Rat

SubK Rat TInt = Rat

SubK TInt Nat = TInt

SubK TInt Rat = Rat

SubK TInt TInt = TInt

type family MulK k1 k2 where ...

The kind of the result of multiplication.

Since: typenums-0.1.2

Equations

MulK Nat Nat = Nat

MulK Nat Rat = Rat

MulK Nat TInt = TInt

MulK Rat Nat = Rat

MulK Rat Rat = Rat

MulK Rat TInt = Rat

MulK TInt Nat = TInt

MulK TInt Rat = Rat

MulK TInt TInt = TInt

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

The sum of two type-level numbers.

Since: typenums-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 (n1 :% d1) (n2 :% d2) = Add (Mul n1 d2) (Mul n2 d1) :% Mul d1 d2

Add (n :% d) (y :: Nat) = Add n (Mul d y) :% d

Add (n :% d) (Pos y) = Add n (Mul d y) :% d

Add (n :% d) (Neg y) = Add n (Mul d (Neg y)) :% d

Add (x :: Nat) (n :% d) = Add (Mul d x) n :% d

Add (Pos x) (n :% d) = Add (Mul d x) n :% d

Add (Neg x) (n :% d) = Add (Mul d (Neg x)) n :% d

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

The difference of two type-level numbers

Since: typenums-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 (n1 :% d1) (n2 :% d2) = Sub (Mul n1 (Pos d2)) (Mul n2 (Pos d1)) :% Mul d1 d2

Sub (n :% d) (y :: Nat) = Sub (n :% d) (y :% 1)

Sub (n :% d) (Pos y) = Sub (n :% d) (Pos y :% 1)

Sub (n :% d) (Neg y) = Sub (n :% d) (Neg y :% 1)

Sub (x :: Nat) (n :% d) = Sub (x :% 1) (n :% d)

Sub (Pos x) (n :% d) = Sub (Pos x :% 1) (n :% d)

Sub (Neg x) (n :% d) = Sub (Neg x :% 1) (n :% d)

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

The product of two type-level numbers

Since: typenums-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 (n1 :% d1) (n2 :% d2) = Mul n1 n2 :% Mul d1 d2

Mul (n :% d) (y :: Nat) = Mul n y :% d

Mul (n :% d) (Pos y) = Mul n (Pos y) :% d

Mul (n :% d) (Neg y) = Mul n (Neg y) :% d

Mul (x :: Nat) (n :% d) = Mul x n :% d

Mul (Pos x) (n :% d) = Mul (Pos x) n :% d

Mul (Neg x) (n :% d) = Mul (Neg x) n :% d