diff --git a/semiring-num.cabal b/semiring-num.cabal --- a/semiring-num.cabal +++ b/semiring-num.cabal @@ -1,5 +1,5 @@ name: semiring-num -version: 0.9.0.1 +version: 1.0.0.0 synopsis: Basic semiring class and instances description: Adds a basic semiring class homepage: https://github.com/oisdk/semiring-num @@ -17,9 +17,9 @@ exposed-modules: Data.Semiring , Data.Semiring.Numeric , Data.Semiring.Free + , Data.Semiring.Infinite , Test.Semiring - other-modules: Data.Semiring.Infinite - , Data.Semiring.TH + other-modules: Data.Semiring.TH build-depends: base >= 4.9 && < 5 , containers >= 0.5 , template-haskell >= 2.11 diff --git a/src/Data/Semiring.hs b/src/Data/Semiring.hs --- a/src/Data/Semiring.hs +++ b/src/Data/Semiring.hs @@ -16,20 +16,21 @@ -} module Data.Semiring - ( Semiring(..) + ( -- * Semiring classes + Semiring(..) , StarSemiring(..) + -- * Helper classes , HasPositiveInfinity(..) , HasNegativeInfinity(..) - , PositiveInfinite(..) - , NegativeInfinite(..) - , Infinite(..) + , DetectableZero(..) + -- * Monoidal wrappers , Add(..) , Mul(..) , add , mul + -- * Ordering wrappers , Max(..) , Min(..) - , DetectableZero(..) ) where import Data.Functor.Identity (Identity (..)) @@ -55,14 +56,12 @@ import Data.Semigroup hiding (Max (..), Min (..)) -import Control.Applicative (liftA2) import Data.Coerce (coerce) import GHC.Generics (Generic, Generic1) import Data.Typeable (Typeable) import Foreign.Storable (Storable) -import Data.Semiring.Infinite import Data.Semiring.TH @@ -147,16 +146,56 @@ star x = one <+> plus x plus x = x <.> star x +-- | Useful for operations where zeroes may need to be discarded: for instance +-- in sparse matrix calculations. class Semiring a => DetectableZero a where + -- | 'True' if x is 'zero'. isZero :: a -> Bool default isZero :: Eq a => a -> Bool isZero = (zero==) ------------------------------------------------------------------------- --- Instances ------------------------------------------------------------------------- -type CoerceBinary a b = (a -> a -> a) -> b -> b -> b +-------------------------------------------------------------------------------- +-- Infinites +-------------------------------------------------------------------------------- +-- | A class for semirings with a concept of "infinity". It's important that +-- this isn't regarded as the same as "bounded": +-- @x '<+>' 'positiveInfinity'@ should probably equal 'positiveInfinity'. +class HasPositiveInfinity a where + -- | A positive infinite value + positiveInfinity :: a + default positiveInfinity :: RealFloat a => a + positiveInfinity = 1/0 + -- | Test if a value is positive infinity. + isPositiveInfinity :: a -> Bool + default isPositiveInfinity :: RealFloat a => a -> Bool + isPositiveInfinity x = isInfinite x && x > 0 + +-- | A class for semirings with a concept of "negative infinity". It's important\ +-- that this isn't regarded as the same as "bounded": +-- @x '<+>' 'negativeInfinity'@ should probably equal 'negativeInfinity'. +class HasNegativeInfinity a where + -- | A negative infinite value + negativeInfinity :: a + default negativeInfinity :: RealFloat a => a + negativeInfinity = negate (1/0) + -- | Test if a value is negative infinity. + isNegativeInfinity :: a -> Bool + default isNegativeInfinity :: RealFloat a => a -> Bool + isNegativeInfinity x = isInfinite x && x < 0 + +instance HasPositiveInfinity Double +instance HasNegativeInfinity Double +instance HasPositiveInfinity Float +instance HasNegativeInfinity Float +instance HasPositiveInfinity CDouble +instance HasNegativeInfinity CDouble +instance HasPositiveInfinity CFloat +instance HasNegativeInfinity CFloat + +-------------------------------------------------------------------------------- +-- Instances +-------------------------------------------------------------------------------- instance Semiring Bool where one = True zero = False @@ -175,67 +214,7 @@ instance DetectableZero Bool --- | Not lawful. Only for convenience. -instance DetectableZero a => - Semiring (NegativeInfinite a) where - one = pure one - zero = pure zero - (<+>) = - (coerce :: CoerceBinary (NegativeInfinite (Add a)) (NegativeInfinite a)) - mappend - x <.> y | any isZero x || any isZero y = zero - | otherwise = liftA2 (<.>) x y - {-# INLINE zero #-} - {-# INLINE one #-} - {-# INLINE (<+>) #-} - {-# INLINE (<.>) #-} --- | Not lawful. Only for convenience. -instance (DetectableZero a) => - Semiring (PositiveInfinite a) where - one = pure one - zero = pure zero - (<+>) = - (coerce :: CoerceBinary (PositiveInfinite (Add a)) (PositiveInfinite a)) - mappend - x <.> y | any isZero x || any isZero y = zero - | otherwise = liftA2 (<.>) x y - {-# INLINE zero #-} - {-# INLINE one #-} - {-# INLINE (<+>) #-} - {-# INLINE (<.>) #-} - --- | Not lawful. Only for convenience. -instance (DetectableZero a) => - Semiring (Infinite a) where - one = pure one - zero = pure zero - (<+>) = (coerce :: CoerceBinary (Infinite (Add a)) (Infinite a)) mappend - x <.> y | any isZero x || any isZero y = zero - | otherwise = liftA2 (<.>) x y - {-# INLINE zero #-} - {-# INLINE one #-} - {-# INLINE (<+>) #-} - {-# INLINE (<.>) #-} - -instance (DetectableZero a) => - StarSemiring (PositiveInfinite a) where - star (PosFinite x) - | isZero x = one - star _ = PositiveInfinity - -instance DetectableZero a => - DetectableZero (NegativeInfinite a) where - isZero = any isZero - -instance DetectableZero a => - DetectableZero (PositiveInfinite a) where - isZero = any isZero - -instance DetectableZero a => - DetectableZero (Infinite a) where - isZero = any isZero - instance Semiring () where one = () zero = () @@ -256,7 +235,8 @@ -- | A polynomial in /x/ can be defined as a list of its coefficients, -- where the /i/th element is the coefficient of /x^i/. This is the --- semiring for such a list. Adapted from . +-- semiring for such a list. Adapted from +-- . instance Semiring a => Semiring [a] where one = [one] @@ -272,9 +252,9 @@ instance Semiring a => DetectableZero [a] where isZero = null ------------------------------------------------------------------------- +-------------------------------------------------------------------------------- -- Addition and multiplication newtypes ------------------------------------------------------------------------- +-------------------------------------------------------------------------------- type WrapBinary f a = (a -> a -> a) -> f a -> f a -> f a -- | Monoid under '<+>'. Analogous to 'Data.Monoid.Sum', but uses the @@ -317,9 +297,9 @@ {-# INLINE mempty #-} {-# INLINE mappend #-} ------------------------------------------------------------------------- +-------------------------------------------------------------------------------- -- Addition and multiplication folds ------------------------------------------------------------------------- +-------------------------------------------------------------------------------- -- | Takes the sum of the elements of a 'Foldable'. Analogous to 'sum' -- on numbers, or 'or' on 'Bool's. -- @@ -352,9 +332,9 @@ => f a -> a mul = getMul . foldMap Mul ------------------------------------------------------------------------- +-------------------------------------------------------------------------------- -- Ord wrappers ------------------------------------------------------------------------- +-------------------------------------------------------------------------------- -- | The "" or -- min-plus semiring. It is a semiring where: -- @@ -463,9 +443,9 @@ instance (Semiring a, Ord a, HasNegativeInfinity a) => DetectableZero (Max a) where isZero (Max x) = isNegativeInfinity x ------------------------------------------------------------------------- +-------------------------------------------------------------------------------- -- (->) instance ------------------------------------------------------------------------- +-------------------------------------------------------------------------------- -- | The @(->)@ instance is analogous to the one for 'Monoid'. instance Semiring b => Semiring (a -> b) where @@ -479,9 +459,9 @@ star f x = star (f x) plus f x = plus (f x) ------------------------------------------------------------------------- +-------------------------------------------------------------------------------- -- Endo instance ------------------------------------------------------------------------- +-------------------------------------------------------------------------------- -- | This is /not/ a true semiring. In particular, it requires the -- underlying monoid to be commutative, and even then, it is only a near -- semiring. It is, however, extremely useful. For instance, this type: @@ -519,9 +499,9 @@ instance (Enum a, Bounded a, Eq a, Monoid a) => DetectableZero (Endo a) where isZero (Endo f) = all (mempty==) (map f [minBound..maxBound]) ------------------------------------------------------------------------- +-------------------------------------------------------------------------------- -- Instances for Bool wrappers ------------------------------------------------------------------------- +-------------------------------------------------------------------------------- instance Semiring Any where (<+>) = coerce (||) zero = Any False @@ -557,9 +537,9 @@ instance DetectableZero Any instance DetectableZero All ------------------------------------------------------------------------- +-------------------------------------------------------------------------------- -- Boring instances ------------------------------------------------------------------------- +-------------------------------------------------------------------------------- instance Semiring Int instance Semiring Int8 @@ -685,9 +665,9 @@ instance HasResolution a => DetectableZero (Fixed a) deriving instance DetectableZero a => DetectableZero (Identity a) ------------------------------------------------------------------------- +-------------------------------------------------------------------------------- -- Very boring instances ------------------------------------------------------------------------- +-------------------------------------------------------------------------------- $(traverse semiringIns [2..9]) $(traverse starIns [2..9]) diff --git a/src/Data/Semiring/Infinite.hs b/src/Data/Semiring/Infinite.hs --- a/src/Data/Semiring/Infinite.hs +++ b/src/Data/Semiring/Infinite.hs @@ -1,4 +1,3 @@ -{-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE DeriveFoldable #-} {-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE DeriveGeneric #-} @@ -6,6 +5,8 @@ {-# LANGUAGE LambdaCase #-} {-# LANGUAGE ScopedTypeVariables #-} +-- | This module provides various "infinite" wrappers, which can provide +-- a detectable infinity to an otherwise non-infinite type. module Data.Semiring.Infinite ( HasPositiveInfinity(..) , HasNegativeInfinity(..) @@ -14,8 +15,6 @@ , Infinite(..) ) where -import Foreign.C.Types (CDouble, CFloat) - import Control.Applicative (liftA2) import Data.Typeable (Typeable) import GHC.Generics (Generic, Generic1) @@ -28,37 +27,18 @@ import Data.Coerce import Data.Monoid -class HasPositiveInfinity a where - positiveInfinity :: a - default positiveInfinity :: RealFloat a => a - positiveInfinity = 1/0 - isPositiveInfinity :: a -> Bool - default isPositiveInfinity :: RealFloat a => a -> Bool - isPositiveInfinity x = isInfinite x && x > 0 - -class HasNegativeInfinity a where - negativeInfinity :: a - default negativeInfinity :: RealFloat a => a - negativeInfinity = negate (1/0) - isNegativeInfinity :: a -> Bool - default isNegativeInfinity :: RealFloat a => a -> Bool - isNegativeInfinity x = isInfinite x && x < 0 - -instance HasPositiveInfinity Double -instance HasNegativeInfinity Double -instance HasPositiveInfinity Float -instance HasNegativeInfinity Float -instance HasPositiveInfinity CDouble -instance HasNegativeInfinity CDouble -instance HasPositiveInfinity CFloat -instance HasNegativeInfinity CFloat +import Data.Semiring +-- | Adds negative infinity to a type. Useful for expressing detectable infinity +-- in types like 'Integer', etc. data NegativeInfinite a = NegativeInfinity | NegFinite !a deriving (Eq, Ord, Read, Show, Generic, Generic1, Typeable, Functor ,Foldable, Traversable) +-- | Adds positive infinity to a type. Useful for expressing detectable infinity +-- in types like 'Integer', etc. data PositiveInfinite a = PosFinite !a | PositiveInfinity @@ -79,12 +59,94 @@ _ <*> _ = PositiveInfinity {-# INLINE (<*>) #-} +-- | Adds positive and negative infinity to a type. Useful for expressing +-- detectable infinity in types like 'Integer', etc. data Infinite a = Negative | Finite !a | Positive deriving (Eq, Ord, Read, Show, Generic, Generic1, Typeable, Functor ,Foldable, Traversable) + +-- | Doesn't follow 'annihilateL' or 'mulDistribR'. +instance DetectableZero a => + Semiring (NegativeInfinite a) where + one = pure one + zero = pure zero + (<+>) = + (coerce :: CoerceBinary (NegativeInfinite (Add a)) (NegativeInfinite a)) + mappend + x <.> y | any isZero x = zero + | otherwise = liftA2 (<.>) x y + {-# INLINE zero #-} + {-# INLINE one #-} + {-# INLINE (<+>) #-} + {-# INLINE (<.>) #-} + +-- | Only lawful when used with positive numbers. +instance DetectableZero a => + Semiring (PositiveInfinite a) where + one = pure one + zero = pure zero + (<+>) = + (coerce :: CoerceBinary (PositiveInfinite (Add a)) (PositiveInfinite a)) + mappend + x <.> y | any isZero x || any isZero y = zero + | otherwise = liftA2 (<.>) x y + {-# INLINE zero #-} + {-# INLINE one #-} + {-# INLINE (<+>) #-} + {-# INLINE (<.>) #-} + +-- | Not distributive. +instance (DetectableZero a, Ord a) => + Semiring (Infinite a) where + one = pure one + zero = pure zero + (<+>) = (coerce :: CoerceBinary (Infinite (Add a)) (Infinite a)) mappend + Finite x <.> Finite y = Finite (x <.> y) + Finite x <.> Negative = case compare x zero of + LT -> Positive + EQ -> zero + GT -> Negative + Finite x <.> Positive = case compare x zero of + LT -> Negative + EQ -> zero + GT -> Positive + Negative <.> Finite y = case compare y zero of + LT -> Positive + EQ -> zero + GT -> Negative + Positive <.> Finite y = case compare y zero of + LT -> Negative + EQ -> zero + GT -> Positive + Negative <.> Negative = Positive + Negative <.> Positive = Negative + Positive <.> Negative = Negative + Positive <.> Positive = Positive + {-# INLINE zero #-} + {-# INLINE one #-} + {-# INLINE (<+>) #-} + {-# INLINE (<.>) #-} + +instance (DetectableZero a) => + StarSemiring (PositiveInfinite a) where + star (PosFinite x) + | isZero x = one + star _ = PositiveInfinity + +instance DetectableZero a => + DetectableZero (NegativeInfinite a) where + isZero = any isZero + +instance DetectableZero a => + DetectableZero (PositiveInfinite a) where + isZero = any isZero + +instance (DetectableZero a, Ord a) => + DetectableZero (Infinite a) where + isZero = any isZero instance Applicative Infinite where pure = Finite diff --git a/src/Data/Semiring/Numeric.hs b/src/Data/Semiring/Numeric.hs --- a/src/Data/Semiring/Numeric.hs +++ b/src/Data/Semiring/Numeric.hs @@ -133,7 +133,7 @@ -- -- @('<.>') = ('+') --x '<+>' y = -('log' ('exp' (-x) + 'exp' (-y))) ---'zero' = ∞ +--'zero' = 'positiveInfinity' --'one' = 0@ newtype Log a = Log { getLog :: a @@ -154,6 +154,13 @@ instance (Floating a, HasPositiveInfinity a) => DetectableZero (Log a) where isZero (Log x) = isPositiveInfinity x +-- | Adds a star operation to fractional types. +-- +-- @('<+>') = ('<+>') +--('<.>') = ('<.>') +--'zero' = 'zero' +--'one' = 'one' +--'star' x = if x < 1 then 1 / (1 - x) else 'positiveInfinity'@ newtype PosFrac a = PosFrac { getPosFrac :: a } deriving (Eq, Ord, Read, Show, Generic, Generic1, Num @@ -182,6 +189,14 @@ | n < 1 = PosFrac (1 / (1 - n)) | otherwise = PosFrac positiveInfinity +-- | Adds a star operation to integral types. +-- +-- @('<+>') = ('<+>') +--('<.>') = ('<.>') +--'zero' = 'zero' +--'one' = 'one' +--'star' 0 = 1 +--'star' _ = 'positiveInfinity'@ newtype PosInt a = PosInt { getPosInt :: a } deriving (Eq, Ord, Read, Show, Generic, Generic1, Num diff --git a/src/Test/Semiring.hs b/src/Test/Semiring.hs --- a/src/Test/Semiring.hs +++ b/src/Test/Semiring.hs @@ -2,285 +2,599 @@ {-| Module: Test.Semiring -Description: Some QuickCheck properties for Semirings +Description: Some functions for generating tests for 'Semiring's. License: MIT Maintainer: mail@doisinkidney.com Stability: experimental --} +This module provides functions which can be quickly converted into + or +-like properties. +The functions are of the form: + +> a -> Either String String + +where the left case is failure of the test, and the right case is success. + +For smallcheck, this function can be used directly as a property: + +> smallCheck 10 (plusId :: UnaryLaws Integer) + +(the typealias is provided as well) + +For QuickCheck, you might want to provide an instance like this: + +> instance Testable (Either String String) where +> property = either (`counterexample` False) (const (property True)) + +And then testing is as simple as: + +> quickCheck (plusAssoc :: TernaryLaws Integer) + +There are also functions provided to test multiple laws at once. Putting all of +this together, writing a test for all the semiring laws for, say, 'Integer' +looks like this: + +> quickCheck (unaryLaws :: UnaryLaws Integer) +> quickCheck (binaryLaws :: BinaryLaws Integer) +> quickCheck (ternaryLaws :: TernaryLaws Integer) +-} module Test.Semiring - ( plusAssoc - , mulAssoc - , plusComm - , mulDistribL - , mulDistribR - , plusId - , mulId - , annihilate - , unaryLaws - , binaryLaws - , ternaryLaws - , starLaw - , plusLaw - , starLaws - , nearTernaryLaws - , ordLaws - , zeroLaw - , zeroIsZero - , zeroLaws - , nearUnaryLaws - ) where + ( + -- * Type Aliases + UnaryLaws + ,BinaryLaws + ,TernaryLaws + , + -- * Semiring Laws + -- ** Unary + plusId + ,mulId + ,annihilateL + ,annihilateR + ,unaryLaws + , + -- ** Binary + plusComm + ,binaryLaws + , + -- ** Ternary + plusAssoc + ,mulAssoc + ,mulDistribL + ,mulDistribR + ,ternaryLaws + , + -- * Near-semiring laws + -- ** Unary + nearUnaryLaws + , + -- ** Ternary + nearTernaryLaws + , + -- * StarSemiring Laws + -- ** Unary + starLaw + ,plusLaw + ,starLaws + , + -- * DetectableZero Laws + -- ** Unary + zeroLaw + ,zeroIsZero + ,zeroLaws + , + -- * Ordering Laws + -- ** Ternary + ordMulLaw + ,ordAddLaw + ,ordLaws) + where -import Data.Semiring (Semiring (..), StarSemiring (..), DetectableZero(..)) +import Data.Semiring + (Semiring(..), StarSemiring(..), DetectableZero(..)) +-- | Typealias for unary laws. Can be used like so: +-- +-- > smallCheck 10 (unaryLaws :: UnaryLaws Int) +type UnaryLaws a = a -> Either String String + +-- | Typealias for binary laws. Can be used like so: +-- +-- > smallCheck 8 (binaryLaws :: BinaryLaws Int) +type BinaryLaws a = a -> a -> Either String String + +-- | Typealias for ternary laws. Can be used like so: +-- +-- > smallCheck 6 (ternaryLaws :: TernaryLaws Int) +type TernaryLaws a = a -> a -> a -> Either String String + -- | Plus is associative. -plusAssoc :: (Eq a, Semiring a, Show a) => a -> a -> a -> Either String String -plusAssoc x y z = if res then Right s else Left s where - res = lp == rp - l = x <+> y - r = y <+> z - lp = l <+> z - rp = x <+> r - s = unlines - [ "<+> is " ++ (if res then "" else "not ") ++ "associative." - , " Law:" - , " (x <+> y) <+> z = x <+> (y <+> z)" - , " x = " ++ show x - , " y = " ++ show y - , " z = " ++ show z - , " x <+> y = " ++ show l - , " y <+> z = " ++ show r - , " (x <+> y) <+> z = " ++ show lp - , " x <+> (y <+> z) = " ++ show rp ] +-- +-- @(x '<+>' y) '<+>' z = x '<+>' (y '<+>' z)@ +plusAssoc + :: (Eq a, Semiring a, Show a) + => a -> a -> a -> Either String String +plusAssoc x y z = + if res + then Right s + else Left s + where + res = lp == rp + l = x <+> y + r = y <+> z + lp = l <+> z + rp = x <+> r + s = + unlines + [ "<+> is " ++ + (if res + then "" + else "not ") ++ + "associative." + , " Law:" + , " (x <+> y) <+> z = x <+> (y <+> z)" + , " x = " ++ show x + , " y = " ++ show y + , " z = " ++ show z + , " x <+> y = " ++ show l + , " y <+> z = " ++ show r + , " (x <+> y) <+> z = " ++ show lp + , " x <+> (y <+> z) = " ++ show rp] -- | Multiplication is associative. -mulAssoc :: (Eq a, Semiring a, Show a) => a -> a -> a -> Either String String -mulAssoc x y z = if res then Right s else Left s where - res = lp == rp - l = x <.> y - r = y <.> z - lp = l <.> z - rp = x <.> r - s = unlines - [ "<+> is " ++ (if res then "" else "not ") ++ "associative." - , " Law:" - , " (x <.> y) <.> z = x <.> (y <.> z)" - , " x = " ++ show x - , " y = " ++ show y - , " z = " ++ show z - , " x <.> y = " ++ show l - , " y <.> z = " ++ show r - , " (x <.> y) <.> z = " ++ show lp - , " x <.> (y <.> z) = " ++ show rp] +-- +-- @(x '<.>' y) '<.>' z = x '<.>' (y '<.>' z)@ +mulAssoc + :: (Eq a, Semiring a, Show a) + => a -> a -> a -> Either String String +mulAssoc x y z = + if res + then Right s + else Left s + where + res = lp == rp + l = x <.> y + r = y <.> z + lp = l <.> z + rp = x <.> r + s = + unlines + [ "<+> is " ++ + (if res + then "" + else "not ") ++ + "associative." + , " Law:" + , " (x <.> y) <.> z = x <.> (y <.> z)" + , " x = " ++ show x + , " y = " ++ show y + , " z = " ++ show z + , " x <.> y = " ++ show l + , " y <.> z = " ++ show r + , " (x <.> y) <.> z = " ++ show lp + , " x <.> (y <.> z) = " ++ show rp] -- | Plus is commutative. -plusComm :: (Eq a, Semiring a, Show a) => a -> a -> Either String String -plusComm x y = if res then Right s else Left s where - res = l == r - l = x <+> y - r = y <+> x - s = unlines - [ "<+> is " ++ (if res then "" else "not ") ++ "commutative." - , " Law:" - , " x <+> y = y <+> x" - , " x = " ++ show x - , " y = " ++ show y - , " x <+> y = " ++ show l - , " y <+> x = " ++ show r ] +-- +-- @x '<+>' y = y '<+>' x@ +plusComm + :: (Eq a, Semiring a, Show a) + => a -> a -> Either String String +plusComm x y = + if res + then Right s + else Left s + where + res = l == r + l = x <+> y + r = y <+> x + s = + unlines + [ "<+> is " ++ + (if res + then "" + else "not ") ++ + "commutative." + , " Law:" + , " x <+> y = y <+> x" + , " x = " ++ show x + , " y = " ++ show y + , " x <+> y = " ++ show l + , " y <+> x = " ++ show r] -- | Multiplication distributes left. -mulDistribL :: (Eq a, Semiring a, Show a) => a -> a -> a -> Either String String -mulDistribL x y z = if res then Right s else Left s where - res = l == r - l = x <.> (y <+> z) - r = x <.> y <+> x <.> z - s = unlines - [ "<.> does " ++ (if res then "" else "not ") ++ "distribute left over <+>." - , " Law:" - , " x <.> (y <+> z) = x <.> y <+> x <.> z" - , " x = " ++ show x - , " y = " ++ show y - , " z = " ++ show z - , " x <.> (y <+> z) = " ++ show l - , " x <.> y <+> x <.> z = " ++ show r ] +-- +-- @x '<.>' (y '<+>' z) = x '<.>' y '<+>' x '<.>' z@ +mulDistribL + :: (Eq a, Semiring a, Show a) + => a -> a -> a -> Either String String +mulDistribL x y z = + if res + then Right s + else Left s + where + res = l == r + l = x <.> (y <+> z) + r = x <.> y <+> x <.> z + s = + unlines + [ "<.> does " ++ + (if res + then "" + else "not ") ++ + "distribute left over <+>." + , " Law:" + , " x <.> (y <+> z) = x <.> y <+> x <.> z" + , " x = " ++ show x + , " y = " ++ show y + , " z = " ++ show z + , " x <.> (y <+> z) = " ++ show l + , " x <.> y <+> x <.> z = " ++ show r] -- | Multiplication distributes right. -mulDistribR :: (Eq a, Semiring a, Show a) => a -> a -> a -> Either String String -mulDistribR x y z = if res then Right s else Left s where - res = l == r - l = (x <+> y) <.> z - r = x <.> z <+> y <.> z - s = unlines - [ "<.> does " ++ (if res then "" else "not ") ++ "distribute right over <+>." - , " Law:" - , " (x <+> y) <.> z = x <.> z <+> y <.> z" - , " x = " ++ show x - , " y = " ++ show y - , " z = " ++ show z - , " (x <+> y) <.> z = " ++ show l - , " x <.> z <+> y <.> z = " ++ show r ] +-- +-- @(x '<+>' y) '<.>' z = x '<.>' z '<+>' y '<.>' z@ +mulDistribR + :: (Eq a, Semiring a, Show a) + => a -> a -> a -> Either String String +mulDistribR x y z = + if res + then Right s + else Left s + where + res = l == r + l = (x <+> y) <.> z + r = x <.> z <+> y <.> z + s = + unlines + [ "<.> does " ++ + (if res + then "" + else "not ") ++ + "distribute right over <+>." + , " Law:" + , " (x <+> y) <.> z = x <.> z <+> y <.> z" + , " x = " ++ show x + , " y = " ++ show y + , " z = " ++ show z + , " (x <+> y) <.> z = " ++ show l + , " x <.> z <+> y <.> z = " ++ show r] -- | Additive identity. -plusId :: (Eq a, Semiring a, Show a) => a -> Either String String -plusId (x :: a) = if res then Right s else Left s where - res = l == x && r ==x - l = x <+> zero - r = zero <+> x - s = unlines - [ "zero is" ++ (if res then "" else " not") ++ " the identity of <+>." - , " Law:" - , " x <+> zero = zero <+> x = x" - , " x = " ++ show x - , " zero = " ++ show (zero :: a) - , " x <+> zero = " ++ show l - , " zero <+> x = " ++ show r ] +-- +-- @x '<+>' 'zero' = 'zero' '<+>' x = x@ +plusId + :: (Eq a, Semiring a, Show a) + => a -> Either String String +plusId (x :: a) = + if res + then Right s + else Left s + where + res = l == x && r == x + l = x <+> zero + r = zero <+> x + s = + unlines + [ "zero is" ++ + (if res + then "" + else " not") ++ + " the identity of <+>." + , " Law:" + , " x <+> zero = zero <+> x = x" + , " x = " ++ show x + , " zero = " ++ show (zero :: a) + , " x <+> zero = " ++ show l + , " zero <+> x = " ++ show r] -- | Multiplicative identity. -mulId :: (Eq a, Semiring a, Show a) => a -> Either String String -mulId (x :: a) = if res then Right s else Left s where - res = l == x && r == x - l = x <.> one - r = one <.> x - s = unlines - [ "one is" ++ (if res then "" else " not") ++ " the identity of <+>." - , " Law:" - , " x <.> one = one <.> x = x" - , " x = " ++ show x - , " one = " ++ show (one :: a) - , " x <.> one = " ++ show l - , " one <.> x = " ++ show r ] +-- +-- @x '<.>' 'one' = 'one' '<.>' x = x@ +mulId + :: (Eq a, Semiring a, Show a) + => a -> Either String String +mulId (x :: a) = + if res + then Right s + else Left s + where + res = l == x && r == x + l = x <.> one + r = one <.> x + s = + unlines + [ "one is" ++ + (if res + then "" + else " not") ++ + " the identity of <+>." + , " Law:" + , " x <.> one = one <.> x = x" + , " x = " ++ show x + , " one = " ++ show (one :: a) + , " x <.> one = " ++ show l + , " one <.> x = " ++ show r] --- | Annihilation of '<.>' by 'zero'. -annihilate :: (Eq a, Semiring a, Show a) => a -> Either String String -annihilate (x :: a) = if res then Right s else Left s where - res = l == zero && r == zero - l = x <.> zero - r = zero <.> x - s = unlines - [ "zero does " ++ (if res then "" else "not ") ++ "annihilate with <.>." - , " Law:" - , " x <.> zero = zero <.> x = zero" - , " x = " ++ show x - , " zero = " ++ show (zero :: a) - , " x <.> zero = " ++ show l - , " zero <.> x = " ++ show r ] +-- | Right annihilation of '<.>' by 'zero'. +-- +-- @'zero' '<.>' x = 'zero'@ +annihilateR + :: (Eq a, Semiring a, Show a) + => a -> Either String String +annihilateR (x :: a) = + if res + then Right s + else Left s + where + res = r == zero + r = zero <.> x + s = + unlines + [ "zero does " ++ + (if res + then "" + else "not ") ++ + "annihilate right with <.>." + , " Law:" + , " zero <.> x = zero" + , " x = " ++ show x + , " zero = " ++ show (zero :: a) + , " zero <.> x = " ++ show r] -unaryLaws :: (Eq a, Semiring a, Show a) => a -> Either String String -unaryLaws x = fmap unlines (sequence [plusId x, mulId x, annihilate x]) +-- | Left annihilation of '<.>' by 'zero'. +-- +-- @x '<.>' 'zero' = 'zero'@ +annihilateL + :: (Eq a, Semiring a, Show a) + => a -> Either String String +annihilateL (x :: a) = + if res + then Right s + else Left s + where + res = l == zero + l = x <.> zero + s = + unlines + [ "zero does " ++ + (if res + then "" + else "not ") ++ + "annihilate left with <.>." + , " Law:" + , " x <.> zero = zero" + , " x = " ++ show x + , " zero = " ++ show (zero :: a) + , " x <.> zero = " ++ show l] -nearUnaryLaws :: (Eq a, Semiring a, Show a) => a -> Either String String -nearUnaryLaws x = fmap unlines (sequence [plusId x, annihilate x]) +-- | A test for all three unary laws for 'Semiring's ('plusId', 'mulId', +-- 'annihilateL', and 'annihilateR'). +unaryLaws + :: (Eq a, Semiring a, Show a) + => a -> Either String String +unaryLaws x = + fmap unlines (sequence [plusId x, mulId x, annihilateL x, annihilateR x]) -nearTernaryLaws :: (Eq a, Semiring a, Show a) - => a -> a -> a -> Either String String +-- | A test for the unary laws for near-'Semiring's ('plusId', 'mulId', and +-- 'annihilateR'). +nearUnaryLaws + :: (Eq a, Semiring a, Show a) + => a -> Either String String +nearUnaryLaws x = fmap unlines (sequence [plusId x, mulId x, annihilateR x]) + +-- | A test for all of the ternary laws for near-'Semiring's ('plusAssoc', +-- 'mulAssoc', 'mulDistribR'). +nearTernaryLaws + :: (Eq a, Semiring a, Show a) + => a -> a -> a -> Either String String nearTernaryLaws x y z = - fmap unlines (sequence [ plusAssoc x y z - , mulAssoc x y z - , mulDistribR x y z]) + fmap + unlines + (sequence [plusAssoc x y z, mulAssoc x y z, mulDistribR x y z]) -binaryLaws :: (Eq a, Semiring a, Show a) - => a -> a -> Either String String +-- | A test for all of the binary laws for 'Semiring's (just 'plusComm'). +binaryLaws + :: (Eq a, Semiring a, Show a) + => a -> a -> Either String String binaryLaws = plusComm -ternaryLaws :: (Eq a, Semiring a, Show a) - => a -> a -> a -> Either String String +-- | A test for all of the ternary laws for 'Semiring's ('plusAssoc', 'mulAssoc', +-- 'mulDistribL', 'mulDistribR'). +ternaryLaws + :: (Eq a, Semiring a, Show a) + => a -> a -> a -> Either String String ternaryLaws x y z = - fmap unlines (sequence [ plusAssoc x y z - , mulAssoc x y z - , mulDistribL x y z - , mulDistribR x y z]) + fmap + unlines + (sequence + [ plusAssoc x y z + , mulAssoc x y z + , mulDistribR x y z + , mulDistribL x y z]) -starLaw :: (Eq a, StarSemiring a, Show a) => a -> Either String String -starLaw (x :: a) = if res then Right s else Left s where - res = l == st && r == st - l = one <+> x <.> star x - r = one <+> star x <.> x - st = star x - s = unlines - [ "star law" ++ (if res then "" else " not") ++ " followed." - , " Law:" - , " star x = one <+> x <.> star x = one <+> star x <.> x" - , " x = " ++ show x - , " one = " ++ show (one :: a) - , " star x = " ++ show st - , " one <+> x <.> star x = " ++ show l - , " one <+> star x <.> x = " ++ show r ] +-- | The star law for 'StarSemiring's. +-- +-- @'star' x = 'one' '<+>' x '<.>' 'star' x = 'one' '<+>' 'star' x '<.>' x@ +starLaw + :: (Eq a, StarSemiring a, Show a) + => a -> Either String String +starLaw (x :: a) = + if res + then Right s + else Left s + where + res = l == st && r == st + l = one <+> x <.> star x + r = one <+> star x <.> x + st = star x + s = + unlines + [ "star law" ++ + (if res + then "" + else " not") ++ + " followed." + , " Law:" + , " star x = one <+> x <.> star x = one <+> star x <.> x" + , " x = " ++ show x + , " one = " ++ show (one :: a) + , " star x = " ++ show st + , " one <+> x <.> star x = " ++ show l + , " one <+> star x <.> x = " ++ show r] -plusLaw :: (Eq a, StarSemiring a, Show a) => a -> Either String String -plusLaw (x :: a) = if res then Right s else Left s where - res = r == st - r = x <.> star x - st = plus x - s = unlines - [ "plus law" ++ (if res then "" else " not") ++ " followed." - , " Law:" - , " plus x = x <.> star x" - , " x = " ++ show x - , " star x = " ++ show st - , " x <.> star x = " ++ show r ] +-- | The plus law for 'StarSemiring's. +-- +-- @'plus' x = x '<.>' 'star' x@ +plusLaw + :: (Eq a, StarSemiring a, Show a) + => a -> Either String String +plusLaw (x :: a) = + if res + then Right s + else Left s + where + res = r == st + r = x <.> star x + st = plus x + s = + unlines + [ "plus law" ++ + (if res + then "" + else " not") ++ + " followed." + , " Law:" + , " plus x = x <.> star x" + , " x = " ++ show x + , " star x = " ++ show st + , " x <.> star x = " ++ show r] -starLaws :: (Eq a, StarSemiring a, Show a) => a -> Either String String +-- | The laws for 'StarSemiring's ('starLaw', 'plusLaw'). +starLaws + :: (Eq a, StarSemiring a, Show a) + => a -> Either String String starLaws x = fmap unlines (sequence [starLaw x, plusLaw x]) - -ordAddLaw :: (Ord a, Semiring a, Show a) => a -> a -> a -> Either String String -ordAddLaw (x :: a) (y :: a) (z :: a) = if res then Right s else Left s where - cnd = x <= y - lhs = x <+> z <= y <+> z - rhs = z <+> x <= z <+> y - res = not cnd || lhs && rhs - s = unlines - [ "ordering law" ++ (if res then "" else " not") ++ " followed." - , " Law:" - , " x <= y => x <+> z <= y <+> z && z <+> x <= z <+> y" - , " x = " ++ show x - , " y = " ++ show y - , " z = " ++ show z ] - -ordMulLaw :: (Ord a, Semiring a, Show a) => a -> a -> a -> Either String String -ordMulLaw (x :: a) (y :: a) (z :: a) = if res then Right s else Left s where - cnd = x <= y && zero <= z - lhs = x <.> z <= y <.> z - rhs = z <.> x <= z <.> y - res = not cnd || lhs && rhs - s = unlines - [ "ordering law" ++ (if res then "" else " not") ++ " followed." - , " Law:" - , " x <= y => x <.> z <= y <.> z && z <.> x <= z <.> y" - , " x = " ++ show x - , " y = " ++ show y - , " z = " ++ show z ] +-- | Addition law for ordered 'Semiring's. +-- +-- @x '<=' y => x '<+>' z '<=' y '<+>' z '&&' z '<+>' x '<=' z '<+>' y@ +ordAddLaw + :: (Ord a, Semiring a, Show a) + => a -> a -> a -> Either String String +ordAddLaw (x :: a) (y :: a) (z :: a) = + if res + then Right s + else Left s + where + cnd = x <= y + lhs = x <+> z <= y <+> z + rhs = z <+> x <= z <+> y + res = not cnd || lhs && rhs + s = + unlines + [ "additive ordering law" ++ + (if res + then "" + else " not") ++ + " followed." + , " Law:" + , " x <= y => x <+> z <= y <+> z && z <+> x <= z <+> y" + , " x = " ++ show x + , " y = " ++ show y + , " z = " ++ show z] +-- | Multiplication law for ordered 'Semiring's. +-- +-- @x '<=' y => x '<.>' z '<=' y '<.>' z '&&' z '<.>' x '<=' z '<.>' y@ +ordMulLaw + :: (Ord a, Semiring a, Show a) + => a -> a -> a -> Either String String +ordMulLaw (x :: a) (y :: a) (z :: a) = + if res + then Right s + else Left s + where + cnd = x <= y && zero <= z + lhs = x <.> z <= y <.> z + rhs = z <.> x <= z <.> y + res = not cnd || lhs && rhs + s = + unlines + [ "ordering law" ++ + (if res + then "" + else " not") ++ + " followed." + , " Law:" + , " x <= y => x <.> z <= y <.> z && z <.> x <= z <.> y" + , " x = " ++ show x + , " y = " ++ show y + , " z = " ++ show z] -ordLaws :: (Ord a, Semiring a, Show a) => a -> a -> a -> Either String String +-- | Laws for ordered 'Semiring's ('ordMulLaw', 'ordAddLaw'). +ordLaws + :: (Ord a, Semiring a, Show a) + => a -> a -> a -> Either String String ordLaws x y z = fmap unlines (sequence [ordAddLaw x y z, ordMulLaw x y z]) - -zeroLaw :: (Eq a, DetectableZero a, Show a) => a -> Either String String -zeroLaw (x :: a) = if res then Right s else Left s where - lhs_1 = x == zero - lhs_2 = zero == x - rhs = isZero x - res = lhs_1 == rhs && lhs_2 == rhs - s = unlines - [ "zero law" ++ (if res then "" else " not") ++ " followed." - , " Law:" - , " x == zero = zero == x = isZero x" - , " x = " ++ show x - , " x == zero = " ++ show lhs_1 - , " zero == x = " ++ show lhs_2 - , " isZero x = " ++ show rhs ] +-- | Law for result of 'isZero' operation. +-- +-- @x '==' 'zero' = 'zero' '==' x = 'isZero' x@ +zeroLaw + :: (Eq a, DetectableZero a, Show a) + => a -> Either String String +zeroLaw (x :: a) = + if res + then Right s + else Left s + where + lhs_1 = x == zero + lhs_2 = zero == x + rhs = isZero x + res = lhs_1 == rhs && lhs_2 == rhs + s = + unlines + [ "zero law" ++ + (if res + then "" + else " not") ++ + " followed." + , " Law:" + , " x == zero = zero == x = isZero x" + , " x = " ++ show x + , " x == zero = " ++ show lhs_1 + , " zero == x = " ++ show lhs_2 + , " isZero x = " ++ show rhs] -zeroIsZero :: (DetectableZero a, Show a) => f a -> Either String String -zeroIsZero (_ :: f a) = if res then Right s else Left s where - z = zero :: a - res = isZero z - s = unlines - [ "zero is zero law" ++ (if res then "" else " not") ++ " followed." - , " Law:" - , " isZero zero = True" - , " zero = " ++ show z - , " isZero zero = " ++ show res ] +-- | Zero is zero law. +-- +-- @'isZero' 'zero' = 'True'@ +zeroIsZero + :: (DetectableZero a, Show a) + => f a -> Either String String +zeroIsZero (_ :: f a) = + if res + then Right s + else Left s + where + z = zero :: a + res = isZero z + s = + unlines + [ "zero is zero law" ++ + (if res + then "" + else " not") ++ + " followed." + , " Law:" + , " isZero zero = True" + , " zero = " ++ show z + , " isZero zero = " ++ show res] -zeroLaws :: (DetectableZero a, Show a, Eq a) => a -> Either String String +-- | The laws for 'DetectableZero' 'Semiring's ('zeroLaw', 'zeroIsZero'). +zeroLaws + :: (DetectableZero a, Show a, Eq a) + => a -> Either String String zeroLaws x = zeroLaw x *> zeroIsZero [x] diff --git a/test/Spec.hs b/test/Spec.hs --- a/test/Spec.hs +++ b/test/Spec.hs @@ -19,6 +19,7 @@ import Data.Monoid import Data.Semiring import Data.Semiring.Free +import Data.Semiring.Infinite import Data.Semiring.Numeric import GHC.TypeLits import Numeric.Sized.WordOfSize @@ -30,6 +31,8 @@ import Test.SmallCheck.Series hiding (Positive) import qualified Test.SmallCheck.Series as SC +import Numeric.Natural + ------------------------------------------------------------------------ main :: IO () @@ -146,23 +149,29 @@ smallCheck 100 (binaryLaws :: BinaryLaws Int) smallCheck 10 (ternaryLaws :: TernaryLaws Int) - putStrLn "PosInf Integer" - smallCheck 1000 (nearUnaryLaws :: UnaryLaws (PositiveInfinite Integer)) - smallCheck 100 (binaryLaws :: BinaryLaws (PositiveInfinite Integer)) - -- smallCheck 10 (nearTernaryLaws :: TernaryLaws (PositiveInfinite Integer)) - -- smallCheck 10 (ordLaws :: TernaryLaws (PositiveInfinite Integer)) + putStrLn "PosInf Natural" + smallCheck 1000 (unaryLaws :: UnaryLaws (PositiveInfinite Natural)) + smallCheck 1000 (zeroLaws :: UnaryLaws (PositiveInfinite Natural)) + smallCheck 100 (binaryLaws :: BinaryLaws (PositiveInfinite Natural)) + smallCheck 10 (ternaryLaws :: TernaryLaws (PositiveInfinite Natural)) + smallCheck 10 (ordLaws :: TernaryLaws (PositiveInfinite Natural)) putStrLn "NegInf Integer" - smallCheck 1000 (nearUnaryLaws :: UnaryLaws (NegativeInfinite Integer)) - smallCheck 100 (binaryLaws :: BinaryLaws (NegativeInfinite Integer)) - -- smallCheck 10 (nearTernaryLaws :: TernaryLaws (NegativeInfinite Integer)) - -- smallCheck 10 (ordLaws :: TernaryLaws (NegativeInfinite Integer)) + smallCheck 1000 (nearUnaryLaws :: UnaryLaws (NegativeInfinite Integer)) + smallCheck 1000 (zeroLaws :: UnaryLaws (NegativeInfinite Integer)) + smallCheck 100 (binaryLaws :: BinaryLaws (NegativeInfinite Integer)) + smallCheck 10 (plusAssoc :: TernaryLaws (NegativeInfinite Integer)) + smallCheck 10 (mulAssoc :: TernaryLaws (NegativeInfinite Integer)) + smallCheck 10 (mulDistribL :: TernaryLaws (NegativeInfinite Integer)) + smallCheck 10 (ordLaws :: TernaryLaws (NegativeInfinite Integer)) putStrLn "Inf Integer" - smallCheck 1000 (nearUnaryLaws :: UnaryLaws (Infinite Integer)) - smallCheck 100 (binaryLaws :: BinaryLaws (Infinite Integer)) - -- smallCheck 10 (nearTernaryLaws :: TernaryLaws (Infinite Integer)) - -- smallCheck 10 (ordLaws :: TernaryLaws (Infinite Integer)) + smallCheck 1000 (unaryLaws :: UnaryLaws (Infinite Integer)) + smallCheck 1000 (zeroLaws :: UnaryLaws (Infinite Integer)) + smallCheck 100 (binaryLaws :: BinaryLaws (Infinite Integer)) + smallCheck 10 (plusAssoc :: TernaryLaws (Infinite Integer)) + smallCheck 10 (mulAssoc :: TernaryLaws (Infinite Integer)) + smallCheck 10 (ordLaws :: TernaryLaws (Infinite Integer)) putStrLn "()" smallCheck 1 (unaryLaws :: UnaryLaws ()) @@ -253,26 +262,16 @@ putStrLn "Endo (Add Bool)" - smallCheck 3 (unOn plusId eFromFunc :: UnaryLaws (Bool -> Bool)) - smallCheck 3 (zeroLaws . eFromFunc :: UnaryLaws (Bool -> Bool)) - smallCheck 3 (unOn mulId eFromFunc :: UnaryLaws (Bool -> Bool)) - smallCheck 2 (binLawsOn eFromFunc :: BinaryLaws (Bool -> Bool)) - smallCheck 2 (ternOn plusAssoc eFromFunc :: TernaryLaws (Bool -> Bool)) - smallCheck 2 (ternOn mulAssoc eFromFunc :: TernaryLaws (Bool -> Bool)) - smallCheck 2 (ternOn mulDistribR eFromFunc :: TernaryLaws (Bool -> Bool)) + smallCheck 3 (nearUnaryLaws . eFromFunc :: UnaryLaws (Bool -> Bool)) + smallCheck 3 (zeroLaws . eFromFunc :: UnaryLaws (Bool -> Bool)) + smallCheck 2 (binLawsOn eFromFunc :: BinaryLaws (Bool -> Bool)) + smallCheck 2 (ternOn nearTernaryLaws eFromFunc :: TernaryLaws (Bool -> Bool)) doctest [ "-isrc" - , "src/Data/Semiring.hs" - , "src/Data/Semiring/Numeric.hs" - , "src/Test/Semiring.hs" - , "src/Data/Semiring/Free.hs" ] + , "src/" ] ------------------------------------------------------------------------- --- Test helpers -type UnaryLaws a = a -> Either String String -type BinaryLaws a = a -> a -> Either String String -type TernaryLaws a = a -> a -> a -> Either String String +-- Test helpers unOn :: UnaryLaws b -> (a -> b) -> UnaryLaws a unOn = (.) @@ -356,6 +355,9 @@ instance (Monad m, Serial m a) => Serial m (Infinite a) where series = fmap (either (bool Positive Negative) Finite) series + +instance Monad m => Serial m Natural where + series = generate (`take` [0..]) ------------------------------------------------------------------------ -- Function Equality