numtype (empty) → 1.0

raw patch · 6 files changed

+590/−0 lines, 6 filesdep +basesetup-changed

Dependencies added: base

Files

• LICENSE +31/−0
• Numeric/NumType.lhs +408/−0
• Numeric/NumTypeTests.hs +111/−0
• README +10/−0
• Setup.lhs +3/−0
• numtype.cabal +27/−0

@@ -0,0 +1,31 @@+Copyright (c) 2008, Bjorn Buckwalter.+All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions+are met:++  * Redistributions of source code must retain the above copyright+    notice, this list of conditions and the following disclaimer.++  * Redistributions in binary form must reproduce the above+    copyright notice, this list of conditions and the following+    disclaimer in the documentation and/or other materials provided+    with the distribution.++  * Neither the name of the copyright holder(s) nor the names of+    contributors may be used to endorse or promote products derived+    from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS+FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE+COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,+INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,+BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER+CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT+LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN+ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE+POSSIBILITY OF SUCH DAMAGE.

@@ -0,0 +1,408 @@+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+> #-}++> {- |+>    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 ((+), (-))++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+> 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+> 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+> 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) => 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''))+>       => 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''))+>       => 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''))+>       => 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 (PosTypeI p, Div c (Pos p) a) => Mul a (Pos p) c+> instance (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+

@@ -0,0 +1,111 @@+{-# LANGUAGE NoMonomorphismRestriction #-}++module Numeric.NumTypeTests where++import Numeric.NumType+import Prelude hiding ((*), (/), (+), (-), negate)+import qualified Prelude as P ((*), (/), (+), (-), negate)+import Test.HUnit+++-- Compares a type level unary function with a value level unary function+-- by converting 'NumType' to 'Integral'. This assumes that the 'toIntegral'+-- function is solid.+unaryTest :: (NumType n, NumType n', Num a)+          => (n -> n') -> (a -> a) -> n -> Test+unaryTest f f' x = TestCase $ assertEqual+    "Unary function Integral equivalence"+    (f' (toNum x)) (toNum (f x))++-- Compares a type level binary function with a value level binary function+-- by converting 'NumType' to 'Integral'. This assumes that the 'toIntegral'+-- function is solid.+binaryTest :: (NumType n, NumType n', NumType n'', Num a)+           => (n -> n' -> n'') -> (a -> a -> a) -> n -> n' -> Test+binaryTest f f' x y = TestCase $ assertEqual+    "Binary function Integral equivalence"+    (f' (toNum x) (toNum y)) (toNum (f x y))++-- Test that conversion to 'Integral' works as expected. This is sort of a+-- prerequisite for the other tests.+testAsIntegral = TestLabel "Integral equivalence tests" $ TestList+    [ TestCase $ -2 @=? toNum neg2+    , TestCase $ -1 @=? toNum neg1+    , TestCase $  0 @=? toNum zero+    , TestCase $  1 @=? toNum pos1+    , TestCase $  2 @=? toNum pos2+    ] -- By induction all other NumTypes should be good if these are.++-- Test increment and decrement for a bunch of 'NumTypes'.+testIncrDecr = TestLabel "Increment and decrement tests" $ TestList+    [ t neg2+    , t neg1+    , t zero+    , t pos1+    , t pos1+    ] where+        t x = TestList [ unaryTest incr (P.+ 1) x+                       , unaryTest decr (P.- 1) x+                       ]++-- Test negation.+testNegate = TestLabel "Negation tests" $ TestList+    [ unaryTest negate P.negate neg2+    , unaryTest negate P.negate neg1+    , unaryTest negate P.negate zero+    , unaryTest negate P.negate pos1+    , unaryTest negate P.negate pos1+    ]++-- Test addition.+testAddition = TestLabel "Addition tests" $ TestList+    [ binaryTest (+) (P.+) pos2 pos3+    , binaryTest (+) (P.+) neg2 pos3+    , binaryTest (+) (P.+) pos2 neg3+    , binaryTest (+) (P.+) neg2 neg3+    ]++-- Test subtraction.+testSubtraction = TestLabel "Subtraction tests" $ TestList+    [ binaryTest (-) (P.-) pos2 pos5+    , binaryTest (-) (P.-) neg2 pos5+    , binaryTest (-) (P.-) pos2 neg5+    , binaryTest (-) (P.-) neg2 neg5+    ]++-- Test multiplication.+testMultiplication = TestLabel "Multiplication tests" $ TestList+    [ binaryTest (*) (P.*) pos2 pos5+    , binaryTest (*) (P.*) neg2 pos5+    , binaryTest (*) (P.*) pos2 neg5+    , binaryTest (*) (P.*) neg2 neg5+    , binaryTest (*) (P.*) pos2 zero+    , binaryTest (*) (P.*) neg2 zero+    , binaryTest (*) (P.*) zero pos5+    , binaryTest (*) (P.*) zero neg5+    ]++-- Test division.+testDivision = TestLabel "Division tests" $ TestList+    [ binaryTest (/) (P./) pos4 pos2+    , binaryTest (/) (P./) zero pos5+    , binaryTest (/) (P./) zero neg3+    , binaryTest (/) (P./) neg4 pos2+    , binaryTest (/) (P./) pos4 neg2+    , binaryTest (/) (P./) neg4 neg2+    , binaryTest (/) (P./) pos5 pos5+    ]+++-- Collect the test cases.+tests = TestList+    [ testAsIntegral+    , testIncrDecr+    , testNegate+    , testAddition+    , testSubtraction+    , testMultiplication+    , testDivision+    ]++main = runTestTT tests

@@ -0,0 +1,10 @@+For documentation see the literate haskell source code.++For project information (issues, updates, wiki, examples) see:+    http://code.google.com/p/dimensional/++To install (requires GHC 6.6 or later):+    runhaskell Setup.lhs configure+    runhaskell Setup.lhs build+    runhaskell Setup.lhs install+

@@ -0,0 +1,3 @@+#!/usr/bin/env runhaskell+> import Distribution.Simple+> main = defaultMain

@@ -0,0 +1,27 @@+Name:                numtype+Version:             1.0+License:             BSD3+License-File:        LICENSE+Copyright:           Bjorn Buckwalter 2009+Author:              Bjorn Buckwalter+Maintainer:          bjorn.buckwalter@gmail.com+Stability:           stable+Homepage:            http://dimensional.googlecode.com/+Synopsis:            Type-level (low cardinality) integers.+Description:+    This package provides unary type level representations of the+    (positive and negative) integers and basic operations (addition,+    subtraction, multiplication, division) on these.+    Due to the unary implementation the practical size of the+    NumTypes is severely limited making them unsuitable for+    large-cardinality applications. If you will be working with+    integers beyond (-20, 20) this package probably isn't for you.+    It is, however, eminently suitable for applications such as+    representing physical dimensions (see the 'Dimensional' library).+    Requires GHC 6.6.1 or later.+Category:            Math+Build-Type:          Simple+Build-Depends:       base < 5+Exposed-Modules:     Numeric.NumType+Extra-source-files:  README,+                     Numeric/NumTypeTests.hs