-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Type-level (low cardinality) integers, implemented
using type families.
--   
--   This package provides unary type level representations of the
--   (positive and negative) integers and basic operations (addition,
--   subtraction, multiplication, division) on these. Due to the unary
--   implementation the practical size of the NumTypes is severely limited
--   making them unsuitable for large-cardinality applications. If you will
--   be working with integers beyond (-20, 20) this package probably isn't
--   for you. The numtype-tf packade differs from the numtype package in
--   that the NumTypes are implemented using type families rather than
--   functional dependencies. Requires GHC 7.0 or later.
@package numtype-tf
@version 0.1


-- | This Module provides unary type-level representations, hereafter
--   referred to as <a>NumType</a>s, of the (positive and negative)
--   integers and basic operations (addition, subtraction, multiplication,
--   division) on these. While functions are provided for the operations
--   <a>NumType</a>s exist solely at the type level and their only value is
--   <a>undefined</a>.
--   
--   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 <a>NumType</a>s is limited by the type
--   checker stack. If the <a>NumType</a>s grow too large (which can happen
--   quickly with multiplication) an error message similar to the following
--   will be emitted:
--   
--   <pre>
--   Context reduction stack overflow; size = 20
--   Use -fcontext-stack=N to increase stack size to N
--   </pre>
--   
--   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.
module Numeric.NumType.TF

-- | Class encompassing all valid type level integers.
class NumTypeI n => NumType n

-- | Type level zero.
data Z

-- | Successor type for building type level natural numbers.
data S n

-- | Negation type, used to represent negative numbers by negating type
--   level naturals.
data N n

-- | Addition (<tt>a + b</tt>).

-- | Subtraction (<tt>a - b</tt>).

-- | Division (<tt>a / b</tt>).

-- | Multiplication (<tt>a * b</tt>).
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

-- | Convert a type level integer to an instance of <a>Num</a>.
toNum :: (NumTypeI n, Num a) => n -> a

-- | Increment a <a>NumType</a> by one.
incr :: NumType a => a -> Succ a

-- | Decrement a <a>NumType</a> by one.
decr :: NumType a => a -> Pred a

-- | Negate a <a>NumType</a>.
negate :: NumType a => a -> Negate a

-- | Add two <a>NumType</a>s.
(+) :: (NumType a, NumType b) => a -> b -> Add a b

-- | Subtract the second <a>NumType</a> from the first.
(-) :: (NumType a, NumType b) => a -> b -> Sub a b

-- | Multiply two <a>NumType</a>s.
(*) :: (NumType a, NumType b) => a -> b -> Mul a b

-- | Divide the first <a>NumType</a> by the second.
(/) :: (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
instance NumTypeI (N n) => Show (N n)
instance NumTypeI (S n) => Show (S n)
instance Show Z
instance NumTypeI (S n) => NumTypeI (N (S n))
instance NumTypeI (S n) => NumTypeI (S (S n))
instance NumTypeI (S Z)
instance NumTypeI Z
instance NumTypeI n => NumType n