Numeric.NumType.TF -- Type-level (low cardinality) integers
Bjorn Buckwalter, bjorn.buckwalter@gmail.com
License: BSD3


= Preliminaries =

This module requires GHC 7.0 or later.

> {-# LANGUAGE UndecidableInstances
>            , TypeFamilies
>            , EmptyDataDecls
>            , FlexibleInstances
>            , ScopedTypeVariables
>            , DeriveDataTypeable
> #-}


= Summary =

> {- |
>    Copyright  : Copyright (C) 2006-2012 Bjorn Buckwalter
>    License    : BSD3
>
>    Maintainer : bjorn.buckwalter@gmail.com
>    Stability  : Stable
>    Portability: GHC only?
>
> 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.
>
> -}

> module Numeric.NumType.TF (
>   -- * Type level integers
>     NumType
>   -- * Data types
>   -- | These are exported to avoid lengthy qualified types in complier
>   -- error messages.
>   , Z, S, N
>   -- * Type level arithmetics
>   , Pred, Succ, Negate, Add, Sub, Div, Mul
>   -- * Type synonyms for convenience
>   , Zero, Pos1, Pos2, Pos3, Pos4, Pos5, Neg1, Neg2, Neg3, Neg4, Neg5
>   -- * Value level functions
>   -- $functions
>   , toNum, incr, decr, negate, (+), (-), (*), (/)
>   -- * Values for convenience
>   -- | For use with the value level functions.
>   , zero, pos1, pos2, pos3, pos4, pos5, neg1, neg2, neg3, neg4, neg5
>   ) where

> import Prelude hiding ((*), (/), (+), (-), negate)
> import qualified Prelude ((+), negate)
> import Data.Typeable (Typeable)

Use the same fixity for operators as the Prelude.

> infixl 7  *, /
> infixl 6  +, -


= NumTypes =

We start by defining a class encompassing all integers with the
class function 'toNum' that converts from the type-level to a
value-level 'Num'.

> class NumTypeI n where
>   -- | Negation.
>   type Negate n
>   -- | Predecessor.
>   type Pred n
>   -- | Successor.
>   type Succ n
>   -- | Convert a type level integer to an instance of 'Prelude.Num'.
>   toNum :: Num a => n -> a


Now we use a trick from Oleg Kiselyov and Chung-chieh Shan [2]:

    -- The well-formedness condition, the kind predicate
    class Nat0 a where toInt :: a -> Int
    class Nat0 a => Nat a           -- (positive) naturals

    -- To prevent the user from adding new instances to Nat0 and especially
    -- to Nat (e.g., to prevent the user from adding the instance |Nat B0|)
    -- we do NOT export Nat0 and Nat. Rather, we export the following proxies.
    -- The proxies entail Nat and Nat0 and so can be used to add Nat and Nat0
    -- constraints in the signatures. However, all the constraints below
    -- are expressed in terms of Nat0 and Nat rather than proxies. Thus,
    -- even if the user adds new instances to proxies, it would not matter.
    -- Besides, because the following proxy instances are most general,
    -- one may not add further instances without overlapping instance extension.
    class    Nat0 n => Nat0E n
    instance Nat0 n => Nat0E n
    class    Nat n => NatE n
    instance Nat n => NatE n

We apply this trick to our NumTypeI class. In our case we will elect to
append an "I" to the internal (non-exported) classes rather than
appending an "E" to the exported classes.

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

Now we Define the data types used to represent integers. We begin
with 'Zero', which we allow to be used as both a positive and a
negative number in the sense of the previously defined type classes.
'Z' corresponds to HList's 'HZero'.

> -- | Type level zero.
> data Z deriving Typeable

Next we define the "successor" type, here called 'S' (corresponding
to HList's 'HSucc').

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

Finally we define the "negation" type used to represent negative
numbers.

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

The 'NumTypeI' instances restrict how 'Z', 'S', and 'N' may be combined
to assemble 'NumType's, and the type synonym declarations demonstrate
some basic arithmetic.

> instance NumTypeI Z where  -- Zero.
>   type Negate Z = Z       -- Still zero.
>   type Pred Z = N (S Z)   -- Negative one.
>   type Succ Z = S Z       -- One.
>   toNum _ = 0

> instance NumTypeI (S Z) where   -- One.
>   type Negate (S Z) = N (S Z)  -- Minus one.
>   type Pred (S Z) = Z          -- Zero.
>   type Succ (S Z) = S (S Z)    -- Two.
>   toNum _ = 1

> -- Naturals greater than one.
> instance NumTypeI (S n) => NumTypeI (S (S n)) where  -- N.
>   type Negate (S (S n)) = N (S (S n))              -- -N.
>   type Pred (S (S n)) = S n                        -- N-1
>   type Succ (S (S n)) = S (S (S n))                -- N+1
>   toNum _ = 1 Prelude.+ toNum (undefined :: S n)

> -- Negatives (minus one and below).
> instance NumTypeI (S n) => NumTypeI (N (S n)) where  -- -N
>   type Negate (N (S n)) = S n                      -- N
>   type Pred (N (S n)) = N (S (S n))                -- -(N+1)
>   type Succ (N (S n)) = Negate n                   -- -(N-1)
>        -- NOTE: `N n` would be invalid for `Succ (N (S Z))`
>   toNum _ = Prelude.negate $ toNum (undefined :: S n)


= Show instances =

For convenience we create show instances for the defined NumTypes.

> instance Show Z where show = ("NumType " ++) . show . toNum
> instance NumTypeI (S n) => Show (S n) where show = ("NumType " ++) . show . toNum
> instance NumTypeI (N n) => Show (N n) where show = ("NumType " ++) . show . toNum


= Addition and subtraction =

Now let us move on towards more complex arithmetic operations. We
define type families for addition and subtraction of NumTypes.

> -- | Addition (@a + b@).
> type family Add a b  -- a + b.
> -- | Subtraction (@a - b@).
> type family Sub a b  -- a - b.

Adding anything to Zero gives "anything".

> type instance Add Z n = n
> --type instance Add n Z = n  -- Not accepted by GHC 7.8.

When adding to a non-Zero number our strategy is to "transfer" type
constructors from the first type to the second type until the first
type is Zero.

> type instance Add (S n) n' = Add n (Succ n')
> type instance Add (N n) n' = Add (Succ (N n)) (Pred n')

