numtype-tf (empty) → 0.1

raw patch · 6 files changed

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

Dependencies added: base

Files

• LICENSE +31/−0
• Numeric/NumType/TF.lhs +354/−0
• Numeric/NumType/TFTests.hs +111/−0
• README +10/−0
• Setup.lhs +3/−0
• numtype-tf.cabal +34/−0

@@ -0,0 +1,31 @@+Copyright (c) 2008-2012, 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,354 @@+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+> #-}+++= 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)++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++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++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++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++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++> -- | 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.+> type instance DivP Z (S n) = Z  -- Trivially.++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'))  -- 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

@@ -0,0 +1,111 @@+{-# LANGUAGE NoMonomorphismRestriction #-}++module Numeric.NumType.TFTests where++import Numeric.NumType.TF+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,34 @@+Name:                numtype-tf+Version:             0.1+License:             BSD3+License-File:        LICENSE+Copyright:           Bjorn Buckwalter 2012+Author:              Bjorn Buckwalter+Maintainer:          bjorn.buckwalter@gmail.com+Stability:           stable+Homepage:            http://dimensional.googlecode.com/+Synopsis:            Type-level (low cardinality) integers, implemented+                     using type families.+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.++    The numtype-tf packade differs from the numtype package in that+    the NumTypes are implemented using type families rather than+    functional dependencies.++    Requires GHC 7.0 or later.++Category:            Math+Build-Type:          Simple+Build-Depends:       base < 5+Exposed-Modules:     Numeric.NumType.TF+Extra-source-files:  README,+                     Numeric/NumType/TFTests.hs