Numeric.NumType.TF -- Type-level (low cardinality) integers
Bjorn Buckwalter, firstname.lastname@example.org
= Preliminaries =
This module requires GHC 7.0 or later.
= Summary =
> module Numeric.NumType.TF (
> , Z, S, N
> , Pred, Succ, Negate, Add, Sub, Div, Mul
> , Zero, Pos1, Pos2, Pos3, Pos4, Pos5, Neg1, Neg2, Neg3, Neg4, Neg5
> , toNum, incr, decr, negate, (+), (), (*), (/)
> , zero, pos1, pos2, pos3, pos4, pos5, neg1, neg2, neg3, neg4, neg5
> ) where
> import Prelude hiding ((*), (/), (+), (), negate)
> import qualified Prelude ((+), negate)
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
> class NumTypeI n where
> type Negate n
> type Pred n
> type Succ n
> toNum :: Num a => n -> a
Now we use a trick from Oleg Kiselyov and Chung-chieh Shan :
-- 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 (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'.
> data Z
Next we define the "successor" type, here called 'S' (corresponding
to HList's 'HSucc').
> data S n
Finally we define the "negation" type used to represent negative
> data N n
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
> type Negate Z = Z
> type Pred Z = N (S Z)
> type Succ Z = S Z
> toNum _ = 0
> instance NumTypeI (S Z) where
> type Negate (S Z) = N (S Z)
> type Pred (S Z) = Z
> type Succ (S Z) = S (S Z)
> toNum _ = 1
> instance NumTypeI (S n) => NumTypeI (S (S n)) where
> type Negate (S (S n)) = N (S (S n))
> type Pred (S (S n)) = S n
> type Succ (S (S n)) = S (S (S n))
> toNum _ = 1 Prelude.+ toNum (undefined :: S n)
> instance NumTypeI (S n) => NumTypeI (N (S n)) where
> type Negate (N (S n)) = S n
> type Pred (N (S n)) = N (S (S n))
> type Succ (N (S n)) = Negate n
> 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.
> type family Add a b
> type family Sub a b
Adding anything to Zero gives "anything".
> type instance Add Z n = n
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')
Substitution 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
> type family Mul a b
> type instance Mul Z n = Z
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')
> type instance Mul (N n) n' = Negate (Mul n n')
= 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
> type instance DivP Z (S n) = Z
The recursive instance for division is quite complex and in fact I
do not recall how I derived it. But it works (I promise!).
> type instance DivP (S n) (S n') = S (DivP (Pred (Sub (S n) n')) (S n'))
Now we can generalize division to negative numbers too, building on
top of 'DivP'. A trivial but tedious exercise.
> type family Div a b
> type instance Div Z (N n) = 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 =
The main reason to collect all functions here is to keep the
preceeding sections free from distraction.
> negate :: NumType a => a -> Negate a
> negate _ = undefined
> incr :: NumType a => a -> Succ a
> incr _ = undefined
> decr :: NumType a => a -> Pred a
> decr _ = undefined
> (+) :: (NumType a, NumType b) => a -> b -> Add a b
> _ + _ = undefined
> () :: (NumType a, NumType b) => a -> b -> Sub a b
> _ _ = undefined
> (*) :: (NumType a, NumType b) => a -> b -> Mul a b
> _ * _ = undefined
> (/) :: (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
> 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 =