Subtraction is defined trivially with addition and negation.

> type instance Sub a b = Add a (Negate b)


= Multiplication =

Type family for multiplication. Multiplication is limited by the
type checker stack. If the result of multiplication is too large
this error message will be emitted:

    Context reduction stack overflow; size = 20
    Use -fcontext-stack=N to increase stack size to N

> -- | Multiplication (@a * b@).
> type family Mul a b        -- a * b.
> type instance Mul Z n = Z  -- Trivially.

Multiplication is performed by recursive addition of one number
to itself. The recursion is terminated by the `Mul Z n` instance.

> type instance Mul (S n) n' = Add n' (Mul n n')  -- a*b = b+(a-1)*b
> type instance Mul (N n) n' = Negate (Mul n n')  -- (-a)*b = -(a*b)


= Division =

Division is more complicated than multiplication. We start by
defining division only for positive (natural) numbers. This is
necessary to ensure bad division terminates with a proper error
instead of overflowing the context stack (more confusing).

> type family DivP n m            -- n / m.

The instances for division is based on the identities:

    0 / y = 0,               for y >= 1.
    x / y = (x - y) / y + 1, for x >= y >= 1.

> type instance DivP Z (S n) = Z  -- Trivially.
> type instance DivP (S n) (S m) = S (DivP (Sub (S n) (S m)) (S m))  -- Oh my!

Now we can generalize division to negative numbers too, building on
top of 'DivP'. A trivial but tedious exercise.

> -- | Division (@a / b@).
> type family Div a b            -- a / b.
> type instance Div Z (N n) = Z  -- Mustn't allow “Div Z Z”!
> type instance Div Z (S n) = Z
> type instance Div (S n) (S n') = DivP (S n) (S n')
> type instance Div (N n) (N n') = DivP n n'
> type instance Div (N n) (S n') = N (DivP n (S n'))
> type instance Div (S n) (N n') = N (DivP (S n) n')


= Value level functions =

> {- $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.
> -}

The main reason to collect all functions here is to keep the
preceeding sections free from distraction.

> -- | Negate a 'NumType'.
> negate :: NumType a => a -> Negate a
> negate _ = undefined

> -- | Increment a 'NumType' by one.
> incr :: NumType a => a -> Succ a
> incr _ = undefined

> -- | Decrement a 'NumType' by one.
> decr :: NumType a => a -> Pred a
> decr _ = undefined

> -- | Add two 'NumType's.
> (+) :: (NumType a, NumType b) => a -> b -> Add a b
> _ + _ = undefined

> -- | Subtract the second 'NumType' from the first.
> (-) :: (NumType a, NumType b) => a -> b -> Sub a b
> _ - _ = undefined

> -- | Multiply two 'NumType's.
> (*) :: (NumType a, NumType b) => a -> b -> Mul a b
> _ * _ = undefined

> -- | Divide the first 'NumType' by the second.
> (/) :: (NumType a, NumType b) => a -> b -> Div a b
> _ / _ = undefined


= Convenince types and values =

Finally we define some type synonyms for the convenience of clients
of the library.

> 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

Analogously we also define some convenience values (all 'undefined'
but with the expected types).

> zero :: Z  -- ~ hZero
> zero = undefined
> pos1 :: Pos1
> pos1 = incr zero
> pos2 :: Pos2
> pos2 = incr pos1
> pos3 :: Pos3
> pos3 = incr pos2
> pos4 :: Pos4
> pos4 = incr pos3
> pos5 :: Pos5
> pos5 = incr pos4
> neg1 :: Neg1
> neg1 = decr zero
> neg2 :: Neg2
> neg2 = decr neg1
> neg3 :: Neg3
> neg3 = decr neg2
> neg4 :: Neg4
> neg4 = decr neg3
> neg5 :: Neg5
> neg5 = decr neg4


= References =

[1] http://homepages.cwi.nl/~ralf/HList/
[2] http://okmij.org/ftp/Computation/resource-aware-prog/BinaryNumber.hs