numtype-dk (empty) → 0.5
raw patch · 7 files changed
+1013/−0 lines, 7 filesdep +basesetup-changed
Dependencies added: base
Files
- LICENSE +31/−0
- Numeric/NumType/DK/Integers.hs +459/−0
- Numeric/NumType/DK/Naturals.hs +52/−0
- Numeric/NumType/DKTests.hs +427/−0
- README +4/−0
- Setup.lhs +3/−0
- numtype-dk.cabal +37/−0
+ LICENSE view
@@ -0,0 +1,31 @@+Copyright (c) 2008-2014, 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.
+ Numeric/NumType/DK/Integers.hs view
@@ -0,0 +1,459 @@+{-# OPTIONS_HADDOCK show-extensions #-} + +{-# LANGUAGE AutoDeriveTypeable #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +{- | + Copyright : Copyright (C) 2006-2015 Bjorn Buckwalter + License : BSD3 + + Maintainer : bjorn.buckwalter@gmail.com + Stability : Stable + Portability: GHC only + += Summary + +Type-level integers for GHC 7.8+. + +We provide type level arithmetic operations. We also provide term-level arithmetic operations on proxys, +and conversion from the type level to the term level. + += Planned Obsolesence + +We commit this package to hackage in sure and certain hope of the coming of glorious GHC integer type literals, +when the sea shall give up her dead, and this package shall be rendered unto obsolescence. + +-} +module Numeric.NumType.DK.Integers +( + -- * Type-Level Integers + type TypeInt(..), + -- * Type-level Arithmetic + Pred, Succ, Negate, Abs, Signum, + type (+), type (-), type (*), type (/), type (^), + -- * Arithmetic on Proxies + pred, succ, negate, abs, signum, + (+), (-), (*), (/), (^), + -- * Convenience Synonyms for Proxies + zero, + pos1, pos2, pos3, pos4, pos5, pos6, pos7, pos8, pos9, + neg1, neg2, neg3, neg4, neg5, neg6, neg7, neg8, neg9, + -- * Conversion from Types to Terms + KnownTypeInt(..) +) +where + +import Data.Proxy +import Prelude hiding ((+), (-), (*), (/), (^), pred, succ, negate, abs, signum) +import qualified Prelude + +#if MIN_VERSION_base(4, 8, 0) +-- Use @Nat@s from @GHC.TypeLits@. +import GHC.TypeLits hiding ((+)(), (*)(), (-)(), (^)()) +import qualified GHC.TypeLits as N + +type Z = 0 -- GHC.TypeLits +type N1 = 1 -- GHC.TypeLits +#else +-- Use custom @Typeable@ @Nat@s. +import Numeric.NumType.DK.Naturals (Nat (S, Z)) +import qualified Numeric.NumType.DK.Naturals as N + +type N1 = 'S 'Z -- TypeInt.DK.Nats +#endif + +-- Use the same fixity for operators as the Prelude. +infixr 8 ^ +infixl 7 *, / +infixl 6 +, - + + +-- Natural numbers +-- =============== + +type family NatPred (n::Nat) :: Nat where NatPred n = n N.- N1 +type family NatSucc (n::Nat) :: Nat where NatSucc n = n N.+ N1 + + +-- Integers +-- ======== + +data TypeInt = Neg10Minus Nat -- 10, 11, 12, 13, ... + | Neg9 + | Neg8 + | Neg7 + | Neg6 + | Neg5 + | Neg4 + | Neg3 + | Neg2 + | Neg1 + | Zero -- 0 + | Pos1 + | Pos2 + | Pos3 + | Pos4 + | Pos5 + | Pos6 + | Pos7 + | Pos8 + | Pos9 + | Pos10Plus Nat -- -10, -11, -12, -13, ... + + +-- Unary operations +-- ---------------- + +type family Pred (i::TypeInt) :: TypeInt where + Pred ('Neg10Minus n) = 'Neg10Minus (NatSucc n) + Pred 'Neg9 = 'Neg10Minus Z + Pred 'Neg8 = 'Neg9 + Pred 'Neg7 = 'Neg8 + Pred 'Neg6 = 'Neg7 + Pred 'Neg5 = 'Neg6 + Pred 'Neg4 = 'Neg5 + Pred 'Neg3 = 'Neg4 + Pred 'Neg2 = 'Neg3 + Pred 'Neg1 = 'Neg2 + Pred 'Zero = 'Neg1 + Pred 'Pos1 = 'Zero + Pred 'Pos2 = 'Pos1 + Pred 'Pos3 = 'Pos2 + Pred 'Pos4 = 'Pos3 + Pred 'Pos5 = 'Pos4 + Pred 'Pos6 = 'Pos5 + Pred 'Pos7 = 'Pos6 + Pred 'Pos8 = 'Pos7 + Pred 'Pos9 = 'Pos8 + Pred ('Pos10Plus Z) = 'Pos9 + Pred ('Pos10Plus n) = 'Pos10Plus (NatPred n) + +type family Succ (i::TypeInt) :: TypeInt where + Succ ('Neg10Minus Z) = 'Neg9 + Succ ('Neg10Minus n) = 'Neg10Minus (NatPred n) + Succ 'Neg9 = 'Neg8 + Succ 'Neg8 = 'Neg7 + Succ 'Neg7 = 'Neg6 + Succ 'Neg6 = 'Neg5 + Succ 'Neg5 = 'Neg4 + Succ 'Neg4 = 'Neg3 + Succ 'Neg3 = 'Neg2 + Succ 'Neg2 = 'Neg1 + Succ 'Neg1 = 'Zero + Succ 'Zero = 'Pos1 + Succ 'Pos1 = 'Pos2 + Succ 'Pos2 = 'Pos3 + Succ 'Pos3 = 'Pos4 + Succ 'Pos4 = 'Pos5 + Succ 'Pos5 = 'Pos6 + Succ 'Pos6 = 'Pos7 + Succ 'Pos7 = 'Pos8 + Succ 'Pos8 = 'Pos9 + Succ 'Pos9 = 'Pos10Plus Z + Succ ('Pos10Plus n) = 'Pos10Plus (NatSucc n) + +-- | TypeInt negation. +type family Negate (i::TypeInt) :: TypeInt where + Negate ('Neg10Minus n) = 'Pos10Plus n + Negate 'Neg9 = 'Pos9 + Negate 'Neg8 = 'Pos8 + Negate 'Neg7 = 'Pos7 + Negate 'Neg6 = 'Pos6 + Negate 'Neg5 = 'Pos5 + Negate 'Neg4 = 'Pos4 + Negate 'Neg3 = 'Pos3 + Negate 'Neg2 = 'Pos2 + Negate 'Neg1 = 'Pos1 + Negate 'Zero = 'Zero + Negate 'Pos1 = 'Neg1 + Negate 'Pos2 = 'Neg2 + Negate 'Pos3 = 'Neg3 + Negate 'Pos4 = 'Neg4 + Negate 'Pos5 = 'Neg5 + Negate 'Pos6 = 'Neg6 + Negate 'Pos7 = 'Neg7 + Negate 'Pos8 = 'Neg8 + Negate 'Pos9 = 'Neg9 + Negate ('Pos10Plus n) = 'Neg10Minus n + +-- | Absolute value. +type family Abs (i::TypeInt) :: TypeInt where + Abs ('Neg10Minus n) = 'Pos10Plus n + Abs 'Neg9 = 'Pos9 + Abs 'Neg8 = 'Pos8 + Abs 'Neg7 = 'Pos7 + Abs 'Neg6 = 'Pos6 + Abs 'Neg5 = 'Pos5 + Abs 'Neg4 = 'Pos4 + Abs 'Neg3 = 'Pos3 + Abs 'Neg2 = 'Pos2 + Abs 'Neg1 = 'Pos1 + Abs i = i + +-- | Signum. +type family Signum (i::TypeInt) :: TypeInt where + Signum ('Neg10Minus n) = 'Neg1 + Signum 'Neg9 = 'Neg1 + Signum 'Neg8 = 'Neg1 + Signum 'Neg7 = 'Neg1 + Signum 'Neg6 = 'Neg1 + Signum 'Neg5 = 'Neg1 + Signum 'Neg4 = 'Neg1 + Signum 'Neg3 = 'Neg1 + Signum 'Neg2 = 'Neg1 + Signum 'Neg1 = 'Neg1 + Signum 'Zero = 'Zero + Signum i = 'Pos1 + + +-- Binary operations +-- ----------------- + +-- | TypeInt addition. +type family (i::TypeInt) + (i'::TypeInt) :: TypeInt where + 'Zero + i = i + i + 'Neg10Minus n = Pred i + Succ ('Neg10Minus n) + i + 'Neg9 = Pred i + 'Neg8 + i + 'Neg8 = Pred i + 'Neg7 + i + 'Neg7 = Pred i + 'Neg6 + i + 'Neg6 = Pred i + 'Neg5 + i + 'Neg5 = Pred i + 'Neg4 + i + 'Neg4 = Pred i + 'Neg3 + i + 'Neg3 = Pred i + 'Neg2 + i + 'Neg2 = Pred i + 'Neg1 + i + 'Neg1 = Pred i + i + 'Zero = i + i + i' = Succ i + Pred i' -- i + Pos + +-- | TypeInt subtraction. +type family (i::TypeInt) - (i'::TypeInt) :: TypeInt where + i - i' = i + Negate i' + +-- | TypeInt multiplication. +type family (i::TypeInt) * (i'::TypeInt) :: TypeInt + where + 'Zero * i = 'Zero + i * 'Zero = 'Zero + i * 'Pos1 = i + i * 'Pos2 = i + i + i * 'Pos3 = i + i + i + i * 'Pos4 = i + i + i + i + i * 'Pos5 = i + i + i + i + i + i * 'Pos6 = i + i + i + i + i + i + i * 'Pos7 = i + i + i + i + i + i + i + i * 'Pos8 = i + i + i + i + i + i + i + i + i * 'Pos9 = i + i + i + i + i + i + i + i + i + i * 'Pos10Plus n = i + i * Pred ('Pos10Plus n) + i * i' = Negate (i * Negate i') + +-- | TypeInt exponentiation. +type family (i::TypeInt) ^ (i'::TypeInt) :: TypeInt + where + i ^ 'Zero = 'Pos1 + i ^ 'Pos1 = i + i ^ 'Pos2 = i * i + i ^ 'Pos3 = i * i * i + i ^ 'Pos4 = i * i * i * i + i ^ 'Pos5 = i * i * i * i * i + i ^ 'Pos6 = i * i * i * i * i * i + i ^ 'Pos7 = i * i * i * i * i * i * i + i ^ 'Pos8 = i * i * i * i * i * i * i * i + i ^ 'Pos9 = i * i * i * i * i * i * i * i * i + i ^ 'Pos10Plus n = i * i ^ Pred ('Pos10Plus n) + +-- | TypeInt division. +type family (i::TypeInt) / (i'::TypeInt) :: TypeInt + where + + i / 'Pos1 = i + i / 'Neg1 = Negate i + -- @Zero / n = Zero@ would allow division by zero. + -- @i / i = Pos1@ would allow division by zero. + 'Zero / ('Neg10Minus n) = 'Zero + 'Zero / 'Neg9 = 'Zero + 'Zero / 'Neg8 = 'Zero + 'Zero / 'Neg7 = 'Zero + 'Zero / 'Neg6 = 'Zero + 'Zero / 'Neg5 = 'Zero + 'Zero / 'Neg4 = 'Zero + 'Zero / 'Neg3 = 'Zero + 'Zero / 'Neg2 = 'Zero + 'Zero / 'Pos2 = 'Zero + 'Zero / 'Pos3 = 'Zero + 'Zero / 'Pos4 = 'Zero + 'Zero / 'Pos5 = 'Zero + 'Zero / 'Pos6 = 'Zero + 'Zero / 'Pos7 = 'Zero + 'Zero / 'Pos8 = 'Zero + 'Zero / 'Pos9 = 'Zero + 'Zero / ('Pos10Plus n) = 'Zero + + 'Neg2 / 'Neg2 = 'Pos1 + 'Neg3 / 'Neg3 = 'Pos1 + 'Neg4 / 'Neg4 = 'Pos1 + 'Neg5 / 'Neg5 = 'Pos1 + 'Neg6 / 'Neg6 = 'Pos1 + 'Neg7 / 'Neg7 = 'Pos1 + 'Neg8 / 'Neg8 = 'Pos1 + 'Neg9 / 'Neg9 = 'Pos1 + 'Neg10Minus n / 'Neg10Minus n = 'Pos1 + + 'Neg2 / 'Pos2 = 'Neg1 + 'Neg3 / 'Pos3 = 'Neg1 + 'Neg4 / 'Pos4 = 'Neg1 + 'Neg5 / 'Pos5 = 'Neg1 + 'Neg6 / 'Pos6 = 'Neg1 + 'Neg7 / 'Pos7 = 'Neg1 + 'Neg8 / 'Pos8 = 'Neg1 + 'Neg9 / 'Pos9 = 'Neg1 + 'Neg10Minus n / 'Pos10Plus n = 'Neg1 + + 'Pos2 / 'Neg2 = 'Neg1 + 'Pos3 / 'Neg3 = 'Neg1 + 'Pos4 / 'Neg4 = 'Neg1 + 'Pos5 / 'Neg5 = 'Neg1 + 'Pos6 / 'Neg6 = 'Neg1 + 'Pos7 / 'Neg7 = 'Neg1 + 'Pos8 / 'Neg8 = 'Neg1 + 'Pos9 / 'Neg9 = 'Neg1 + 'Pos10Plus n / 'Neg10Minus n = 'Neg1 + + 'Pos2 / 'Pos2 = 'Pos1 + 'Pos3 / 'Pos3 = 'Pos1 + 'Pos4 / 'Pos4 = 'Pos1 + 'Pos5 / 'Pos5 = 'Pos1 + 'Pos6 / 'Pos6 = 'Pos1 + 'Pos7 / 'Pos7 = 'Pos1 + 'Pos8 / 'Pos8 = 'Pos1 + 'Pos9 / 'Pos9 = 'Pos1 + 'Pos10Plus n / 'Pos10Plus n = 'Pos1 + + 'Neg4 / 'Neg2 = 'Pos2 + 'Neg6 / 'Neg2 = 'Pos3 + 'Neg8 / 'Neg2 = 'Pos4 + 'Neg6 / 'Neg3 = 'Pos2 + 'Neg9 / 'Neg3 = 'Pos3 + 'Neg8 / 'Neg4 = 'Pos2 + 'Neg10Minus n / i = ('Neg10Minus n + Abs i) / i - Signum i + + 'Neg4 / 'Pos2 = 'Neg2 + 'Neg6 / 'Pos2 = 'Neg3 + 'Neg8 / 'Pos2 = 'Neg4 + 'Neg6 / 'Pos3 = 'Neg2 + 'Neg9 / 'Pos3 = 'Neg3 + 'Neg8 / 'Pos4 = 'Neg2 + + 'Pos4 / 'Neg2 = 'Neg2 + 'Pos6 / 'Neg2 = 'Neg3 + 'Pos8 / 'Neg2 = 'Neg4 + 'Pos6 / 'Neg3 = 'Neg2 + 'Pos9 / 'Neg3 = 'Neg3 + 'Pos8 / 'Neg4 = 'Neg2 + + 'Pos4 / 'Pos2 = 'Pos2 + 'Pos6 / 'Pos2 = 'Pos3 + 'Pos8 / 'Pos2 = 'Pos4 + 'Pos6 / 'Pos3 = 'Pos2 + 'Pos9 / 'Pos3 = 'Pos3 + 'Pos8 / 'Pos4 = 'Pos2 + 'Pos10Plus n / i = ('Pos10Plus n - Abs i) / i + Signum i + + +-- Term level +-- ========== + +-- Term level operators +-- -------------------- + +pred :: Proxy i -> Proxy (Pred i); pred _ = Proxy +succ :: Proxy i -> Proxy (Succ i); succ _ = Proxy +negate :: Proxy i -> Proxy (Negate i); negate _ = Proxy +abs :: Proxy i -> Proxy (Abs i); abs _ = Proxy +signum :: Proxy i -> Proxy (Signum i); signum _ = Proxy + +(+) :: Proxy i -> Proxy i' -> Proxy (i + i'); _ + _ = Proxy +(-) :: Proxy i -> Proxy i' -> Proxy (i - i'); _ - _ = Proxy +(*) :: Proxy i -> Proxy i' -> Proxy (i * i'); _ * _ = Proxy +(/) :: Proxy i -> Proxy i' -> Proxy (i / i'); _ / _ = Proxy +(^) :: Proxy i -> Proxy i' -> Proxy (i ^ i'); _ ^ _ = Proxy + + +-- Term level TypeNats for convenience +-- ----------------------------------- + +neg9 :: Proxy 'Neg9 +neg9 = Proxy :: Proxy 'Neg9 +neg8 :: Proxy 'Neg8 +neg8 = Proxy :: Proxy 'Neg8 +neg7 :: Proxy 'Neg7 +neg7 = Proxy :: Proxy 'Neg7 +neg6 :: Proxy 'Neg6 +neg6 = Proxy :: Proxy 'Neg6 +neg5 :: Proxy 'Neg5 +neg5 = Proxy :: Proxy 'Neg5 +neg4 :: Proxy 'Neg4 +neg4 = Proxy :: Proxy 'Neg4 +neg3 :: Proxy 'Neg3 +neg3 = Proxy :: Proxy 'Neg3 +neg2 :: Proxy 'Neg2 +neg2 = Proxy :: Proxy 'Neg2 +neg1 :: Proxy 'Neg1 +neg1 = Proxy :: Proxy 'Neg1 +zero :: Proxy 'Zero +zero = Proxy :: Proxy 'Zero +pos1 :: Proxy 'Pos1 +pos1 = Proxy :: Proxy 'Pos1 +pos2 :: Proxy 'Pos2 +pos2 = Proxy :: Proxy 'Pos2 +pos3 :: Proxy 'Pos3 +pos3 = Proxy :: Proxy 'Pos3 +pos4 :: Proxy 'Pos4 +pos4 = Proxy :: Proxy 'Pos4 +pos5 :: Proxy 'Pos5 +pos5 = Proxy :: Proxy 'Pos5 +pos6 :: Proxy 'Pos6 +pos6 = Proxy :: Proxy 'Pos6 +pos7 :: Proxy 'Pos7 +pos7 = Proxy :: Proxy 'Pos7 +pos8 :: Proxy 'Pos8 +pos8 = Proxy :: Proxy 'Pos8 +pos9 :: Proxy 'Pos9 +pos9 = Proxy :: Proxy 'Pos9 + + +-- Reification +-- ----------- + +-- | Conversion to a @Num@. +class KnownTypeInt (i::TypeInt) where toNum :: Num a => Proxy i -> a + +instance KnownTypeInt (Succ ('Neg10Minus n)) => KnownTypeInt ('Neg10Minus n) + where toNum = (Prelude.- 1) . toNum . succ + +instance KnownTypeInt 'Neg9 where toNum _ = -9 +instance KnownTypeInt 'Neg8 where toNum _ = -8 +instance KnownTypeInt 'Neg7 where toNum _ = -7 +instance KnownTypeInt 'Neg6 where toNum _ = -6 +instance KnownTypeInt 'Neg5 where toNum _ = -5 +instance KnownTypeInt 'Neg4 where toNum _ = -4 +instance KnownTypeInt 'Neg3 where toNum _ = -3 +instance KnownTypeInt 'Neg2 where toNum _ = -2 +instance KnownTypeInt 'Neg1 where toNum _ = -1 +instance KnownTypeInt 'Zero where toNum _ = 0 +instance KnownTypeInt 'Pos1 where toNum _ = 1 +instance KnownTypeInt 'Pos2 where toNum _ = 2 +instance KnownTypeInt 'Pos3 where toNum _ = 3 +instance KnownTypeInt 'Pos4 where toNum _ = 4 +instance KnownTypeInt 'Pos5 where toNum _ = 5 +instance KnownTypeInt 'Pos6 where toNum _ = 6 +instance KnownTypeInt 'Pos7 where toNum _ = 7 +instance KnownTypeInt 'Pos8 where toNum _ = 8 +instance KnownTypeInt 'Pos9 where toNum _ = 9 + +instance KnownTypeInt (Pred ('Pos10Plus n)) => KnownTypeInt ('Pos10Plus n) + where toNum = (Prelude.+ 1) . toNum . pred
+ Numeric/NumType/DK/Naturals.hs view
@@ -0,0 +1,52 @@+{-# LANGUAGE AutoDeriveTypeable #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +module Numeric.NumType.DK.Naturals where + +import Prelude hiding (pred) + +-- Use the same fixity for operators as the Prelude. +infixr 8 ^ +infixl 7 * +infixl 6 + + +data Nat = Z | S Nat -- Natural numbers starting at 0. + +-- | Nat addition. +type family (n::Nat) + (n'::Nat) :: Nat where + -- Z + n = n -- Redundant. + n + 'Z = n + n + 'S n' = 'S n + n' + +-- | Nat subtraction. +type family (n::Nat) - (n'::Nat) :: Nat where + n - 'Z = n + 'S n - 'S n' = n - n' + +-- | Nat multiplication. +type family (n::Nat) * (n'::Nat) :: Nat + where + --Z * n = Z -- Redundant + n * 'Z = 'Z + n * ('S n') = n + n * n' -- i * Pos n + +-- | Nat exponentiation. +type family (n::Nat) ^ (n'::Nat) :: Nat + where + --Zero ^ Pos n = Zero -- Redundant. + n ^ 'Z = 'S 'Z + n ^ 'S n' = n * n ^ n' + + +class KnownNat (n::Nat) where natVal :: proxy n -> Integer + +instance KnownNat 'Z where natVal _ = 0 +instance KnownNat n => KnownNat ('S n) where + natVal = (1 +) . natVal . pred + where + pred :: proxy ('S n) -> proxy n + pred = undefined
+ Numeric/NumType/DKTests.hs view
@@ -0,0 +1,427 @@+{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE KindSignatures #-} + +module Numeric.NumType.DKTests where + +import Numeric.NumType.DK.Integers +import Prelude hiding ((*), (/), (+), (-), (^), pred, succ, negate, abs, signum) +import qualified Prelude as P ((*), (/), (+), (-), (^), pred, succ, negate, abs, signum) +import Data.Proxy +import Test.HUnit + +-- Some “large” NumTypes. +neg12 = pred neg11 +neg11 = pred neg10 +neg10 = pred neg9 + +pos10 = succ pos9 +pos11 = succ pos10 +pos12 = succ pos11 + +-- | Compares a type level unary function with a value level unary function + -- by converting 'NumType' to a @Num@. This assumes that the 'toNum' + -- function is solid. +unaryTest :: (KnownNumType i, KnownNumType i', Num a, Eq a, Show a) + => (Proxy i -> Proxy i') -> (a -> a) -> Proxy i -> Test +unaryTest f f' x = TestCase $ assertEqual + "Unary function Num equivalence" + (f' (toNum x)) (toNum (f x)) + +-- | 'unaryTest' with @Num a@ fixed to @Integer@. This is needed by + -- 'testIncrDecr'. +unaryTest' :: (KnownNumType i, KnownNumType i') + => (Proxy i -> Proxy i') -> (Integer -> Integer) -> Proxy i -> Test +unaryTest' = unaryTest + +-- | Compares a type level binary function with a value level binary function + -- by converting 'NumType' to 'Num'. This assumes that the 'toNum' + -- function is solid. +binaryTest :: (KnownNumType i, KnownNumType i', KnownNumType i'', Num a, Eq a, Show a) + => (Proxy i -> Proxy i' -> Proxy i'') + -> (a -> a -> a) + -> Proxy i -> Proxy i' -> Test +binaryTest f f' x y = TestCase $ assertEqual + "Binary function Num equivalence" + (f' (toNum x) (toNum y)) (toNum (f x y)) + +binaryTest' :: (KnownNumType i, KnownNumType i', KnownNumType i'', Num a, Eq a, Show a) + => (Proxy i -> Proxy i' -> Proxy i'') + -> (Integer -> Integer -> Integer) + -> Proxy i -> Proxy i' -> Test +binaryTest' = binaryTest + + +-- | Test that conversion to 'Num a' works as expected. This is sort of a + -- prerequisite for the other tests. +testAsIntegral = TestLabel "Num equivalence tests" $ TestList + [ TestCase $ -12 @=? toNum neg12 + , TestCase $ -11 @=? toNum neg11 + , TestCase $ -10 @=? toNum neg10 + , TestCase $ -9 @=? toNum neg9 + , TestCase $ -8 @=? toNum neg8 + , TestCase $ -7 @=? toNum neg7 + , TestCase $ -6 @=? toNum neg6 + , TestCase $ -5 @=? toNum neg5 + , TestCase $ -4 @=? toNum neg4 + , TestCase $ -3 @=? toNum neg3 + , TestCase $ -2 @=? toNum neg2 + , TestCase $ -1 @=? toNum neg1 + , TestCase $ 0 @=? toNum zero + , TestCase $ 1 @=? toNum pos1 + , TestCase $ 2 @=? toNum pos2 + , TestCase $ 3 @=? toNum pos3 + , TestCase $ 4 @=? toNum pos4 + , TestCase $ 5 @=? toNum pos5 + , TestCase $ 6 @=? toNum pos6 + , TestCase $ 7 @=? toNum pos7 + , TestCase $ 8 @=? toNum pos8 + , TestCase $ 9 @=? toNum pos9 + , TestCase $ 10 @=? toNum pos10 + , TestCase $ 11 @=? toNum pos11 + , TestCase $ 12 @=? toNum pos12 + ] -- By induction all other NumTypes should be good if these are. + +-- | Test incrementing and decrementing. +testIncrDecr = TestLabel "Increment and decrement tests" $ TestList + [ t neg12 + , t neg11 + , t neg10 + , t neg9 + , t neg8 + , t neg7 + , t neg6 + , t neg5 + , t neg4 + , t neg3 + , t neg2 + , t neg1 + , t zero + , t pos1 + , t pos2 + , t pos3 + , t pos4 + , t pos5 + , t pos6 + , t pos7 + , t pos8 + , t pos9 + , t pos10 + , t pos11 + , t pos12 + ] where + t x = TestList [ unaryTest' (+ pos1) (P.+ 1) x + , unaryTest' (+ neg1) (P.- 1) x + , unaryTest' (\x -> x - neg1) (P.+ 1) x + , unaryTest' (\x -> x - pos1) (P.- 1) x + , unaryTest' pred P.pred x + , unaryTest' succ P.succ x + ] + +-- | Test negation. +testNegate = TestLabel "Negation tests" $ TestList + [ unaryTest negate P.negate neg12 + , unaryTest negate P.negate neg11 + , unaryTest negate P.negate neg10 + , unaryTest negate P.negate neg9 + , unaryTest negate P.negate neg8 + , unaryTest negate P.negate neg7 + , unaryTest negate P.negate neg6 + , unaryTest negate P.negate neg5 + , unaryTest negate P.negate neg4 + , unaryTest negate P.negate neg3 + , unaryTest negate P.negate neg2 + , unaryTest negate P.negate neg1 + , unaryTest negate P.negate zero + , unaryTest negate P.negate pos1 + , unaryTest negate P.negate pos2 + , unaryTest negate P.negate pos3 + , unaryTest negate P.negate pos4 + , unaryTest negate P.negate pos5 + , unaryTest negate P.negate pos6 + , unaryTest negate P.negate pos7 + , unaryTest negate P.negate pos8 + , unaryTest negate P.negate pos9 + , unaryTest negate P.negate pos10 + , unaryTest negate P.negate pos11 + , unaryTest negate P.negate pos12 + ] + +-- | Test absolute value. +testAbs = TestLabel "Absolute value tests" $ TestList + [ unaryTest abs P.abs neg12 + , unaryTest abs P.abs neg11 + , unaryTest abs P.abs neg10 + , unaryTest abs P.abs neg9 + , unaryTest abs P.abs neg8 + , unaryTest abs P.abs neg7 + , unaryTest abs P.abs neg6 + , unaryTest abs P.abs neg5 + , unaryTest abs P.abs neg4 + , unaryTest abs P.abs neg3 + , unaryTest abs P.abs neg2 + , unaryTest abs P.abs neg1 + , unaryTest abs P.abs zero + , unaryTest abs P.abs pos1 + , unaryTest abs P.abs pos2 + , unaryTest abs P.abs pos3 + , unaryTest abs P.abs pos4 + , unaryTest abs P.abs pos5 + , unaryTest abs P.abs pos6 + , unaryTest abs P.abs pos7 + , unaryTest abs P.abs pos8 + , unaryTest abs P.abs pos9 + , unaryTest abs P.abs pos10 + , unaryTest abs P.abs pos11 + , unaryTest abs P.abs pos12 + ] + +-- | Test signum. +testSignum = TestLabel "Signum tests" $ TestList + [ unaryTest signum P.signum neg12 + , unaryTest signum P.signum neg11 + , unaryTest signum P.signum neg10 + , unaryTest signum P.signum neg9 + , unaryTest signum P.signum neg8 + , unaryTest signum P.signum neg7 + , unaryTest signum P.signum neg6 + , unaryTest signum P.signum neg5 + , unaryTest signum P.signum neg4 + , unaryTest signum P.signum neg3 + , unaryTest signum P.signum neg2 + , unaryTest signum P.signum neg1 + , unaryTest signum P.signum zero + , unaryTest signum P.signum pos1 + , unaryTest signum P.signum pos2 + , unaryTest signum P.signum pos3 + , unaryTest signum P.signum pos4 + , unaryTest signum P.signum pos5 + , unaryTest signum P.signum pos6 + , unaryTest signum P.signum pos7 + , unaryTest signum P.signum pos8 + , unaryTest signum P.signum pos9 + , unaryTest signum P.signum pos10 + , unaryTest signum P.signum pos11 + , unaryTest signum P.signum pos12 + ] + +-- | Test absolute value. +testAbs = TestLabel "Absolute value tests" $ TestList + [ unaryTest abs P.abs neg2 + , unaryTest abs P.abs neg1 + , unaryTest abs P.abs zero + , unaryTest abs P.abs pos1 + , unaryTest abs P.abs pos1 + ] + +-- | Test signum. +testSignum = TestLabel "Signum tests" $ TestList + [ unaryTest signum P.signum neg2 + , unaryTest signum P.signum neg1 + , unaryTest signum P.signum zero + , unaryTest signum P.signum pos1 + , unaryTest signum P.signum pos1 + ] + +-- | Test addition. +testAddition = TestLabel "Addition tests" $ TestList + [ binaryTest (+) (P.+) pos2 pos5 + , binaryTest (+) (P.+) pos12 pos2 + , binaryTest (+) (P.+) pos11 pos2 + , binaryTest (+) (P.+) pos10 pos2 + , binaryTest (+) (P.+) pos2 pos12 + , binaryTest (+) (P.+) pos2 pos11 + , binaryTest (+) (P.+) pos2 pos10 + , binaryTest (+) (P.+) neg2 pos5 + , binaryTest (+) (P.+) pos2 neg5 + , binaryTest (+) (P.+) neg2 neg5 + , binaryTest (+) (P.+) neg2 neg12 + , binaryTest (+) (P.+) neg2 neg11 + , binaryTest (+) (P.+) neg2 neg10 + , binaryTest (+) (P.+) neg12 neg2 + , binaryTest (+) (P.+) neg11 neg2 + , binaryTest (+) (P.+) neg10 neg2 + , binaryTest (+) (P.+) zero zero + , binaryTest (+) (P.+) pos2 zero + , binaryTest (+) (P.+) neg2 zero + , binaryTest (+) (P.+) zero pos5 + , binaryTest (+) (P.+) zero neg5 + ] + +-- | Test subtraction. +testSubtraction = TestLabel "Subtraction tests" $ TestList + [ binaryTest (-) (P.-) pos2 pos5 + , binaryTest (-) (P.-) pos12 pos2 + , binaryTest (-) (P.-) pos11 pos2 + , binaryTest (-) (P.-) pos10 pos2 + , binaryTest (-) (P.-) pos2 pos12 + , binaryTest (-) (P.-) pos2 pos11 + , binaryTest (-) (P.-) pos2 pos10 + , binaryTest (-) (P.-) neg2 pos5 + , binaryTest (-) (P.-) pos2 neg5 + , binaryTest (-) (P.-) neg2 neg5 + , binaryTest (-) (P.-) neg2 neg12 + , binaryTest (-) (P.-) neg2 neg11 + , binaryTest (-) (P.-) neg2 neg10 + , binaryTest (-) (P.-) neg12 neg2 + , binaryTest (-) (P.-) neg11 neg2 + , binaryTest (-) (P.-) neg10 neg2 + , binaryTest (-) (P.-) zero zero + , binaryTest (-) (P.-) pos2 zero + , binaryTest (-) (P.-) neg2 zero + , binaryTest (-) (P.-) zero pos5 + , binaryTest (-) (P.-) zero neg5 + ] + +-- | Test multiplication. +testMultiplication = TestLabel "Multiplication tests" $ TestList + [ binaryTest (*) (P.*) pos2 pos5 + , binaryTest (*) (P.*) pos12 pos2 + , binaryTest (*) (P.*) pos11 pos2 + , binaryTest (*) (P.*) pos10 pos2 + , binaryTest (*) (P.*) pos2 pos12 + , binaryTest (*) (P.*) pos2 pos11 + , binaryTest (*) (P.*) pos2 pos10 + , binaryTest (*) (P.*) neg2 pos5 + , binaryTest (*) (P.*) pos2 neg5 + , binaryTest (*) (P.*) neg2 neg5 + , binaryTest (*) (P.*) neg2 neg12 + , binaryTest (*) (P.*) neg2 neg11 + , binaryTest (*) (P.*) neg2 neg10 + , binaryTest (*) (P.*) neg12 neg2 + , binaryTest (*) (P.*) neg11 neg2 + , binaryTest (*) (P.*) neg10 neg2 + , binaryTest (*) (P.*) zero zero + , binaryTest (*) (P.*) pos2 zero + , binaryTest (*) (P.*) neg2 zero + , binaryTest (*) (P.*) zero pos5 + , binaryTest (*) (P.*) zero neg5 + -- Probably some duplicates in the below. + , binaryTest (*) (P.*) pos10 pos2 + , binaryTest (*) (P.*) pos9 pos3 + , binaryTest (*) (P.*) pos8 pos4 + , binaryTest (*) (P.*) pos8 pos2 + , binaryTest (*) (P.*) pos6 pos3 + , binaryTest (*) (P.*) pos6 pos2 + , binaryTest (*) (P.*) pos4 pos2 + , binaryTest (*) (P.*) pos9 neg3 + , binaryTest (*) (P.*) pos8 neg4 + , binaryTest (*) (P.*) pos8 neg2 + , binaryTest (*) (P.*) pos6 neg3 + , binaryTest (*) (P.*) pos6 neg2 + , binaryTest (*) (P.*) pos4 neg2 + , binaryTest (*) (P.*) zero pos5 + , binaryTest (*) (P.*) zero neg3 + , binaryTest (*) (P.*) neg4 pos2 + , binaryTest (*) (P.*) neg6 pos2 + , binaryTest (*) (P.*) neg6 pos3 + , binaryTest (*) (P.*) neg8 pos2 + , binaryTest (*) (P.*) neg8 pos4 + , binaryTest (*) (P.*) neg9 pos3 + , binaryTest (*) (P.*) neg4 neg2 + , binaryTest (*) (P.*) neg6 neg2 + , binaryTest (*) (P.*) neg6 neg3 + , binaryTest (*) (P.*) neg8 neg2 + , binaryTest (*) (P.*) neg8 neg4 + , binaryTest (*) (P.*) neg9 neg3 + , binaryTest (*) (P.*) neg12 pos4 + ] + +-- | Test division. +testDivision = TestLabel "Division tests" $ TestList + [ binaryTest (/) (P./) pos12 pos4 + , binaryTest (/) (P./) pos12 neg4 + , binaryTest (/) (P./) pos10 pos5 + , binaryTest (/) (P./) pos10 pos2 + , binaryTest (/) (P./) pos9 pos3 + , binaryTest (/) (P./) pos8 pos4 + , binaryTest (/) (P./) pos8 pos2 + , binaryTest (/) (P./) pos6 pos3 + , binaryTest (/) (P./) pos6 pos2 + , binaryTest (/) (P./) pos4 pos2 + , binaryTest (/) (P./) pos9 neg3 + , binaryTest (/) (P./) pos8 neg4 + , binaryTest (/) (P./) pos8 neg2 + , binaryTest (/) (P./) pos6 neg3 + , binaryTest (/) (P./) pos6 neg2 + , binaryTest (/) (P./) pos4 neg2 + , binaryTest (/) (P./) zero pos5 + , binaryTest (/) (P./) zero neg3 + , binaryTest (/) (P./) neg4 pos2 + , binaryTest (/) (P./) neg6 pos2 + , binaryTest (/) (P./) neg6 pos3 + , binaryTest (/) (P./) neg8 pos2 + , binaryTest (/) (P./) neg8 pos4 + , binaryTest (/) (P./) neg9 pos3 + , binaryTest (/) (P./) neg4 neg2 + , binaryTest (/) (P./) neg6 neg2 + , binaryTest (/) (P./) neg6 neg3 + , binaryTest (/) (P./) neg8 neg2 + , binaryTest (/) (P./) neg8 neg4 + , binaryTest (/) (P./) neg9 neg3 + , binaryTest (/) (P./) neg12 pos4 + , binaryTest (/) (P./) neg12 neg4 + , binaryTest (/) (P./) neg10 neg5 + , binaryTest (/) (P./) neg10 neg2 + + , binaryTest (/) (P./) pos5 pos5 + , binaryTest (/) (P./) neg5 pos5 + , binaryTest (/) (P./) pos5 neg5 + , binaryTest (/) (P./) zero neg5 + , binaryTest (/) (P./) zero pos5 + , binaryTest (/) (P./) pos5 pos1 + , binaryTest (/) (P./) pos5 neg1 + + , binaryTest (/) (P./) pos12 pos12 + , binaryTest (/) (P./) neg12 pos12 + , binaryTest (/) (P./) pos12 neg12 + , binaryTest (/) (P./) zero neg12 + , binaryTest (/) (P./) zero pos12 + , binaryTest (/) (P./) pos12 pos1 + , binaryTest (/) (P./) pos12 neg1 + ] + +-- | Test exponentiation. +testExponentiation = TestLabel "Exponentiation tests" $ TestList + [ binaryTest (^) (P.^) pos2 pos3 + , binaryTest (^) (P.^) zero pos5 + , binaryTest (^) (P.^) neg2 pos3 + + , binaryTest (^) (P.^) pos3 pos3 + , binaryTest (^) (P.^) pos3 pos2 + , binaryTest (^) (P.^) pos3 pos1 + , binaryTest (^) (P.^) pos2 pos4 + , binaryTest (^) (P.^) pos2 pos3 + , binaryTest (^) (P.^) pos2 pos2 + , binaryTest (^) (P.^) pos2 pos1 + , binaryTest (^) (P.^) pos1 pos12 + , binaryTest (^) (P.^) pos1 pos9 + , binaryTest (^) (P.^) pos1 zero + + , binaryTest (^) (P.^) neg3 pos3 + , binaryTest (^) (P.^) neg3 pos2 + , binaryTest (^) (P.^) neg3 pos1 + , binaryTest (^) (P.^) neg2 pos4 + , binaryTest (^) (P.^) neg2 pos3 + , binaryTest (^) (P.^) neg2 pos2 + , binaryTest (^) (P.^) neg2 pos1 + , binaryTest (^) (P.^) neg1 pos12 + , binaryTest (^) (P.^) neg1 pos9 + , binaryTest (^) (P.^) neg1 zero + ] + +-- | Collect the test cases. +tests = TestList + [ testAsIntegral + , testIncrDecr + , testNegate + , testAbs + , testSignum + , testAddition + , testSubtraction + , testMultiplication + , testDivision + , testExponentiation + ] + +main = runTestTT tests
+ README view
@@ -0,0 +1,4 @@+Experimental. Requires GHC 7.8 or later. + +For project information (issues, updates, wiki, examples) see: + http://github.com/bjornbm/numtype-dk
+ Setup.lhs view
@@ -0,0 +1,3 @@+#!/usr/bin/env runhaskell +> import Distribution.Simple +> main = defaultMain
+ numtype-dk.cabal view
@@ -0,0 +1,37 @@+name: numtype-dk +version: 0.5 +license: BSD3 +license-File: LICENSE +copyright: Bjorn Buckwalter 2012-2014 +author: Bjorn Buckwalter +maintainer: bjorn@buckwalter.se +category: Math +stability: provisional +cabal-version: >= 1.6 +build-type: Simple +homepage: https://github.com/bjornbm/numtype-dk +synopsis: Type-level integers, using TypeNats, Data + Kinds, and Closed Type Families. +description: + + This package provides type level representations of the + (positive and negative) integers and basic operations (addition, + subtraction, multiplication, division, exponentiation) on these. + + The numtype-dk package differs from the numtype package in that + the NumTypes are implemented using Data Kinds, TypeNats, and + Closed Type Families rather than Functional Dependencies. + + Requires GHC 7.8 or later. + +extra-source-files: README, + Numeric/NumType/DKTests.hs + +source-repository head + type: git + location: https://github.com/bjornbm/numtype-dk/ + +library + build-depends: base < 5 + exposed-modules: Numeric.NumType.DK.Integers + other-modules: Numeric.NumType.DK.Naturals