packages feed

rings 0.0.2 → 0.0.2.1

raw patch · 20 files changed

+615/−830 lines, 20 filesdep −contravariantdep ~connectionssetup-changed

Dependencies removed: contravariant

Dependency ranges changed: connections

Files

− Setup.hs 
@@ -1,2 +0,0 @@-import Distribution.Simple-main = defaultMain
rings.cabal view
@@ -1,29 +1,35 @@ name:                rings-version:             0.0.2+version:             0.0.2.1 synopsis:            Rings, semirings, and dioids.-description:         Lawful versions of the numeric typeclasses in base.+description:         Lawful versions of several of the numeric typeclasses in base. homepage:            https://github.com/cmk/rings license:             BSD3 license-file:        LICENSE author:              Chris McKinlay maintainer:          chris.mckinlay@gmail.com category:            Math, Numerical+stability:           Experimental build-type:          Simple+tested-with:         GHC == 8.6.3 extra-source-files:  ChangeLog.md cabal-version:       >=1.10  library   exposed-modules:       Data.Dioid-    , Data.Dioid.Interval     , Data.Dioid.Property-    , Data.Dioid.Signed     , Data.Group-    , Data.Ring-    , Data.Semigroup.Orphan-    , Data.Semigroup.Quantale     , Data.Semiring     , Data.Semiring.Property+    , Data.Ring+    , Data.Bool.Instance+    , Data.Complex.Instance+    , Data.Double.Instance+    , Data.Fixed.Instance+    , Data.Float.Instance+    , Data.Int.Instance+    , Data.Word.Instance+   default-extensions:       ScopedTypeVariables     , TypeApplications@@ -32,12 +38,11 @@     , FlexibleInstances    build-depends:       -      base           >= 4.10  && < 5.0-    , containers     >= 0.4.0 && < 0.7+      base           >= 4.10    && < 5.0+    , containers     >= 0.4.0   && < 0.7     , semigroupoids  == 5.*-    , property       >= 0.0.1 && < 1.0-    , connections    >= 0.0.2 && < 1.0-    , contravariant  >= 1     && < 2+    , property       >= 0.0.1   && < 1.0+    , connections    >= 0.0.2.1 && < 0.0.3    hs-source-dirs: src   default-language: Haskell2010
+ src/Data/Bool/Instance.hs view
@@ -0,0 +1,28 @@+-- | Instance instances from base.+module Data.Bool.Instance where++import Data.Prd+import Data.Dioid+import Data.Semiring+import Prelude++instance Semigroup Bool where+  (<>) = (||)+  {-# INLINE (<>) #-}++instance Monoid Bool where mempty = False++instance Semiring Bool where+  (><) = (&&)+  {-# INLINE (><) #-}++  fromBoolean = id+  {-# INLINE fromBoolean #-}++instance Kleene Bool where+  star = const True -- == (|| True)+  plus = id -- == (&& True)+  {-# INLINE star #-}+  {-# INLINE plus #-}++instance Dioid Bool where
+ src/Data/Complex/Instance.hs view
@@ -0,0 +1,12 @@+-- | Instance instances from base.+module Data.Complex.Instance where++import Data.Complex+import Prelude++instance Semigroup a => Semigroup (Complex a) where+  (x :+ y) <> (x' :+ y') = (x <> x') :+ (y <> y')+  {-# INLINE (<>) #-}++instance Monoid a => Monoid (Complex a) where+  mempty = mempty :+ mempty
src/Data/Dioid.hs view
@@ -1,9 +1,49 @@ {-# Language ConstraintKinds #-}+ module Data.Dioid where  import Data.Connection.Yoneda import Data.Semiring+import Data.Prd -type Dioid a = (Yoneda a, Semiring a)+-- A constraint kind for topological dioids+type Topological a = (Dioid a, Kleene a, Yoneda a) +{-+An idempotent dioid is a dioid in which the addition /<>/ is idempotent. A frequently encountered special case is one where addition /<>/ is not only idempotent but also selective. A selective dioid is a dioid in which the addition /<>/ is selective (i.e.: ∀a, b ∈ E: a /<>/ b = a or b). +Idempotent dioids form a particularly rich class of dioids which contains many sub-classes, in particular:+– Doubly-idempotent dioids and distributive lattices+– Doubly selective dioids+– Idempotent-cancellative dioids and selective-cancellative dioids+– Idempotent-invertible dioids and selective-invertible dioids++Dioids (idempotent dioids in particular) play an important role in many applications in computer science, ranging from regular languages and Kleene algebras to shortest path algorithms using tropical semirings such as the max-plus semiring. They are also generalizations of distributive lattices, quantales, residuated lattices and relation algebras, each of which have been studied extensively in mathematics and logic.++-}++-- | Right pre-dioids and dioids.+--+-- A right-dioid is a semiring with a right-canonical pre-order relation relative to '<>':+-- @a <~ b@ iff @b ≡ a <> c@ for some @c@.+-- +-- In other words we have that:+--+-- @+-- a '<~' (a '<>' b) ≡ 'True'+-- @+--+-- Consequently '<~' is both reflexive and transitive:+--+-- @+-- a '<~' a ≡ 'True'+-- a '<~' b && b '<~' c ==> a '<~' c ≡ 'True'+-- @+--+-- Finally '<~' is an order relation:+--+-- @(a '=~' b) <==> (a '==' b)@+--+-- See 'Data.Dioid.Property'+--+class (Prd a, Semiring a) => Dioid a where
− src/Data/Dioid/Interval.hs 
@@ -1,116 +0,0 @@--- | <https://en.wikipedia.org/wiki/Partially_ordered_set#Intervals>-module Data.Dioid.Interval (-    Interval()-  , (...)-  , endpts-  , singleton-  , upset-  , dnset-  , empty-) where--import Data.Prd-import Data.Prd.Lattice-import Data.Connection--import Prelude--{---ivllat :: (Lattice a, Bound a) => Trip (Interval a) a-ivllat = Trip f g h where-  f = maybe minimal (uncurry (\/)) . endpts-  g = singleton-  h = maybe maximal (uncurry (/\)) . endpts --indexed :: Index a => Conn (Interval a) (Maybe (Down a, a))--https://en.wikipedia.org/wiki/Locally_finite_poset-https://en.wikipedia.org/wiki/Incidence_algebra--An interval in a poset P is a subset I of P with the property that, for any x and y in I and any z in P, if x ≤ z ≤ y, then z is also in I. ---}--data Interval a = I !a !a | Empty deriving (Eq, Show)---- Interval order--- https://en.wikipedia.org/wiki/Interval_order-instance Ord a => Prd (Interval a) where-  Empty <~ Empty = True-  Empty <~ _ = False--  i@(I _ x) <~ j@(I y _) = x < y || i == j--{---- Containment order--- https://en.wikipedia.org/wiki/Containment_order-instance Prd a => Prd (Interval a) where-  Empty <~ _ = True-  I x y <~ I x' y' = x' <~ x && y <~ y'--}---infix 3 ...---- | Construct an interval from a pair of points.------ If @a <~ b@ then @a ... b = Empty@.----(...) :: Prd a => a -> a -> Interval a-a ... b-  | a <~ b = I a b-  | otherwise = Empty-{-# INLINE (...) #-}---- | Obtain the endpoints of an interval.----endpts :: Interval a -> Maybe (a, a)-endpts Empty = Nothing-endpts (I x y) = Just (x, y)-{-# INLINE endpts #-}---- | Construct an interval containing a single point.------ >>> singleton 1--- 1 ... 1----singleton :: a -> Interval a-singleton a = I a a-{-# INLINE singleton #-}--{--properties: --Yoneda lemma for preorders:-x <~ y <==> upset x <~ upset y --containment order---}---- | \( X_\geq(x) = \{ y \in X | y \geq x \} \)------ Construct the upper set of an element /x/.------ This function is monotone wrt the containment order.----upset :: Max a => a -> Interval a-upset x = x ... maximal-{-# INLINE upset #-}---- | \( X_\leq(x) = \{ y \in X | y \leq x \} \)------ Construct the lower set of an element /x/.------ This function is antitone wrt the containment order.----dnset :: Min a => a -> Interval a-dnset x = minimal ... x-{-# INLINE dnset #-}---- | The empty interval.------ >>> empty--- Empty-empty :: Interval a-empty = Empty-{-# INLINE empty #-}
src/Data/Dioid/Property.hs view
@@ -1,224 +1,109 @@ {-# Language AllowAmbiguousTypes #-}  module Data.Dioid.Property (-  -- * Properties of pre-semirings & semirings-    neutral_addition-  , neutral_addition'-  , neutral_multiplication-  , neutral_multiplication'-  , associative_addition -  , associative_multiplication -  , distributive -  -- * Properties of non-unital (near-)semirings-  , nonunital-  -- * Properties of unital semirings-  , annihilative_multiplication -  , Prop.homomorphism_boolean-  -- * Properties of cancellative semirings -  , cancellative_addition -  , cancellative_multiplication -  -- * Properties of commutative semirings -  , commutative_addition -  , commutative_multiplication-  -- * Properties of absorbative semirings +  -- * Properties of dioids (aka ordered semirings) +    ordered_preordered+  , ordered_monotone_zero+  , ordered_monotone_addition+  , ordered_positive_addition+  , ordered_monotone_multiplication+  , ordered_annihilative_sunit +  , ordered_idempotent_addition+  , ordered_positive_multiplication+  -- * Properties of absorbative dioids    , absorbative_addition   , absorbative_addition'   , idempotent_addition   , absorbative_multiplication   , absorbative_multiplication' -  -- * Properties of annihilative semirings +  -- * Properties of annihilative dioids    , annihilative_addition    , annihilative_addition'    , codistributive-  -- * Properties of ordered semirings -  , ordered_preordered-  , ordered_monotone_zero-  , ordered_monotone_addition-  , ordered_positive_addition-  , ordered_monotone_multiplication-  , ordered_annihilative_unit -  , ordered_idempotent_addition-  , ordered_positive_multiplication+  -- * Properties of kleene dioids+  , kleene_pstable+  , kleene_paffine +  , kleene_stable +  , kleene_affine +  , idempotent_star ) where  import Data.Prd+import Data.Dioid import Data.List (unfoldr) import Data.List.NonEmpty (NonEmpty(..))-import Data.Semiring-import Data.Semigroup.Orphan ()+import Data.Semiring hiding (nonunital)+import Numeric.Natural import Test.Property.Util ((<==>),(==>)) import qualified Test.Property as Prop hiding (distributive_on) import qualified Data.Semiring.Property as Prop -- --------------------------------------------------------------------------------------- Properties of pre-semirings & semirings+-- Properties of ordered semirings (aka dioids). --- | \( \forall a \in R: (z + a) = a \)------ A (pre-)semiring with a right-neutral additive unit must satisfy:------ @--- 'neutral_addition' 'mempty' ~~ const True--- @--- --- Or, equivalently:------ @--- 'mempty' '<>' r ~~ r--- @+-- | '<~' is a preordered relation relative to '<>'. -- -- This is a required property. ---neutral_addition :: (Eq r, Prd r, Semigroup r) => r -> r -> Bool-neutral_addition = Prop.neutral_addition_on (~~)--neutral_addition' :: (Eq r, Prd r, Monoid r, Semigroup r) => r -> Bool-neutral_addition' = Prop.neutral_addition_on' (~~)+ordered_preordered :: Dioid r => r -> r -> Bool+ordered_preordered a b = a <~ (a <> b) --- | \( \forall a \in R: (o * a) = a \)------ A (pre-)semiring with a right-neutral multiplicative unit must satisfy:------ @--- 'neutral_multiplication' 'unit' ~~ const True--- @--- --- Or, equivalently:------ @--- 'unit' '><' r ~~ r--- @+-- | 'mempty' is a minimal or least element of @r@. -- -- This is a required property. ---neutral_multiplication :: (Eq r, Prd r, Semiring r) => r -> r -> Bool-neutral_multiplication = Prop.neutral_multiplication_on (~~)--neutral_multiplication' :: (Eq r, Prd r, Monoid r, Semiring r) => r -> Bool-neutral_multiplication' = Prop.neutral_multiplication_on' (~~)+ordered_monotone_zero :: (Monoid r, Dioid r) => r -> Bool+ordered_monotone_zero a = mempty ?~ a ==> mempty <~ a  --- | \( \forall a, b, c \in R: (a + b) + c = a + (b + c) \)------ /R/ must right-associate addition.+-- | \( \forall a, b, c: b \leq c \Rightarrow b + a \leq c + a ----- This should be verified by the underlying 'Semigroup' instance,--- but is included here for completeness.+-- In an ordered semiring this follows directly from the definition of '<~'. --+-- Compare 'cancellative_addition'.+--  -- This is a required property. ---associative_addition :: (Eq r, Prd r, Semigroup r) => r -> r -> r -> Bool-associative_addition = Prop.associative_addition_on (~~)+ordered_monotone_addition :: Dioid r => r -> r -> r -> Bool+ordered_monotone_addition a = Prop.monotone_on (<~) (<~) (<> a) --- | \( \forall a, b, c \in R: (a * b) * c = a * (b * c) \)------ /R/ must right-associate multiplication.+-- |  \( \forall a, b: a + b = 0 \Rightarrow a = 0 \wedge b = 0 \) -- -- This is a required property. ---associative_multiplication :: (Eq r, Prd r, Semiring r) => r -> r -> r -> Bool-associative_multiplication = Prop.associative_multiplication_on (~~)+ordered_positive_addition :: (Prd r, Monoid r) => r -> r -> Bool+ordered_positive_addition a b = a <> b =~ mempty ==> a =~ mempty && b =~ mempty --- | \( \forall a, b, c \in R: (a + b) * c = (a * c) + (b * c) \)------ /R/ must right-distribute multiplication.------ When /R/ is a functor and the semiring structure is derived from 'Alternative', --- this translates to: +-- | \( \forall a, b, c: b \leq c \Rightarrow b * a \leq c * a ----- @--- (a '<|>' b) '*>' c = (a '*>' c) '<|>' (b '*>' c)--- @  +-- In an ordered semiring this follows directly from 'distributive' and the definition of '<~'. ----- See < https://en.wikibooks.org/wiki/Haskell/Alternative_and_MonadPlus >.+-- Compare 'cancellative_multiplication'. -- -- This is a required property. ---distributive :: (Eq r, Prd r, Semiring r) => r -> r -> r -> Bool-distributive = Prop.distributive_on (~~)----------------------------------------------------------------------------------------- Properties of non-unital semirings (aka near-semirings)---- | \( \forall a, b \in R: a * b = a * b + b \)------ 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: \( \forall a, b \in R: a * b = a + a * b + b \)------ See also 'Data.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-nonunital = Prop.nonunital_on (~~)----------------------------------------------------------------------------------------- Properties of unital semirings+ordered_monotone_multiplication :: Dioid r => r -> r -> r -> Bool+ordered_monotone_multiplication a = Prop.monotone_on (<~) (<~) (>< a) --- | \( \forall a \in R: (z * a) = u \)------ 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'--- @+-- | '<~' is consistent with annihilativity. ----- 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: +-- This means that a dioid with an annihilative multiplicative sunit must satisfy: -- -- @--- 'mempty' '><' NaN ~~ NaN+-- ('one' <~) ≡ ('one' ==) -- @ ----- This is a required property.----annihilative_multiplication :: (Eq r, Prd r, Monoid r, Semiring r) => r -> Bool-annihilative_multiplication = Prop.annihilative_multiplication_on (~~)----------------------------------------------------------------------------------------- Properties of cancellative & commutative semirings----- | \( \forall a, b, c \in R: b + a = c + a \Rightarrow b = c \)------ 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-cancellative_addition = Prop.cancellative_addition_on (~~)----- | \( \forall a, b, c \in R: b * a = c * a \Rightarrow b = c \)------ 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-cancellative_multiplication = Prop.cancellative_multiplication_on (~~)+ordered_annihilative_sunit :: (Monoid r, Dioid r) => r -> Bool+ordered_annihilative_sunit a = sunit <~ a <==> sunit =~ a --- | \( \forall a, b \in R: a + b = b + a \)+-- | \( \forall a, b: a \leq b \Rightarrow a + b = b ---commutative_addition :: (Eq r, Prd r, Semigroup r) => r -> r -> Bool-commutative_addition = Prop.commutative_addition_on (=~)-+ordered_idempotent_addition :: (Prd r, Monoid r) => r -> r -> Bool+ordered_idempotent_addition a b = (a <~ b) <==> (a <> b =~ b) --- | \( \forall a, b \in R: a * b = b * a \)+-- |  \( \forall a, b: a * b = 0 \Rightarrow a = 0 \vee b = 0 \) ---commutative_multiplication :: (Eq r, Prd r, Semiring r) => r -> r -> Bool-commutative_multiplication = Prop.commutative_multiplication_on (=~)-+ordered_positive_multiplication :: (Monoid r, Dioid r) => r -> r -> Bool+ordered_positive_multiplication a b = a >< b =~ mempty ==> a =~ mempty || b =~ mempty  ------------------------------------------------------------------------------------ -- Properties of idempotent & absorbative semirings@@ -228,24 +113,24 @@ -- Right-additive absorbativity is a generalized form of idempotency: -- -- @--- 'absorbative_addition' 'unit' a ~~ a <> a ~~ a+-- 'absorbative_addition' 'sunit' a ~~ a <> a ~~ a -- @ ---absorbative_addition :: (Eq r, Prd r, Semiring r) => r -> r -> Bool+absorbative_addition :: (Eq r, Dioid r) => r -> r -> Bool absorbative_addition a b = a >< b <> b ~~ b -idempotent_addition :: (Eq r, Prd r, Monoid r, Semiring r) => r -> Bool-idempotent_addition = absorbative_addition unit+idempotent_addition :: (Eq r, Monoid r, Dioid r) => r -> Bool+idempotent_addition = absorbative_addition sunit   -- | \( \forall a, b \in R: b + b * a = b \) -- -- Left-additive absorbativity is a generalized form of idempotency: -- -- @--- 'absorbative_addition' 'unit' a ~~ a <> a ~~ a+-- 'absorbative_addition' 'sunit' a ~~ a <> a ~~ a -- @ ---absorbative_addition' :: (Eq r, Prd r, Semiring r) => r -> r -> Bool+absorbative_addition' :: (Eq r, Dioid r) => r -> r -> Bool absorbative_addition' a b = b <> b >< a ~~ b  -- | \( \forall a, b \in R: (a + b) * b = b \)@@ -258,12 +143,12 @@ -- -- See < https://en.wikipedia.org/wiki/Absorption_law >. ---absorbative_multiplication :: (Eq r, Prd r, Semiring r) => r -> r -> Bool+absorbative_multiplication :: (Eq r, Dioid r) => r -> r -> Bool absorbative_multiplication a b = (a <> b) >< b ~~ b  --absorbative_multiplication a b c = (a <> b) >< c ~~ c---closed a = ---  absorbative_multiplication (star a) unit a && absorbative_multiplication unit (star a) a +--kleene a = +--  absorbative_multiplication (star a) sunit a && absorbative_multiplication sunit (star a) a   -- | \( \forall a, b \in R: b * (b + a) = b \) --@@ -275,21 +160,24 @@ -- -- See < https://en.wikipedia.org/wiki/Absorption_law >. ---absorbative_multiplication' :: (Eq r, Prd r, Semiring r) => r -> r -> Bool+absorbative_multiplication' :: (Eq r, Dioid r) => r -> r -> Bool absorbative_multiplication' a b = b >< (b <> a) ~~ b +------------------------------------------------------------------------------------+-- Properties of idempotent and annihilative dioids.+ -- | \( \forall a \in R: o + a = o \) ----- A unital semiring with a right-annihilative muliplicative unit must satisfy:+-- A unital semiring with a right-annihilative muliplicative sunit must satisfy: -- -- @--- 'unit' <> a ~~ 'unit'+-- 'sunit' <> a ~~ 'sunit' -- @ -- -- For a dioid this is equivalent to: --  -- @--- ('unit' '<~') ~~ ('unit' '~~')+-- ('sunit' '<~') ~~ ('sunit' '~~') -- @ -- -- For 'Alternative' instances this is known as the left-catch law:@@ -298,31 +186,30 @@ -- 'pure' a '<|>' _ ~~ 'pure' a -- @ ---annihilative_addition :: (Eq r, Prd r, Monoid r, Semiring r) => r -> Bool-annihilative_addition r = Prop.annihilative_on (~~) (<>) unit r-+annihilative_addition :: (Eq r, Monoid r, Dioid r) => r -> Bool+annihilative_addition r = Prop.annihilative_on (~~) (<>) sunit r  -- | \( \forall a \in R: a + o = o \) ----- A unital semiring with a left-annihilative muliplicative unit must satisfy:+-- A unital semiring with a left-annihilative muliplicative sunit must satisfy: -- -- @--- a '<>' 'unit' ~~ 'unit'+-- a '<>' 'sunit' ~~ 'sunit' -- @ -- -- 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.+-- This is because it requires that any effects that /r/ generates be undsunit. -- -- See < https://winterkoninkje.dreamwidth.org/90905.html >. ---annihilative_addition' :: (Eq r, Prd r, Monoid r, Semiring r) => r -> Bool-annihilative_addition' r = Prop.annihilative_on' (~~) (<>) unit r+annihilative_addition' :: (Eq r, Monoid r, Dioid r) => r -> Bool+annihilative_addition' r = Prop.annihilative_on' (~~) (<>) sunit r  -- | \( \forall a, b, c \in R: c + (a * b) \equiv (c + a) * (c + b) \) ----- A right-codistributive semiring has a right-annihilative muliplicative unit:+-- A right-codistributive semiring has a right-annihilative muliplicative sunit: ----- @ 'codistributive' 'unit' a 'mempty' ~~ 'unit' ~~ 'unit' '<>' a @+-- @ 'codistributive' 'sunit' a 'mempty' ~~ 'sunit' ~~ 'sunit' '<>' a @ -- -- idempotent mulitiplication: --@@ -334,75 +221,63 @@ -- -- Furthermore if /R/ is commutative then it is a right-distributive lattice. ---codistributive :: (Eq r, Prd r, Semiring r) => r -> r -> r -> Bool+codistributive :: (Eq r, Dioid r) => r -> r -> r -> Bool codistributive = Prop.distributive_on' (~~) (><) (<>)  --------------------------------------------------------------------------------------- Properties of ordered semirings (aka dioids).---- | '<~' is a preordered relation relative to '<>'.------ This is a required property.----ordered_preordered :: (Prd r, Semiring r) => r -> r -> Bool-ordered_preordered a b = a <~ (a <> b)+-- Properties of kleene dioids --- | 'mempty' is a minimal or least element of @r@.+-- | \( 1 + \sum_{i=1}^{P+1} a^i = 1 + \sum_{i=1}^{P} a^i \) ----- This is a required property.+-- If /a/ is p-stable for some /p/, then we have: ---ordered_monotone_zero :: (Prd r, Monoid r) => r -> Bool-ordered_monotone_zero a = mempty ?~ a ==> mempty <~ a ---- | \( \forall a, b, c: b \leq c \Rightarrow b + a \leq c + a+-- @+-- 'powers' p a ~~ a '><' 'powers' p a '<>' 'sunit'  ~~ 'powers' p a '><' a '<>' 'sunit' +-- @ ----- In an ordered semiring this follows directly from the definition of '<~'.+-- If '<>' and '><' are idempotent then every element is 1-stable: ----- Compare 'cancellative_addition'.--- --- This is a required property.+-- @ a '><' a '<>' a '<>' 'sunit' = a '<>' a '<>' 'sunit' = a '<>' 'sunit' @ ---ordered_monotone_addition :: (Prd r, Semiring r) => r -> r -> r -> Bool-ordered_monotone_addition a = Prop.monotone_on (<~) (<~) (<> a)+kleene_pstable :: (Eq r, Prd r, Monoid r, Dioid r) => Natural -> r -> Bool+kleene_pstable p a = powers p a ~~ powers (p + 1) a --- |  \( \forall a, b: a + b = 0 \Rightarrow a = 0 \wedge b = 0 \)+-- | \( x = a * x + b \Rightarrow x = (1 + \sum_{i=1}^{P} a^i) * b \) ----- This is a required property.+-- If /a/ is p-stable for some /p/, then we have: ---ordered_positive_addition :: (Prd r, Monoid r) => r -> r -> Bool-ordered_positive_addition a b = a <> b =~ mempty ==> a =~ mempty && b =~ mempty+kleene_paffine :: (Eq r, Monoid r, Dioid r) => Natural -> r -> r -> Bool+kleene_paffine p a b = kleene_pstable p a ==> x ~~ a >< x <> b +  where x = powers p a >< b --- | \( \forall a, b, c: b \leq c \Rightarrow b * a \leq c * a+-- | \( \forall a \in R : a^* = a^* * a + 1 \) ----- In an ordered semiring this follows directly from 'distributive' and the definition of '<~'.+-- Closure is /p/-stability for all /a/ in the limit as \( p \to \infinity \). ----- Compare 'cancellative_multiplication'.+-- One way to think of this property is that all geometric series+-- "converge": ----- This is a required property.+-- \( \forall a \in R : 1 + \sum_{i \geq 1} a^i \in R \) ---ordered_monotone_multiplication :: (Prd r, Semiring r) => r -> r -> r -> Bool-ordered_monotone_multiplication a = Prop.monotone_on (<~) (<~) (>< a)+kleene_stable :: (Eq r, Monoid r, Dioid r, Kleene r) => r -> Bool+kleene_stable a = star a ~~ star a >< a <> sunit ---------------------------------------------------------------------------------------- Properties of idempotent and annihilative dioids.+kleene_stable' :: (Eq r, Monoid r, Dioid r, Kleene r) => r -> Bool+kleene_stable' a = star a ~~ sunit <> a >< star a --- | '<~' is consistent with annihilativity.------ This means that a dioid with an annihilative multiplicative unit must satisfy:+kleene_affine :: (Eq r, Monoid r, Dioid r, Kleene r) => r -> r -> Bool+kleene_affine a b = x ~~ a >< x <> b where x = star a >< b++-- If /R/ is kleene then 'star' must be idempotent: ----- @--- ('one' <~) ≡ ('one' ==)--- @+-- @'star' ('star' a) ~~ 'star' a@ ---ordered_annihilative_unit :: (Prd r, Monoid r, Semiring r) => r -> Bool-ordered_annihilative_unit a = unit <~ a <==> unit =~ a+idempotent_star :: (Eq r, Monoid r, Dioid r, Kleene r) => r -> Bool+idempotent_star = Prop.idempotent star --- | \( \forall a, b: a \leq b \Rightarrow a + b = b+-- If @r@ is a kleene dioid then 'star' must be monotone: ---ordered_idempotent_addition :: (Prd r, Monoid r) => r -> r -> Bool-ordered_idempotent_addition a b = (a <~ b) <==> (a <> b =~ b)---- |  \( \forall a, b: a * b = 0 \Rightarrow a = 0 \vee b = 0 \)+-- @x '<~' y ==> 'star' x '<~' 'star' y@ ---ordered_positive_multiplication :: (Prd r, Monoid r, Semiring r) => r -> r -> Bool-ordered_positive_multiplication a b = a >< b =~ mempty ==> a =~ mempty || b =~ mempty+monotone_star :: (Monoid r, Dioid r, Kleene r) => r -> r -> Bool+monotone_star = Prop.monotone_on (<~) (<~) star
− src/Data/Dioid/Signed.hs 
@@ -1,195 +0,0 @@-{-# Language ConstraintKinds #-}-{-# Language Rank2Types #-}--module Data.Dioid.Signed where--import Data.Bifunctor (first)-import Data.Connection-import Data.Connection.Float-import Data.Float-import Data.Ord (Down(..))-import Data.Prd-import Data.Prd.Lattice-import Data.Semigroup.Quantale-import Data.Semiring-import Prelude---- | '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 | Negative | Positive | Indeterminate deriving (Show, Eq)--signOf :: (Eq a, Num a, Prd a) => a -> Sign-signOf x = case sign x of-    Nothing -> Indeterminate-    Just EQ -> Zero-    Just LT -> Negative-    Just GT -> Positive--instance Semigroup Sign where-    Positive <> Positive            = Positive-    Positive <> Negative            = Indeterminate-    Positive <> Zero                = Positive-    Positive <> Indeterminate       = Indeterminate--    Negative <> Positive            = Indeterminate-    Negative <> Negative            = Negative-    Negative <> Zero                = Negative-    Negative <> Indeterminate       = Indeterminate--    Zero <> a                       = a--    Indeterminate <> _              = Indeterminate--instance Monoid Sign where-    mempty = Zero--instance Semiring Sign where-    Positive >< a = a--    Negative >< Positive            = Negative-    Negative >< Negative            = Positive-    Negative >< Zero                = Zero-    Negative >< Indeterminate       = Indeterminate--    Zero >< _                       = Zero--    --NB: measure theoretic zero-    Indeterminate >< Zero           = Zero-    Indeterminate >< _              = Indeterminate--    fromBoolean = fromBooleanDef Positive---- TODO if we dont use canonical ordering then we can define a--- monotone map to floats-instance Prd Sign where-    Positive <~ Positive         = True-    Positive <~ Negative         = False-    Positive <~ Zero             = False-    Positive <~ Indeterminate    = True --    Negative <~ Positive         = False-    Negative <~ Negative         = True-    Negative <~ Zero             = False-    Negative <~ Indeterminate    = True-    -    --Zero <~ Indeterminate        = False-    Zero <~ _                    = True--    Indeterminate <~ Indeterminate  = True-    Indeterminate <~ _              = False--instance Min Sign where-    minimal = Zero--instance Max Sign where-    maximal = Indeterminate--instance Bounded Sign where-    minBound = minimal-    maxBound = maximal---- Signed--newtype Signed = Signed { unSigned :: Float }--instance Show Signed where-    show (Signed x) = show x--instance Eq Signed where-    (Signed x) == (Signed y) | isNan x && isNan y = True -                             | isNan x || isNan y = False-                             | otherwise = split x == split y -- 0 /= -0--instance Prd Signed where-    Signed x <~ Signed y | isNan x && isNan y = True-                         | isNan x || isNan y = False-                         | otherwise = (first Down $ split x) <~ (first Down $ split y)--    pcompare (Signed x) (Signed y) | isNan x && isNan y = Just EQ -                                   | isNan x || isNan y = Nothing -                                   | otherwise = pcompare (first Down $ split x) (first Down $ split y)--f32sgn :: Conn Float Signed-f32sgn = Conn f g where-  f x | x == nInf = Signed $ -0-      | otherwise = Signed $ either (const 0) id $ split x--  g (Signed x) = either (const nInf) id $ split x--ugnsgn :: Conn Unsigned Signed-ugnsgn = Conn f g where-  f (Unsigned x) = Signed $ abs x-  g (Signed x) = Unsigned $ either (const 0) id $ split x--{--ugnf32 :: Conn Unsigned (Down Float)-ugnf32 = Conn f g where-  g (Down x) = Unsigned . max 0 $ x-  f (Unsigned x) = Down x--}----TODO ---dont export constructor, qquoters and/or rebindable syntax--newtype Unsigned = Unsigned Float--unsigned :: Signed -> Unsigned-unsigned (Signed x) = Unsigned (abs x)--instance Show Unsigned where-    show (Unsigned x) = show $ abs x--instance Eq Unsigned where-    (Unsigned x) == (Unsigned y) | finite x && finite y = (abs x) == (abs y) -                                 | not (finite x) && not (finite y) = True-                                 | otherwise = False---- Unsigned has a 2-Ulp interval semiorder containing all joins and meets.-instance Prd Unsigned where-    u <~ v = u `ltugn` v || u == v --ltugn :: Unsigned -> Unsigned -> Bool-ltugn (Unsigned x) (Unsigned y) | finite x && finite y = (abs x) < shift (-2) (abs y) -                                | finite x && not (finite y) = True-                                | otherwise = False--instance Min Unsigned where-    minimal = Unsigned 0--instance Max Unsigned where-    maximal = Unsigned pInf--instance Lattice Unsigned where-  (Unsigned x) \/ (Unsigned y) | finite x && finite y = Unsigned $ max (abs x) (abs y)-                               | otherwise = Unsigned x--  (Unsigned x) /\ (Unsigned y) | finite x && finite y = Unsigned $ min (abs x) (abs y)-                               | not (finite x)  && finite y = Unsigned y-                               | otherwise = Unsigned x--instance Semigroup Unsigned where-    Unsigned x <> Unsigned y = Unsigned $ abs x + abs y--instance Monoid Unsigned where-    mempty = Unsigned 0--instance Semiring Unsigned where-    Unsigned x >< Unsigned y | zero x || zero y = Unsigned 0-                             | otherwise = Unsigned $ abs x * abs y--    fromBoolean = fromBooleanDef (Unsigned 1)--instance Quantale Unsigned where-    x \\ y = y // x--    Unsigned y // Unsigned x = Unsigned . max 0 $ y // x
+ src/Data/Double/Instance.hs view
@@ -0,0 +1,32 @@+{-# LANGUAGE CPP #-}+module Data.Double.Instance where++import Data.Semiring+import Foreign.C.Types (CDouble(..))+import Prelude (Monoid(..), Semigroup(..), Double)+import qualified Prelude as N (Num(..))++#define deriveSemigroup(ty)        \+instance Semigroup (ty) where {    \+   (<>) = (N.+)                    \+;  {-# INLINE (<>) #-}             \+}++#define deriveMonoid(ty)           \+instance Monoid (ty) where {       \+   mempty = 0                      \+}+#define deriveSemiring(ty)         \+instance Semiring (ty) where {     \+   (><) = (N.*)                    \+;  fromBoolean = fromBooleanDef 1  \+;  {-# INLINE (><) #-}             \+;  {-# INLINE fromBoolean #-}      \+}++deriveSemigroup(Double)+deriveSemigroup(CDouble)+deriveMonoid(Double)+deriveMonoid(CDouble)+deriveSemiring(Double)+deriveSemiring(CDouble)
+ src/Data/Fixed/Instance.hs view
@@ -0,0 +1,84 @@+{-# LANGUAGE CPP #-}+module Data.Fixed.Instance where++import Data.Fixed+import Data.Semiring+import Data.Group+import Data.Ring+import Prelude (Monoid(..), Semigroup(..))+import qualified Prelude as N (Num(..))++#define deriveSemigroup(ty)        \+instance Semigroup (ty) where {    \+   (<>) = (N.+)                    \+;  {-# INLINE (<>) #-}             \+}++#define deriveMonoid(ty)           \+instance Monoid (ty) where {       \+   mempty = 0                      \+}++#define deriveGroup(ty)            \+instance Group (ty) where {        \+   (<<) = (N.-)                    \+;  negate = N.negate               \+;  {-# INLINE (<<) #-}             \+;  {-# INLINE negate #-}           \+}++#define deriveSemiring(ty)         \+instance Semiring (ty) where {     \+   (><) = (N.*)                    \+;  fromBoolean = fromBooleanDef 1  \+;  {-# INLINE (><) #-}             \+;  {-# INLINE fromBoolean #-}      \+}++#define deriveRing(ty)             \+instance Ring (ty) where {         \+   abs = N.abs                     \+;  signum = N.signum               \+;  {-# INLINE abs #-}              \+;  {-# INLINE signum #-}           \+}++deriveSemigroup(Uni)+deriveSemigroup(Deci)+deriveSemigroup(Centi)+deriveSemigroup(Milli)+deriveSemigroup(Micro)+deriveSemigroup(Nano)+deriveSemigroup(Pico)++deriveMonoid(Uni)+deriveMonoid(Deci)+deriveMonoid(Centi)+deriveMonoid(Milli)+deriveMonoid(Micro)+deriveMonoid(Nano)+deriveMonoid(Pico)++deriveGroup(Uni)+deriveGroup(Deci)+deriveGroup(Centi)+deriveGroup(Milli)+deriveGroup(Micro)+deriveGroup(Nano)+deriveGroup(Pico)++deriveSemiring(Uni)+deriveSemiring(Deci)+deriveSemiring(Centi)+deriveSemiring(Milli)+deriveSemiring(Micro)+deriveSemiring(Nano)+deriveSemiring(Pico)++deriveRing(Uni)+deriveRing(Deci)+deriveRing(Centi)+deriveRing(Milli)+deriveRing(Micro)+deriveRing(Nano)+deriveRing(Pico)
+ src/Data/Float/Instance.hs view
@@ -0,0 +1,32 @@+{-# LANGUAGE CPP #-}+module Data.Float.Instance where++import Data.Semiring+import Foreign.C.Types (CFloat(..))+import Prelude (Monoid(..), Semigroup(..), Float)+import qualified Prelude as N (Num(..))++#define deriveSemigroup(ty)        \+instance Semigroup (ty) where {    \+   (<>) = (N.+)                    \+;  {-# INLINE (<>) #-}             \+}++#define deriveMonoid(ty)           \+instance Monoid (ty) where {       \+   mempty = 0                      \+}+#define deriveSemiring(ty)         \+instance Semiring (ty) where {     \+   (><) = (N.*)                    \+;  fromBoolean = fromBooleanDef 1  \+;  {-# INLINE (><) #-}             \+;  {-# INLINE fromBoolean #-}      \+}++deriveSemigroup(Float)+deriveSemigroup(CFloat)+deriveMonoid(Float)+deriveMonoid(CFloat)+deriveSemiring(Float)+deriveSemiring(CFloat)
src/Data/Group.hs view
@@ -1,5 +1,6 @@ module Data.Group where +import Data.Complex import Prelude hiding (Num(..))  infixl 6 <<@@ -18,3 +19,6 @@    (<<) :: a -> a -> a   x << y = x <> negate y++instance (Monoid (Complex a), Group a) => Group (Complex a) where+  negate (x :+ y) = negate x :+ negate y
+ src/Data/Int/Instance.hs view
@@ -0,0 +1,79 @@+{-# LANGUAGE CPP #-}+module Data.Int.Instance where++import Data.Semiring+import Data.Group+import Data.Ring+import Data.Int+import Prelude (Monoid(..), Semigroup(..), Integer)+import qualified Prelude as N (Num(..))++#define deriveSemigroup(ty)        \+instance Semigroup (ty) where {    \+   (<>) = (N.+)                    \+;  {-# INLINE (<>) #-}             \+}++#define deriveMonoid(ty)           \+instance Monoid (ty) where {       \+   mempty = 0                      \+}++#define deriveGroup(ty)            \+instance Group (ty) where {        \+   (<<) = (N.-)                    \+;  negate = N.negate               \+;  {-# INLINE (<<) #-}             \+;  {-# INLINE negate #-}           \+}++#define deriveSemiring(ty)         \+instance Semiring (ty) where {     \+   (><) = (N.*)                    \+;  fromBoolean = fromBooleanDef 1  \+;  {-# INLINE (><) #-}             \+;  {-# INLINE fromBoolean #-}      \+}++#define deriveRing(ty)             \+instance Ring (ty) where {         \+   abs = N.abs                     \+;  signum = N.signum               \+;  {-# INLINE abs #-}              \+;  {-# INLINE signum #-}           \+}++deriveSemigroup(Int)+deriveSemigroup(Int8)+deriveSemigroup(Int16)+deriveSemigroup(Int32)+deriveSemigroup(Int64)+deriveSemigroup(Integer)++deriveMonoid(Int)+deriveMonoid(Int8)+deriveMonoid(Int16)+deriveMonoid(Int32)+deriveMonoid(Int64)+deriveMonoid(Integer)++deriveGroup(Int)+deriveGroup(Int8)+deriveGroup(Int16)+deriveGroup(Int32)+deriveGroup(Int64)+deriveGroup(Integer)++deriveSemiring(Int)+deriveSemiring(Int8)+deriveSemiring(Int16)+deriveSemiring(Int32)+deriveSemiring(Int64)+deriveSemiring(Integer)++deriveRing(Int)+deriveRing(Int8)+deriveRing(Int16)+deriveRing(Int32)+deriveRing(Int64)+deriveRing(Integer)
src/Data/Ring.hs view
@@ -1,4 +1,10 @@-module Data.Ring where+module Data.Ring (+    (<<)+  , (><)+  , (<>)+  , negate+  , Ring(..)+) where  import Data.Group import Data.Semiring
− src/Data/Semigroup/Orphan.hs 
@@ -1,37 +0,0 @@--- | Orphan instances from base.-module Data.Semigroup.Orphan where--import Control.Applicative-import Data.Complex-import Data.Functor.Alt-import Data.Functor.Plus-import Numeric.Natural (Natural)---instance Semigroup Word where (<>) = (+)--instance Monoid Word where mempty = 0--instance Semigroup Int where (<>) = (+)--instance Monoid Int where mempty = 0--instance Semigroup Bool where (<>) = (||)--instance Monoid Bool where mempty = False--instance Semigroup Float where (<>) = (+)--instance Monoid Float where mempty = 0--instance Semigroup a => Semigroup (Complex a) where-  (x :+ y) <> (x' :+ y') = (x <> x') :+ (y <> y')--instance Monoid a => Monoid (Complex a) where-  mempty = mempty :+ mempty--instance Semigroup Natural where (<>) = (+)--instance Monoid Natural where mempty = 0--
− src/Data/Semigroup/Quantale.hs 
@@ -1,68 +0,0 @@-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE AllowAmbiguousTypes #-}--module Data.Semigroup.Quantale where--import Data.Connection hiding (floor', ceiling')-import Data.Connection.Yoneda-import Data.Float-import Data.Group-import Data.Prd-import Data.Prd.Lattice-import Data.Word-import Data.Semigroup.Orphan ()-import Prelude hiding (negate, until, filter)-import Test.Property.Util ((<==>),(==>))-import qualified Prelude as Pr--residuated :: Quantale a => a -> a -> a -> Bool-residuated x y z = x <> y <~ z <==> y <~ x \\ z <==> x <~ z // y----- | 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 where-    residr :: a -> Conn a a-    residr x = Conn (x<>) (x\\)--    residl :: a -> Conn a a-    residl x = Conn (<>x) (//x)--    (\\) :: a -> a -> a-    x \\ y = connr (residr x) y--    (//) :: a -> a -> a-    x // y = connl (residl x) y--instance Quantale Float where-    x \\ y = y // x--    --x <> y <~ z iff y <~ x \\ z iff x <~ z // y.-    y // x | y =~ x = 0-           | otherwise = let z = y - x in if z + x <~ y then upper' z (x<>) y else lower' z (x<>) y ---- @'lower'' x@ is the least element /y/ in the descending--- chain such that @not $ f y '<~' x@.----lower' :: Prd a => Float -> (Float -> a) -> a -> Float-lower' z f x = until (\y -> f y <~ x) ge (shift $ -1) z---- @'upper' y@ is the greatest element /x/ in the ascending--- chain such that @g x '<~' y@.----upper' :: Prd a => Float -> (Float -> a) -> a -> Float-upper' z g y = while (\x -> g x <~ y) le (shift 1) z--incBy :: Yoneda a => Quantale a => a -> Rep a -> Rep a-incBy x = connl filter . (x <>) . connr filter--decBy :: Yoneda a => Quantale a => a -> Rep a -> Rep a-decBy x = connl filter . (x \\) . connr filter
src/Data/Semiring.hs view
@@ -1,5 +1,5 @@ {-# Language ConstrainedClassMethods #-}-+{-# Language DefaultSignatures #-} {-# Language DeriveFunctor #-} {-# Language DeriveGeneric #-} @@ -7,18 +7,17 @@  import Control.Applicative import Control.Monad+import Data.Complex import Data.Foldable hiding (product) import Data.Functor.Apply import Data.Functor.Classes-import Data.Functor.Contravariant import Data.Functor.Contravariant (Predicate(..), Equivalence(..), Op(..))-import Data.Functor.Contravariant.Divisible import Data.Functor.Identity (Identity(..))+import Data.Group import Data.List (unfoldr) import Data.List.NonEmpty (NonEmpty(..)) import Data.Semigroup import Data.Semigroup.Foldable-import Data.Semigroup.Orphan () import Data.Typeable (Typeable) import Foreign.Storable (Storable) import GHC.Generics (Generic, Generic1)@@ -30,24 +29,27 @@ import qualified Data.Set as Set import qualified Data.IntMap as IntMap +infixr 7 ><+ -- | 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) >< c = (a >< c) <> (b >< c)@+-- @+-- (a <> b) >< c ≡ (a >< c) <> (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+-- and 'sunit', such that 'mempty' is right-neutral wrt addition, 'sunit' 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. +-- Note that 'sunit' needn't be distinct from 'mempty', moreover addition and multiplication+-- needn't be commutative or left-distributive. -- -- See the properties module for a detailed specification of the laws. --@@ -57,22 +59,21 @@   (><) :: r -> r -> r      -- A semiring homomorphism from the Boolean semiring to @r@. -  -- If this map is injective then @r@ has a distinct unit.+  -- If this map is injective then @r@ has a distinct sunit.   fromBoolean :: Monoid r => Bool -> r   fromBoolean _ = mempty -unit :: (Monoid r, Semiring r) => r-unit = fromBoolean True+sunit :: (Monoid r, Semiring r) => r+sunit = fromBoolean True  fromBooleanDef :: (Monoid r, Semiring r) => r -> Bool -> r fromBooleanDef _ False = mempty fromBooleanDef o True = o - -- | Fold over a collection using the multiplicative operation of a semiring. --  -- @--- 'product' f ≡ 'Data.foldr'' ((><) . f) 'unit'+-- 'product' f ≡ 'Data.foldr'' ((><) . f) 'sunit' -- @ -- -- >>> (foldMap . product) id [[1, 2], [3, (4 :: Int)]] -- 1 >< 2 <> 3 >< 4@@ -81,15 +82,15 @@ -- >>> (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@:+-- For semirings without a distinct multiplicative sunit 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-product f = foldr' ((><) . f) unit+product :: Foldable t => Monoid r => Semiring r => (a -> r) -> t a -> r+product f = foldr' ((><) . f) sunit  -- | Fold over a non-empty collection using the multiplicative operation of a semiring. --@@ -98,39 +99,27 @@ -- >>> product1 Just $ 1 :| [2..(5 :: Int)] -- Just 120 ---product1 :: (Foldable1 t, Semiring r) => (a -> r) -> t a -> r+product1 :: Foldable1 t => Semiring r => (a -> r) -> t a -> r product1 f = getProd . foldMap1 (Prod . f)  -- | Cross-multiply two collections. ----- >>> cross [1,2,3 ::Int] [1,2,3]+-- >>> cross [1,2,3 :: Int] [1,2,3] -- 36 ----- >>> cross [1,2,3 ::Int] []+-- >>> cross [1,2,3 :: Int] [] -- 0 ---cross :: (Foldable t, Applicative t, Monoid r, Semiring r) => t r -> t r -> r+cross :: Foldable f => Applicative f => Monoid r => Semiring r => f r -> f r -> r cross a b = fold $ liftA2 (><) a b +-- | Cross-multiply two non-empty collections.+-- -- >>> cross1 (Right 2 :| [Left "oops"]) (Right 2 :| [Right 3]) :: Either [Char] Int -- Right 4-cross1 :: (Foldable1 t, Apply t, Semiring r) => t r -> t r -> r-cross1 a b = fold1 $ liftF2 (><) a b---- | Fold with no additive or multiplicative unit.-foldPresemiring :: Semiring r => (a -> r) -> NonEmpty (NonEmpty a) -> r-foldPresemiring = foldMap1 . product1---- | Fold with no multiplicative unit.-foldNonunital :: (Monoid r, Semiring r) => (a -> r) -> [NonEmpty a] -> r-foldNonunital = foldMap . product1---- | 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-foldUnital = foldMap . product+cross1 :: Foldable1 f => Apply f => Semiring r => f r -> f r -> r+cross1 a b = fold1 $ liftF2 (><) a b  -- | A generalization of 'Data.List.replicate' to an arbitrary 'Monoid'.  --@@ -151,19 +140,69 @@             | otherwise = g (x <> x) ((y - 1) `quot` 2) (x <> z) {-# INLINE replicate #-} -replicate' :: (Monoid r, Semiring r) => Natural -> r -> r+replicate' :: Monoid r => Semiring r => Natural -> r -> r replicate' n r = getProd $ replicate n (Prod r)  infixr 8 ^ -(^) :: (Monoid r, Semiring r) => r -> Natural -> r+(^) :: Monoid r => Semiring r => r -> Natural -> r (^) = flip replicate' -powers :: (Monoid r, Semiring r) => Natural -> r -> r-powers n a = foldr' (<>) unit . flip unfoldr n $ \m -> +powers :: Monoid r => Semiring r => Natural -> r -> r+powers n a = foldr' (<>) sunit . flip unfoldr n $ \m ->    if m == 0 then Nothing else Just (a^m,m-1)  -------------------------------------------------------------------------------+-- 'Kleene'+-------------------------------------------------------------------------------++-- | Infinite closures of a semiring.+--+-- 'Kleene' adds a Kleene 'star' operator to a 'Semiring', with an infinite closure property:+--+-- @'star' x ≡ 'star' x '><' x '<>' 'sunit' ≡ x '><' 'star' x '<>' 'sunit'@+--+-- If @r@ is a dioid then 'star' must be monotonic:+--+-- @x '<~' y ==> 'star' x '<~' 'star' y+--+-- See also <https://en.wikipedia.org/wiki/Semiring#Kleene_semirings closed semiring>+--+class Semiring a => Kleene a where+  {-# MINIMAL star | plus #-} ++  star :: a -> a+  default star :: Monoid a => a -> a+  star a = sunit <> plus a++  plus :: a -> a+  plus a = a >< star a++-- This only works if * is idempotent (a lattice?), as it just sums w/o powers+--star = fmap fold . many+--plus = fmap fold . some++--interior :: (r -> r) -> r -> r+--interior f r = (r ><) . f+--adjoint . star = plus . adjoint++--star = (>< mempty) . (<> mempty)+--plus = (<> sunit) . (>< sunit)++instance Kleene () where+  star  _ = ()+  plus _ = ()+  {-# INLINE star #-}+  {-# INLINE plus #-}++instance (Monoid b, Kleene b) => Kleene (a -> b) where+  plus = fmap plus+  {-# INLINE plus #-}++  star = fmap star+  {-# INLINE star #-}++------------------------------------------------------------------------------- -- Pre-semirings ------------------------------------------------------------------------------- @@ -225,26 +264,6 @@    fromBoolean = fromBooleanDef GT -instance Semiring Bool where-  (><) = (&&)--  fromBoolean = id--instance Semiring Natural where-  (><) = (*)--  fromBoolean = fromBooleanDef 1--instance Semiring Int where-  (><) = (*)--  fromBoolean = fromBooleanDef 1--instance Semiring Word where-  (><) = (*)--  fromBoolean = fromBooleanDef 1- -- >>> (> (0::Int)) >< ((< 10) <> (== 15)) $ 10 -- False -- >>> (> (0::Int)) >< ((< 10) <> (== 15)) $ 15@@ -259,7 +278,7 @@   Op f >< Op g = Op $ \x -> f x >< g x   {-# INLINE (><) #-} -  fromBoolean = fromBooleanDef $ Op (const unit)+  fromBoolean = fromBooleanDef $ Op (const sunit)  instance (Monoid a, Monoid b, Semiring a, Semiring b) => Semiring (a, b) where   (a, b) >< (c, d) = (a><c, b><d)@@ -267,6 +286,14 @@    fromBoolean = liftA2 (,) fromBoolean fromBoolean +instance (Semigroup (Complex a), Group a, Semiring a) => Semiring (Complex a) where+  (x :+ y) >< (x' :+ y') = (x >< x' << y >< y') :+ (x >< y' <> y >< x')+  {-# INLINE (><) #-}++  fromBoolean False = mempty+  fromBoolean True = fromBoolean True :+ mempty+  {-# INLINE fromBoolean #-}+ instance Monoid a => Semiring [a] where    (><) = liftA2 (<>)   {-# INLINE (><) #-}@@ -350,13 +377,6 @@   fromBoolean False = Equivalence $ \_ _ -> True   fromBoolean True = Equivalence $ \_ _ -> False --instance Semiring (Comparison a) where-  Comparison f >< Comparison g = Comparison $ \x y -> f x y >< g x y-  {-# INLINE (><) #-}--  fromBoolean = fromBooleanDef $ Comparison $ \_ _ -> GT- --------------------------------------------------------------------- --  Instances (containers) ---------------------------------------------------------------------@@ -399,7 +419,7 @@   (<>) = liftA2 (><)   {-# INLINE (<>) #-} --- Note that 'unit' must be distinct from 'mempty' for this instance to be legal.+-- Note that 'sunit' must be distinct from 'mempty' for this instance to be legal. instance (Monoid a, Semiring a) => Monoid (Prod a) where-  mempty = Prod unit+  mempty = Prod sunit   {-# INLINE mempty #-}
src/Data/Semiring/Property.hs view
@@ -25,14 +25,6 @@   , distributive_finite1_on    , distributive_cross_on   , distributive_cross1_on -{--  -- * Properties of closed semirings-  , closed_pstable-  , closed_paffine -  , closed_stable -  , closed_affine -  , idempotent_star--} ) where  import Data.List.NonEmpty (NonEmpty(..))@@ -47,7 +39,7 @@  -- | \( \forall a \in R: (z + a) \sim a \) ----- A (pre-)semiring with a right-neutral additive unit must satisfy:+-- A (pre-)semiring with a right-neutral additive sunit must satisfy: -- -- @ -- 'neutral_addition' 'mempty' ~~ const True@@ -69,16 +61,16 @@  -- | \( \forall a \in R: (o * a) \sim a \) ----- A (pre-)semiring with a right-neutral multiplicative unit must satisfy:+-- A (pre-)semiring with a right-neutral multiplicative sunit must satisfy: -- -- @--- 'neutral_multiplication' 'unit' ~~ const True+-- 'neutral_multiplication' 'sunit' ~~ const True -- @ --  -- Or, equivalently: -- -- @--- 'unit' '><' r ~~ r+-- 'sunit' '><' r ~~ r -- @ -- -- This is a required property.@@ -87,7 +79,7 @@ neutral_multiplication_on (~~) = Prop.neutral_on (~~) (><)   neutral_multiplication_on' :: (Monoid r, Semiring r) => Rel r -> r -> Bool-neutral_multiplication_on' (~~) = Prop.neutral_on (~~) (><) unit+neutral_multiplication_on' (~~) = Prop.neutral_on (~~) (><) sunit  -- | \( \forall a, b, c \in R: (a + b) + c \sim a + (b + c) \) --@@ -133,7 +125,7 @@  -- | \( \forall a, b \in R: a * b \sim a * b + b \) ----- If /R/ is non-unital (i.e. /unit/ is not distinct from /mempty/) then it will instead satisfy +-- If /R/ is non-unital (i.e. /sunit/ is not distinct from /mempty/) then it will instead satisfy  -- a right-absorbtion property.  -- -- This follows from right-neutrality and right-distributivity.@@ -147,13 +139,12 @@ nonunital_on :: (Monoid r, Semiring r) => Rel r -> r -> r -> Bool nonunital_on (~~) a b = (a >< b) ~~ (a >< b <> b) - ------------------------------------------------------------------------------------ -- Properties of unital semirings  -- | \( \forall a \in R: (z * a) \sim u \) ----- A /R/ is unital then its addititive unit must be right-annihilative, i.e.:+-- A /R/ is unital then its addititive sunit must be right-annihilative, i.e.: -- -- @ -- 'mempty' '><' a ~~ 'mempty'@@ -165,7 +156,7 @@ -- 'empty' '*>' a ~~ 'empty' -- @ ----- All right semirings must have a right-absorbative addititive unit,+-- All right semirings must have a right-absorbative addititive sunit, -- however note that depending on the 'Prd' instance this does not preclude  -- IEEE754-mandated behavior such as:  --@@ -184,7 +175,7 @@ -- homomorphism_boolean :: forall r. (Eq r, Monoid r, Semiring r) => Bool -> Bool -> Bool homomorphism_boolean i j =-  fromBoolean True     == (unit @r)  &&+  fromBoolean True     == (sunit @r)  &&   fromBoolean False    == (mempty @r) &&   fromBoolean (i && j) == fi >< fj    &&    fromBoolean (i || j) == fi <> fj @@ -195,7 +186,6 @@ ------------------------------------------------------------------------------------ -- Properties of cancellative & commutative semirings - -- | \( \forall a, b, c \in R: b + a \sim c + a \Rightarrow b = c \) -- -- If /R/ is right-cancellative wrt addition then for all /a/@@ -204,7 +194,6 @@ cancellative_addition_on :: Semigroup r => Rel r -> r -> r -> r -> Bool cancellative_addition_on (~~) a = Prop.injective_on (~~) (<> a) - -- | \( \forall a, b, c \in R: b * a \sim c * a \Rightarrow b = c \) -- -- If /R/ is right-cancellative wrt multiplication then for all /a/@@ -213,13 +202,11 @@ cancellative_multiplication_on :: Semiring r => Rel r -> r -> r -> r -> Bool cancellative_multiplication_on (~~) a = Prop.injective_on (~~) (>< a) - -- | \( \forall a, b \in R: a + b \sim b + a \) -- commutative_addition_on :: Semigroup r => Rel r -> r -> r -> Bool commutative_addition_on (~~) = Prop.commutative_on (~~) (<>) - -- | \( \forall a, b \in R: a * b \sim b * a \) -- commutative_multiplication_on :: Semiring r => Rel r -> r -> r -> Bool@@ -235,7 +222,7 @@ -- For types with exact arithmetic this follows from 'distributive' & 'neutral_multiplication'. -- distributive_finite_on :: (Monoid r, Semiring r) => Rel r -> [r] -> r -> Bool-distributive_finite_on (~~) as b = fold as >< b ~~ foldMap (>< b) as+distributive_finite_on (~~) as b = (fold as >< b) ~~ (foldMap (>< b) as)  -- | \( \forall M \geq 1; a_1 \dots a_M, b \in R: (\sum_{i=1}^M a_i) * b \sim \sum_{i=1}^M a_i * b \) --@@ -244,80 +231,18 @@ -- 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-distributive_finite1_on (~~) as b = fold1 as >< b ~~ foldMap1 (>< b) as+distributive_finite1_on (~~) as b = (fold1 as >< b) ~~ (foldMap1 (>< b) as)  -- | \( \forall M,N \geq 0; a_1 \dots a_M, b_1 \dots b_N \in R: (\sum_{i=1}^M a_i) * (\sum_{j=1}^N b_j) \sim \sum_{i=1 j=1}^{i=M j=N} a_i * b_j \) -- -- If /R/ is also left-distributive then it supports cross-multiplication. -- distributive_cross_on :: (Monoid r, Semiring r) => Rel r -> [r] -> [r] -> Bool-distributive_cross_on (~~) as bs = fold as >< fold bs ~~ cross as bs-+distributive_cross_on (~~) as bs = (fold as >< fold bs) ~~ (cross as bs)  -- | \( \forall M,N \geq 1; a_1 \dots a_M, b_1 \dots b_N \in R: (\sum_{i=1}^M a_i) * (\sum_{j=1}^N b_j) = \sum_{i=1 j=1}^{i=M j=N} a_i * b_j \) -- -- 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-distributive_cross1_on (~~) as bs = fold1 as >< fold1 bs ~~ cross1 as bs----------------------------------------------------------------------------------------- Properties of closed semirings--{---- | \( 1 + \sum_{i=1}^{P+1} a^i = 1 + \sum_{i=1}^{P} a^i \)------ If /a/ is p-stable for some /p/, then we have:------ @--- 'powers' p a ~~ a '><' 'powers' p a '<>' 'unit'  ~~ 'powers' p a '><' a '<>' 'unit' --- @------ If '<>' and '><' are idempotent then every element is 1-stable:------ @ a '><' a '<>' a '<>' 'unit' = a '<>' a '<>' 'unit' = a '<>' 'unit' @----closed_pstable :: (Eq r, Prd r, Monoid r, Semiring r) => Natural -> r -> Bool-closed_pstable p a = powers p a ~~ powers (p <> unit) a---- | \( x = a * x + b \Rightarrow x = (1 + \sum_{i=1}^{P} a^i) * b \)------ If /a/ is p-stable for some /p/, then we have:----closed_paffine :: (Prd r, Monoid r, Semiring r) => Natural -> r -> r -> Bool-closed_paffine p a b = closed_pstable p a ==> x ~~ a >< x <> b -  where x = powers p a >< b---- | \( \forall a \in R : a^* = a^* * a + 1 \)------ Closure is /p/-stability for all /a/ in the limit as \( p \to \infinity \).------ One way to think of this property is that all geometric series--- "converge":------ \( \forall a \in R : 1 + \sum_{i \geq 1} a^i \in R \)----closed_stable :: (Prd r, Monoid r, Closed r) => r -> Bool-closed_stable a = star a ~~ star a >< a <> unit--closed_stable' :: (Prd r, Monoid r, Closed r) => r -> Bool-closed_stable' a = star a ~~ unit <> a >< star a--closed_affine :: (Prd r, Monoid r, Closed r) => r -> r -> Bool-closed_affine a b = x ~~ a >< x <> b where x = star a >< b---- If /R/ is closed then 'star' must be idempotent:------ @'star' ('star' a) ~~ 'star' a@----idempotent_star :: (Prd r, Monoid r, Closed r) => r -> Bool-idempotent_star = Prop.idempotent star---- If @r@ is a closed dioid then 'star' must be monotone:------ @x '<~' y ==> 'star' x '<~' 'star' y@----monotone_star :: (Prd r, Monoid r, Closed r) => r -> r -> Bool-monotone_star = Prop.monotone_on (<~) star---}+distributive_cross1_on (~~) as bs = (fold1 as >< fold1 bs) ~~ (cross1 as bs)
+ src/Data/Word/Instance.hs view
@@ -0,0 +1,61 @@+{-# LANGUAGE CPP #-}+module Data.Word.Instance where++import Data.Dioid+import Data.Prd+import Data.Semiring+import Data.Word+import Numeric.Natural+import Prelude (Monoid(..), Semigroup(..))+import qualified Prelude as N (Num(..))++#define deriveSemigroup(ty)        \+instance Semigroup (ty) where {    \+   (<>) = (N.+)                    \+;  {-# INLINE (<>) #-}             \+}++#define deriveMonoid(ty)           \+instance Monoid (ty) where {       \+   mempty = 0                      \+}++#define deriveSemiring(ty)         \+instance Semiring (ty) where {     \+   (><) = (N.*)                    \+;  fromBoolean = fromBooleanDef 1  \+;  {-# INLINE (><) #-}             \+;  {-# INLINE fromBoolean #-}      \+}++#define deriveDioid(ty)             \+instance Dioid (ty) where {         \+}++deriveSemigroup(Word)+deriveSemigroup(Word8)+deriveSemigroup(Word16)+deriveSemigroup(Word32)+deriveSemigroup(Word64)+deriveSemigroup(Natural)++deriveMonoid(Word)+deriveMonoid(Word8)+deriveMonoid(Word16)+deriveMonoid(Word32)+deriveMonoid(Word64)+deriveMonoid(Natural)++deriveSemiring(Word)+deriveSemiring(Word8)+deriveSemiring(Word16)+deriveSemiring(Word32)+deriveSemiring(Word64)+deriveSemiring(Natural)++deriveDioid(Word)+deriveDioid(Word8)+deriveDioid(Word16)+deriveDioid(Word32)+deriveDioid(Word64)+deriveDioid(Natural)
test/Test/Data/Dioid/Signed.hs view
@@ -146,7 +146,7 @@ x = f 0.37794903 y = f 0.3269925 -counit (residl x) y+cosunit (residl x) y   residl x = Conn (<>x) . (//x) $ y