Numeric.NumType -- Type-level (low cardinality) integers Bjorn Buckwalter, bjorn.buckwalter@gmail.com License: BSD3 = Summary = 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 [1], 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. Also, even if stack size is increased type-checker performance quickly gets painfully slow. If you will be working with type-level integers beyond (-20, 20) this module probably isn't for you. They are, however, eminently suitably for applications such as representing physical dimensions. = Preliminaries = This module requires GHC 6.6 or later. We utilize multi-parameter type classes, phantom types, functional dependencies and undecidable instances (and possibly additional unidentified GHC extensions). 
> {-# LANGUAGE UndecidableInstances
>            , ScopedTypeVariables
>            , EmptyDataDecls
>            , FunctionalDependencies
>            , MultiParamTypeClasses
>            , FlexibleInstances
>            , DeriveDataTypeable
> #-}

> {- |
>    Copyright  : Copyright (C) 2006-2009 Bjorn Buckwalter
>    License    : BSD3
>
>    Maintainer : bjorn.buckwalter@gmail.com
>    Stability  : Stable
>    Portability: GHC only?
>
> Please refer to the literate Haskell code for documentation of both API
> and implementation.
> -}

> module Numeric.NumType
>   -- Basic classes (exported versions).
>   ( NumType, PosType, NegType, NonZero
>   -- Arithmetic classes.
>   , Succ, Negate, Sum, Div, Mul
>   -- Functions.
>   , toNum, incr, decr, negate, (+), (-), (*), (/)
>   -- Data types.
>   , Zero, Pos, Neg
>   -- Type synonyms for convenience.
>   , Pos1, Pos2, Pos3, Pos4, Pos5, Neg1, Neg2, Neg3, Neg4, Neg5
>   -- Values for convenience.
>   , zero, pos1, pos2, pos3, pos4, pos5, neg1, neg2, neg3, neg4, neg5
>   ) where

> import Prelude hiding ((*), (/), (+), (-), negate)
> import qualified Prelude ((+), (-))
> 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 toNum :: (Num a) => n -> a
Then we define classes encompassing all positive and negative integers respectively. The 'PosTypeI' class corresponds to HList's 'HNat'. We also define a class for non-zero numbers (used to prohibit division by zero). 
> class (NumTypeI n) => PosTypeI n
> class (NumTypeI n) => NegTypeI n
> class (NumTypeI n) => NonZeroI n
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 classes. 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    (NumTypeI n) => NumType n
> instance (NumTypeI n) => NumType n
> class    (PosTypeI n) => PosType n
> instance (PosTypeI n) => PosType n
> class    (NegTypeI n) => NegType n
> instance (NegTypeI n) => NegType n
> class    (NonZeroI n) => NonZero n
> instance (NonZeroI n) => NonZero n
We do not have to do this for our other classes. They have the above classes in their constraints and since the instances are complete (not proven) a new instance cannot be defined (actually used in the case of GHC) without overlapping instances. 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. 'Zero' corresponds to HList's 'HZero'. 
> data Zero deriving Typeable
> instance NumTypeI Zero where toNum _ = 0
> instance PosTypeI Zero
> instance NegTypeI Zero
Next we define the "successor" type, here called 'Pos' (corresponding to HList's 'HSucc'). 
> data Pos n deriving Typeable
> instance (PosTypeI n) => NumTypeI (Pos n) where
>   toNum _ = toNum (undefined :: n) Prelude.+ 1
> instance (PosTypeI n) => PosTypeI (Pos n)
> instance (PosTypeI n) => NonZeroI (Pos n)
We could be more restrictive using "data (PosTypeI n) => Pos n" but this constraint will not be checked (by GHC) anyway when 'Pos' is used solely at the type level. Finally we define the "predecessor" type used to represent negative numbers. 
> data Neg n deriving Typeable
> instance (NegTypeI n) => NumTypeI (Neg n) where
>   toNum _ = toNum (undefined :: n) Prelude.- 1
> instance (NegTypeI n) => NegTypeI (Neg n)
> instance (NegTypeI n) => NonZeroI (Neg n)
= Show instances = For convenience we create show instances for the defined NumTypes. 
> instance Show Zero where show _ = "NumType 0"
> instance (PosTypeI n) => Show (Pos n) where show x = "NumType " ++ show (toNum x :: Integer)
> instance (NegTypeI n) => Show (Neg n) where show x = "NumType " ++ show (toNum x :: Integer)
= Negation, incrementing and decrementing = We start off with some basic building blocks. Negation is a simple matter of recursively changing 'Pos' to 'Neg' or vice versa while leaving 'Zero' unchanged. 
> class (NumTypeI a, NumTypeI b) => Negate a b | a -> b, b -> a

> instance Negate Zero Zero
> instance (PosTypeI a, NegTypeI b, Negate a b) => Negate (Pos a) (Neg b)
> instance (NegTypeI a, PosTypeI b, Negate a b) => Negate (Neg a) (Pos b)
We define a type class for incrementing and decrementing NumTypes. The 'incr' and 'decr' functions correspond roughly to HList's 'hSucc' and 'hPred' respectively. 
> class (NumTypeI a, NumTypeI b) => Succ a b | a -> b, b -> a
To increment NumTypes we either prepend 'Pos' to numbers greater than or equal to Zero or remove a 'Neg' from numbers less than Zero. 
> instance Succ Zero (Pos Zero)
> instance (PosTypeI a) => Succ (Pos a) (Pos (Pos a))
> instance Succ (Neg Zero) Zero
> instance (NegTypeI a) => Succ (Neg (Neg a)) (Neg a)
= Addition and subtraction = Now let us move on towards more complex arithmetic operations. We define a class for addition and subtraction of NumTypes. 
> class (Add a b c, Sub c b a)
>    => Sum a b c | a b -> c, a c -> b, b c -> a
In order to provide instances satisfying the functional dependencies of 'Sum', in particular the property that any two parameters uniquely define the third, we must use helper classes. 
> class (NumTypeI a, NumTypeI b, NumTypeI c) => Add a b c | a b -> c
> class (NumTypeI a, NumTypeI b, NumTypeI c) => Sub a b c | a b -> c
Adding anything to Zero gives "anything". 
> instance (NumTypeI a) => Add Zero a a
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. We use the 'Succ' class to do this. 
> instance (PosTypeI a, Succ b c, Add a c d) => Add (Pos a) b d
> instance (NegTypeI a, Succ c b, Add a c d) => Add (Neg a) b d
We define our helper class for subtraction analogously. 
> instance (NumType a) => Sub a Zero a
> instance (Succ a' a, PosTypeI b, Sub a' b c) => Sub a (Pos b) c
> instance (Succ a a', NegTypeI b, Sub a' b c) => Sub a (Neg b) c
While we cold have defined a single 'Sub' instance using negation and addition. ] instance (Negate b b', Add a b' c) => Sub a b c However, the constraints of such a 'Sub' instance which are not also constraints of the 'Sub' class can complicate type signatures (is this true or was I confused by other issues at the time?). Thus we elect to use the lower level instances analoguous to the 'Add' instances. Using the helper classes we can provide an instance of 'Sum' that satisfies its functional dependencies. We provide an instance of 'Sum' in terms of 'Add' and 'Sub'. 
> instance (Add a b c, Sub c b a, Sub c a b) => Sum a b c
= Division = We will do division on NumTypes before we do multiplication. This may be surprising but it will in fact simplify the multiplication. The reason for this is that we can have a "reverse" functional dependency for division but not for multiplication. Consider the expressions "x / y = z". If y and z are known we can always determine x. However, in "x * y = z" we can not determine x if y and z are zero. The 'NonZeroI' class is used as a constraint on the denominator 'b' in our 'Div' class. 
> class (NumTypeI a, NonZeroI b, NumTypeI c) => Div a b c | a b -> c, c b -> a
Zero divided by anything (we don't bother with infinity) equals zero. 
> instance (NonZeroI n) => Div Zero n Zero
Note that We could omit the 'NonZeroI' class completely and instead provide the following two instances. ] instance (PosTypeI n) => Div Zero (Pos n) Zero ] instance (NegTypeI n) => Div Zero (Neg n) Zero Going beyond zero numbers we start with a base case with all numbers positive. We recursively subtract the denominator from nominator while incrementing the result, until we reach the zero case. 
> instance ( Sum n' (Pos n'') (Pos n)
>          , Div n'' (Pos n') n''', PosTypeI n''')
>       => Div (Pos n) (Pos n') (Pos n''')
Now we tackle cases with negative numbers involved. We trivially convert these to the all-positive case and negate the result if appropriate. 
> instance ( NegTypeI n, NegTypeI n'
>          , Negate n p, Negate n' p'
>          , Div (Pos p) (Pos p') (Pos p'')
>          , PosTypeI p'')
>       => Div (Neg n) (Neg n') (Pos p'')
> instance ( NegTypeI n, Negate n p'
>          , Div (Pos p) (Pos p') (Pos p'')
>          , Negate (Pos p'') (Neg n'')
>          , PosTypeI p)
>       => Div (Pos p) (Neg n) (Neg n'')
> instance ( NegTypeI n, Negate n p'
>          , Div (Pos p') (Pos p) (Pos p'')
>          , Negate (Pos p'') (Neg n'')
>          , PosTypeI p)
>       => Div (Neg n) (Pos p) (Neg n'')
= Multiplication = Class for multiplication. Limited by the type checker stack. If the 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 
> class (NumTypeI a, NumTypeI b, NumTypeI c) => Mul a b c | a b -> c
Providing instances for the 'Mul' class is really easy thanks to the 'Div' class having the functional dependency "c b -> a". 
> instance (NumTypeI n) => Mul n Zero Zero
> instance (NumTypeI a, NumTypeI c, PosTypeI p, Div c (Pos p) a) => Mul a (Pos p) c
> instance (NumTypeI a, NumTypeI c, NegTypeI n, Div c (Neg n) a) => Mul a (Neg n) c
= Functions = Using the above type classes 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 :: (Negate a b) => a -> b
> negate _ = undefined

> incr :: (Succ a b) => a -> b
> incr _ = undefined
> decr :: (Succ a b) => b -> a
> decr _ = undefined

> (+) :: (Sum a b c) => a -> b -> c
> _ + _ = undefined
> (-) :: (Sum a b c) => c -> b -> a
> _ - _ = undefined

> (/) :: (Div a b c) => a -> b -> c
> _ / _ = undefined

> (*) :: (Mul a b c) => a -> b -> c
> _ * _ = undefined
= Convenince types and values = Finally we define some type synonyms for the convenience of clients of the library. 
> type Pos1 = Pos Zero
> type Pos2 = Pos Pos1
> type Pos3 = Pos Pos2
> type Pos4 = Pos Pos3
> type Pos5 = Pos Pos4
> type Neg1 = Neg Zero
> type Neg2 = Neg Neg1
> type Neg3 = Neg Neg2
> type Neg4 = Neg Neg3
> type Neg5 = Neg Neg4
Analogously we also define some convenience values (all 'undefined' but with the expected types). 
> zero :: Zero  -- ~ 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