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