Portability | GHC only? |
---|---|

Stability | Stable |

Maintainer | bjorn.buckwalter@gmail.com |

This Module provides unary type-level representations, hereafter
referred to as `NumType`

s, of the (positive and negative) integers
and basic operations (addition, subtraction, multiplication, division)
on these. While functions are provided for the operations `NumType`

s
exist solely at the type level and their only value is `undefined`

.

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 `NumType`

s is limited by the type checker
stack. If the `NumType`

s grow too large (which can happen quickly
with multiplication) an error message similar to the following will
be emitted:

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 NumTypeI n => NumType n Source

Class encompassing all valid type level integers.

NumTypeI n => NumType n |

# Data types

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.