connections 0.0.1 → 0.0.2

raw patch · 12 files changed

+62/−1018 lines, 12 filesdep +connectionsdep −ordersdep −ringsdep ~basePVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: connections

Dependencies removed: orders, rings

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• connections.cabal +5/−11
• src/Data/Connection.hs +1/−1
• src/Data/Connection/Float.hs +3/−1
• src/Data/Connection/Yoneda.hs +10/−1
• src/Data/Dioid/Interval.hs +0/−116
• src/Data/Dioid/Property.hs +0/−408
• src/Data/Dioid/Signed.hs +0/−195
• src/Data/Prd/Lattice.hs +1/−0
• src/Data/Prd/Nan.hs +42/−0
• src/Data/Prd/Property.hs +0/−1
• src/Data/Semigroup/Quantale.hs +0/−78
• test/Test/Data/Dioid/Signed.hs +0/−206

@@ -1,7 +1,7 @@ name:                connections-version:             0.0.1-description:         partial orders-synopsis:            Partial orders, Galois connections, ordered semirings, & residuated lattices.+version:             0.0.2+synopsis:            Partial orders & Galois connections.+description:         A library for precision rounding using Galois connections. homepage:            https://github.com/cmk/connections license:             BSD3 license-file:        LICENSE@@ -18,10 +18,6 @@     , Data.Prd.Property     , Data.Prd.Lattice     , Data.Prd.Nan-    , Data.Dioid.Property-    , Data.Dioid.Interval-    , Data.Dioid.Signed-    , Data.Semigroup.Quantale     , Data.Connection     , Data.Connection.Property     , Data.Connection.Word@@ -31,9 +27,8 @@     , Data.Float    build-depends:       -      base           >= 4.8   && < 5.0+      base           >= 4.10  && < 5.0     , containers     >= 0.4.0 && < 0.7-    , rings          >= 0.0.1 && < 1.0     , semigroupoids  == 5.*     , property       >= 0.0.1 && < 1.0 @@ -50,12 +45,11 @@   type: exitcode-stdio-1.0   other-modules:       Test.Data.Float-    , Test.Data.Dioid.Signed     , Test.Data.Connection.Int     , Test.Data.Connection.Word   build-depends:              base == 4.*-    , orders -any +    , connections -any      , hedgehog     , property   default-extensions:

@@ -128,7 +128,7 @@ ---------------------------------------------------------------------  dual :: Prd a => Prd b => Conn a b -> Conn (Down b) (Down a)-dual (Conn f g) = Conn (fmap g) (fmap f)+dual (Conn f g) = Conn (\(Down b) -> Down $ g b) (\(Down a) -> Down $ f a)  (***) :: Prd a => Prd b => Prd c => Prd d => Conn a b -> Conn c d -> Conn (a, c) (b, d) (***) (Conn ab ba) (Conn cd dc) = Conn f g where

@@ -134,9 +134,11 @@ floatInt32 :: Float -> Int32 floatInt32 = signed32 . floatWord32  +-- Bit-for-bit conversion. word32Float :: Word32 -> Float word32Float = F.castWord32ToFloat --- force to positive representation?+-- TODO force to positive representation?+-- Bit-for-bit conversion. floatWord32 :: Float -> Word32 floatWord32 = (+0) .  F.castFloatToWord32

@@ -12,7 +12,6 @@ import Data.Prd.Nan import Data.Prd.Lattice import Data.Bifunctor-import Data.Dioid.Interval import Data.Function import Data.Functor.Identity import Data.Functor.Product@@ -86,3 +85,13 @@     lower = (>~)     filter = C.id     upper = (<~)++{-++incBy :: Yoneda a => Quantale (Rep a) => Rep a -> a -> a+incBy x = connl filter . (x<>) . connr filter++decBy :: Yoneda a => Quantale (Rep a) => Rep a -> a -> a+decBy x = connl filter . (x\\) . connr filter++-}

@@ -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 #-}

@@ -1,408 +0,0 @@-{-# 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

@@ -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

@@ -13,6 +13,7 @@ import Data.Monoid hiding (First, Last) import Data.Ord import Data.Prd+import Data.Semigroup (Semigroup(..)) import Data.Semigroup.Foldable import Data.Set (Set) import Data.Word (Word, Word8, Word16, Word32, Word64)

@@ -108,4 +108,46 @@ def conn = Conn f g where    Conn f' g' = _R conn   f = eitherNan . f' . nanEither ()+  g = eitherNan . g' . nanEither ()++{-+floatOrdering :: Trip Float (Nan Ordering)+floatOrdering = Trip f g h where+  h x | isNan x = NaN+  h x | posinf x = Def GT+  h x | finite x && x >~ 0 = Def EQ+  h x | otherwise = Def LT++  g (Def GT) = maxBound+  g (Def LT) = minBound+  g (Def EQ) = 0+  g NaN = aNan+  +  f x | isNan x = NaN+  f x | neginf x = Def LT+  f x | finite x && x <~ 0 = Def EQ+  f x | otherwise = Def GT+++_Def' :: Prd a => Prd b => Trip a b -> Trip (Nan a) (Nan b)+_Def' trip = Trip f g h where +  Trip f' g' h' = _R' trip+  f = eitherNan . f' . nanEither ()   g = eitherNan . g' . nanEither () +  h = eitherNan . h' . nanEither () +++instance Semigroup a => Semigroup (Nan a) where+instance Semiring a => Semiring (Nan a) where+instance Semifield a => Semifield (Nan a) where++instance Group a => Group (Nan a) where+instance Ring a => Ring (Nan a) where++instance Field a => Field (Nan a) where++u + NaN = NaN + u = NaN − NaN = NaN+u · NaN = NaN · u = NaN NaN−1 = NaN+NaN  u ⇔ u = NaN u  NaN ⇔ u = NaN+-}+

@@ -27,7 +27,6 @@  import Data.Prd import Data.Prd.Lattice-import Data.Semiring import Test.Property.Util import Prelude hiding (Ord(..)) 

@@ -1,78 +0,0 @@-module Data.Semigroup.Quantale where--import Data.Connection hiding (floor', ceiling')-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)-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--{---In the interest of usability we abuse terminology slightly and use '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.---distributive_cross as bs = maybe True (~~ cross as bs) $ pjoin as <> pjoin bs-  where cross = join (liftA2 (<>) a b)----lattice version-distributive_cross' as bs = cross as bs ~~ join as <> join bs-  where -        cross = join (liftA2 (<>) a b)--join as \\ b ~~ meet (fmap (\\b) as)--a \\ meet bs ~~ meet (fmap (a\\) bs)--ideal_residuated :: (Quantale a, Ideal a, Functor (Rep a)) => a -> a -> Bool-ideal_residuated x y = x \\ y =~ join (fmap (x<>) (connl ideal $ y))--ideal_residuated' :: (Quantale a, Ideal a, Functor (Rep a)) => a -> a -> Bool-ideal_residuated' x y = x // y =~ join (fmap (<>x) (connl ideal $ y))--x \/ y = (x // y) <> y -- unit (minus_plus x) y -- (y // x) + x-x /\ y = x <> (x \\ y) -- (y + x) // x -- x \\ (x + y) --minimal \\ x =~ maximal =~ x \\ maximal-mempty \\ x ~~ unit- --}--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' 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 z g y = while (\x -> g x <~ y) le (shift 1) z

@@ -1,206 +0,0 @@-{-# 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)