> {-# 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 -> aNow 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 nNow 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 TypeableNext 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 TypeableFinally 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 TypeableThe '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 Pos5Analogously 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