-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | Rings, semirings, and dioids. -- -- Lawful versions of the numeric typeclasses in base. @package rings @version 0.0.2 -- | https://en.wikipedia.org/wiki/Partially_ordered_set#Intervals module Data.Dioid.Interval data Interval a -- | Construct an interval from a pair of points. -- -- If a <~ b then a ... b = Empty. (...) :: Prd a => a -> a -> Interval a infix 3 ... -- | Obtain the endpoints of an interval. endpts :: Interval a -> Maybe (a, a) -- | Construct an interval containing a single point. -- --

--   >>> singleton 1
--   1 ... 1
--

singleton :: a -> Interval a -- | <math> -- -- Construct the upper set of an element x. -- -- This function is monotone wrt the containment order. upset :: Max a => a -> Interval a -- | <math> -- -- Construct the lower set of an element x. -- -- This function is antitone wrt the containment order. dnset :: Min a => a -> Interval a -- | The empty interval. -- --

--   >>> empty
--   Empty
--

empty :: Interval a instance GHC.Show.Show a => GHC.Show.Show (Data.Dioid.Interval.Interval a) instance GHC.Classes.Eq a => GHC.Classes.Eq (Data.Dioid.Interval.Interval a) instance GHC.Classes.Ord a => Data.Prd.Prd (Data.Dioid.Interval.Interval a) module Data.Group -- | A Group is a Monoid plus a function, negate, such -- that: -- --

--   a << negate a == mempty
--

-- --

--   negate a << a == mempty
--

