typenums-0.1.2.1: Type level numbers using existing Nat functionality

Safe HaskellSafe
LanguageHaskell2010

Data.TypeNums.Arithmetic.Internal

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

Documentation

type family AddK k1 k2 where ... Source #

The kind of the result of addition.

Since: typenums-0.1.2

type family SubK k1 k2 where ... Source #

The kind of the result of subtraction.

Since: typenums-0.1.2

type family MulK k1 k2 where ... Source #

The kind of the result of multiplication.

Since: typenums-0.1.2

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

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

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

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