diff --git a/connections.cabal b/connections.cabal --- a/connections.cabal +++ b/connections.cabal @@ -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: diff --git a/src/Data/Connection.hs b/src/Data/Connection.hs --- a/src/Data/Connection.hs +++ b/src/Data/Connection.hs @@ -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 diff --git a/src/Data/Connection/Float.hs b/src/Data/Connection/Float.hs --- a/src/Data/Connection/Float.hs +++ b/src/Data/Connection/Float.hs @@ -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 diff --git a/src/Data/Connection/Yoneda.hs b/src/Data/Connection/Yoneda.hs --- a/src/Data/Connection/Yoneda.hs +++ b/src/Data/Connection/Yoneda.hs @@ -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 + +-} diff --git a/src/Data/Dioid/Interval.hs b/src/Data/Dioid/Interval.hs deleted file mode 100644 --- a/src/Data/Dioid/Interval.hs +++ /dev/null @@ -1,116 +0,0 @@ --- | -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 #-} diff --git a/src/Data/Dioid/Property.hs b/src/Data/Dioid/Property.hs deleted file mode 100644 --- a/src/Data/Dioid/Property.hs +++ /dev/null @@ -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 diff --git a/src/Data/Dioid/Signed.hs b/src/Data/Dioid/Signed.hs deleted file mode 100644 --- a/src/Data/Dioid/Signed.hs +++ /dev/null @@ -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 diff --git a/src/Data/Prd/Lattice.hs b/src/Data/Prd/Lattice.hs --- a/src/Data/Prd/Lattice.hs +++ b/src/Data/Prd/Lattice.hs @@ -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) diff --git a/src/Data/Prd/Nan.hs b/src/Data/Prd/Nan.hs --- a/src/Data/Prd/Nan.hs +++ b/src/Data/Prd/Nan.hs @@ -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 +-} + diff --git a/src/Data/Prd/Property.hs b/src/Data/Prd/Property.hs --- a/src/Data/Prd/Property.hs +++ b/src/Data/Prd/Property.hs @@ -27,7 +27,6 @@ import Data.Prd import Data.Prd.Lattice -import Data.Semiring import Test.Property.Util import Prelude hiding (Ord(..)) diff --git a/src/Data/Semigroup/Quantale.hs b/src/Data/Semigroup/Quantale.hs deleted file mode 100644 --- a/src/Data/Semigroup/Quantale.hs +++ /dev/null @@ -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 diff --git a/test/Test/Data/Dioid/Signed.hs b/test/Test/Data/Dioid/Signed.hs deleted file mode 100644 --- a/test/Test/Data/Dioid/Signed.hs +++ /dev/null @@ -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)