class Monoid a => Group a negate :: Group a => a -> a (<<) :: Group a => a -> a -> a infixl 6 << -- | Orphan instances from base. module Data.Semigroup.Orphan instance GHC.Base.Semigroup GHC.Types.Word instance GHC.Base.Monoid GHC.Types.Word instance GHC.Base.Semigroup GHC.Types.Int instance GHC.Base.Monoid GHC.Types.Int instance GHC.Base.Semigroup GHC.Types.Bool instance GHC.Base.Monoid GHC.Types.Bool instance GHC.Base.Semigroup GHC.Types.Float instance GHC.Base.Monoid GHC.Types.Float instance GHC.Base.Semigroup a => GHC.Base.Semigroup (Data.Complex.Complex a) instance GHC.Base.Monoid a => GHC.Base.Monoid (Data.Complex.Complex a) instance GHC.Base.Semigroup GHC.Natural.Natural instance GHC.Base.Monoid GHC.Natural.Natural module Data.Semigroup.Quantale residuated :: Quantale a => a -> a -> a -> Bool -- | Residuated, partially ordered semigroups. -- -- In the interest of usability we abuse terminology slightly and use the -- term quantale to describe any residuated, partially ordered -- semigroup. This admits instances of hoops and triangular (co)-norms. -- -- There are several additional properties that apply when the poset -- structure is lattice-ordered (i.e. a residuated lattice) or when the -- semigroup is a monoid or semiring. See the associated -- Properties module. class (Semigroup a, Prd a) => Quantale a residr :: Quantale a => a -> Conn a a residl :: Quantale a => a -> Conn a a (\\) :: Quantale a => a -> a -> a (//) :: Quantale a => a -> a -> a lower' :: Prd a => Float -> (Float -> a) -> a -> Float upper' :: Prd a => Float -> (Float -> a) -> a -> Float incBy :: Yoneda a => Quantale a => a -> Rep a -> Rep a decBy :: Yoneda a => Quantale a => a -> Rep a -> Rep a instance Data.Semigroup.Quantale.Quantale GHC.Types.Float module Data.Semiring -- | Right pre-semirings and (non-unital and unital) right semirings. -- -- A right pre-semiring (sometimes referred to as a bisemigroup) is a -- type R endowed with two associative binary (i.e. semigroup) -- operations: (<>) and (><), along with a -- right-distributivity property connecting them: -- --

--   (a <> b) >= (a< (b >< c)
--

-- -- A non-unital right semiring (sometimes referred to as a bimonoid) is a -- pre-semiring with a mempty element that is neutral with respect -- to both addition and multiplication. -- -- A unital right semiring is a pre-semiring with two distinct neutral -- elements, mempty and unit, such that mempty is -- right-neutral wrt addition, unit is right-neutral wrt -- multiplication, and mempty is right-annihilative wrt -- multiplication. -- -- Note that unit needn't be distinct from mempty. -- -- Instances also need not be commutative nor left-distributive. -- -- See the properties module for a detailed specification of the laws. class Semigroup r => Semiring r (><) :: Semiring r => r -> r -> r fromBoolean :: (Semiring r, Monoid r) => Bool -> r unit :: (Monoid r, Semiring r) => r fromBooleanDef :: (Monoid r, Semiring r) => r -> Bool -> r -- | Fold over a collection using the multiplicative operation of a -- semiring. -- --

--   product f ≡ foldr' ((><) . f) unit
--

-- --

--   >>> (foldMap . product) id [[1, 2], [3, (4 :: Int)]] -- 1 >< 2 <> 3 >< 4
--   14
--

-- --

--   >>> (product . foldMap) id [[1, 2], [3, (4 :: Int)]] -- 1 <> 2 >< 3 <> 4
--   21
--

-- -- For semirings without a distinct multiplicative unit this is -- equivalent to const mempty: -- --

--   >>> product Just [1..(5 :: Int)]
--   Just 0
--

-- -- In this situation you most likely want to use product1. product :: (Foldable t, Monoid r, Semiring r) => (a -> r) -> t a -> r -- | Fold over a non-empty collection using the multiplicative operation of -- a semiring. -- -- As the collection is non-empty this does not require a distinct -- multiplicative unit: -- --

--   >>> product1 Just $ 1 :| [2..(5 :: Int)]
--   Just 120
--

product1 :: (Foldable1 t, Semiring r) => (a -> r) -> t a -> r -- | Cross-multiply two collections. -- --

--   >>> cross [1,2,3 ::Int] [1,2,3]
--   36
--

-- --

--   >>> cross [1,2,3 ::Int] []
--   0
--

cross :: (Foldable t, Applicative t, Monoid r, Semiring r) => t r -> t r -> r cross1 :: (Foldable1 t, Apply t, Semiring r) => t r -> t r -> r -- | Fold with no additive or multiplicative unit. foldPresemiring :: Semiring r => (a -> r) -> NonEmpty (NonEmpty a) -> r -- | Fold with no multiplicative unit. foldNonunital :: (Monoid r, Semiring r) => (a -> r) -> [NonEmpty a] -> r -- | Fold with additive & multiplicative units. -- -- This function will zero out if there is no multiplicative unit. foldUnital :: (Monoid r, Semiring r) => (a -> r) -> [[a]] -> r -- | A generalization of replicate to an arbitrary Monoid. -- -- Adapted from -- http://augustss.blogspot.com/2008/07/lost-and-found-if-i-write-108-in.html. replicate :: Monoid r => Natural -> r -> r replicate' :: (Monoid r, Semiring r) => Natural -> r -> r (^) :: (Monoid r, Semiring r) => r -> Natural -> r infixr 8 ^ powers :: (Monoid r, Semiring r) => Natural -> r -> r -- | Monoid under ><. Analogous to Product, but uses -- the Semiring constraint, rather than Num. newtype Prod a Prod :: a -> Prod a [getProd] :: Prod a -> a instance GHC.Base.Functor Data.Semiring.Prod instance GHC.Generics.Generic1 Data.Semiring.Prod instance GHC.Generics.Generic (Data.Semiring.Prod a) instance GHC.Enum.Bounded a => GHC.Enum.Bounded (Data.Semiring.Prod a) instance GHC.Show.Show a => GHC.Show.Show (Data.Semiring.Prod a) instance GHC.Classes.Ord a => GHC.Classes.Ord (Data.Semiring.Prod a) instance GHC.Classes.Eq a => GHC.Classes.Eq (Data.Semiring.Prod a) instance GHC.Base.Applicative Data.Semiring.Prod instance Data.Semiring.Semiring a => GHC.Base.Semigroup (Data.Semiring.Prod a) instance (GHC.Base.Monoid a, Data.Semiring.Semiring a) => GHC.Base.Monoid (Data.Semiring.Prod a) instance GHC.Base.Semigroup a => Data.Semiring.Semiring (Data.Semigroup.First a) instance GHC.Base.Semigroup a => Data.Semiring.Semiring (Data.Semigroup.Last a) instance GHC.Classes.Ord a => Data.Semiring.Semiring (Data.Semigroup.Max a) instance GHC.Classes.Ord a => Data.Semiring.Semiring (Data.Semigroup.Min a) instance GHC.Base.Semigroup a => Data.Semiring.Semiring (Data.Either.Either e a) instance GHC.Base.Semigroup a => Data.Semiring.Semiring (GHC.Base.NonEmpty a) instance Data.Semiring.Semiring () instance Data.Semiring.Semiring GHC.Types.Ordering instance Data.Semiring.Semiring GHC.Types.Bool instance Data.Semiring.Semiring GHC.Natural.Natural instance Data.Semiring.Semiring GHC.Types.Int instance Data.Semiring.Semiring GHC.Types.Word instance (GHC.Base.Monoid b, Data.Semiring.Semiring b) => Data.Semiring.Semiring (a -> b) instance (GHC.Base.Monoid a, Data.Semiring.Semiring a) => Data.Semiring.Semiring (Data.Functor.Contravariant.Op a b) instance (GHC.Base.Monoid a, GHC.Base.Monoid b, Data.Semiring.Semiring a, Data.Semiring.Semiring b) => Data.Semiring.Semiring (a, b) instance GHC.Base.Monoid a => Data.Semiring.Semiring [a] instance (GHC.Base.Monoid a, Data.Semiring.Semiring a) => Data.Semiring.Semiring (GHC.Maybe.Maybe a) instance (GHC.Base.Monoid a, Data.Semiring.Semiring a) => Data.Semiring.Semiring (Data.Semigroup.Internal.Dual a) instance (GHC.Base.Monoid a, Data.Semiring.Semiring a) => Data.Semiring.Semiring (Data.Functor.Const.Const a b) instance (GHC.Base.Monoid a, Data.Semiring.Semiring a) => Data.Semiring.Semiring (Data.Functor.Identity.Identity a) instance Data.Semiring.Semiring Data.Semigroup.Internal.Any instance Data.Semiring.Semiring Data.Semigroup.Internal.All instance (GHC.Base.Monoid a, Data.Semiring.Semiring a) => Data.Semiring.Semiring (GHC.Types.IO a) instance Data.Semiring.Semiring (Data.Functor.Contravariant.Predicate a) instance Data.Semiring.Semiring (Data.Functor.Contravariant.Equivalence a) instance Data.Semiring.Semiring (Data.Functor.Contravariant.Comparison a) instance GHC.Classes.Ord a => Data.Semiring.Semiring (Data.Set.Internal.Set a) instance GHC.Base.Monoid a => Data.Semiring.Semiring (Data.Sequence.Internal.Seq a) instance (GHC.Classes.Ord k, GHC.Base.Monoid k, GHC.Base.Monoid a) => Data.Semiring.Semiring (Data.Map.Internal.Map k a) instance GHC.Base.Monoid a => Data.Semiring.Semiring (Data.IntMap.Internal.IntMap a) module Data.Ring class (Group a, Semiring a) => Ring a abs :: Ring a => a -> a signum :: Ring a => a -> a module Data.Dioid.Signed -- | Sign is isomorphic to 'Maybe Ordering' and (Bool,Bool), but has -- a distinct poset ordering: -- -- Indeterminate >= Positive >= Zero -- and Indeterminate >= Negative >= -- Zero -- -- Note that Positive and Negative are not comparable. -- --

Positive can be regarded as representing (0, +∞],
Negative as representing [−∞, 0),
Indeterminate as representing [−∞, +∞] v NaN, and
Zero as representing the set {0}.

data Sign Zero :: Sign Negative :: Sign Positive :: Sign Indeterminate :: Sign signOf :: (Eq a, Num a, Prd a) => a -> Sign newtype Signed Signed :: Float -> Signed [unSigned] :: Signed -> Float f32sgn :: Conn Float Signed ugnsgn :: Conn Unsigned Signed newtype Unsigned Unsigned :: Float -> Unsigned unsigned :: Signed -> Unsigned ltugn :: Unsigned -> Unsigned -> Bool instance GHC.Classes.Eq Data.Dioid.Signed.Sign instance GHC.Show.Show Data.Dioid.Signed.Sign instance GHC.Show.Show Data.Dioid.Signed.Unsigned instance GHC.Classes.Eq Data.Dioid.Signed.Unsigned instance Data.Prd.Prd Data.Dioid.Signed.Unsigned instance Data.Prd.Min Data.Dioid.Signed.Unsigned instance Data.Prd.Max Data.Dioid.Signed.Unsigned instance Data.Prd.Lattice.Lattice Data.Dioid.Signed.Unsigned instance GHC.Base.Semigroup Data.Dioid.Signed.Unsigned instance GHC.Base.Monoid Data.Dioid.Signed.Unsigned instance Data.Semiring.Semiring Data.Dioid.Signed.Unsigned instance Data.Semigroup.Quantale.Quantale Data.Dioid.Signed.Unsigned instance GHC.Show.Show Data.Dioid.Signed.Signed instance GHC.Classes.Eq Data.Dioid.Signed.Signed instance Data.Prd.Prd Data.Dioid.Signed.Signed instance GHC.Base.Semigroup Data.Dioid.Signed.Sign instance GHC.Base.Monoid Data.Dioid.Signed.Sign instance Data.Semiring.Semiring Data.Dioid.Signed.Sign instance Data.Prd.Prd Data.Dioid.Signed.Sign instance Data.Prd.Min Data.Dioid.Signed.Sign instance Data.Prd.Max Data.Dioid.Signed.Sign instance GHC.Enum.Bounded Data.Dioid.Signed.Sign module Data.Dioid type Dioid a = (Yoneda a, Semiring a) module Data.Semiring.Property -- | <math> -- -- A (pre-)semiring with a right-neutral additive unit must satisfy: -- --

--   neutral_addition mempty ~~ const True
--

-- -- Or, equivalently: -- --

--   mempty <> r ~~ r
--

-- -- This is a required property. neutral_addition_on :: Semigroup r => Rel r -> r -> r -> Bool neutral_addition_on' :: Monoid r => Rel r -> r -> Bool -- | <math> -- -- A (pre-)semiring with a right-neutral multiplicative unit must -- satisfy: -- --

--   neutral_multiplication unit ~~ const True
--

-- -- Or, equivalently: -- --

--   unit >< r ~~ r
--

-- -- This is a required property. neutral_multiplication_on :: Semiring r => Rel r -> r -> r -> Bool neutral_multiplication_on' :: (Monoid r, Semiring r) => Rel r -> r -> Bool -- | <math> -- -- R must right-associate addition. -- -- This should be verified by the underlying Semigroup instance, -- but is included here for completeness. -- -- This is a required property. associative_addition_on :: Semigroup r => Rel r -> r -> r -> r -> Bool -- | <math> -- -- R must right-associate multiplication. -- -- This is a required property. associative_multiplication_on :: Semiring r => Rel r -> r -> r -> r -> Bool -- | <math> -- -- R must right-distribute multiplication. -- -- When R is a functor and the semiring structure is derived from -- Alternative, this translates to: -- --

--   (a <|> b) *> c = (a *> c) <|> (b *> c)
--

-- -- See -- https://en.wikibooks.org/wiki/Haskell/Alternative_and_MonadPlus. -- -- This is a required property. distributive_on :: Semiring r => Rel r -> r -> r -> r -> Bool -- | <math> -- -- If R is non-unital (i.e. unit is not distinct from -- mempty) then it will instead satisfy a right-absorbtion -- property. -- -- This follows from right-neutrality and right-distributivity. -- -- Compare codistributive and closed_stable. -- -- When R is also left-distributive we get: <math> -- -- See also Warning and -- https://blogs.ncl.ac.uk/andreymokhov/united-monoids/#whatif. nonunital_on :: (Monoid r, Semiring r) => Rel r -> r -> r -> Bool -- | <math> -- -- A R is unital then its addititive unit must be -- right-annihilative, i.e.: -- --

--   mempty >< a ~~ mempty
--

-- -- For Alternative instances this property translates to: -- --

--   empty *> a ~~ empty
--

-- -- All right semirings must have a right-absorbative addititive unit, -- however note that depending on the Prd instance this does not -- preclude IEEE754-mandated behavior such as: -- --

--   mempty >< NaN ~~ NaN
--

-- -- This is a required property. annihilative_multiplication_on :: (Monoid r, Semiring r) => Rel r -> r -> Bool -- | fromBoolean must be a semiring homomorphism into R. -- -- This is a required property. homomorphism_boolean :: forall r. (Eq r, Monoid r, Semiring r) => Bool -> Bool -> Bool -- | <math> -- -- If R is right-cancellative wrt addition then for all a -- the section (a <>) is injective. cancellative_addition_on :: Semigroup r => Rel r -> r -> r -> r -> Bool -- | <math> -- -- If R is right-cancellative wrt multiplication then for all -- a the section (a ><) is injective. cancellative_multiplication_on :: Semiring r => Rel r -> r -> r -> r -> Bool -- | <math> commutative_addition_on :: Semigroup r => Rel r -> r -> r -> Bool -- | <math> commutative_multiplication_on :: Semiring r => Rel r -> r -> r -> Bool -- | <math> -- -- R must right-distribute multiplication between finite sums. -- -- For types with exact arithmetic this follows from -- distributive & neutral_multiplication. distributive_finite_on :: (Monoid r, Semiring r) => Rel r -> [r] -> r -> Bool -- | <math> -- -- R must right-distribute multiplication over finite (non-empty) -- sums. -- -- For types with exact arithmetic this follows from -- distributive and the universality of fold1. distributive_finite1_on :: Semiring r => Rel r -> NonEmpty r -> r -> Bool -- | <math> -- -- If R is also left-distributive then it supports -- cross-multiplication. distributive_cross_on :: (Monoid r, Semiring r) => Rel r -> [r] -> [r] -> Bool -- | <math> -- -- If R is also left-distributive then it supports (non-empty) -- cross-multiplication. distributive_cross1_on :: Semiring r => Rel r -> NonEmpty r -> NonEmpty r -> Bool module Data.Dioid.Property -- | <math> -- -- A (pre-)semiring with a right-neutral additive unit must satisfy: -- --

--   neutral_addition mempty ~~ const True
--

-- -- Or, equivalently: -- --

--   mempty <> r ~~ r
--

-- -- This is a required property. neutral_addition :: (Eq r, Prd r, Semigroup r) => r -> r -> Bool neutral_addition' :: (Eq r, Prd r, Monoid r, Semigroup r) => r -> Bool -- | <math> -- -- A (pre-)semiring with a right-neutral multiplicative unit must -- satisfy: -- --

--   neutral_multiplication unit ~~ const True
--

-- -- Or, equivalently: -- --

--   unit >< r ~~ r
--

-- -- This is a required property. neutral_multiplication :: (Eq r, Prd r, Semiring r) => r -> r -> Bool neutral_multiplication' :: (Eq r, Prd r, Monoid r, Semiring r) => r -> Bool -- | <math> -- -- R must right-associate addition. -- -- This should be verified by the underlying Semigroup instance, -- but is included here for completeness. -- -- This is a required property. associative_addition :: (Eq r, Prd r, Semigroup r) => r -> r -> r -> Bool -- | <math> -- -- R must right-associate multiplication. -- -- This is a required property. associative_multiplication :: (Eq r, Prd r, Semiring r) => r -> r -> r -> Bool -- | <math> -- -- R must right-distribute multiplication. -- -- When R is a functor and the semiring structure is derived from -- Alternative, this translates to: -- --

--   (a <|> b) *> c = (a *> c) <|> (b *> c)
--

-- -- See -- https://en.wikibooks.org/wiki/Haskell/Alternative_and_MonadPlus. -- -- This is a required property. distributive :: (Eq r, Prd r, Semiring r) => r -> r -> r -> Bool -- | <math> -- -- If R is non-unital (i.e. unit equals mempty) then -- it will instead satisfy a right-absorbtion property. -- -- This follows from right-neutrality and right-distributivity. -- -- Compare codistributive and closed_stable. -- -- When R is also left-distributive we get: <math> -- -- See also Warning and -- https://blogs.ncl.ac.uk/andreymokhov/united-monoids/#whatif. nonunital :: forall r. (Eq r, Prd r, Monoid r, Semiring r) => r -> r -> Bool -- | <math> -- -- A R is unital then its addititive unit must be -- right-annihilative, i.e.: -- --

--   mempty >< a ~~ mempty
--

-- -- For Alternative instances this property translates to: -- --

--   empty *> a ~~ empty
--

-- -- All right semirings must have a right-absorbative addititive unit, -- however note that depending on the Prd instance this does not -- preclude IEEE754-mandated behavior such as: -- --

--   mempty >< NaN ~~ NaN
--

-- -- This is a required property. annihilative_multiplication :: (Eq r, Prd r, Monoid r, Semiring r) => r -> Bool -- | fromBoolean must be a semiring homomorphism into R. -- -- This is a required property. homomorphism_boolean :: forall r. (Eq r, Monoid r, Semiring r) => Bool -> Bool -> Bool -- | <math> -- -- If R is right-cancellative wrt addition then for all a -- the section (a <>) is injective. cancellative_addition :: (Eq r, Prd r, Semigroup r) => r -> r -> r -> Bool -- | <math> -- -- If R is right-cancellative wrt multiplication then for all -- a the section (a ><) is injective. cancellative_multiplication :: (Eq r, Prd r, Semiring r) => r -> r -> r -> Bool -- | <math> commutative_addition :: (Eq r, Prd r, Semigroup r) => r -> r -> Bool -- | <math> commutative_multiplication :: (Eq r, Prd r, Semiring r) => r -> r -> Bool -- | <math> -- -- Right-additive absorbativity is a generalized form of idempotency: -- --

--   absorbative_addition unit a ~~ a <> a ~~ a
--

absorbative_addition :: (Eq r, Prd r, Semiring r) => r -> r -> Bool -- | <math> -- -- Left-additive absorbativity is a generalized form of idempotency: -- --

--   absorbative_addition unit a ~~ a <> a ~~ a
--

absorbative_addition' :: (Eq r, Prd r, Semiring r) => r -> r -> Bool idempotent_addition :: (Eq r, Prd r, Monoid r, Semiring r) => r -> Bool -- | <math> -- -- Right-mulitplicative absorbativity is a generalized form of -- idempotency: -- --

--   absorbative_multiplication mempty a ~~ a >< a ~~ a
--

-- -- See https://en.wikipedia.org/wiki/Absorption_law. absorbative_multiplication :: (Eq r, Prd r, Semiring r) => r -> r -> Bool -- | <math> -- -- Left-mulitplicative absorbativity is a generalized form of -- idempotency: -- --

--   absorbative_multiplication' mempty a ~~ a >< a ~~ a
--

-- -- See https://en.wikipedia.org/wiki/Absorption_law. absorbative_multiplication' :: (Eq r, Prd r, Semiring r) => r -> r -> Bool -- | <math> -- -- A unital semiring with a right-annihilative muliplicative unit must -- satisfy: -- --

--   unit <> a ~~ unit
--

-- -- For a dioid this is equivalent to: -- --

--   (unit <~) ~~ (unit ~~)
--

-- -- For Alternative instances this is known as the left-catch -- law: -- --

--   pure a <|> _ ~~ pure a
--

annihilative_addition :: (Eq r, Prd r, Monoid r, Semiring r) => r -> Bool -- | <math> -- -- A unital semiring with a left-annihilative muliplicative unit must -- satisfy: -- --

--   a <> unit ~~ unit
--

-- -- Note that the left-annihilative property is too strong for many -- instances. This is because it requires that any effects that r -- generates be undunit. -- -- See https://winterkoninkje.dreamwidth.org/90905.html. annihilative_addition' :: (Eq r, Prd r, Monoid r, Semiring r) => r -> Bool -- | <math> -- -- A right-codistributive semiring has a right-annihilative muliplicative -- unit: -- --

--   codistributive unit a mempty ~~ unit ~~ unit <> a
--

-- -- idempotent mulitiplication: -- --

--   codistributive mempty mempty a ~~ a ~~ a >< a
--

-- -- and idempotent addition: -- --

--   codistributive a mempty a ~~ a ~~ a <> a
--

-- -- Furthermore if R is commutative then it is a right-distributive -- lattice. codistributive :: (Eq r, Prd r, Semiring r) => r -> r -> r -> Bool -- | <~ is a preordered relation relative to <>. -- -- This is a required property. ordered_preordered :: (Prd r, Semiring r) => r -> r -> Bool -- | mempty is a minimal or least element of r. -- -- This is a required property. ordered_monotone_zero :: (Prd r, Monoid r) => r -> Bool -- | ( forall a, b, c: b leq c Rightarrow b + a leq c + a -- -- In an ordered semiring this follows directly from the definition of -- <~. -- -- Compare cancellative_addition. -- -- This is a required property. ordered_monotone_addition :: (Prd r, Semiring r) => r -> r -> r -> Bool -- | <math> -- -- This is a required property. ordered_positive_addition :: (Prd r, Monoid r) => r -> r -> Bool -- | ( forall a, b, c: b leq c Rightarrow b * a leq c * a -- -- In an ordered semiring this follows directly from distributive -- and the definition of <~. -- -- Compare cancellative_multiplication. -- -- This is a required property. ordered_monotone_multiplication :: (Prd r, Semiring r) => r -> r -> r -> Bool -- | <~ is consistent with annihilativity. -- -- This means that a dioid with an annihilative multiplicative unit must -- satisfy: -- --

--   (one <~) ≡ (one ==)
--

ordered_annihilative_unit :: (Prd r, Monoid r, Semiring r) => r -> Bool -- | ( forall a, b: a leq b Rightarrow a + b = b ordered_idempotent_addition :: (Prd r, Monoid r) => r -> r -> Bool -- | <math> ordered_positive_multiplication :: (Prd r, Monoid r, Semiring r) => r -> r -> Bool