Portability	GHC only?
Stability	Stable
Maintainer	bjorn.buckwalter@gmail.com
Safe Haskell	Safe-Inferred

Numeric.NumType.TF

Contents

Type level integers
Data types
Type level arithmetics
Type synonyms for convenience
Value level functions
Values for convenience

Description

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.

Synopsis

Type level integers

class NumTypeI n => NumType n Source

Class encompassing all valid type level integers.

Instances

NumTypeI n => NumType n

Data types

These are exported to avoid lengthy qualified types in complier error messages.

data Z Source

Type level zero.

Instances

Show Z
Typeable Z

data S n Source

Successor type for building type level natural numbers.

Instances

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

data N n Source

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

Instances

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 = Z Source

type Pos1 = S Z Source

type Pos2 = S Pos1 Source

type Pos3 = S Pos2 Source

type Pos4 = S Pos3 Source

type Pos5 = S Pos4 Source

type Neg1 = N Pos1 Source

type Neg2 = N Pos2 Source

type Neg3 = N Pos3 Source

type Neg4 = N Pos4 Source

type Neg5 = N Pos5 Source

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.