diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,12 @@ +Copyright (c) 2015,2016, Michal Konecny, Pieter Collins +All rights reserved. + +Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: + +1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer. + +2. 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. + +3. Neither the name of the software nor the names of its 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 HOLDER 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. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/mixed-types-num.cabal b/mixed-types-num.cabal new file mode 100644 --- /dev/null +++ b/mixed-types-num.cabal @@ -0,0 +1,174 @@ +name: mixed-types-num +version: 0.1.0.0 +cabal-version: >= 1.9.2 +build-type: Simple +homepage: https://github.com/michalkonecny/mixed-types-num +author: Michal Konecny +maintainer: Michal Konecny +copyright: (c) 2015-2017 Michal Konecny +license: BSD3 +license-file: LICENSE +stability: experimental +tested-with: GHC==7.10.3, GHC==8.0.2 +category: Math +synopsis: Alternative Prelude with numeric and logic expressions typed bottom-up +Description: + = Main purpose + . + This package provides a version of Prelude where + unary and binary operations such as @not@, @+@, @==@ + have their result type derived from the parameter type(s), + allowing, /e.g./: + . + * dividing an integer by an integer, giving a rational: + . + @let n = 1 :: Integer in n/(n+1) :: Rational@ + . + @1/2 :: Rational@ + . + (The type Rational would be derived automatically because + integer literals are always of type @Integer@, not @Num t => t@.) + . + * adding an integer and a rational, giving a rational: + . + @(length [x])+1/3 :: Rational@ + . + * taking natural, integer and fractional power using the same operator: + . + @2^2 :: Integer@ + . + @2.0^(-2) :: Rational@ + . + @(double 2)^(1/2) :: Double@ + -- . + -- @negate 1 :: Integer@ + -- . + -- @negate (x == 1) :: Bool@ + . + The following examples require package : + . + @2^(1/2) :: CauchyReal@ + . + @pi :: CauchyReal@ + . + @sqrt 2 :: CauchyReal@ + . + * comparing an integer with an (exact) real number, giving a @Maybe Bool@: + . + @... x :: CauchyReal ... if (isCertainlyTrue (x > 1)) then ...@ + . + = Type classes + . + Arithmetic operations are provided via multi-parameter type classes + and the result type is given by associated + type families. For example: + . + @(+) :: (CanAddAsymmetric t1 t2) => t1 -> t2 -> AddType t1 t2@ + . + The type constraint @CanAdd t1 t2@ implies both + @CanAddAsymmetric t1 t2@ and @CanAddAsymmetric t2 t1@. + . + For convenience there are other aggregate type constraints such as + @CanAddThis t1 t2@, which implies that the result is of type @t1@, + and @CanAddSameType t@, which is a shortcut for @CanAddThis t t@. + . + == Testable specification + . + The arithmetic type classes are accompanied by generic hspec test suites, + which are specialised to concrete instance types for their testing. + These test suites include the expected algebraic properties of operations, + such as commutativity and associativity of addition. + . + = Limitations + . + * Not all numerical operations are supported yet. + Eg @tan@, @atan@ are missing at the moment. + . + * Inferred types can be very large. Eg for @f a b c = sqrt (a + b * c + 1)@ the inferred type is: + . + @ + f: (CanMulAsymmetric t1 t2, CanAddAsymmetric t4 (MulType t1 t2), + CanAddAsymmetric (AddType t4 (MulType t1 t2)) Integer, + CanSqrt (AddType (AddType t4 (MulType t1 t2)) Integer)) => + t4 + -> t1 + -> t2 + -> SqrtType (AddType (AddType t4 (MulType t1 t2)) Integer) + @ + . + * Due to limitations of some versions of ghc, type inferrence sometimes fails. + Eg @add1 = (+ 1)@ fails (eg with ghc 8.0.2) unless we explicitly declare the type + @add1 :: (CanAdd Integer t) => t -> AddType t Integer@ + or use an explicit parameter, eg @add1 x = x + 1@. + . + = Further reading + . + To find out more, please read the documentation for the modules + in the order specified in "Numeric.MixedTypes". + . + = Origin + . + The idea of having numeric expressions in Haskell with types + derived bottom-up was initially suggested and implemented by Pieter Collins. + This version is a fresh rewrite by Michal Konečný. + +source-repository head + type: git + location: https://github.com/mikkonecny/mixed-types-num + +library + hs-source-dirs: src + build-depends: + base == 4.* + , convertible >= 1.1.1.0 && < 1.2 + , hspec >= 2.1 && < 2.5 + , hspec-smallcheck >= 0.3 && < 0.5 + , smallcheck == 1.1.* + , QuickCheck >= 2.7 && < 2.10 + ghc-options: -Wall -fno-warn-orphans + extensions: + RebindableSyntax, + PostfixOperators, + ScopedTypeVariables, + TypeFamilies, + TypeOperators, + ConstraintKinds, + DefaultSignatures, + MultiParamTypeClasses, + FlexibleContexts, + FlexibleInstances, + UndecidableInstances + exposed-modules: + Numeric.MixedTypes + Numeric.MixedTypes.PreludeHiding + Numeric.MixedTypes.Literals + Numeric.MixedTypes.Bool + Numeric.MixedTypes.Eq + Numeric.MixedTypes.Ord + Numeric.MixedTypes.MinMaxAbs + Numeric.MixedTypes.AddSub + Numeric.MixedTypes.Round + Numeric.MixedTypes.Ring + Numeric.MixedTypes.Field + Numeric.MixedTypes.Elementary + +test-suite spec + type: + exitcode-stdio-1.0 + ghc-options: + -Wall + extensions: + RebindableSyntax, + PostfixOperators, + ScopedTypeVariables, + FlexibleContexts + hs-source-dirs: + test + main-is: + Spec.hs + build-depends: + base == 4.* + , mixed-types-num + , hspec >= 2.1 && < 2.3 + , hspec-smallcheck >= 0.3 && < 0.5 + , QuickCheck >= 2.7 && < 2.9 diff --git a/src/Numeric/MixedTypes.hs b/src/Numeric/MixedTypes.hs new file mode 100644 --- /dev/null +++ b/src/Numeric/MixedTypes.hs @@ -0,0 +1,43 @@ +{-| + Module : Numeric.MixedType + Description : Bottom-up typed numeric expressions + Copyright : (c) Michal Konecny, Pieter Collins + License : BSD3 + + Maintainer : mikkonecny@gmail.com + Stability : experimental + Portability : portable + + A single-import module for the package + mixed-types-num. Please see the package description (under Contents). +-} + +module Numeric.MixedTypes +( + -- ** Re-exporting Prelude, hiding the operators we are changing + module Numeric.MixedTypes.PreludeHiding, + -- ** Modules with Prelude alternatives + module Numeric.MixedTypes.Literals, + module Numeric.MixedTypes.Bool, + module Numeric.MixedTypes.Eq, + module Numeric.MixedTypes.Ord, + module Numeric.MixedTypes.MinMaxAbs, + module Numeric.MixedTypes.AddSub, + module Numeric.MixedTypes.Round, + module Numeric.MixedTypes.Ring, + module Numeric.MixedTypes.Field, + module Numeric.MixedTypes.Elementary +) +where + +import Numeric.MixedTypes.PreludeHiding +import Numeric.MixedTypes.Literals +import Numeric.MixedTypes.Bool +import Numeric.MixedTypes.Eq +import Numeric.MixedTypes.Ord +import Numeric.MixedTypes.MinMaxAbs +import Numeric.MixedTypes.AddSub +import Numeric.MixedTypes.Round +import Numeric.MixedTypes.Ring +import Numeric.MixedTypes.Field +import Numeric.MixedTypes.Elementary diff --git a/src/Numeric/MixedTypes/AddSub.hs b/src/Numeric/MixedTypes/AddSub.hs new file mode 100644 --- /dev/null +++ b/src/Numeric/MixedTypes/AddSub.hs @@ -0,0 +1,355 @@ +{-| + Module : Numeric.MixedType.AddSub + Description : Bottom-up typed addition and subtraction + Copyright : (c) Michal Konecny + License : BSD3 + + Maintainer : mikkonecny@gmail.com + Stability : experimental + Portability : portable + +-} + +module Numeric.MixedTypes.AddSub +( + -- * Addition + CanAdd, CanAddAsymmetric(..), CanAddThis, CanAddSameType + , (+), sum + -- ** Tests + , specCanAdd, specCanAddNotMixed, specCanAddSameType, CanAddX, CanAddXX, + -- * Subtraction + CanSub(..), CanSubThis, CanSubSameType + , (-) + -- ** Tests + , specCanSub, specCanSubNotMixed, CanSubX +) +where + +import Numeric.MixedTypes.PreludeHiding +import qualified Prelude as P +import Text.Printf + +import qualified Data.List as List + +import Test.Hspec +import Test.QuickCheck + +import Numeric.MixedTypes.Literals +import Numeric.MixedTypes.Bool (CanNeg(..)) +import Numeric.MixedTypes.Eq +import Numeric.MixedTypes.Ord +import Numeric.MixedTypes.MinMaxAbs () + +{---- Addition -----} + +type CanAdd t1 t2 = + (CanAddAsymmetric t1 t2, CanAddAsymmetric t2 t1, + AddType t1 t2 ~ AddType t2 t1) + +{-| + A replacement for Prelude's `P.+`. If @t1 = t2@ and @Num t1@, + then one can use the default implementation to mirror Prelude's @+@. +-} +class CanAddAsymmetric t1 t2 where + type AddType t1 t2 + type AddType t1 t2 = t1 -- default + add :: t1 -> t2 -> AddType t1 t2 + default add :: (AddType t1 t2 ~ t1, t1~t2, P.Num t1) => t1 -> t1 -> t1 + add = (P.+) + +infixl 6 +, - + +(+) :: (CanAddAsymmetric t1 t2) => t1 -> t2 -> AddType t1 t2 +(+) = add + +type CanAddThis t1 t2 = + (CanAdd t1 t2, AddType t1 t2 ~ t1) +type CanAddSameType t = + CanAddThis t t + +sum :: (CanAddSameType t, ConvertibleExactly Integer t) => [t] -> t +sum xs = List.foldl' add (convertExactly 0) xs + +{-| Compound type constraint useful for test definition. -} +type CanAddX t1 t2 = + (CanAdd t1 t2, + Show t1, Arbitrary t1, + Show t2, Arbitrary t2, + Show (AddType t1 t2), + HasEqCertainly t1 (AddType t1 t2), + HasEqCertainly t2 (AddType t1 t2), + HasEqCertainly (AddType t1 t2) (AddType t1 t2), + HasOrderCertainly t1 (AddType t1 t2), + HasOrderCertainly t2 (AddType t1 t2), + HasOrderCertainly (AddType t1 t2) (AddType t1 t2)) + +{-| Compound type constraint useful for test definition. -} +type CanAddXX t1 t2 = + (CanAddX t1 t2, + HasEqCertainly (AddType t1 t2) (AddType t2 t1)) + +{-| + HSpec properties that each implementation of CanAdd should satisfy. + -} +specCanAdd :: + (CanAddXX t1 t1, + CanAddXX t1 t2, + CanAddXX t1 t3, CanAddXX t2 t3, + CanAddXX t1 (AddType t2 t3), + CanAddXX (AddType t1 t2) t3, + ConvertibleExactly Integer t1, + CanTestPosNeg t1, + HasEqCertainly (AddType t1 (AddType t2 t3)) (AddType (AddType t1 t2) t3)) + => + T t1 -> T t2 -> T t3 -> Spec +specCanAdd (T typeName1 :: T t1) (T typeName2 :: T t2) (T typeName3 :: T t3) = + describe (printf "CanAdd %s %s, CanAdd %s %s" typeName1 typeName2 typeName2 typeName3) $ do + it "absorbs 0" $ do + property $ \ (x :: t1) -> let z = (convertExactly 0 :: t1) in (x + z) ?==?$ x + it "is commutative" $ do + property $ \ (x :: t1) (y :: t2) -> (x + y) ?==?$ (y + x) + it "is associative" $ do + property $ \ (x :: t1) (y :: t2) (z :: t3) -> + (x + (y + z)) ?==?$ ((x + y) + z) + it "increases when positive" $ do + property $ \ (x :: t1) (y :: t2) -> + (isCertainlyPositive x) ==> (x + y) ?>?$ y + it "decreases when negative" $ do + property $ \ (x :: t1) (y :: t2) -> + (isCertainlyNegative x) ==> (x + y) ? a -> b -> Property + (?==?$) = printArgsIfFails2 "?==?" (?==?) + (?>?$) :: (HasOrderCertainlyAsymmetric a b, Show a, Show b) => a -> b -> Property + (?>?$) = printArgsIfFails2 "?>?" (?>?) + (? a -> b -> Property + (? + T t -> Spec +specCanAddNotMixed t = specCanAdd t t t + +{-| + HSpec properties that each implementation of CanAddSameType should satisfy. + -} +specCanAddSameType :: + (ConvertibleExactly Integer t, Show t, + HasEqCertainly t t, CanAddSameType t) + => + T t -> Spec +specCanAddSameType (T typeName :: T t) = + describe (printf "CanAddSameType %s" typeName) $ do + it "has sum working over integers" $ do + property $ \ (xsi :: [Integer]) -> + (sum $ (map convertExactly xsi :: [t])) ?==?$ (convertExactly (sum xsi) :: t) + it "has sum [] = 0" $ do + (sum ([] :: [t])) ?==?$ (convertExactly 0 :: t) + where + (?==?$) :: (HasEqCertainlyAsymmetric a b, Show a, Show b) => a -> b -> Property + (?==?$) = printArgsIfFails2 "?==?" (?==?) + +instance CanAddAsymmetric Int Int where + type AddType Int Int = Integer -- do not risk overflow + add a b = (integer a) P.+ (integer b) + +instance CanAddAsymmetric Integer Integer +instance CanAddAsymmetric Rational Rational +instance CanAddAsymmetric Double Double + +instance CanAddAsymmetric Int Integer where + type AddType Int Integer = Integer + add = convertFirst add +instance CanAddAsymmetric Integer Int where + type AddType Integer Int = Integer + add = convertSecond add + +instance CanAddAsymmetric Int Rational where + type AddType Int Rational = Rational + add = convertFirst add +instance CanAddAsymmetric Rational Int where + type AddType Rational Int = Rational + add = convertSecond add + +instance CanAddAsymmetric Integer Rational where + type AddType Integer Rational = Rational + add = convertFirst add +instance CanAddAsymmetric Rational Integer where + type AddType Rational Integer = Rational + add = convertSecond add + +instance CanAddAsymmetric Int Double where + type AddType Int Double = Double + add = convertFirst add +instance CanAddAsymmetric Double Int where + type AddType Double Int = Double + add = convertSecond add + +instance CanAddAsymmetric Integer Double where + type AddType Integer Double = Double + add = convertFirst add +instance CanAddAsymmetric Double Integer where + type AddType Double Integer = Double + add = convertSecond add + +instance CanAddAsymmetric Rational Double where + type AddType Rational Double = Double + add = convertFirst add +instance CanAddAsymmetric Double Rational where + type AddType Double Rational = Double + add = convertSecond add + +instance (CanAddAsymmetric a b) => CanAddAsymmetric [a] [b] where + type AddType [a] [b] = [AddType a b] + add (x:xs) (y:ys) = (add x y) : (add xs ys) + add _ _ = [] + +instance (CanAddAsymmetric a b) => CanAddAsymmetric (Maybe a) (Maybe b) where + type AddType (Maybe a) (Maybe b) = Maybe (AddType a b) + add (Just x) (Just y) = Just (add x y) + add _ _ = Nothing + +{---- Subtraction -----} + +{-| + A replacement for Prelude's binary `P.-`. + + If @CanNeg t2@ and @CanAdd t1 (NegType t2)@, + then one can use the default implementation + via @a-b = a + (-b)@. +-} +class CanSub t1 t2 where + type SubType t1 t2 + type SubType t1 t2 = AddType t1 (NegType t2) -- default + sub :: t1 -> t2 -> SubType t1 t2 + default sub :: + (SubType t1 t2 ~ AddType t1 (NegType t2), + CanNeg t2, CanAdd t1 (NegType t2)) + => + t1 -> t2 -> SubType t1 t2 + a `sub` b = a + (negate b) + +(-) :: (CanSub t1 t2) => t1 -> t2 -> SubType t1 t2 +(-) = sub + +type CanSubThis t1 t2 = + (CanSub t1 t2, SubType t1 t2 ~ t1) +type CanSubSameType t = + CanSubThis t t + +{-| Compound type constraint useful for test definition. -} +type CanSubX t1 t2 = + (CanSub t1 t2, + HasEqCertainly t1 (SubType t1 t2), + CanAddXX t1 t2, + Show (SubType t1 t2)) + +{-| + HSpec properties that each implementation of CanSub should satisfy. + -} +specCanSub :: + (CanSubX t1 t1, + CanSubX t1 t2, + CanNeg t2, + CanAdd t1 (NegType t2), + HasEqCertainly (SubType t1 t2) (AddType t1 (NegType t2)), + Show (AddType t1 (NegType t2)), + ConvertibleExactly Integer t1) + => + T t1 -> T t2 -> Spec +specCanSub (T typeName1 :: T t1) (T typeName2 :: T t2) = + describe (printf "CanSub %s %s" typeName1 typeName2) $ do + it "x-0 = x" $ do + property $ \ (x :: t1) -> let z = (convertExactly 0 :: t1) in (x - z) ?==?$ x + it "x-x = 0" $ do + property $ \ (x :: t1) -> let z = (convertExactly 0 :: t1) in (x - x) ?==?$ z + it "x-y = x+(-y)" $ do + property $ \ (x :: t1) (y :: t2) -> + (x - y) ?==?$ (x + (negate y)) + where + (?==?$) :: (HasEqCertainlyAsymmetric a b, Show a, Show b) => a -> b -> Property + (?==?$) = printArgsIfFails2 "?==?" (?==?) + +-- +{-| + HSpec properties that each implementation of CanSub should satisfy. + -} +specCanSubNotMixed :: + (CanSubX t t, + CanSubX t (SubType t t), + CanNeg t, + CanAdd t (NegType t), + Show (AddType t (NegType t)), + HasEqCertainly (SubType t t) (AddType t (NegType t)), + ConvertibleExactly Integer t) + => + T t -> Spec +specCanSubNotMixed t = specCanSub t t + +instance CanSub Int Int where + type SubType Int Int = Integer -- do not risk overflow + sub a b = (integer a) P.- (integer b) + +instance CanSub Integer Integer +instance CanSub Rational Rational +instance CanSub Double Double + +instance CanSub Int Integer where + type SubType Int Integer = Integer + sub = convertFirst sub +instance CanSub Integer Int where + type SubType Integer Int = Integer + sub = convertSecond sub + +instance CanSub Int Rational where + type SubType Int Rational = Rational + sub = convertFirst sub +instance CanSub Rational Int where + type SubType Rational Int = Rational + sub = convertSecond sub + +instance CanSub Integer Rational where + type SubType Integer Rational = Rational + sub = convertFirst sub +instance CanSub Rational Integer where + type SubType Rational Integer = Rational + sub = convertSecond sub + +instance CanSub Int Double where + type SubType Int Double = Double + sub = convertFirst sub +instance CanSub Double Int where + type SubType Double Int = Double + sub = convertSecond sub + +instance CanSub Integer Double where + type SubType Integer Double = Double + sub = convertFirst sub +instance CanSub Double Integer where + type SubType Double Integer = Double + sub = convertSecond sub + +instance CanSub Rational Double where + type SubType Rational Double = Double + sub = convertFirst sub +instance CanSub Double Rational where + type SubType Double Rational = Double + sub = convertSecond sub + +instance (CanSub a b) => CanSub [a] [b] where + type SubType [a] [b] = [SubType a b] + sub (x:xs) (y:ys) = (sub x y) : (sub xs ys) + sub _ _ = [] + +instance (CanSub a b) => CanSub (Maybe a) (Maybe b) where + type SubType (Maybe a) (Maybe b) = Maybe (SubType a b) + sub (Just x) (Just y) = Just (sub x y) + sub _ _ = Nothing diff --git a/src/Numeric/MixedTypes/Bool.hs b/src/Numeric/MixedTypes/Bool.hs new file mode 100644 --- /dev/null +++ b/src/Numeric/MixedTypes/Bool.hs @@ -0,0 +1,358 @@ +{-| + Module : Numeric.MixedType.Bool + Description : Bottom-up typed Boolean operations + Copyright : (c) Michal Konecny + License : BSD3 + + Maintainer : mikkonecny@gmail.com + Stability : experimental + Portability : portable + +-} + +module Numeric.MixedTypes.Bool +( + IsBool, specIsBool + -- * Conversion to/from Bool + , HasBools, CanTestCertainly(..), specCanTestCertainly, CanTestCertainlyX + , isNotTrue, isNotFalse + , stronglyImplies, stronglyEquivalentTo + , weaklyImplies, weaklyEquivalentTo + -- * Negation + , CanNeg(..), not, CanNegSameType + -- ** Tests + , specCanNegBool, CanNegBoolX + -- * And and or + , CanAndOr, CanAndOrAsymmetric(..), (&&), (||), CanAndOrWith, CanAndOrSameType, and, or + -- ** Tests + , specCanAndOr, specCanAndOrNotMixed, CanAndOrX +) +where + +import Numeric.MixedTypes.PreludeHiding +import qualified Prelude as P +import Text.Printf + +import qualified Data.List as List + +import Numeric.MixedTypes.Literals + +import Test.Hspec +-- import qualified Test.QuickCheck as QC +import qualified Test.Hspec.SmallCheck as HSC +import qualified Test.SmallCheck as SC +import qualified Test.SmallCheck.Series as SCS +-- import Control.Exception (evaluate) + +type HasBools t = ConvertibleExactly Bool t + +{-| + Tests for truth or falsity. Beware, when @isCertainlyTrue@ returns @False@, + it does not mean that the proposition is false. It usually means that + we failed to prove the proposition. +-} +class (HasBools t) => CanTestCertainly t + where + isCertainlyTrue :: t -> Bool + isCertainlyFalse :: t -> Bool + +isNotFalse :: (CanTestCertainly t) => t -> Bool +isNotFalse = P.not . isCertainlyFalse + +isNotTrue :: (CanTestCertainly t) => t -> Bool +isNotTrue = P.not . isCertainlyTrue + +{-| + If l is certainly True, then r is also certainly True. +-} +stronglyImplies :: (CanTestCertainly t1, CanTestCertainly t2) => t1 -> t2 -> Bool +stronglyImplies l r = + (P.not (isCertainlyTrue l) P.|| isCertainlyTrue r) + +{-| + If l is certainly True, then r is not certainly False. +-} +weaklyImplies :: (CanTestCertainly t1, CanTestCertainly t2) => t1 -> t2 -> Bool +weaklyImplies l r = + (P.not $ isCertainlyTrue l) P.|| (P.not $ isCertainlyFalse r) + +stronglyEquivalentTo :: (CanTestCertainly t1, CanTestCertainly t2) => t1 -> t2 -> Bool +stronglyEquivalentTo l r = + stronglyImplies l r P.&& stronglyImplies r l + +weaklyEquivalentTo :: (CanTestCertainly t1, CanTestCertainly t2) => t1 -> t2 -> Bool +weaklyEquivalentTo l r = + weaklyImplies l r P.&& weaklyImplies r l + +{-| + HSpec properties that each implementation of CanTestCertainly should satisfy. + -} +specCanTestCertainly :: (CanTestCertainly t) => T t -> Spec +specCanTestCertainly (T typeName :: T t) = + describe (printf "CanTestCertainly %s" typeName) $ do + it "detects True using isCertainlyTrue" $ do + isCertainlyTrue (convertExactly True :: t) `shouldBe` True + it "does not detect False using isCertainlyTrue" $ do + isCertainlyTrue (convertExactly False :: t) `shouldBe` False + it "detects False using isCertainlyFalse" $ do + isCertainlyFalse (convertExactly False :: t) `shouldBe` True + it "does not detect True using isCertainlyFalse" $ do + isCertainlyFalse (convertExactly True :: t) `shouldBe` False + +instance ConvertibleExactly Bool Bool where + safeConvertExactly b = Right b + +instance CanTestCertainly Bool where + isCertainlyTrue = id + isCertainlyFalse = not + +instance (ConvertibleExactly Bool t) => ConvertibleExactly Bool (Maybe t) where + safeConvertExactly b = + case (safeConvertExactly b) of + Left _ -> Right Nothing + Right r -> Right (Just r) + +instance (CanTestCertainly t) => CanTestCertainly (Maybe t) where + isCertainlyTrue (Just b) = isCertainlyTrue b + isCertainlyTrue _ = False + isCertainlyFalse (Just b) = isCertainlyFalse b + isCertainlyFalse _ = False + +{---- Negation ----} + +{-| + This is negation is both the numeric negation as well as the Boolean negation. + Example of non-standard Boolean negation: + + @ + negate (Just True) = Just False + @ + -} +class CanNeg t where + type NegType t + type NegType t = t + negate :: t -> NegType t + +{-| A synonym of 'negate'. -} +not :: (CanNeg t) => t -> NegType t +not = negate + +type CanNegSameType t = (CanNeg t, NegType t ~ t) + +{-| Compound type constraint useful for test definition. -} +type CanTestCertainlyX t = (CanTestCertainly t, Show t, SCS.Serial IO t) + +{-| Compound type constraint useful for test definition. -} +type CanNegBoolX t = + (CanNeg t, CanTestCertainlyX t, CanTestCertainlyX (NegType t)) + +{-| + HSpec properties that each Boolean implementation of CanNeg should satisfy. + -} +specCanNegBool :: + (CanNegBoolX t, CanNegBoolX (NegType t)) + => + T t -> Spec +specCanNegBool (T typeName :: T t) = + describe (printf "CanNeg %s" typeName) $ do + it "ignores double negation" $ do + HSC.property $ \ (x :: t) -> (not (not x)) `scEquals` x + it "negates True to False" $ do + HSC.property $ \ (x :: t) -> + (isCertainlyTrue x) SC.==> (isCertainlyFalse (not x)) + it "negates False to True" $ do + HSC.property $ \ (x :: t) -> + (isCertainlyFalse x) SC.==> (isCertainlyTrue (not x)) + + +instance CanNeg Bool where negate = P.not + +instance CanNeg t => CanNeg (Maybe t) where + type NegType (Maybe t) = Maybe (NegType t) + negate = fmap negate + +_testNeg1 :: Maybe Bool +_testNeg1 = not (Just True) + +{---- And/Or ----} + +type CanAndOr t1 t2 = + (CanAndOrAsymmetric t1 t2, CanAndOrAsymmetric t2 t1, + AndOrType t1 t2 ~ AndOrType t2 t1) + +{-| + Binary logical `and' and `or' for generalised Booleans. For example: + + @ + (Just True) && False = Just False + (Just (Just True)) || False = (Just (Just True)) + @ + -} +class CanAndOrAsymmetric t1 t2 where + type AndOrType t1 t2 + and2 :: t1 -> t2 -> AndOrType t1 t2 + or2 :: t1 -> t2 -> AndOrType t1 t2 + +type CanAndOrWith t1 t2 = (CanAndOr t1 t2, AndOrType t1 t2 ~ t1) +type CanAndOrSameType t = (CanAndOrWith t t) + +infixr 3 && +infixr 2 || + +{-| A synonym of 'and2'. -} +(&&) :: (CanAndOrAsymmetric a b) => a -> b -> AndOrType a b +(&&) = and2 +{-| A synonym of 'or2'. -} +(||) :: (CanAndOrAsymmetric a b) => a -> b -> AndOrType a b +(||) = or2 + +and :: (CanAndOrSameType t, CanTestCertainly t) => [t] -> t +and = List.foldl' (&&) (convertExactly True) + +or :: (CanAndOrSameType t, CanTestCertainly t) => [t] -> t +or = List.foldl' (||) (convertExactly False) + +{-| Compound type constraint useful for test definition. -} +type CanAndOrX t1 t2 = + (CanAndOr t1 t2, + CanNeg t1, + CanNeg t2, + CanAndOr (NegType t1) t2, + CanAndOr t1 (NegType t2), + CanAndOr (NegType t1) (NegType t2), + CanTestCertainlyX t1, + CanTestCertainlyX t2, + CanTestCertainlyX (AndOrType t1 t2), + CanTestCertainlyX (NegType (AndOrType t1 t2)), + CanTestCertainlyX (AndOrType (NegType t1) t2), + CanTestCertainlyX (AndOrType t1 (NegType t2)), + CanTestCertainlyX (AndOrType (NegType t1) (NegType t2)) + ) + +{-| + HSpec properties that each implementation of CanAndOr should satisfy. + -} +specCanAndOr :: + (CanAndOrX t1 t1, + CanAndOrX t1 t2, CanAndOrX t2 t1, + CanAndOrX t1 t3, CanAndOrX t2 t3, + CanAndOrX (AndOrType t1 t2) t3, CanAndOrX t1 (AndOrType t2 t3), + CanAndOrX (AndOrType t1 t2) (AndOrType t1 t3)) + => + T t1 -> T t2 -> T t3 -> Spec +specCanAndOr (T typeName1 ::T t1) (T typeName2 :: T t2) (T typeName3 :: T t3) = + describe (printf "CanAndOr %s %s, CanAndOr %s %s" typeName1 typeName2 typeName2 typeName3) $ do + it "has idempotent ||" $ do + HSC.property $ \ (x :: t1) -> (x || x) `scEquals` x + it "has idempotent &&" $ do + HSC.property $ \ (x :: t1) -> (x && x) `scEquals` x + it "has commutative ||" $ do + HSC.property $ \ (x :: t1) (y :: t2) -> (x || y) `scEquals` (y || x) + it "has commutative &&" $ do + HSC.property $ \ (x :: t1) (y :: t2) -> (x && y) `scEquals` (y && x) + it "has associative ||" $ do + HSC.property $ \ (x :: t1) (y :: t2) (z :: t3) -> + (x || (y || z)) `scEquals` ((x || y) || z) + it "has associative &&" $ do + HSC.property $ \ (x :: t1) (y :: t2) (z :: t3) -> + (x && (y && z)) `scEquals` ((x && y) && z) + it "distributes || over &&" $ do + HSC.property $ \ (x :: t1) (y :: t2) (z :: t3) -> + (x || (y && z)) `scEquals` ((x || y) && (x || z)) + it "distributes && over ||" $ do + HSC.property $ \ (x :: t1) (y :: t2) (z :: t3) -> + (x && (y || z)) `scEquals` ((x && y) || (x && z)) + it "distributes not over ||" $ do + HSC.property $ \ (x :: t1) (y :: t2) -> (not (x || y)) `scEquals` ((not x) && (not y)) + it "distributes not over &&" $ do + HSC.property $ \ (x :: t1) (y :: t2) -> (not (x && y)) `scEquals` ((not x) || (not y)) + +{-| + HSpec properties that each implementation of CanAndOr should satisfy. + -} +specCanAndOrNotMixed :: + (CanAndOrX t t, + CanAndOrX (AndOrType t t) t, CanAndOrX t (AndOrType t t), + CanAndOrX (AndOrType t t) (AndOrType t t)) + => + T t -> Spec +specCanAndOrNotMixed t = specCanAndOr t t t + +instance CanAndOrAsymmetric Bool Bool where + type AndOrType Bool Bool = Bool + and2 = (P.&&) + or2 = (P.||) + +instance (CanAndOrAsymmetric t1 t2, CanTestCertainly t1, CanTestCertainly t2, CanTestCertainly (AndOrType t1 t2)) => + CanAndOrAsymmetric (Maybe t1) (Maybe t2) + where + type AndOrType (Maybe t1) (Maybe t2) = Maybe (AndOrType t1 t2) + and2 (Just b1) _ | isCertainlyFalse b1 = Just (convertExactly False) + and2 _ (Just b2) | isCertainlyFalse b2 = Just (convertExactly False) + and2 (Just b1) (Just b2) = Just (b1 && b2) + and2 _ _ = Nothing + or2 (Just b1) _ | isCertainlyTrue b1 = Just (convertExactly True) + or2 _ (Just b2) | isCertainlyTrue b2 = Just (convertExactly True) + or2 (Just b1) (Just b2) = Just (b1 || b2) + or2 _ _ = Nothing + +instance (CanAndOrAsymmetric Bool t2, CanTestCertainly t2, CanTestCertainly (AndOrType Bool t2)) => + CanAndOrAsymmetric Bool (Maybe t2) + where + type AndOrType Bool (Maybe t2) = Maybe (AndOrType Bool t2) + and2 False _ = Just (convertExactly False) + and2 _ (Just b2) | isCertainlyFalse b2 = Just (convertExactly False) + and2 b1 (Just b2) = Just (b1 && b2) + and2 _ _ = Nothing + or2 True _ = Just (convertExactly True) + or2 _ (Just b2) | isCertainlyTrue b2 = Just (convertExactly True) + or2 b1 (Just b2) = Just (b1 || b2) + or2 _ _ = Nothing + +instance (CanAndOrAsymmetric t1 Bool, CanTestCertainly t1, CanTestCertainly (AndOrType t1 Bool)) => + CanAndOrAsymmetric (Maybe t1) Bool + where + type AndOrType (Maybe t1) Bool = Maybe (AndOrType t1 Bool) + and2 _ False = Just (convertExactly False) + and2 (Just b1) _ | isCertainlyFalse b1 = Just (convertExactly False) + and2 (Just b1) b2 = Just (b1 && b2) + and2 _ _ = Nothing + or2 _ True = Just (convertExactly True) + or2 (Just b1) _ | isCertainlyTrue b1 = Just (convertExactly True) + or2 (Just b1) b2 = Just (b1 || b2) + or2 _ _ = Nothing + +_testAndOr1 :: Maybe Bool +_testAndOr1 = (Just True) && False + +_testAndOr2 :: Maybe (Maybe Bool) +_testAndOr2 = (Just (Just True)) || False + +_testAndOr3 :: Maybe Bool +_testAndOr3 = and [Just True, Nothing, Just False] + +{-| + A type constraint synonym that stipulates that the type behaves very + much like Bool, except it does not necessarily satisfy the law of excluded middle, + which means that the type can contain a "do-not-know" value. + + Examples: @Bool@, @Maybe Bool@, @Maybe (Maybe Bool)@ +-} +type IsBool t = (HasBools t, CanNegSameType t, CanAndOrSameType t) + +{-| + HSpec properties that each implementation of IsBool should satisfy. + -} +specIsBool :: (IsBool t, CanTestCertainly t, Show t, SCS.Serial IO t) => T t -> Spec +specIsBool t@(T typeName :: T t) = + describe (printf "IsBool %s" typeName) $ do + specCanTestCertainly t + specCanNegBool t + specCanAndOrNotMixed t + +scEquals :: + (Show t1, CanTestCertainly t1, Show t2, CanTestCertainly t2) => + t1 -> t2 -> Either String String +scEquals l r + | l `stronglyEquivalentTo` r = Right "OK" + | otherwise = Left $ printf "(%s) /= (%s)" (show l) (show r) diff --git a/src/Numeric/MixedTypes/Elementary.hs b/src/Numeric/MixedTypes/Elementary.hs new file mode 100644 --- /dev/null +++ b/src/Numeric/MixedTypes/Elementary.hs @@ -0,0 +1,343 @@ +{-| + Module : Numeric.MixedType.Elementary + Description : Bottom-up typed pi, sqrt, cos, etc + Copyright : (c) Michal Konecny + License : BSD3 + + Maintainer : mikkonecny@gmail.com + Stability : experimental + Portability : portable + +-} + +module Numeric.MixedTypes.Elementary +( + -- * Square root + CanSqrt(..), CanSqrtSameType, specCanSqrtReal + -- * Exp + , CanExp(..), CanExpSameType, specCanExpReal + -- * Log + , CanLog(..), CanLogSameType, specCanLogReal + , powUsingExpLog + -- * Sine and cosine + , CanSinCos(..), CanSinCosSameType, specCanSinCosReal + , approxPi +) +where + +import Numeric.MixedTypes.PreludeHiding +import qualified Prelude as P +import Text.Printf + +-- import qualified Data.List as List + +import Test.Hspec +import Test.QuickCheck + +import Numeric.MixedTypes.Literals +import Numeric.MixedTypes.Bool +import Numeric.MixedTypes.Eq +import Numeric.MixedTypes.Ord +-- import Numeric.MixedTypes.MinMaxSqrt +import Numeric.MixedTypes.AddSub +import Numeric.MixedTypes.Ring +import Numeric.MixedTypes.Field + +{---- sqrt -----} + +{-| + A replacement for Prelude's `P.sqrt`. If @Floating t@, + then one can use the default implementation to mirror Prelude's @sqrt@. +-} +class CanSqrt t where + type SqrtType t + type SqrtType t = t -- default + sqrt :: t -> SqrtType t + default sqrt :: (SqrtType t ~ t, P.Floating t) => t -> t + sqrt = P.sqrt + +type CanSqrtSameType t = (CanSqrt t, SqrtType t ~ t) + +type CanSqrtX t = + (CanSqrt t, + CanTestPosNeg t, + HasEqCertainly t (SqrtType t), + HasOrderCertainly Integer (SqrtType t), + Show t, Arbitrary t, Show (SqrtType t)) + +{-| + HSpec properties that each implementation of CanSqrt should satisfy. + -} +specCanSqrtReal :: + (CanSqrtX t, + CanPowX (SqrtType t) Integer, + HasEqCertainly t (PowType (SqrtType t) Integer)) + => + T t -> Spec +specCanSqrtReal (T typeName :: T t) = + describe (printf "CanSqrt %s" typeName) $ do + it "sqrt(x) >= 0" $ do + property $ \ (x :: t) -> + isCertainlyNonNegative x ==> + (sqrt x) ?>=?$ 0 + it "sqrt(x)^2 = x" $ do + property $ \ (x :: t) -> + isCertainlyNonNegative x ==> + (sqrt x)^2 ?==?$ x + where + infix 4 ?==?$ + (?==?$) :: (HasEqCertainlyAsymmetric a b, Show a, Show b) => a -> b -> Property + (?==?$) = printArgsIfFails2 "?==?" (?==?) + infix 4 ?>=?$ + (?>=?$) :: (HasOrderCertainlyAsymmetric a b, Show a, Show b) => a -> b -> Property + (?>=?$) = printArgsIfFails2 "?>=?" (?>=?) + +{- + Instances for Integer, Rational etc need an algebraic real or exact real type. + Such type is not provided in this package. See eg aern2-real. +-} + +instance CanSqrt Double -- not exact, will not pass the tests + +{---- exp -----} + +{-| + A replacement for Prelude's `P.exp`. If @Floating t@, + then one can use the default implementation to mirror Prelude's @exp@. +-} +class CanExp t where + type ExpType t + type ExpType t = t -- default + exp :: t -> ExpType t + default exp :: (ExpType t ~ t, P.Floating t) => t -> t + exp = P.exp + +type CanExpSameType t = (CanExp t, ExpType t ~ t) + +type CanExpX t = + (CanExp t, + Ring t, + Field (ExpType t), + CanTestPosNeg t, + CanTestPosNeg (ExpType t), + HasEqCertainly (ExpType t) (ExpType t), + HasOrderCertainly Integer t, + HasOrderCertainly Integer (ExpType t), + Show t, Arbitrary t, Show (ExpType t)) + +{-| + HSpec properties that each implementation of CanExp should satisfy. + -} +specCanExpReal :: + (CanExpX t) + => + T t -> Spec +specCanExpReal (T typeName :: T t) = + describe (printf "CanExp %s" typeName) $ do + it "exp(x) >= 0" $ do + property $ \ (x :: t) -> + ((-100000) ! + exp x ?>=?$ 0 + it "exp(-x) == 1/(exp x)" $ do + property $ \ (x :: t) -> + ((-100000) ! + (exp x !>! 0) ==> + exp (-x) ?==?$ 1/(exp x) + it "exp(x+y) = exp(x)*exp(y)" $ do + property $ \ (x :: t) (y :: t) -> + ((-100000) ! + (exp $ x + y) ?==?$ (exp x) * (exp y) + where + infix 4 ?==?$ + (?==?$) :: (HasEqCertainlyAsymmetric a b, Show a, Show b) => a -> b -> Property + (?==?$) = printArgsIfFails2 "?==?" (?==?) + infix 4 ?>=?$ + (?>=?$) :: (HasOrderCertainlyAsymmetric a b, Show a, Show b) => a -> b -> Property + (?>=?$) = printArgsIfFails2 "?>=?" (?>=?) + +{- + Instances for Integer, Rational etc need an algebraic real or exact real type. + Such type is not provided in this package. See eg aern2-real. +-} + +instance CanExp Double -- not exact, will not pass the tests + +{---- log -----} + +{-| + A replacement for Prelude's `P.log`. If @Floating t@, + then one can use the default implementation to mirror Prelude's @log@. +-} +class CanLog t where + type LogType t + type LogType t = t -- default + log :: t -> LogType t + default log :: (LogType t ~ t, P.Floating t) => t -> t + log = P.log + +type CanLogSameType t = (CanLog t, LogType t ~ t) + +type CanLogX t = + (CanLog t, + Field t, + Ring (LogType t), + HasOrderCertainly t Integer, + HasEqCertainly (LogType t) (LogType t), + Show t, Arbitrary t, Show (LogType t)) + +{-| + HSpec properties that each implementation of CanLog should satisfy. + -} +specCanLogReal :: + (CanLogX t, + CanLogX (DivType Integer t), + CanExp t, CanLogX (ExpType t), + HasEqCertainly t (LogType (ExpType t))) + => + T t -> Spec +specCanLogReal (T typeName :: T t) = + describe (printf "CanLog %s" typeName) $ do + it "log(1/x) == -(log x)" $ do + property $ \ (x :: t) -> + x !>! 0 && (1/x) !>! 0 ==> + log (1/x) ?==?$ -(log x) + it "log(x*y) = log(x)+log(y)" $ do + property $ \ (x :: t) (y :: t) -> + x !>! 0 && y !>! 0 && x*y !>! 0 ==> + (log $ x * y) ?==?$ (log x) + (log y) + it "log(exp x) == x" $ do + property $ \ (x :: t) -> + ((-100000) ! + log (exp x) ?==?$ x + where + infix 4 ?==?$ + (?==?$) :: (HasEqCertainlyAsymmetric a b, Show a, Show b) => a -> b -> Property + (?==?$) = printArgsIfFails2 "?==?" (?==?) + +{- + Instances for Integer, Rational etc need an algebraic real or exact real type. + Such type is not provided in this package. See eg aern2-real. +-} + +instance CanLog Double -- not exact, will not pass the tests + +instance CanPow Double Double where + pow = (P.**) + -- pow = powUsingExpLog +instance CanPow Double Rational where + type PowType Double Rational = Double + pow x y = x ^ (double y) +instance CanPow Rational Double where + type PowType Rational Double = Double + pow x y = (double x) ^ y +instance CanPow Integer Double where + type PowType Integer Double = Double + pow x y = (double x) ^ y +instance CanPow Int Double where + type PowType Int Double = Double + pow x y = (double x) ^ y + +powUsingExpLog :: + (CanTestPosNeg t1, + CanMulSameType t1, + HasIntegers t1, + CanTestZero t1, + CanRecipSameType t1, + CanTestInteger t2, + CanTestPosNeg t2, + CanMulAsymmetric (LogType t1) t2, + CanLog t1, + CanExp (MulType (LogType t1) t2), + ExpType (MulType (LogType t1) t2) ~ t1) + => + t1 -> t2 -> ExpType (MulType (LogType t1) t2) +powUsingExpLog x y + | isCertainlyPositive x = exp ((log x) * y) + | otherwise = + case certainlyIntegerGetIt y of + Just n -> + powUsingMulRecip x n + Nothing -> + if isCertainlyZero x && isCertainlyPositive y then convertExactly 0 + else + error $ "powUsingExpLog: potential illegal power a^b with negative a and non-integer b" + +{---- sine and cosine -----} + +{-| + A replacement for Prelude's `P.cos` and `P.sin`. If @Floating t@, + then one can use the default implementation to mirror Prelude's @sin@, @cos@. +-} +class CanSinCos t where + type SinCosType t + type SinCosType t = t -- default + cos :: t -> SinCosType t + default cos :: (SinCosType t ~ t, P.Floating t) => t -> t + cos = P.cos + sin :: t -> SinCosType t + default sin :: (SinCosType t ~ t, P.Floating t) => t -> t + sin = P.sin + +type CanSinCosSameType t = (CanSinCos t, SinCosType t ~ t) + +type CanSinCosX t = + (CanSinCos t, + OrderedCertainlyField t, + OrderedCertainlyField (SinCosType t), + HasOrderCertainly (SinCosType t) t, + Show t, Arbitrary t, Show (SinCosType t)) + +{-| + HSpec properties that each implementation of CanSinCos should satisfy. + + Derived partially from + http://math.stackexchange.com/questions/1303044/axiomatic-definition-of-sin-and-cos + -} +specCanSinCosReal :: + (CanSinCosX t) + => + T t -> Spec +specCanSinCosReal (T typeName :: T t) = + describe (printf "CanSinCos %s" typeName) $ do + it "-1 <= sin(x) <= 1" $ do + property $ \ (x :: t) -> + (-1) ?<=?$ (sin x) .&&. (sin x) ?<=?$ 1 + it "-1 <= cos(x) <= 1" $ do + property $ \ (x :: t) -> + (-1) ?<=?$ (cos x) .&&. (cos x) ?<=?$ 1 + it "cos(x)^2 + sin(x)^2 = 1" $ do + property $ \ (x :: t) -> + (sin x)^2 + (cos x)^2 ?==?$ 1 + it "sin(x-y) = sin(x)cos(y) - cos(x)sin(y)" $ do + property $ \ (x :: t) (y :: t) -> + (sin $ x - y) ?==?$ (sin x)*(cos y) - (cos x)*(sin y) + it "cos(x-y) = cos(x)cos(y) + sin(x)sin(y)" $ do + property $ \ (x :: t) (y :: t) -> + (cos $ x - y) ?==?$ (cos x)*(cos y) + (sin x)*(sin y) + it "sin(x) < x < tan(x) for x in [0,pi/2]" $ do + property $ \ (x :: t) -> + x !>=! 0 && x !<=! 1.57 && (cos x) !>! 0 ==> + (sin x) ?<=?$ x .&&. x ?<=?$ (sin x)/(cos x) + where + infix 4 ?==?$ + (?==?$) :: (HasEqCertainlyAsymmetric a b, Show a, Show b) => a -> b -> Property + (?==?$) = printArgsIfFails2 "?==?" (?==?) + infix 4 ?<=?$ + (?<=?$) :: (HasOrderCertainlyAsymmetric a b, Show a, Show b) => a -> b -> Property + (?<=?$) = printArgsIfFails2 "?<=?" (?<=?) + +{- + Instances for Integer, Rational etc need an algebraic real or exact real type. + Such type is not provided in this package. See eg aern2-real. +-} + +instance CanSinCos Double -- not exact, will not pass the tests + +{-| + Approximate pi, synonym for Prelude's `P.pi`. + + We do not define (exect) @pi@ in this package as we have no type + that can represent it exactly. +-} +approxPi :: (P.Floating t) => t +approxPi = P.pi diff --git a/src/Numeric/MixedTypes/Eq.hs b/src/Numeric/MixedTypes/Eq.hs new file mode 100644 --- /dev/null +++ b/src/Numeric/MixedTypes/Eq.hs @@ -0,0 +1,359 @@ +{-| + Module : Numeric.MixedType.Eq + Description : Bottom-up typed equality comparisons + Copyright : (c) Michal Konecny + License : BSD3 + + Maintainer : mikkonecny@gmail.com + Stability : experimental + Portability : portable + +-} + +module Numeric.MixedTypes.Eq +( + -- * Equality checks + HasEq, HasEqAsymmetric(..), (==), (/=) + , HasEqCertainly, HasEqCertainlyAsymmetric + , notCertainlyDifferentFrom, certainlyEqualTo, certainlyNotEqualTo + , (?==?), (!==!), (!/=!) + -- ** Tests + , specHasEq, specHasEqNotMixed, HasEqX + , specConversion + -- ** Specific comparisons + , CanTestFinite(..) + , CanTestInteger(..) + , CanTestZero(..), specCanTestZero + , CanPickNonZero(..), specCanPickNonZero +) +where + +import Numeric.MixedTypes.PreludeHiding +import qualified Prelude as P +import Text.Printf +import Data.Ratio + +import Test.Hspec +import Test.QuickCheck as QC +import Control.Exception (evaluate) + +import Numeric.MixedTypes.Literals +import Numeric.MixedTypes.Bool + +infix 4 ==, /= +infix 4 ?==? +infix 4 !==!, !/=! + +{---- Equality tests -----} + +type HasEq t1 t2 = + (HasEqAsymmetric t1 t2, HasEqAsymmetric t2 t1, + EqCompareType t1 t2 ~ EqCompareType t2 t1) + +type HasEqCertainlyAsymmetric t1 t2 = + (HasEqAsymmetric t1 t2, CanTestCertainly (EqCompareType t1 t2)) + +type HasEqCertainly t1 t2 = + (HasEq t1 t2, CanTestCertainly (EqCompareType t1 t2)) + +class (IsBool (EqCompareType a b)) => HasEqAsymmetric a b where + type EqCompareType a b + type EqCompareType a b = Bool -- default + equalTo :: a -> b -> (EqCompareType a b) + -- default equalToA via Prelude for (->) and Bool: + default equalTo :: (EqCompareType a b ~ Bool, a~b, P.Eq a) => a -> b -> Bool + equalTo = (P.==) + notEqualTo :: a -> b -> (EqCompareType a b) + -- default notEqualToA via equalToA for Bool: + default notEqualTo :: + (CanNegSameType (EqCompareType a b)) => + a -> b -> (EqCompareType a b) + notEqualTo a b = not $ equalTo a b + +(==) :: (HasEqAsymmetric a b) => a -> b -> EqCompareType a b +(==) = equalTo +(/=) :: (HasEqAsymmetric a b) => a -> b -> EqCompareType a b +(/=) = notEqualTo + +certainlyEqualTo :: (HasEqCertainlyAsymmetric a b) => a -> b -> Bool +certainlyEqualTo a b = isCertainlyTrue $ a == b +certainlyNotEqualTo :: (HasEqCertainlyAsymmetric a b) => a -> b -> Bool +certainlyNotEqualTo a b = isCertainlyTrue $ a /= b +notCertainlyDifferentFrom :: (HasEqCertainlyAsymmetric a b) => a -> b -> Bool +notCertainlyDifferentFrom a b = isNotFalse $ a == b + +(?==?) :: (HasEqCertainlyAsymmetric a b) => a -> b -> Bool +(?==?) = notCertainlyDifferentFrom + +(!==!) :: (HasEqCertainlyAsymmetric a b) => a -> b -> Bool +(!==!) = certainlyEqualTo + +(!/=!) :: (HasEqCertainlyAsymmetric a b) => a -> b -> Bool +(!/=!) = certainlyNotEqualTo + +{-| Compound type constraint useful for test definition. -} +type HasEqX t1 t2 = + (HasEqCertainly t1 t2, Show t1, Arbitrary t1, Show t2, Arbitrary t2) + +{-| + HSpec properties that each implementation of HasEq should satisfy. + -} +specHasEq :: + (HasEqX t1 t1, + HasEqX t1 t2, HasEqX t2 t1, + HasEqX t1 t3, HasEqX t2 t3, + CanAndOrX (EqCompareType t1 t2) (EqCompareType t2 t3)) + => + T t1 -> T t2 -> T t3 -> Spec +specHasEq (T typeName1 :: T t1) (T typeName2 :: T t2) (T typeName3 :: T t3) = + describe (printf "HasEq %s %s, HasEq %s %s" typeName1 typeName2 typeName2 typeName3) $ do + it "has reflexive ==" $ do + property $ \ (x :: t1) -> not $ isCertainlyFalse (x == x) + it "has anti-reflexive /=" $ do + property $ \ (x :: t1) -> not $ isCertainlyTrue (x /= x) + it "has stronly commutative ==" $ do + property $ \ (x :: t1) (y :: t2) -> (x == y) `stronglyEquivalentTo` (y == x) + it "has stronly commutative /=" $ do + property $ \ (x :: t1) (y :: t2) -> (x /= y) `stronglyEquivalentTo` (y /= x) + it "has stronly transitive ==" $ do + property $ \ (x :: t1) (y :: t2) (z :: t3) -> ((x == y) && (y == z)) `stronglyImplies` (y == z) + +{-| + HSpec properties that each implementation of HasEq should satisfy. + -} +specHasEqNotMixed :: + (HasEqX t t, + CanAndOrX (EqCompareType t t) (EqCompareType t t)) + => + T t -> Spec +specHasEqNotMixed t = specHasEq t t t + +{-| + HSpec property of there-and-back conversion. +-} +specConversion :: -- this definition cannot be in Literals because it needs HasEq + (Arbitrary t1, Show t1, HasEqCertainly t1 t1) => + T t1 -> T t2 -> (t1 -> t2) -> (t2 -> t1) -> Spec +specConversion (T typeName1 :: T t1) (T typeName2 :: T t2) conv12 conv21 = + describe "conversion" $ do + it (printf "%s -> %s -> %s" typeName1 typeName2 typeName1) $ do + property $ \ (x1 :: t1) -> + x1 ?==? (conv21 $ conv12 x1) + +instance HasEqAsymmetric () () +instance HasEqAsymmetric Bool Bool +instance HasEqAsymmetric Char Char + +instance HasEqAsymmetric Int Int +instance HasEqAsymmetric Integer Integer +instance HasEqAsymmetric Rational Rational +instance HasEqAsymmetric Double Double + +instance HasEqAsymmetric Int Integer where + equalTo = convertFirst equalTo +instance HasEqAsymmetric Integer Int where + equalTo = convertSecond equalTo + +instance HasEqAsymmetric Int Rational where + equalTo = convertFirst equalTo +instance HasEqAsymmetric Rational Int where + equalTo = convertSecond equalTo + +instance HasEqAsymmetric Integer Rational where + equalTo = convertFirst equalTo +instance HasEqAsymmetric Rational Integer where + equalTo = convertSecond equalTo + +instance HasEqAsymmetric Integer Double where + equalTo n d = ((P.floor d :: Integer) == n) && (n == (P.ceiling d :: Integer)) +instance HasEqAsymmetric Double Integer where + equalTo d n = ((P.floor d :: Integer) == n) && (n == (P.ceiling d :: Integer)) + +instance HasEqAsymmetric Int Double where + equalTo n d = equalTo (integer n) d +instance HasEqAsymmetric Double Int where + equalTo d n = equalTo (integer n) d + +instance + (HasEqAsymmetric a1 b1, + HasEqAsymmetric a2 b2, + CanAndOrAsymmetric (EqCompareType a1 b1) (EqCompareType a2 b2), + IsBool (AndOrType (EqCompareType a1 b1) (EqCompareType a2 b2)) + ) => + HasEqAsymmetric (a1,a2) (b1,b2) where + type EqCompareType (a1,a2) (b1,b2) = + AndOrType (EqCompareType a1 b1) (EqCompareType a2 b2) + equalTo (a1,a2) (b1,b2) = + (a1 == b1) && (a2 == b2) + +instance + (HasEqAsymmetric ((a1,a2), a3) ((b1,b2), b3)) + => + HasEqAsymmetric (a1,a2,a3) (b1,b2,b3) where + type EqCompareType (a1,a2,a3) (b1,b2,b3) = + EqCompareType ((a1,a2), a3) ((b1,b2), b3) + equalTo (a1,a2,a3) (b1,b2,b3) = + ((a1,a2), a3) == ((b1,b2), b3) + +instance + (HasEqAsymmetric ((a1,a2,a3), a4) ((b1,b2,b3), b4)) + => + HasEqAsymmetric (a1,a2,a3,a4) (b1,b2,b3,b4) where + type EqCompareType (a1,a2,a3,a4) (b1,b2,b3,b4) = + EqCompareType ((a1,a2,a3), a4) ((b1,b2,b3), b4) + equalTo (a1,a2,a3,a4) (b1,b2,b3,b4) = + ((a1,a2,a3), a4) == ((b1,b2,b3), b4) + +instance + (HasEqAsymmetric ((a1,a2,a3,a4), a5) ((b1,b2,b3,b4), b5)) + => + HasEqAsymmetric (a1,a2,a3,a4,a5) (b1,b2,b3,b4,b5) where + type EqCompareType (a1,a2,a3,a4,a5) (b1,b2,b3,b4,b5) = + EqCompareType ((a1,a2,a3,a4), a5) ((b1,b2,b3,b4), b5) + equalTo (a1,a2,a3,a4,a5) (b1,b2,b3,b4,b5) = + ((a1,a2,a3,a4), a5) == ((b1,b2,b3,b4), b5) + +instance (HasEqAsymmetric a b) => HasEqAsymmetric [a] [b] where + type EqCompareType [a] [b] = EqCompareType a b + equalTo [] [] = convertExactly True + equalTo (x:xs) (y:ys) = (x == y) && (xs == ys) + equalTo _ _ = convertExactly False + +instance (HasEqAsymmetric a b) => HasEqAsymmetric (Maybe a) (Maybe b) where + type EqCompareType (Maybe a) (Maybe b) = EqCompareType a b + equalTo Nothing Nothing = convertExactly True + equalTo (Just x) (Just y) = (x == y) + equalTo _ _ = convertExactly False + +{---- Checking whether it is finite -----} + +class CanTestFinite t where + isNaN :: t -> Bool + default isNaN :: (P.RealFloat t) => t -> Bool + isNaN = P.isNaN + isInfinite :: t -> Bool + default isInfinite :: (P.RealFloat t) => t -> Bool + isInfinite = P.isInfinite + isFinite :: t -> Bool + isFinite x = (not $ isNaN x) && (not $ isInfinite x) + +instance CanTestFinite Double +instance CanTestFinite Rational where + isNaN = const False + isInfinite = const False + +{---- Checking whether it is an integer -----} + +class CanTestInteger t where + certainlyNotInteger :: t -> Bool + certainlyInteger :: t -> Bool + certainlyInteger s = case certainlyIntegerGetIt s of Just _ -> True; _ -> False + certainlyIntegerGetIt :: t -> Maybe Integer + +instance CanTestInteger Integer where + certainlyNotInteger _ = False + certainlyInteger _ = True + certainlyIntegerGetIt n = Just n + +instance CanTestInteger Int where + certainlyNotInteger _ = False + certainlyInteger _ = True + certainlyIntegerGetIt n = Just (integer n) + +instance CanTestInteger Rational where + certainlyNotInteger q = (denominator q /= 1) + certainlyInteger q = (denominator q == 1) + certainlyIntegerGetIt q + | denominator q == 1 = Just (numerator q) + | otherwise = Nothing + +instance CanTestInteger Double where + certainlyNotInteger d = + isInfinite d || isNaN d || + (P.floor d :: Integer) P.< P.ceiling d + certainlyIntegerGetIt d + | isFinite d && (dF P.== dC) = Just dF + | otherwise = Nothing + where + dF = P.floor d + dC = P.ceiling d + +{---- Checking whether it is zero -----} + +class CanTestZero t where + isCertainlyZero :: t -> Bool + isNonZero :: t -> Bool + default isCertainlyZero :: (HasEqCertainly t Integer) => t -> Bool + isCertainlyZero a = isCertainlyTrue (a == 0) + default isNonZero :: (HasEqCertainly t Integer) => t -> Bool + isNonZero a = isCertainlyTrue (a /= 0) + +{-| + HSpec properties that each implementation of CanTestZero should satisfy. + -} +specCanTestZero :: + (CanTestZero t, ConvertibleExactly Integer t) + => + T t -> Spec +specCanTestZero (T typeName :: T t) = + describe (printf "CanTestZero %s" typeName) $ do + it "converted non-zero Integer is not isCertainlyZero" $ do + property $ \ (x :: Integer) -> + x /= 0 ==> (not $ isCertainlyZero (convertExactly x :: t)) + it "converted non-zero Integer is isNonZero" $ do + property $ \ (x :: Integer) -> + x /= 0 ==> (isNonZero (convertExactly x :: t)) + it "converted 0.0 is not isNonZero" $ do + (isNonZero (convertExactly 0 :: t)) `shouldBe` False + +instance CanTestZero Int +instance CanTestZero Integer +instance CanTestZero Rational +instance CanTestZero Double + +class CanPickNonZero t where + {-| + Given a list @[(a1,b1),(a2,b2),...]@ and assuming that + at least one of @a1,a2,...@ is non-zero, pick one of them + and return the corresponding pair @(ai,bi)@. + + If none of @a1,a2,...@ is zero, either throws an exception + or loops forever. + + The default implementation is based on a `CanTestZero` instance + and is not parallel. + -} + pickNonZero :: [(t,s)] -> (t,s) + default pickNonZero :: (CanTestZero t, Show t) => [(t,s)] -> (t,s) + pickNonZero list = + case aux list of + Just result -> result + Nothing -> + error $ "pickNonZero: failed to find a non-zero element in " + ++ show (map fst list) + where + aux ((a,b):rest) + | isNonZero a = Just (a,b) + | otherwise = aux rest + aux [] = Nothing + +{-| + HSpec properties that each implementation of CanPickNonZero should satisfy. + -} +specCanPickNonZero :: + (CanPickNonZero t, CanTestZero t, ConvertibleExactly Integer t, Show t, Arbitrary t) + => + T t -> Spec +specCanPickNonZero (T typeName :: T t) = + describe (printf "CanPickNonZero %s" typeName) $ do + it "picks a non-zero element if there is one" $ do + property $ \ (xs :: [(t, ())]) -> + or (map (isNonZero . fst) xs) -- if at least one is non-zero + ==> (isNonZero $ fst $ pickNonZero xs) + it "throws exception when all the elements are 0" $ do + (evaluate $ pickNonZero [(convertExactly i :: t, ()) | i <- [0,0,0]]) + `shouldThrow` anyException + +instance CanPickNonZero Int +instance CanPickNonZero Integer +instance CanPickNonZero Rational diff --git a/src/Numeric/MixedTypes/Field.hs b/src/Numeric/MixedTypes/Field.hs new file mode 100644 --- /dev/null +++ b/src/Numeric/MixedTypes/Field.hs @@ -0,0 +1,225 @@ +{-| + Module : Numeric.MixedType.Field + Description : Bottom-up typed division + Copyright : (c) Michal Konecny + License : BSD3 + + Maintainer : mikkonecny@gmail.com + Stability : experimental + Portability : portable + +-} + +module Numeric.MixedTypes.Field +( + -- * Field + CanAddSubMulDivBy, Field, CertainlyEqField, OrderedField, OrderedCertainlyField + -- * Division + , CanDiv(..), CanDivBy, CanDivSameType, CanRecip, CanRecipSameType + , (/), recip + , powUsingMulRecip + -- ** Tests + , specCanDiv, specCanDivNotMixed, CanDivX +) +where + +import Numeric.MixedTypes.PreludeHiding +import qualified Prelude as P +import Text.Printf + +-- import qualified Data.List as List + +import Test.Hspec +import Test.QuickCheck + +import Numeric.MixedTypes.Literals +import Numeric.MixedTypes.Bool +import Numeric.MixedTypes.Eq +import Numeric.MixedTypes.Ord +-- import Numeric.MixedTypes.MinMaxAbs +-- import Numeric.MixedTypes.AddSub +import Numeric.MixedTypes.Ring + +{----- Field -----} + +type CanAddSubMulDivBy t s = + (CanAddSubMulBy t s, CanDivBy t s) + +type Field t = + (Ring t, CanDivSameType t, CanRecipSameType t, + CanAddSubMulDivBy t Rational, + CanAddSubMulDivBy t Integer, + CanAddSubMulDivBy t Int + ) + +type CertainlyEqField t = (Field t, CertainlyEqRing t) + +type OrderedField t = + (Field t, OrderedRing t, HasOrder t Rational) + +type OrderedCertainlyField t = + (CertainlyEqField t, OrderedCertainlyRing t, HasOrderCertainly t Rational) + +{---- Division -----} + +{-| + A replacement for Prelude's binary `P./`. If @t1 = t2@ and @Fractional t1@, + then one can use the default implementation to mirror Prelude's @/@. +-} +class CanDiv t1 t2 where + type DivType t1 t2 + type DivType t1 t2 = t1 -- default + divide :: t1 -> t2 -> DivType t1 t2 + default divide :: (DivType t1 t2 ~ t1, t1~t2, P.Fractional t1) => t1 -> t1 -> t1 + divide = (P./) + +(/) :: (CanDiv t1 t2) => t1 -> t2 -> DivType t1 t2 +(/) = divide + +type CanRecip t = + (CanDiv Integer t) + +type CanRecipSameType t = + (CanDiv Integer t, DivType Integer t ~ t) + +recip :: (CanRecip t) => t -> DivType Integer t +recip = divide 1 + +type CanDivBy t1 t2 = + (CanDiv t1 t2, DivType t1 t2 ~ t1) +type CanDivSameType t = + CanDivBy t t + +{-| Compound type constraint useful for test definition. -} +type CanDivX t1 t2 = + (CanDiv t1 t2, + Show t1, Arbitrary t1, + Show t2, Arbitrary t2, + Show (DivType t1 t2), + HasEqCertainly t1 (DivType t1 t2)) + +{-| + HSpec properties that each implementation of CanDiv should satisfy. + -} +specCanDiv :: + (CanRecip t1, CanRecip (DivType Integer t1), + Show (DivType Integer (DivType Integer t1)), + HasEqCertainly t1 (DivType Integer (DivType Integer t1)), + CanTestZero (DivType Integer t1), + CanDivX t1 t2, + CanTestZero t1, + CanTestZero t2, + CanDivX t1 t1, + CanMulX t1 (DivType t1 t2), + ConvertibleExactly Integer t2, ConvertibleExactly Integer t1) + => + T t1 -> T t2 -> Spec +specCanDiv (T typeName1 :: T t1) (T typeName2 :: T t2) = + describe (printf "CanDiv %s %s" typeName1 typeName2) $ do + it "recip(recip x) = x" $ do + property $ \ (x :: t1) -> + (isNonZero x && isNonZero (recip x)) ==> + recip (recip x) ?==?$ x + it "x/1 = x" $ do + property $ \ (x :: t1) -> let one = (convertExactly 1 :: t2) in (x / one) ?==?$ x + it "x/x = 1" $ do + property $ \ (x :: t1) -> + (isNonZero x) ==> + let one = (convertExactly 1 :: t1) in (x / x) ?==?$ one + it "x/y = x*(1/y)" $ do + property $ \ (x :: t1) (y :: t2) -> + (isNonZero y) ==> + let one = (convertExactly 1 :: t1) in (x / y) ?==?$ x * (one/y) + where + infix 4 ?==?$ + (?==?$) :: (HasEqCertainlyAsymmetric a b, Show a, Show b) => a -> b -> Property + (?==?$) = printArgsIfFails2 "?==?" (?==?) + +{-| + HSpec properties that each implementation of CanDiv should satisfy. + -} +specCanDivNotMixed :: + (CanRecip t, CanRecip (DivType Integer t), + Show (DivType Integer (DivType Integer t)), + HasEqCertainly t (DivType Integer (DivType Integer t)), + CanTestZero (DivType Integer t), + CanDivX t t, + CanTestZero t, + CanMulX t (DivType t t), + ConvertibleExactly Integer t) + => + T t -> Spec +specCanDivNotMixed t = specCanDiv t t + +instance CanDiv Int Int where + type DivType Int Int = Rational + divide a b = (rational a) P./ (rational b) + +instance CanDiv Integer Integer where + type DivType Integer Integer = Rational + divide a b = (rational a) P./ (rational b) +instance CanDiv Rational Rational +instance CanDiv Double Double + +instance CanDiv Int Integer where + type DivType Int Integer = Rational + divide a b = (rational a) P./ (rational b) +instance CanDiv Integer Int where + type DivType Integer Int = Rational + divide a b = (rational a) P./ (rational b) + +instance CanDiv Int Rational where + type DivType Int Rational = Rational + divide = convertFirst divide +instance CanDiv Rational Int where + type DivType Rational Int = Rational + divide = convertSecond divide + +instance CanDiv Integer Rational where + type DivType Integer Rational = Rational + divide = convertFirst divide +instance CanDiv Rational Integer where + type DivType Rational Integer = Rational + divide = convertSecond divide + +instance CanDiv Int Double where + type DivType Int Double = Double + divide = convertFirst divide +instance CanDiv Double Int where + type DivType Double Int = Double + divide = convertSecond divide + +instance CanDiv Integer Double where + type DivType Integer Double = Double + divide = convertFirst divide +instance CanDiv Double Integer where + type DivType Double Integer = Double + divide = convertSecond divide + +instance CanDiv Rational Double where + type DivType Rational Double = Double + divide = convertFirst divide +instance CanDiv Double Rational where + type DivType Double Rational = Double + divide = convertSecond divide + +instance (CanDiv a b) => CanDiv [a] [b] where + type DivType [a] [b] = [DivType a b] + divide (x:xs) (y:ys) = (divide x y) : (divide xs ys) + divide _ _ = [] + +instance (CanDiv a b) => CanDiv (Maybe a) (Maybe b) where + type DivType (Maybe a) (Maybe b) = Maybe (DivType a b) + divide (Just x) (Just y) = Just (divide x y) + divide _ _ = Nothing + +powUsingMulRecip :: + (CanBeInteger e, + CanRecipSameType t, CanMulSameType t, ConvertibleExactly Integer t) + => + t -> e -> t +powUsingMulRecip x nPre + | n < 0 = recip $ powUsingMul x (negate n) + | otherwise = powUsingMul x n + where + n = integer nPre diff --git a/src/Numeric/MixedTypes/Literals.hs b/src/Numeric/MixedTypes/Literals.hs new file mode 100644 --- /dev/null +++ b/src/Numeric/MixedTypes/Literals.hs @@ -0,0 +1,242 @@ +{-| + Module : Numeric.MixedType.Literals + Description : Fixed-type numeric literals, conversions + Copyright : (c) Michal Konecny + License : BSD3 + + Maintainer : mikkonecny@gmail.com + Stability : experimental + Portability : portable + + This module defines fixed-type integer and rational literals. + This is useful when deriving the type of an expression bottom-up. + Eg we would not be able to write @1 < x@ + when the type of @<@ does not force the two sides to be of the + same type. We would need to write eg @(1::Integer) < x@ with + Prelude's generic literals. + + Moreover, convenient conversion functions are provided for + the most common numeric types. Thus one can say eg: + + * @take (int 1)@ + * @integer (length list)@. + * @double 0.5@ + + To avoid integer overflow, no aritmetic operations return 'Int'. + Nevertheless, one can usually mix 'Int' with other types in expressions. + + Any approximate arithmetic, ie arithmetic involving Doubles, returns + values of type 'Double'. + 'Double' values cannot be easily converted to exact + types such as 'Rational' or 'Integer' so that all such + conversions are clearly visible as labelled as inexact. +-} + +module Numeric.MixedTypes.Literals +( + -- * Fixed-type literals + fromInteger, fromRational + , ifThenElse + -- * Convenient conversions + , CanBeInteger, integer, integers, HasIntegers, fromInteger_ + , CanBeInt, int, ints + , CanBeRational, rational, rationals, HasRationals, fromRational_ + , CanBeDouble, double, doubles + , ConvertibleExactly(..), convertExactly, ConvertResult, ConvertError, convError + -- * Generic list index + , (!!), specCanBeInteger, printArgsIfFails2 + -- * Testing support functions + , T(..), tInt, tInteger, tRational, tDouble + , tBool, tMaybeBool, tMaybeMaybeBool + -- * Helper functions + , convertFirst, convertSecond + , convertFirstUsing, convertSecondUsing +) +where + +import Numeric.MixedTypes.PreludeHiding +import qualified Prelude as P +import Text.Printf + +import Data.Convertible (Convertible(..), convert, ConvertResult, ConvertError, convError) + +import qualified Data.List as List + +import Test.Hspec +import Test.QuickCheck +-- import Control.Exception (evaluate) + +{-| Replacement for 'Prelude.fromInteger' using the RebindableSyntax extension. + This version of fromInteger arranges that integer literals + are always of type 'Integer'. +-} +fromInteger :: Integer -> Integer +fromInteger = id + +{-| Replacement for 'Prelude.fromRational' using the RebindableSyntax extension. + This version of fromRational arranges that rational literals are + always of type 'Rational'. -} +fromRational :: Rational -> Rational +fromRational = id + +{-| + Restore if-then-else with RebindableSyntax +-} +ifThenElse :: Bool -> t -> t -> t +ifThenElse b e1 e2 + | b = e1 + | otherwise = e2 + +_testIf1 :: String +_testIf1 = if True then "yes" else "no" + +{---- Numeric conversions -----} + +type CanBeInteger t = ConvertibleExactly t Integer +integer :: (CanBeInteger t) => t -> Integer +integer = convertExactly +integers :: (CanBeInteger t) => [t] -> [Integer] +integers = map convertExactly + +type HasIntegers t = ConvertibleExactly Integer t +fromInteger_ :: (HasIntegers t) => Integer -> t +fromInteger_ = convertExactly + +(!!) :: (CanBeInteger t) => [a] -> t -> a +list !! ix = List.genericIndex list (integer ix) +-- list !! ix = List.genericIndex list (P.max 0 ((integer ix) P.- 1)) -- deliberately wrong - test the test! + +{-| + HSpec properties that each implementation of CanBeInteger should satisfy. + -} +specCanBeInteger :: + (CanBeInteger t, Show t, Arbitrary t) => + T t -> Spec +specCanBeInteger (T typeName :: T t) = + describe "generic list index (!!)" $ do + it (printf "works using %s index" typeName) $ do + property $ \ (x :: t) -> let xi = integer x in (xi P.>= 0) ==> ([0..xi] !! x) ==$ xi + where + (==$) = printArgsIfFails2 "==" (P.==) + +printArgsIfFails2 :: + (Testable prop, Show a, Show b) => + String -> (a -> b -> prop) -> (a -> b -> Property) +printArgsIfFails2 relName rel a b = + counterexample argsReport $ a `rel` b + where + argsReport = + "FAILED REL: (" ++ show a ++ ") " ++ relName ++ " (" ++ show b ++ ")" + +type CanBeInt t = ConvertibleExactly t Int +int :: (CanBeInt t) => t -> Int +int = convertExactly +ints :: (CanBeInt t) => [t] -> [Int] +ints = map convertExactly + +type CanBeRational t = ConvertibleExactly t Rational +rational :: (CanBeRational t) => t -> Rational +rational = convertExactly +rationals :: (CanBeRational t) => [t] -> [Rational] +rationals = map convertExactly + +type HasRationals t = ConvertibleExactly Rational t +fromRational_ :: (HasRationals t) => Rational -> t +fromRational_ = convertExactly + +type CanBeDouble t = Convertible t Double +double :: (CanBeDouble t) => t -> Double +double = convert +doubles :: (CanBeDouble t) => [t] -> [Double] +doubles = map convert + +{-| +Define our own ConvertibleExactly since convertible is too relaxed for us. +For example, convertible allows conversion from Rational to Integer, +rounding to nearest integer. We prefer to allow only exact conversions. +-} +class ConvertibleExactly t1 t2 where + safeConvertExactly :: t1 -> ConvertResult t2 + default safeConvertExactly :: (Convertible t1 t2) => t1 -> ConvertResult t2 + safeConvertExactly = safeConvert + +convertExactly :: (ConvertibleExactly t1 t2) => t1 -> t2 +convertExactly a = + case safeConvertExactly a of + Right v -> v + Left err -> error (show err) + +instance ConvertibleExactly Integer Integer -- use CVT instance by default +instance ConvertibleExactly Int Integer + +instance ConvertibleExactly Int Int where + safeConvertExactly n = Right n +instance ConvertibleExactly Rational Rational where + safeConvertExactly q = Right q + +instance ConvertibleExactly Integer Int +instance ConvertibleExactly Int Rational +instance ConvertibleExactly Integer Rational + +instance ConvertibleExactly Int Double +instance ConvertibleExactly Integer Double +instance ConvertibleExactly Rational Double +instance ConvertibleExactly Double Double where + safeConvertExactly d = Right d + +{-- we deliberately do not allow converions from Double to any other type --} + +{-- auxiliary type and functions for specifying type(s) to use in tests --} + +{-| + A runtime representative of type @t@. + Used for specialising polymorphic tests to concrete types. +-} +data T t = T String + +tInt :: T Int +tInt = T "Int" + +tInteger :: T Integer +tInteger = T "Integer" + +tRational :: T Rational +tRational = T "Rational" + +tDouble :: T Double +tDouble = T "Double" + +tBool :: T Bool +tBool = T "Bool" + +tMaybeBool :: T (Maybe Bool) +tMaybeBool = T "(Maybe Bool)" + +tMaybeMaybeBool :: T (Maybe (Maybe Bool)) +tMaybeMaybeBool = T "(Maybe (Maybe Bool))" + +{---- Auxiliary functions ----} + +convertFirstUsing :: + (a -> b -> b) {-^ conversion function -} -> + (b -> b -> c) {-^ same-type operation -} -> + (a -> b -> c) {-^ mixed-type operation -} +convertFirstUsing conv op a b = op (conv a b) b + +convertSecondUsing :: + (a -> b -> a) {-^ conversion function -} -> + (a -> a -> c) {-^ same-type operation -} -> + (a -> b -> c) {-^ mixed-type operation -} +convertSecondUsing conv op a b = op a (conv a b) + +convertFirst :: + (ConvertibleExactly a b) => + (b -> b -> c) {-^ same-type operation -} -> + (a -> b -> c) {-^ mixed-type operation -} +convertFirst = convertFirstUsing (\ a _ -> convertExactly a) + +convertSecond :: + (ConvertibleExactly b a) => + (a -> a -> c) {-^ same-type operation -} -> + (a -> b -> c) {-^ mixed-type operation -} +convertSecond = convertSecondUsing (\ _ b -> convertExactly b) diff --git a/src/Numeric/MixedTypes/MinMaxAbs.hs b/src/Numeric/MixedTypes/MinMaxAbs.hs new file mode 100644 --- /dev/null +++ b/src/Numeric/MixedTypes/MinMaxAbs.hs @@ -0,0 +1,300 @@ +{-| + Module : Numeric.MixedType.MinMaxAbs + Description : Bottom-up typed min, max and abs + Copyright : (c) Michal Konecny + License : BSD3 + + Maintainer : mikkonecny@gmail.com + Stability : experimental + Portability : portable + +-} + +module Numeric.MixedTypes.MinMaxAbs +( + -- * Minimum and maximum + CanMinMax, CanMinMaxAsymmetric(..), CanMinMaxThis, CanMinMaxSameType + , minimum, maximum + -- ** Tests + , specCanMinMax, specCanMinMaxNotMixed, CanMinMaxX, CanMinMaxXX + -- * Absolute value + , CanAbs(..), CanAbsSameType + -- ** Tests + , specCanNegNum, specCanAbs +) +where + +import Numeric.MixedTypes.PreludeHiding +import qualified Prelude as P +import Text.Printf + +import qualified Data.List as List + +import Test.Hspec +import Test.QuickCheck + +import Numeric.MixedTypes.Literals +import Numeric.MixedTypes.Bool +import Numeric.MixedTypes.Eq +import Numeric.MixedTypes.Ord + +{---- Min and max -----} + +type CanMinMax t1 t2 = + (CanMinMaxAsymmetric t1 t2, CanMinMaxAsymmetric t2 t1, + MinMaxType t1 t2 ~ MinMaxType t2 t1) + +{-| + A replacement for Prelude's `P.min` and `P.max`. If @t1 = t2@ and @Ord t1@, + then one can use the default implementation to mirror Prelude's @min@ and @max@. +-} +class CanMinMaxAsymmetric t1 t2 where + type MinMaxType t1 t2 + type MinMaxType t1 t2 = t1 -- default + min :: t1 -> t2 -> MinMaxType t1 t2 + max :: t1 -> t2 -> MinMaxType t1 t2 + default min :: (MinMaxType t1 t2 ~ t1, t1~t2, P.Ord t1) => t1 -> t1 -> t1 + min = P.min + default max :: (MinMaxType t1 t2 ~ t1, t1~t2, P.Ord t1) => t1 -> t1 -> t1 + max = P.max + +type CanMinMaxThis t1 t2 = + (CanMinMax t1 t2, MinMaxType t1 t2 ~ t1) +type CanMinMaxSameType t = + CanMinMaxThis t t + +maximum :: (CanMinMaxSameType t) => [t] -> t +maximum (x:xs) = List.foldl' max x xs +maximum [] = error $ "maximum: empty list" + +minimum :: (CanMinMaxSameType t) => [t] -> t +minimum (x:xs) = List.foldl' min x xs +minimum [] = error $ "minimum: empty list" + +{-| Compound type constraint useful for test definition. -} +type CanMinMaxX t1 t2 = + (CanMinMax t1 t2, + Show t1, Arbitrary t1, + Show t2, Arbitrary t2, + Show (MinMaxType t1 t2), + HasEqCertainly t1 t1, + HasEqCertainly t2 t2, + HasEqCertainly t1 (MinMaxType t1 t2), + HasEqCertainly t2 (MinMaxType t1 t2), + HasEqCertainly (MinMaxType t1 t2) (MinMaxType t1 t2), + HasOrderCertainly t1 (MinMaxType t1 t2), + HasOrderCertainly t2 (MinMaxType t1 t2), + HasOrderCertainly (MinMaxType t1 t2) (MinMaxType t1 t2)) + +{-| Compound type constraint useful for test definition. -} +type CanMinMaxXX t1 t2 = + (CanMinMaxX t1 t2, + HasEqCertainly (MinMaxType t1 t2) (MinMaxType t2 t1)) + +{-| + HSpec properties that each implementation of CanMinMax should satisfy. + -} +specCanMinMax :: + (CanMinMaxXX t1 t1, + CanMinMaxXX t1 t2, + CanMinMaxXX t1 t3, CanMinMaxXX t2 t3, + CanMinMaxXX t1 (MinMaxType t2 t3), + CanMinMaxXX (MinMaxType t1 t2) t3, + HasEqCertainly (MinMaxType t1 (MinMaxType t2 t3)) (MinMaxType (MinMaxType t1 t2) t3)) + => + T t1 -> T t2 -> T t3 -> Spec +specCanMinMax (T typeName1 :: T t1) (T typeName2 :: T t2) (T typeName3 :: T t3) = + describe (printf "CanMinMax %s %s, CanMinMax %s %s" typeName1 typeName2 typeName2 typeName3) $ do + it "`min` is not larger than its arguments" $ do + property $ \ (x :: t1) (y :: t2) -> + (x ?==? x) && (y ?==? y) ==> -- avoid NaN + let m = x `min` y in (m ?<=?$ y) .&&. (m ?<=?$ x) + it "`max` is not smaller than its arguments" $ do + property $ \ (x :: t1) (y :: t2) -> + (x ?==? x) && (y ?==? y) ==> -- avoid NaN + let m = x `max` y in (m ?>=?$ y) .&&. (m ?>=?$ x) + it "has idempotent `min`" $ do + property $ \ (x :: t1) -> + (x ?==? x) ==> -- avoid NaN + (x `min` x) ?==?$ x + it "has idempotent `max`" $ do + property $ \ (x :: t1) -> + (x ?==? x) ==> -- avoid NaN + (x `max` x) ?==?$ x + it "has commutative `min`" $ do + property $ \ (x :: t1) (y :: t2) -> + (x ?==? x) && (y ?==? y) ==> -- avoid NaN + (x `min` y) ?==?$ (y `min` x) + it "has commutative `max`" $ do + property $ \ (x :: t1) (y :: t2) -> + (x ?==? x) && (y ?==? y) ==> -- avoid NaN + (x `max` y) ?==?$ (y `max` x) + it "has associative `min`" $ do + property $ \ (x :: t1) (y :: t2) (z :: t3) -> + (x ?==? x) && (y ?==? y) && (z ?==? z) ==> -- avoid NaN + (x `min` (y `min` z)) ?==?$ ((x `min` y) `min` z) + it "has associative `max`" $ do + property $ \ (x :: t1) (y :: t2) (z :: t3) -> + (x ?==? x) && (y ?==? y) && (z ?==? z) ==> -- avoid NaN + (x `max` (y `max` z)) ?==?$ ((x `max` y) `max` z) + where + (?==?$) :: (HasEqCertainlyAsymmetric a b, Show a, Show b) => a -> b -> Property + (?==?$) = printArgsIfFails2 "?==?" (?==?) + (?>=?$) :: (HasOrderCertainlyAsymmetric a b, Show a, Show b) => a -> b -> Property + (?>=?$) = printArgsIfFails2 "?>=?" (?>=?) + (?<=?$) :: (HasOrderCertainlyAsymmetric a b, Show a, Show b) => a -> b -> Property + (?<=?$) = printArgsIfFails2 "?<=?" (?<=?) +-- +{-| + HSpec properties that each implementation of CanMinMax should satisfy. + -} +specCanMinMaxNotMixed :: + (CanMinMaxXX t t, + CanMinMaxXX t (MinMaxType t t), + HasEq (MinMaxType (MinMaxType t t) t) (MinMaxType t (MinMaxType t t)) ) + => + T t -> Spec +specCanMinMaxNotMixed t = specCanMinMax t t t + +instance CanMinMaxAsymmetric Int Int +instance CanMinMaxAsymmetric Integer Integer +instance CanMinMaxAsymmetric Rational Rational +instance CanMinMaxAsymmetric Double Double + +instance CanMinMaxAsymmetric Int Integer where + type MinMaxType Int Integer = Integer + min = convertFirst min + max = convertFirst max +instance CanMinMaxAsymmetric Integer Int where + type MinMaxType Integer Int = Integer + min = convertSecond min + max = convertSecond max + +instance CanMinMaxAsymmetric Int Rational where + type MinMaxType Int Rational = Rational + min = convertFirst min + max = convertFirst max +instance CanMinMaxAsymmetric Rational Int where + type MinMaxType Rational Int = Rational + min = convertSecond min + max = convertSecond max + +instance CanMinMaxAsymmetric Integer Rational where + type MinMaxType Integer Rational = Rational + min = convertFirst min + max = convertFirst max +instance CanMinMaxAsymmetric Rational Integer where + type MinMaxType Rational Integer = Rational + min = convertSecond min + max = convertSecond max + +instance (CanMinMaxAsymmetric a b) => CanMinMaxAsymmetric [a] [b] where + type MinMaxType [a] [b] = [MinMaxType a b] + min (x:xs) (y:ys) = (min x y) : (min xs ys) + min _ _ = [] + max (x:xs) (y:ys) = (max x y) : (max xs ys) + max _ _ = [] + +instance (CanMinMaxAsymmetric a b) => CanMinMaxAsymmetric (Maybe a) (Maybe b) where + type MinMaxType (Maybe a) (Maybe b) = Maybe (MinMaxType a b) + min (Just x) (Just y) = Just (min x y) + min _ _ = Nothing + max (Just x) (Just y) = Just (max x y) + max _ _ = Nothing + +{-| Compound type constraint useful for test definition. -} +type CanNegX t = + (CanNeg t, Show t, Arbitrary t, Show (NegType t)) + +{---- numeric negation tests and instances -----} + +{-| + HSpec properties that each numeric implementation of CanNeg should satisfy. + -} +specCanNegNum :: + (CanNegX t, CanNegX (NegType t), + HasEqCertainly t (NegType (NegType t)), + ConvertibleExactly Integer t, + HasEqCertainly t t, + HasEqCertainly t (NegType t), + CanTestPosNeg t, + CanTestPosNeg (NegType t) + ) + => + T t -> Spec +specCanNegNum (T typeName :: T t) = + describe (printf "CanNeg %s" typeName) $ do + it "ignores double negation" $ do + property $ \ (x :: t) -> + (x ?==? x) ==> -- avoid NaN + (negate (negate x)) ?==?$ x + it "takes 0 to 0" $ do + let z = convertExactly 0 :: t in negate z ?==? z + it "takes positive to negative" $ do + property $ \ (x :: t) -> + (isCertainlyPositive x) ==> (isCertainlyNegative (negate x)) + it "takes negative to positive" $ do + property $ \ (x :: t) -> + (isCertainlyNegative x) ==> (isCertainlyPositive (negate x)) + where + (?==?$) :: (HasEqCertainlyAsymmetric a b, Show a, Show b) => a -> b -> Property + (?==?$) = printArgsIfFails2 "?==?" (?==?) + +instance CanNeg Int where negate = P.negate +instance CanNeg Integer where negate = P.negate +instance CanNeg Rational where negate = P.negate +instance CanNeg Double where negate = P.negate + +{---- abs -----} + +{-| + A replacement for Prelude's `P.abs`. If @Num t@, + then one can use the default implementation to mirror Prelude's @abs@. +-} +class CanAbs t where + type AbsType t + type AbsType t = t -- default + abs :: t -> AbsType t + default abs :: (AbsType t ~ t, P.Num t) => t -> t + abs = P.abs + +type CanAbsSameType t = (CanAbs t, AbsType t ~ t) + +instance CanAbs Int +instance CanAbs Integer +instance CanAbs Rational +instance CanAbs Double + +type CanAbsX t = + (CanAbs t, + CanNegSameType t, + CanTestPosNeg t, + CanTestPosNeg (AbsType t), + HasEqCertainly t t, + HasEqCertainly t (AbsType t), + Show t, Arbitrary t, Show (AbsType t)) + +{-| + HSpec properties that each implementation of CanAbs should satisfy. + -} +specCanAbs :: + (CanAbsX t, CanAbsX (AbsType t)) + => + T t -> Spec +specCanAbs (T typeName :: T t) = + describe (printf "CanAbs %s" typeName) $ do + it "is idempotent" $ do + property $ \ (x :: t) -> + (x ?==? x) ==> -- avoid NaN + (abs (abs x)) ?==?$ (abs x) + it "is identity on non-negative arguments" $ do + property $ \ (x :: t) -> + isCertainlyNonNegative x ==> x ?==?$ (abs x) + it "is negation on non-positive arguments" $ do + property $ \ (x :: t) -> + isCertainlyNonPositive x ==> (negate x) ?==?$ (abs x) + it "does not give negative results" $ do + property $ \ (x :: t) -> not $ isCertainlyNegative (abs x) + where + (?==?$) :: (HasEqCertainlyAsymmetric a b, Show a, Show b) => a -> b -> Property + (?==?$) = printArgsIfFails2 "?==?" (?==?) diff --git a/src/Numeric/MixedTypes/Ord.hs b/src/Numeric/MixedTypes/Ord.hs new file mode 100644 --- /dev/null +++ b/src/Numeric/MixedTypes/Ord.hs @@ -0,0 +1,213 @@ +{-| + Module : Numeric.MixedType.Ord + Description : Bottom-up typed order comparisons + Copyright : (c) Michal Konecny + License : BSD3 + + Maintainer : mikkonecny@gmail.com + Stability : experimental + Portability : portable + +-} + +module Numeric.MixedTypes.Ord +( + -- * Comparisons in numeric order + HasOrder, HasOrderAsymmetric(..), (>), (<), (<=), (>=) + , HasOrderCertainlyAsymmetric, HasOrderCertainly + , (?<=?), (?=?), (?>?) + , (!<=!), (!=!), (!>!) + -- ** Tests + , specHasOrder, specHasOrderNotMixed, HasOrderX + -- ** Specific comparisons + , CanTestPosNeg(..) +) +where + +import Numeric.MixedTypes.PreludeHiding +import qualified Prelude as P +import Text.Printf + +import Test.Hspec +import qualified Test.QuickCheck as QC + +import Numeric.MixedTypes.Literals +import Numeric.MixedTypes.Bool +-- import Numeric.MixedTypes.Eq + +infix 4 <, <=, >=, > +infix 4 ?<=?, ?=?, ?>? +infix 4 !<=!, !=!, !>! + +{---- Inequality -----} + +type HasOrder t1 t2 = + (HasOrderAsymmetric t1 t2, HasOrderAsymmetric t2 t1, + OrderCompareType t1 t2 ~ OrderCompareType t2 t1) + +type HasOrderCertainly t1 t2 = + (HasOrder t1 t2, CanTestCertainly (OrderCompareType t1 t2)) + +type HasOrderCertainlyAsymmetric t1 t2 = + (HasOrderAsymmetric t1 t2, CanTestCertainly (OrderCompareType t1 t2)) + +class (IsBool (OrderCompareType a b)) => HasOrderAsymmetric a b where + type OrderCompareType a b + type OrderCompareType a b = Bool -- default + lessThan :: a -> b -> (OrderCompareType a b) + -- default lessThan via Prelude for Bool: + default lessThan :: (OrderCompareType a b ~ Bool, a~b, P.Ord a) => a -> b -> Bool + lessThan = (P.<) + greaterThan :: a -> b -> (OrderCompareType a b) + default greaterThan :: + (HasOrder b a, OrderCompareType b a ~ OrderCompareType a b) => + a -> b -> (OrderCompareType a b) + greaterThan a b = lessThan b a + leq :: a -> b -> (OrderCompareType a b) + -- default lessThan via Prelude for Bool: + default leq :: (OrderCompareType a b ~ Bool, a~b, P.Ord a) => a -> b -> Bool + leq = (P.<=) + geq :: a -> b -> (OrderCompareType a b) + default geq :: + (HasOrder b a, OrderCompareType b a ~ OrderCompareType a b) => + a -> b -> (OrderCompareType a b) + geq a b = leq b a + +(>) :: (HasOrderAsymmetric a b) => a -> b -> OrderCompareType a b +(>) = greaterThan +(<) :: (HasOrderAsymmetric a b) => a -> b -> OrderCompareType a b +(<) = lessThan + +(>=) :: (HasOrderAsymmetric a b) => a -> b -> OrderCompareType a b +(>=) = geq +(<=) :: (HasOrderAsymmetric a b) => a -> b -> OrderCompareType a b +(<=) = leq + +(?>?) :: (HasOrderCertainlyAsymmetric a b) => a -> b -> Bool +a ?>? b = isNotFalse $ a > b + +(? a -> b -> Bool +a ?=?) :: (HasOrderCertainlyAsymmetric a b) => a -> b -> Bool +a ?>=? b = isNotFalse $ a >= b + +(?<=?) :: (HasOrderCertainlyAsymmetric a b) => a -> b -> Bool +a ?<=? b = isNotFalse $ a <= b + +(!>!) :: (HasOrderCertainlyAsymmetric a b) => a -> b -> Bool +a !>! b = isCertainlyTrue $ a > b + +(! a -> b -> Bool +a !=!) :: (HasOrderCertainlyAsymmetric a b) => a -> b -> Bool +a !>=! b = isCertainlyTrue $ a >= b + +(!<=!) :: (HasOrderCertainlyAsymmetric a b) => a -> b -> Bool +a !<=! b = isCertainlyTrue $ a <= b + +{-| Compound type constraint useful for test definition. -} +type HasOrderX t1 t2 = + (HasOrderCertainly t1 t2, Show t1, QC.Arbitrary t1, Show t2, QC.Arbitrary t2) + +{-| + HSpec properties that each implementation of 'HasOrder' should satisfy. + -} +specHasOrder :: + (HasOrderX t1 t1, + HasOrderX t1 t2, + HasOrderX t1 t3, HasOrderX t2 t3, + CanAndOrX (OrderCompareType t1 t2) (OrderCompareType t2 t3)) + => + T t1 -> T t2 -> T t3 -> Spec +specHasOrder (T typeName1 :: T t1) (T typeName2 :: T t2) (T typeName3 :: T t3) = + describe (printf "HasOrd %s %s, HasOrd %s %s" typeName1 typeName2 typeName2 typeName3) $ do + it "has reflexive >=" $ do + QC.property $ \ (x :: t1) -> not $ isCertainlyFalse (x >= x) + it "has reflexive <=" $ do + QC.property $ \ (x :: t1) -> not $ isCertainlyFalse (x <= x) + it "has anti-reflexive >" $ do + QC.property $ \ (x :: t1) -> not $ isCertainlyTrue (x > x) + it "has anti-reflexive <" $ do + QC.property $ \ (x :: t1) -> not $ isCertainlyTrue (x < x) + it "> stronly implies >=" $ do + QC.property $ \ (x :: t1) (y :: t2) -> (x > y) `stronglyImplies` (x >= y) + it "< stronly implies <=" $ do + QC.property $ \ (x :: t1) (y :: t2) -> (x < y) `stronglyImplies` (x <= y) + it "has stronly equivalent > and <" $ do + QC.property $ \ (x :: t1) (y :: t2) -> (x < y) `stronglyEquivalentTo` (y > x) + it "has stronly equivalent >= and <=" $ do + QC.property $ \ (x :: t1) (y :: t2) -> (x <= y) `stronglyEquivalentTo` (y >= x) + it "has stronly transitive <" $ do + QC.property $ \ (x :: t1) (y :: t2) (z :: t3) -> ((x < y) && (y < z)) `stronglyImplies` (y < z) + +{-| + HSpec properties that each implementation of 'HasOrder' should satisfy. + -} +specHasOrderNotMixed :: + (HasOrderX t t, + CanAndOrX (OrderCompareType t t) (OrderCompareType t t)) + => + T t -> Spec +specHasOrderNotMixed t = specHasOrder t t t + +instance HasOrderAsymmetric Int Int +instance HasOrderAsymmetric Integer Integer +instance HasOrderAsymmetric Rational Rational +instance HasOrderAsymmetric Double Double + +instance HasOrderAsymmetric Int Integer where + lessThan = convertFirst lessThan + leq = convertFirst leq +instance HasOrderAsymmetric Integer Int where + lessThan = convertSecond lessThan + leq = convertSecond leq + +instance HasOrderAsymmetric Int Rational where + lessThan = convertFirst lessThan + leq = convertFirst leq +instance HasOrderAsymmetric Rational Int where + lessThan = convertSecond lessThan + leq = convertSecond leq + +instance HasOrderAsymmetric Integer Rational where + lessThan = convertFirst lessThan + leq = convertFirst leq +instance HasOrderAsymmetric Rational Integer where + lessThan = convertSecond lessThan + leq = convertSecond leq + +instance HasOrderAsymmetric Integer Double where + lessThan n d = (n <= (P.floor d :: Integer)) && (n < (P.ceiling d :: Integer)) + leq n d = (n <= (P.floor d :: Integer)) +instance HasOrderAsymmetric Double Integer where + lessThan d n = ((P.floor d :: Integer) < n) && ((P.ceiling d :: Integer) <= n) + leq d n = ((P.ceiling d :: Integer) <= n) + +instance HasOrderAsymmetric Int Double where + lessThan n d = lessThan (integer n) d + leq n d = leq (integer n) d +instance HasOrderAsymmetric Double Int where + lessThan d n = lessThan d (integer n) + leq d n = leq d (integer n) + + +class CanTestPosNeg t where + isCertainlyPositive :: t -> Bool + isCertainlyNonNegative :: t -> Bool + isCertainlyNegative :: t -> Bool + isCertainlyNonPositive :: t -> Bool + default isCertainlyPositive :: (HasOrderCertainly t Integer) => t -> Bool + isCertainlyPositive a = isCertainlyTrue $ a > 0 + default isCertainlyNonNegative :: (HasOrderCertainly t Integer) => t -> Bool + isCertainlyNonNegative a = isCertainlyTrue $ a >= 0 + default isCertainlyNegative :: (HasOrderCertainly t Integer) => t -> Bool + isCertainlyNegative a = isCertainlyTrue $ a < 0 + default isCertainlyNonPositive :: (HasOrderCertainly t Integer) => t -> Bool + isCertainlyNonPositive a = isCertainlyTrue $ a <= 0 + +instance CanTestPosNeg Int +instance CanTestPosNeg Integer +instance CanTestPosNeg Rational +instance CanTestPosNeg Double diff --git a/src/Numeric/MixedTypes/PreludeHiding.hs b/src/Numeric/MixedTypes/PreludeHiding.hs new file mode 100644 --- /dev/null +++ b/src/Numeric/MixedTypes/PreludeHiding.hs @@ -0,0 +1,27 @@ +{-| + Module : Numeric.MixedType.PreludeHiding + Description : Prelude without operations that clash with MixedTypes + Copyright : (c) Michal Konecny + License : BSD3 + + Maintainer : mikkonecny@gmail.com + Stability : experimental + Portability : portable + + Prelude without operations that clash with MixedTypes +-} +module Numeric.MixedTypes.PreludeHiding +( + module Prelude +) +where + +import Prelude hiding + ( + fromInteger, fromRational, (!!) + , Eq(..), Ord(..), Num(..), Fractional(..), RealFrac(..), Floating(..) + , not, (&&), (||), and, or + , (^), (^^) + , minimum, maximum, sum, product + , isInfinite, isNaN + ) diff --git a/src/Numeric/MixedTypes/Ring.hs b/src/Numeric/MixedTypes/Ring.hs new file mode 100644 --- /dev/null +++ b/src/Numeric/MixedTypes/Ring.hs @@ -0,0 +1,354 @@ +{-| + Module : Numeric.MixedType.Ring + Description : Bottom-up typed multiplication and exponent + Copyright : (c) Michal Konecny + License : BSD3 + + Maintainer : mikkonecny@gmail.com + Stability : experimental + Portability : portable + +-} + +module Numeric.MixedTypes.Ring +( + -- * Ring + CanAddSubMulBy, Ring, CertainlyEqRing, OrderedRing, OrderedCertainlyRing + -- * Multiplication + , CanMul, CanMulAsymmetric(..), CanMulBy, CanMulSameType + , (*), product + -- ** Tests + , specCanMul, specCanMulNotMixed, specCanMulSameType, CanMulX + -- * Exponentiation + , CanPow(..), CanPowBy + , (^), (^^), (**) + , powUsingMul + -- ** Tests + , specCanPow, CanPowX +) +where + +import Numeric.MixedTypes.PreludeHiding +import qualified Prelude as P +import Text.Printf + +import qualified Data.List as List + +import Test.Hspec +import Test.QuickCheck + +import Numeric.MixedTypes.Literals +import Numeric.MixedTypes.Bool +import Numeric.MixedTypes.Eq +import Numeric.MixedTypes.Ord +-- import Numeric.MixedTypes.MinMaxAbs +import Numeric.MixedTypes.AddSub + +{----- Ring -----} + +type CanAddSubMulBy t s = + (CanAddThis t s, CanSubThis t s, CanMulBy t s) + +type Ring t = + (CanNegSameType t, CanAddSameType t, CanSubSameType t, CanMulSameType t, + CanPowBy t Integer, CanPowBy t Int, + HasEq t t, + HasEq t Integer, CanAddSubMulBy t Integer, + CanSub Integer t, SubType Integer t ~ t, + HasEq t Int, CanAddSubMulBy t Int, + CanSub Int t, SubType Int t ~ t, + ConvertibleExactly Integer t) + +type CertainlyEqRing t = + (Ring t, HasEqCertainly t t, HasEqCertainly t Int, HasEqCertainly t Integer) + +type OrderedRing t = + (Ring t, HasOrder t t, HasOrder t Int, HasOrder t Integer) + +type OrderedCertainlyRing t = + (CertainlyEqRing t, HasOrderCertainly t t, HasOrderCertainly t Int, HasOrderCertainly t Integer, + CanTestPosNeg t) + +{---- Multiplication -----} + +type CanMul t1 t2 = + (CanMulAsymmetric t1 t2, CanMulAsymmetric t2 t1, + MulType t1 t2 ~ MulType t2 t1) + +{-| + A replacement for Prelude's `P.*`. If @t1 = t2@ and @Num t1@, + then one can use the default implementation to mirror Prelude's @*@. +-} +class CanMulAsymmetric t1 t2 where + type MulType t1 t2 + type MulType t1 t2 = t1 -- default + mul :: t1 -> t2 -> MulType t1 t2 + default mul :: (MulType t1 t2 ~ t1, t1~t2, P.Num t1) => t1 -> t1 -> t1 + mul = (P.*) + +infixl 8 ^, ^^ +infixl 7 * + +(*) :: (CanMulAsymmetric t1 t2) => t1 -> t2 -> MulType t1 t2 +(*) = mul + +type CanMulBy t1 t2 = + (CanMul t1 t2, MulType t1 t2 ~ t1) +type CanMulSameType t = + CanMulBy t t + +product :: (CanMulSameType t, ConvertibleExactly Integer t) => [t] -> t +product xs = List.foldl' mul (convertExactly 1) xs + +{-| Compound type constraint useful for test definition. -} +type CanMulX t1 t2 = + (CanMul t1 t2, + Show t1, Arbitrary t1, + Show t2, Arbitrary t2, + Show (MulType t1 t2), + HasEqCertainly t1 (MulType t1 t2), + HasEqCertainly t2 (MulType t1 t2), + HasEqCertainly (MulType t1 t2) (MulType t1 t2), + HasOrderCertainly t1 (MulType t1 t2), + HasOrderCertainly t2 (MulType t1 t2), + HasOrderCertainly (MulType t1 t2) (MulType t1 t2)) + +{-| + HSpec properties that each implementation of CanMul should satisfy. + -} +specCanMul :: + (CanMulX t1 t2, + CanMulX t1 t3, + CanMulX t2 t3, + CanMulX t1 (MulType t2 t3), + CanMulX (MulType t1 t2) t3, + HasEqCertainly (MulType t1 (MulType t2 t3)) (MulType (MulType t1 t2) t3), + CanAdd t2 t3, + CanMulX t1 (AddType t2 t3), + CanAddX (MulType t1 t2) (MulType t1 t3), + HasEqCertainly (MulType t1 (AddType t2 t3)) (AddType (MulType t1 t2) (MulType t1 t3)), + ConvertibleExactly Integer t2) + => + T t1 -> T t2 -> T t3 -> Spec +specCanMul (T typeName1 :: T t1) (T typeName2 :: T t2) (T typeName3 :: T t3) = + describe (printf "CanMul %s %s, CanMul %s %s" typeName1 typeName2 typeName2 typeName3) $ do + it "absorbs 1" $ do + property $ \ (x :: t1) -> let one = (convertExactly 1 :: t2) in (x * one) ?==?$ x + it "is commutative" $ do + property $ \ (x :: t1) (y :: t2) -> (x * y) ?==?$ (y * x) + it "is associative" $ do + property $ \ (x :: t1) (y :: t2) (z :: t3) -> + (x * (y * z)) ?==?$ ((x * y) * z) + it "distributes over addition" $ do + property $ \ (x :: t1) (y :: t2) (z :: t3) -> + (x * (y + z)) ?==?$ (x * y) + (x * z) + where + infix 4 ?==?$ + (?==?$) :: (HasEqCertainlyAsymmetric a b, Show a, Show b) => a -> b -> Property + (?==?$) = printArgsIfFails2 "?==?" (?==?) + +{-| + HSpec properties that each implementation of CanMul should satisfy. + -} +specCanMulNotMixed :: + (CanMulX t t, + CanMulX t (MulType t t), + HasEqCertainly (MulType (MulType t t) t) (MulType t (MulType t t)), + CanAdd t t, + CanMulX t (AddType t t), + CanAddX (MulType t t) (MulType t t), + HasEqCertainly (MulType t (AddType t t)) (AddType (MulType t t) (MulType t t)), + ConvertibleExactly Integer t) + => + T t -> Spec +specCanMulNotMixed t = specCanMul t t t + +{-| + HSpec properties that each implementation of CanMulSameType should satisfy. + -} +specCanMulSameType :: + (ConvertibleExactly Integer t, Show t, + HasEqCertainly t t, CanMulSameType t) + => + T t -> Spec +specCanMulSameType (T typeName :: T t) = + describe (printf "CanMulSameType %s" typeName) $ do + it "has product working over integers" $ do + property $ \ (xsi :: [Integer]) -> + (product $ (map convertExactly xsi :: [t])) ?==?$ (convertExactly (product xsi) :: t) + it "has product [] = 1" $ do + (product ([] :: [t])) ?==?$ (convertExactly 1 :: t) + where + infix 4 ?==?$ + (?==?$) :: (HasEqCertainlyAsymmetric a b, Show a, Show b) => a -> b -> Property + (?==?$) = printArgsIfFails2 "?==?" (?==?) + +instance CanMulAsymmetric Int Int where + type MulType Int Int = Integer -- do not risk overflow + mul a b = (integer a) P.* (integer b) +instance CanMulAsymmetric Integer Integer +instance CanMulAsymmetric Rational Rational +instance CanMulAsymmetric Double Double + +instance CanMulAsymmetric Int Integer where + type MulType Int Integer = Integer + mul = convertFirst mul +instance CanMulAsymmetric Integer Int where + type MulType Integer Int = Integer + mul = convertSecond mul + +instance CanMulAsymmetric Int Rational where + type MulType Int Rational = Rational + mul = convertFirst mul +instance CanMulAsymmetric Rational Int where + type MulType Rational Int = Rational + mul = convertSecond mul + +instance CanMulAsymmetric Integer Rational where + type MulType Integer Rational = Rational + mul = convertFirst mul +instance CanMulAsymmetric Rational Integer where + type MulType Rational Integer = Rational + mul = convertSecond mul + +instance CanMulAsymmetric Int Double where + type MulType Int Double = Double + mul = convertFirst mul +instance CanMulAsymmetric Double Int where + type MulType Double Int = Double + mul = convertSecond mul + +instance CanMulAsymmetric Integer Double where + type MulType Integer Double = Double + mul = convertFirst mul +instance CanMulAsymmetric Double Integer where + type MulType Double Integer = Double + mul = convertSecond mul + +instance CanMulAsymmetric Rational Double where + type MulType Rational Double = Double + mul = convertFirst mul +instance CanMulAsymmetric Double Rational where + type MulType Double Rational = Double + mul = convertSecond mul + +instance (CanMulAsymmetric a b) => CanMulAsymmetric [a] [b] where + type MulType [a] [b] = [MulType a b] + mul (x:xs) (y:ys) = (mul x y) : (mul xs ys) + mul _ _ = [] + +instance (CanMulAsymmetric a b) => CanMulAsymmetric (Maybe a) (Maybe b) where + type MulType (Maybe a) (Maybe b) = Maybe (MulType a b) + mul (Just x) (Just y) = Just (mul x y) + mul _ _ = Nothing + +{---- Exponentiation -----} + +{-| + A replacement for Prelude's binary `P.^` and `P.^^`. If @Num t1@ and @Integral t2@, + then one can use the default implementation to mirror Prelude's @^@. +-} +class CanPow t1 t2 where + type PowType t1 t2 + type PowType t1 t2 = t1 -- default + pow :: t1 -> t2 -> PowType t1 t2 + default pow :: (PowType t1 t2 ~ t1, P.Num t1, P.Integral t2) => t1 -> t2 -> t1 + pow = (P.^) + +powUsingMul :: + (CanBeInteger e, + CanMulSameType t, ConvertibleExactly Integer t) + => + t -> e -> t +powUsingMul x nPre + | n < 0 = error $ "powUsingMul is not defined for negative exponent " ++ show n + | n == 0 = convertExactly 1 + | otherwise = aux n + where + n = integer nPre + aux m + | m == 1 = x + | even m = + let s = aux (m `div` 2) in s * s + | otherwise = + let s = aux ((m-1) `div` 2) in x * s * s + +(^) :: (CanPow t1 t2) => t1 -> t2 -> PowType t1 t2 +(^) = pow + +{-| A synonym of `^` -} +(^^) :: (CanPow t1 t2) => t1 -> t2 -> PowType t1 t2 +(^^) = (^) + +{-| A synonym of `^` -} +(**) :: (CanPow t1 t2) => t1 -> t2 -> (PowType t1 t2) +(**) = (^) + +type CanPowBy t1 t2 = + (CanPow t1 t2, PowType t1 t2 ~ t1) + +{-| Compound type constraint useful for test definition. -} +type CanPowX t1 t2 = + (CanPow t1 t2, + Show t1, Arbitrary t1, + Show t2, Arbitrary t2, + Show (PowType t1 t2)) + +{-| + HSpec properties that each implementation of CanPow should satisfy. + -} +specCanPow :: + (CanPowX t1 t2, + HasEqCertainly t1 (PowType t1 t2), + ConvertibleExactly Integer t1, + ConvertibleExactly Integer t2, + CanTestPosNeg t2, + CanAdd t2 Integer, + CanMulX t1 (PowType t1 t2), + CanPowX t1 (AddType t2 Integer), + HasEqCertainly (MulType t1 (PowType t1 t2)) (PowType t1 (AddType t2 Integer))) + => + T t1 -> T t2 -> Spec +specCanPow (T typeName1 :: T t1) (T typeName2 :: T t2) = + describe (printf "CanPow %s %s" typeName1 typeName2) $ do + it "x^0 = 1" $ do + property $ \ (x :: t1) -> + let one = (convertExactly 1 :: t1) in + let z = (convertExactly 0 :: t2) in + (x ^ z) ?==?$ one + it "x^1 = x" $ do + property $ \ (x :: t1) -> + let one = (convertExactly 1 :: t2) in + (x ^ one) ?==?$ x + it "x^(y+1) = x*x^y" $ do + property $ \ (x :: t1) (y :: t2) -> + (isCertainlyNonNegative y) ==> + x * (x ^ y) ?==?$ (x ^ (y + 1)) + where + infix 4 ?==?$ + (?==?$) :: (HasEqCertainlyAsymmetric a b, Show a, Show b) => a -> b -> Property + (?==?$) = printArgsIfFails2 "?==?" (?==?) + +instance CanPow Integer Integer +instance CanPow Integer Int +instance CanPow Int Integer where + type PowType Int Integer = Integer + pow x n = (integer x) P.^ n +instance CanPow Int Int where + type PowType Int Int = Integer + pow x n = (integer x) P.^ n +instance CanPow Rational Int where pow = (P.^^) +instance CanPow Rational Integer where pow = (P.^^) +instance CanPow Double Int where pow = (P.^^) +instance CanPow Double Integer where pow = (P.^^) +{- No exponentiation of Int to avoid overflows. -} + +-- instance (CanPow a b) => CanPow [a] [b] where +-- type PowType [a] [b] = [PowType a b] +-- pow (x:xs) (y:ys) = (pow x y) : (pow xs ys) +-- pow _ _ = [] + +instance (CanPow a b) => CanPow (Maybe a) (Maybe b) where + type PowType (Maybe a) (Maybe b) = Maybe (PowType a b) + pow (Just x) (Just y) = Just (pow x y) + pow _ _ = Nothing diff --git a/src/Numeric/MixedTypes/Round.hs b/src/Numeric/MixedTypes/Round.hs new file mode 100644 --- /dev/null +++ b/src/Numeric/MixedTypes/Round.hs @@ -0,0 +1,164 @@ +{-| + Module : Numeric.MixedType.Round + Description : Bottom-up typed round, floor, etc. + Copyright : (c) Michal Konecny + License : BSD3 + + Maintainer : mikkonecny@gmail.com + Stability : experimental + Portability : portable + +-} + +module Numeric.MixedTypes.Round +( + -- * Rounding operations + CanRound(..), HasIntegerBounds(..) + -- ** Tests + , specCanRound, specHasIntegerBounds +) +where + +import Numeric.MixedTypes.PreludeHiding +import qualified Prelude as P +import Text.Printf + +-- import qualified Data.List as List + +import Test.Hspec +import Test.QuickCheck as QC + +import Numeric.MixedTypes.Literals +import Numeric.MixedTypes.Bool +import Numeric.MixedTypes.Eq +import Numeric.MixedTypes.Ord +-- import Numeric.MixedTypes.MinMaxAbs +import Numeric.MixedTypes.AddSub + +{---- rounding -----} + +{-| + A replacement for Prelude's `P.RealFrac` operations, such as round in + which the result type is fixed to Integer. + + If @RealFrac t@ and @CanTestPosNeg t@, + then one can use the default implementation to mirror Prelude's @round@, etc. + + In other cases, it is sufficient to define `properFraction`. +-} +class CanRound t where + properFraction :: t -> (Integer, t) + default properFraction :: (P.RealFrac t) => t -> (Integer, t) + properFraction = P.properFraction + truncate :: t -> Integer + truncate = fst . properFraction + round :: t -> Integer + default round :: (HasOrderCertainly t Rational) => t -> Integer + round x + | -0.5 !! 0.5 = n + 1 + | even n = n + | r !! 0.0 = n + 1 + | otherwise = error "round default defn: Bad value" + where + (n,r) = properFraction x + ceiling :: t -> Integer + default ceiling :: (CanTestPosNeg t) => t -> Integer + ceiling x + | isCertainlyPositive r = n + 1 + | otherwise = n + where + (n,r) = properFraction x + floor :: t -> Integer + default floor :: (CanTestPosNeg t) => t -> Integer + floor x + | isCertainlyNegative r = n - 1 + | otherwise = n + where + (n,r) = properFraction x + +instance CanRound Rational +instance CanRound Double where + round = P.round + ceiling = P.ceiling + floor = P.floor + +type CanRoundX t = + (CanRound t, + CanNegSameType t, + CanTestPosNeg t, + HasOrderCertainly t Integer, + CanTestFinite t, + Show t, Arbitrary t) + +{-| + HSpec properties that each implementation of CanRound should satisfy. + -} +specCanRound :: + (CanRoundX t, HasIntegers t) + => + T t -> Spec +specCanRound (T typeName :: T t) = + describe (printf "CanRound %s" typeName) $ do + it "holds floor x <= x <= ceiling x" $ do + property $ \ (x :: t) -> + isFinite x ==> + (floor x ?<=?$ x) .&&. (x ?<=?$ ceiling x) + it "holds floor x <= round x <= ceiling x" $ do + property $ \ (x :: t) -> + isFinite x ==> + (floor x !<=!$ round x) .&&. (round x !<=!$ ceiling x) + it "0 <= ceiling x - floor x <= 1" $ do + property $ \ (x :: t) -> + isFinite x ==> + (ceiling x - floor x) `elem_PF` [0,1] + it "holds floor x = round x = ceiling x for integers" $ do + property $ \ (xi :: Integer) -> + let x = convertExactly xi :: t in + (floor x !==!$ round x) .&&. (round x !==!$ ceiling x) + where + (?<=?$) :: (HasOrderCertainlyAsymmetric a b, Show a, Show b) => a -> b -> Property + (?<=?$) = printArgsIfFails2 "?<=?" (?<=?) + (!<=!$) :: (HasOrderCertainlyAsymmetric a b, Show a, Show b) => a -> b -> Property + (!<=!$) = printArgsIfFails2 "!<=!" (!<=!) + (!==!$) :: (HasEqCertainlyAsymmetric a b, Show a, Show b) => a -> b -> Property + (!==!$) = printArgsIfFails2 "!==!" (!==!) + elem_PF = printArgsIfFails2 "elem" elem + + +class HasIntegerBounds t where + integerBounds :: t -> (Integer, Integer) + default integerBounds :: (CanRound t) => t -> (Integer, Integer) + integerBounds x = (floor x, ceiling x) + +instance HasIntegerBounds Rational +instance HasIntegerBounds Double + +type HasIntegerBoundsX t = + (HasIntegerBounds t, + -- CanNegSameType t, + -- CanTestPosNeg t, + HasOrderCertainly t Integer, + CanTestFinite t, + Show t, Arbitrary t) + + +{-| + HSpec properties that each implementation of CanRound should satisfy. + -} +specHasIntegerBounds :: + (HasIntegerBoundsX t) + => + T t -> Spec +specHasIntegerBounds (T typeName :: T t) = + describe (printf "HasIntegerBounds %s" typeName) $ do + it "holds l <= x <= r" $ do + property $ \ (x :: t) -> + isFinite x ==> + let (l,r) = integerBounds x in + (l ?<=?$ x) .&&. (x ?<=?$ r) + where + (?<=?$) :: (HasOrderCertainlyAsymmetric a b, Show a, Show b) => a -> b -> Property + (?<=?$) = printArgsIfFails2 "?<=?" (?<=?) diff --git a/test/Spec.hs b/test/Spec.hs new file mode 100644 --- /dev/null +++ b/test/Spec.hs @@ -0,0 +1,1 @@ +{-# OPTIONS_GHC -F -pgmF hspec-discover #-}