This Module provides unary type-level representations, hereafter
referred to as
NumTypes, of the (positive and negative) integers
and basic operations (addition, subtraction, multiplication, division)
on these. While functions are provided for the operations
exist solely at the type level and their only value is
There are similarities with the HNats of the HList library, which was indeed a source of inspiration. Occasionally references are made to the HNats. The main addition in this module is negative numbers.
The practical size of the
NumTypes is limited by the type checker
stack. If the
NumTypes grow too large (which can happen quickly
with multiplication) an error message similar to the following will
Context reduction stack overflow; size = 20 Use -fcontext-stack=N to increase stack size to N
This situation could concievably be mitigated significantly by using e.g. a binary representation of integers rather than Peano numbers.
Please refer to the literate Haskell code for a narrative of the implementation.
- class NumTypeI n => NumType n
- data Z
- data S n
- data N n
- type family Add a b
- type family Sub a b
- type family Div a b
- type family Mul a b
- type Zero = Z
- type Pos1 = S Z
- type Pos2 = S Pos1
- type Pos3 = S Pos2
- type Pos4 = S Pos3
- type Pos5 = S Pos4
- type Neg1 = N Pos1
- type Neg2 = N Pos2
- type Neg3 = N Pos3
- type Neg4 = N Pos4
- type Neg5 = N Pos5
- toNum :: (NumTypeI n, Num a) => n -> a
- incr :: NumType a => a -> Succ a
- decr :: NumType a => a -> Pred a
- negate :: NumType a => a -> Negate a
- (+) :: (NumType a, NumType b) => a -> b -> Add a b
- (-) :: (NumType a, NumType b) => a -> b -> Sub a b
- (*) :: (NumType a, NumType b) => a -> b -> Mul a b
- (/) :: (NumType a, NumType b) => a -> b -> Div a b
- zero :: Z
- pos1 :: Pos1
- pos2 :: Pos2
- pos3 :: Pos3
- pos4 :: Pos4
- pos5 :: Pos5
- neg1 :: Neg1
- neg2 :: Neg2
- neg3 :: Neg3
- neg4 :: Neg4
- neg5 :: Neg5
Type level integers
Class encompassing all valid type level integers.
|NumTypeI n => NumType n|
These are exported to avoid lengthy qualified types in complier error messages.
Successor type for building type level natural numbers.
Negation type, used to represent negative numbers by negating type level naturals.
Type level arithmetics
Type synonyms for convenience
Value level functions
Using the above type families we define functions for various arithmetic operations. All functions are undefined and only operate on the type level. Their main contribution is that they facilitate NumType arithmetic without explicit (and tedious) type declarations.
Values for convenience
For use with the value level functions.