packages feed

rings 0.0.1 → 0.0.2

raw patch · 8 files changed

+1058/−15 lines, 8 filesdep +connectionsdep +hedgehogdep +ringsdep ~basedep ~containersdep ~contravariant

Dependencies added: connections, hedgehog, rings

Dependency ranges changed: base, containers, contravariant, property, semigroupoids

Files

rings.cabal view
@@ -1,24 +1,29 @@ name:                rings-version:             0.0.1-synopsis:            basic algebra-description:         Groups, rings, and semirings. -homepage:            https://github.com/cmk/algebras+version:             0.0.2+synopsis:            Rings, semirings, and dioids.+description:         Lawful versions 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+category:            Math, Numerical build-type:          Simple extra-source-files:  ChangeLog.md cabal-version:       >=1.10  library   exposed-modules:-      Data.Group-      Data.Ring-      Data.Semigroup.Orphan-      Data.Semiring-      Data.Semiring.Property+      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   default-extensions:       ScopedTypeVariables     , TypeApplications@@ -27,11 +32,30 @@     , FlexibleInstances    build-depends:       -      base <5.0-    , containers-    , contravariant-    , property-    , semigroupoids+      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    hs-source-dirs: src   default-language: Haskell2010++test-suite test+  type: exitcode-stdio-1.0+  other-modules:+      Test.Data.Dioid.Signed+  build-depends:       +      base == 4.*+    , connections -any +    , hedgehog+    , property+    , rings+  default-extensions:+      ScopedTypeVariables,+      TypeApplications+  main-is: test.hs+  hs-source-dirs: test+  default-language: Haskell2010+  ghc-options: -threaded -rtsopts -with-rtsopts=-N -Wall
+ src/Data/Dioid.hs view
@@ -0,0 +1,9 @@+{-# Language ConstraintKinds #-}+module Data.Dioid where++import Data.Connection.Yoneda+import Data.Semiring++type Dioid a = (Yoneda a, Semiring a)++
+ src/Data/Dioid/Interval.hs view
@@ -0,0 +1,116 @@+-- | <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
@@ -0,0 +1,408 @@+{-# 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 +  , absorbative_addition+  , absorbative_addition'+  , idempotent_addition+  , absorbative_multiplication+  , absorbative_multiplication' +  -- * Properties of annihilative semirings +  , 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+) where++import Data.Prd+import Data.List (unfoldr)+import Data.List.NonEmpty (NonEmpty(..))+import Data.Semiring+import Data.Semigroup.Orphan ()+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++-- | \( \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+-- @+--+-- 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' (~~)++-- | \( \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+-- @+--+-- 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' (~~)++-- | \( \forall a, b, c \in R: (a + b) + c = a + (b + c) \)+--+-- /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+associative_addition = Prop.associative_addition_on (~~)++-- | \( \forall a, b, c \in R: (a * b) * c = a * (b * c) \)+--+-- /R/ must right-associate multiplication.+--+-- This is a required property.+--+associative_multiplication :: (Eq r, Prd r, Semiring r) => r -> r -> r -> Bool+associative_multiplication = Prop.associative_multiplication_on (~~)++-- | \( \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: +--+-- @+-- (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+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++-- | \( \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'+-- @+--+-- 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+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 (~~)++-- | \( \forall a, b \in R: a + b = b + a \)+--+commutative_addition :: (Eq r, Prd r, Semigroup r) => r -> r -> Bool+commutative_addition = Prop.commutative_addition_on (=~)+++-- | \( \forall a, b \in R: a * b = b * a \)+--+commutative_multiplication :: (Eq r, Prd r, Semiring r) => r -> r -> Bool+commutative_multiplication = Prop.commutative_multiplication_on (=~)+++------------------------------------------------------------------------------------+-- Properties of idempotent & absorbative semirings++-- | \( \forall a, b \in R: a * b + b = b \)+--+-- 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+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+ +-- | \( \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' :: (Eq r, Prd r, Semiring r) => r -> r -> Bool+absorbative_addition' a b = b <> b >< a ~~ b++-- | \( \forall a, b \in R: (a + b) * b = b \)+--+-- 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+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 ++-- | \( \forall a, b \in R: b * (b + a) = b \)+--+-- 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+absorbative_multiplication' a b = b >< (b <> a) ~~ b++-- | \( \forall a \in R: o + a = o \)+--+-- 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+annihilative_addition r = Prop.annihilative_on (~~) (<>) unit r+++-- | \( \forall a \in R: a + o = o \)+--+-- 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+annihilative_addition' r = Prop.annihilative_on' (~~) (<>) unit 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:+--+-- @ '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+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)++-- | 'mempty' is a minimal or least element of @r@.+--+-- This is a required property.+--+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+--+-- 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+ordered_monotone_addition a = Prop.monotone_on (<~) (<~) (<> a)++-- |  \( \forall a, b: a + b = 0 \Rightarrow a = 0 \wedge b = 0 \)+--+-- This is a required property.+--+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: 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+ordered_monotone_multiplication a = Prop.monotone_on (<~) (<~) (>< a)++------------------------------------------------------------------------------------+-- Properties of idempotent and annihilative dioids.++-- | '<~' 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+ordered_annihilative_unit a = unit <~ a <==> unit =~ a++-- | \( \forall a, b: a \leq b \Rightarrow a + b = b+--+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 \)+--+ordered_positive_multiplication :: (Prd r, Monoid r, Semiring r) => r -> r -> Bool+ordered_positive_multiplication a b = a >< b =~ mempty ==> a =~ mempty || b =~ mempty
+ src/Data/Dioid/Signed.hs view
@@ -0,0 +1,195 @@+{-# 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/Semigroup/Quantale.hs view
@@ -0,0 +1,68 @@+{-# 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
+ test/Test/Data/Dioid/Signed.hs view
@@ -0,0 +1,206 @@+{-# LANGUAGE TemplateHaskell #-}+module Test.Data.Dioid.Signed where++import Prelude ++import Data.Ord (Down(..))+import Data.Prd+import Data.Semiring+import Data.Connection+import Data.Dioid.Signed+import Data.Float+import Data.Semigroup.Quantale++import qualified Data.Prd.Property as Prop+import qualified Data.Semiring.Property as Prop+import qualified Data.Connection.Property as Prop++import Hedgehog+import Test.Data.Float+import Test.Property.Util+import qualified Hedgehog.Gen as G+import qualified Hedgehog.Range as R++gen_sign :: Gen Sign+gen_sign = G.choice $ fmap pure [Zero, Positive, Negative, Indeterminate]++gen_signed :: Gen Signed+gen_signed = Signed <$> gen_flt32'++gen_unsigned :: Gen Unsigned+gen_unsigned = Unsigned <$> gen_flt32++gen_unsigned' :: Gen Unsigned+gen_unsigned' = Unsigned <$> gen_flt32'++prop_prd_signed :: Property+prop_prd_signed = withTests 1 $ property $ do+  x <- forAll gen_signed+  y <- forAll gen_signed+  z <- forAll gen_signed++  assert $ Prop.reflexive_eq x+  assert $ Prop.reflexive_le x+  assert $ Prop.irreflexive_lt x+  assert $ Prop.symmetric x y+  assert $ Prop.asymmetric x y+  assert $ Prop.antisymmetric x y+  assert $ Prop.transitive_lt x y z+  assert $ Prop.transitive_le x y z+  assert $ Prop.transitive_eq x y z++prop_connection_flt32_signed :: Property+prop_connection_flt32_signed = withTests 1 $ property $ do+  x <- forAll gen_flt32'+  y <- forAll gen_signed+  x' <- forAll gen_flt32'+  y' <- forAll gen_signed++  assert $ Prop.connection f32sgn x y+  assert $ Prop.monotone' f32sgn x x'+  assert $ Prop.monotone  f32sgn y y'+  assert $ Prop.closed f32sgn x+  assert $ Prop.kernel f32sgn y ++prop_prd_unsigned :: Property+prop_prd_unsigned = withTests 1000 $ property $ do+  x <- forAll gen_unsigned'+  y <- forAll gen_unsigned'+  z <- forAll gen_unsigned'+  w <- forAll gen_unsigned'++  assert $ Prop.reflexive_eq x+  assert $ Prop.reflexive_le x+  assert $ Prop.irreflexive_lt x+  assert $ Prop.symmetric x y+  assert $ Prop.asymmetric x y+  assert $ Prop.antisymmetric x y+  assert $ Prop.transitive_lt x y z+  assert $ Prop.transitive_le x y z+  assert $ Prop.transitive_eq x y z++  assert $ Prop.connex x y+  assert $ Prop.semiconnex x y+  assert $ Prop.trichotomous x y+  assert $ Prop.chain_22 x y z w+  assert $ Prop.chain_31 x y z w++prop_semiring_unsigned :: Property+prop_semiring_unsigned = withTests 1000 $ property $ do+  x <- forAll gen_unsigned'+  y <- forAll gen_unsigned'+  z <- forAll gen_unsigned'++  assert $ Prop.annihilative_multiplication x+  assert $ Prop.neutral_addition' x+  assert $ Prop.neutral_multiplication' x+  assert $ Prop.associative_addition x y z+  assert $ Prop.associative_multiplication x y z+  assert $ Prop.distributive x y z++prop_quantale_unsigned :: Property+prop_quantale_unsigned = withTests 1000 . withShrinks 0 $ property $ do+  x <- forAll gen_unsigned -- we do not require `residr pInf` etc+  y <- forAll gen_unsigned'+  z <- forAll gen_unsigned'++  --assert $ Prop.connection (residl x) y z+  assert $ Prop.connection (residr x) y z++  --assert $ Prop.monotone' (residl x) y z+  assert $ Prop.monotone' (residr x) y z++  --assert $ Prop.monotone (residl x) y z+  assert $ Prop.monotone (residr x) y z++  --assert $ Prop.closed (residl x) y+  assert $ Prop.closed (residr x) y++  --assert $ Prop.kernel (residl x) y+  assert $ Prop.kernel (residr x) y++  assert $ residuated x y z+++f32ugn :: Conn Float Unsigned+f32ugn = Conn f g where+  f x | finite x  = Unsigned $ max 0 $ x+      | otherwise = Unsigned x+  g (Unsigned x) = x++mono f x y = x <~ y ==> f x <~ f y++{-+u = Unsigned+f = id :: Float -> Float++x = u 2.3380933+y = u 6.049403++x = u 0.37794903+y = u 0.3269925++x = f 2.3380933+y = f 6.049403++x = f 0.37794903+y = f 0.3269925++counit (residl x) y+++residl x = Conn (<>x) . (//x) $ y++(//x) . (<>x) $ y++x = u 1+shift' n (Unsigned x) = Unsigned $ shift n x+xs = flip shift' x <$> [-4,-3,-2,-1,0,1,2,3,4]+fmap (cvn x) xs+y = shift' 2 x+z = shift' 4 x+Prop.transitive_eq x y z+++fmap (cvn x) xs+λ> fmap (Prop.semiconnex x) xs+[True,True,False,False,True,False,False,True,True]+λ> fmap (<~ x) xs+[True,True,False,False,True,False,False,False,False]+λ> fmap (~~ x) xs+[False,False,True,True,True,True,True,False,False]+-}++{-+prop_connection_flt32_unsigned :: Property+prop_connection_flt32_unsigned = withTests 1000 $ property $ do+  x <- forAll gen_flt32+  y <- forAll gen_unsigned+  x' <- forAll gen_flt32+  y' <- forAll gen_unsigned++  assert $ Prop.connection f32ugn x y+  assert $ Prop.monotone' f32ugn x x'+  assert $ mono (connr f32ugn) y y'+  assert $ Prop.closed f32ugn x+  assert $ Prop.kernel f32ugn y +-}++{-+prop_connection_unsigned_signed :: Property+prop_connection_unsigned_signed = withTests 10000 $ property $ do+  x <- forAll gen_unsigned+  y <- forAll gen_signed+  x' <- forAll gen_unsigned+  y' <- forAll gen_signed++  assert $ Prop.connection ugnsgn x y+  assert $ Prop.monotone' ugnsgn x x'+  assert $ Prop.monotone  ugnsgn y y'+  assert $ Prop.closed ugnsgn x+  assert $ Prop.kernel ugnsgn y +-}+++tests :: IO Bool+tests = checkParallel $$(discover)
+ test/test.hs view
@@ -0,0 +1,17 @@+import Control.Monad+import System.Exit (exitFailure)+import System.IO (BufferMode(..), hSetBuffering, stdout, stderr)++import qualified Test.Data.Number.Tropical as NT++tests :: IO [Bool]+tests = sequence [NT.tests]++main :: IO ()+main = do+  hSetBuffering stdout LineBuffering+  hSetBuffering stderr LineBuffering++  results <- tests++  unless (and results) exitFailure