numtype-tf-0.1.1: Type-level (low cardinality) integers, implemented using type families.

PortabilityGHC only?
Safe HaskellSafe-Inferred




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


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.

data Z Source

Type level zero.


data S n Source

Successor type for building type level natural numbers.


Typeable1 S 
NumTypeI (S n) => Show (S n) 

data N n Source

Negation type, used to represent negative numbers by negating type level naturals.


Typeable1 N 
NumTypeI (N n) => Show (N n) 

Type level arithmetics

type family Add a b Source

Addition (a + b).

type family Sub a b Source

Subtraction (a - b).

type family Div a b Source

Division (a / b).

type family Mul a b Source

Multiplication (a * b).

Type synonyms for convenience

type Zero = ZSource

type Pos1 = S ZSource

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.

toNum :: (NumTypeI n, Num a) => n -> aSource

Convert a type level integer to an instance of Num.

incr :: NumType a => a -> Succ aSource

Increment a NumType by one.

decr :: NumType a => a -> Pred aSource

Decrement a NumType by one.

negate :: NumType a => a -> Negate aSource

Negate a NumType.

(+) :: (NumType a, NumType b) => a -> b -> Add a bSource

Add two NumTypes.

(-) :: (NumType a, NumType b) => a -> b -> Sub a bSource

Subtract the second NumType from the first.

(*) :: (NumType a, NumType b) => a -> b -> Mul a bSource

Multiply two NumTypes.

(/) :: (NumType a, NumType b) => a -> b -> Div a bSource

Divide the first NumType by the second.

Values for convenience

For use with the value level functions.