connections 0.2.0 → 0.3.0

raw patch · 16 files changed

+1562/−1000 lines, 16 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• connections.cabal +6/−4
• src/Data/Connection/Class.hs +175/−210
• src/Data/Connection/Conn.hs +368/−337
• src/Data/Connection/Fixed.hs +152/−0
• src/Data/Connection/Float.hs +170/−112
• src/Data/Connection/Int.hs +31/−30
• src/Data/Connection/Property.hs +78/−57
• src/Data/Connection/Ratio.hs +76/−58
• src/Data/Lattice.hs +12/−13
• src/Data/Order.hs +15/−1
• test/Test/Data/Connection.hs +7/−4
• test/Test/Data/Connection/Fixed.hs +153/−0
• test/Test/Data/Connection/Float.hs +153/−58
• test/Test/Data/Connection/Ratio.hs +160/−112
• test/Test/Data/Order.hs +4/−4
• test/test.hs +2/−0

@@ -1,7 +1,7 @@ name:                connections-version:             0.2.0+version:             0.3.0 synopsis:            Orders, Galois connections, and lattices.-description:         A library for order manipulation using Galois connections.+description:         A library for order manipulation using Galois connections. See the README for a brief overview. homepage:            https://github.com/cmk/connections license:             BSD3 license-file:        LICENSE@@ -22,10 +22,11 @@       Data.Connection     , Data.Connection.Conn     , Data.Connection.Class+    , Data.Connection.Fixed+    , Data.Connection.Float     , Data.Connection.Int-    , Data.Connection.Word     , Data.Connection.Ratio-    , Data.Connection.Float+    , Data.Connection.Word     , Data.Connection.Property      , Data.Lattice@@ -49,6 +50,7 @@     , Test.Data.Connection     , Test.Data.Connection.Int     , Test.Data.Connection.Word+    , Test.Data.Connection.Fixed     , Test.Data.Connection.Float     , Test.Data.Connection.Ratio   build-depends:       

@@ -2,6 +2,7 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE KindSignatures #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE RankNTypes #-}@@ -11,71 +12,36 @@ {-# LANGUAGE ViewPatterns #-}  module Data.Connection.Class (-    -- * Conn-    Conn (),-    identity,--    -- * Connection k+    -- * Types+    Left,+    left,+    Right,+    right,     Triple,-    pattern Conn,-    ConnK,-    embed,-    extremal,++    -- * Lattices+    (\/),+    (/\),     lub,     glb,-    half,-    midpoint,-    range,-    round,-    round1,-    round2,-    truncate,-    truncate1,-    truncate2,--    -- * Connection L-    Left,-    pattern ConnL,-    ConnL,-    connL,-    embedL,+    choose,+    divide,     minimal,-    join,-    ceiling,-    ceiling1,-    ceiling2,--    -- * Connection R-    Right,-    pattern ConnR,-    ConnR,-    connR,-    embedR,     maximal,-    meet,-    floor,-    floor1,-    floor2,--    -- * Combinators-    (>>>),-    (<<<),-    (/|\),-    (\|/),-    choice,-    strong,+    extremal,      -- * Connection-    Kan (..),+    Connection (..),++    -- ** RebindableSyntax     ConnInteger,     ConnRational,-    ConnExtended,-    Connection (..), ) where  import safe Control.Category ((>>>)) import safe Data.Bool (bool) import safe Data.Connection.Conn+import safe Data.Connection.Fixed import safe Data.Connection.Float import safe Data.Connection.Int import safe Data.Connection.Ratio@@ -102,8 +68,18 @@  type Left = Connection 'L +-- | A specialization of /conn/ to left-side connections.+--+left :: Left a b => ConnL a b+left = conn @ 'L+ type Right = Connection 'R +-- | A specialization of /conn/ to right-side connections.+--+right :: Right a b => ConnR a b+right = conn @ 'R+ -- | A constraint kind representing an <https://ncatlab.org/nlab/show/adjoint+triple adjoint triple> of Galois connections. type Triple a b = (Left a b, Right a b) @@ -111,18 +87,16 @@ -- --  Usable in conjunction with /RebindableSyntax/: -----  > fromInteger = embedL . Just :: ConnInteger a => Integer -> a+--  > fromInteger = upper conn . Just :: ConnInteger a => Integer -> a type ConnInteger a = Left a (Maybe Integer)  -- | A constraint kind for 'Rational' conversions. -- -- Usable in conjunction with /RebindableSyntax/: -----  > fromRational = round :: ConnRational a => Rational -> a+--  > fromRational = round conn :: ConnRational a => Rational -> a type ConnRational a = Triple Rational a -type ConnExtended a b = Triple a (Extended b)- -- | An < https://ncatlab.org/nlab/show/adjoint+string adjoint string > of Galois connections of length 2 or 3. class (Preorder a, Preorder b) => Connection k a b where     -- |@@ -133,64 +107,7 @@     -- (3.1415925,3.1415927)     conn :: Conn k a b -infixr 3 \|/---- | A preorder variant of 'Control.Arrow.|||'.-(\|/) :: Conn k c a -> Conn k c b -> Conn k c (Either a b)-f \|/ g = Conn Left (either id id) Right >>> f `choice` g--infixr 4 /|\---- | A preorder variant of 'Control.Arrow.&&&'.-(/|\) :: Connection k (c, c) c => Conn k a c -> Conn k b c -> Conn k (a, b) c-f /|\ g = f `strong` g >>> conn-------------------------------------------------------------------------- Connection k-------------------------------------------------------------------------- | The canonical connections against a 'Bool'.-extremal :: Triple () a => Conn k a Bool-extremal = Conn f g h-  where-    g False = minimal-    g True = maximal--    f i-        | i ~~ minimal = False-        | otherwise = True--    h i-        | i ~~ maximal = True-        | otherwise = False---- | Least upper bound operator.------ The order dual of 'glb'.------ >>> lub 1.0 9.0 7.0--- 7.0--- >>> lub 1.0 9.0 (0.0 / 0.0)--- 1.0-lub :: Triple (a, a) a => a -> a -> a -> a-lub x y z = (x `meet` y) `join` (y `meet` z) `join` (z `meet` x)---- | Greatest lower bound operator.------ > glb x x y = x--- > glb x y z = glb z x y--- > glb x y z = glb x z y--- > glb (glb x w y) w z = glb x w (glb y w z)------ >>> glb 1.0 9.0 7.0--- 7.0--- >>> glb 1.0 9.0 (0.0 / 0.0)--- 9.0--- >>> glb (fromList [1..3]) (fromList [3..5]) (fromList [5..7]) :: Set Int--- fromList [3,5]-glb :: Triple (a, a) a => a -> a -> a -> a-glb x y z = (x `join` y) `meet` (y `join` z) `meet` (z `join` x)-+{- -- | Return the nearest value to x. -- -- > round @a @a = id@@ -205,8 +122,8 @@     Just LT -> floor x     _ -> truncate x   where-    halfR = x - lower (connR @a @b) x -- dist from lower bound-    halfL = upper (connL @a @b) x - x -- dist from upper bound+    halfR = x - right (connR @a @b) x -- dist from lower bound+    halfL = left (connL @a @b) x - x -- dist from upper bound  -- | Lift a unary function over a 'Conn'. --@@ -255,112 +172,103 @@ truncate2 :: (Num a, Triple a b) => (a -> a -> a) -> b -> b -> b truncate2 f x y = truncate $ f (g x) (g y) where Conn _ g _ = connL {-# INLINE truncate2 #-}+-}  ------------------------------------------------------------------------ Connection L+-- Lattices --------------------------------------------------------------------- --- | A specialization of /conn/ to left-side connections.------ This is a convenience function provided primarily to avoid needing--- to enable /DataKinds/.-connL :: Left a b => ConnL a b-connL = conn @ 'L---- | Extract the center of a 'Conn' or upper half of a 'ConnL'.-embedL :: Left a b => b -> a-embedL = embed connL+infixr 5 \/ --- | A minimal element of a preorder.------ 'minimal' needn't be unique, but it must obey:+-- | Lattice join. ----- > x <~ minimal => x ~~ minimal-minimal :: Left () a => a-minimal = ceiling ()+-- > (\/) = curry $ lower semilattice+(\/) :: Left (a, a) a => a -> a -> a+(\/) = join conn -infixr 5 `join`+infixr 6 /\ -- comment for the parser --- | Semigroup operation on a join-lattice.-join :: Left (a, a) a => a -> a -> a-join = curry ceiling+-- | Lattice meet.+--+-- > (/\) = curry $ floor semilattice+(/\) :: Right (a, a) a => a -> a -> a+(/\) = meet conn --- | Extract the ceiling of a 'Conn' or lower half of a 'ConnL'.+-- | Least upper bound operator. ----- > ceiling @a @a = id--- > ceiling (x1 `join` a2) = ceiling x1 `join` ceiling x2+-- The order dual of 'glb'. ----- The latter law is the adjoint functor theorem for preorders.+-- >>> lub 1.0 9.0 7.0+-- 7.0+-- >>> lub 1.0 9.0 (0.0 / 0.0)+-- 1.0+lub :: Triple (a, a) a => a -> a -> a -> a+lub x y z = x /\ y \/ y /\ z \/ z /\ x++-- | Greatest lower bound operator. ----- >>> Data.Connection.ceiling @Rational @Float (0 :% 0)--- NaN--- >>> Data.Connection.ceiling @Rational @Float (1 :% 0)--- Infinity--- >>> Data.Connection.ceiling @Rational @Float (13 :% 10)--- 1.3000001-ceiling :: Left a b => a -> b-ceiling = ceilingWith conn+-- > glb x x y = x+-- > glb x y z = glb z x y+-- > glb x y z = glb x z y+-- > glb (glb x w y) w z = glb x w (glb y w z)+--+-- >>> glb 1.0 9.0 7.0+-- 7.0+-- >>> glb 1.0 9.0 (0.0 / 0.0)+-- 9.0+-- >>> glb (fromList [1..3]) (fromList [3..5]) (fromList [5..7]) :: Set Int+-- fromList [3,5]+glb :: Triple (a, a) a => a -> a -> a -> a+glb x y z = (x \/ y) /\ (y \/ z) /\ (z \/ x) --- | Lift a unary function over a 'ConnL'.-ceiling1 :: Left a b => (a -> a) -> b -> b-ceiling1 = ceilingWith1 conn+infixr 3 `choose` --- | Lift a binary function over a 'ConnL'.-ceiling2 :: Left a b => (a -> a -> a) -> b -> b -> b-ceiling2 = ceilingWith2 conn+-- | A preorder variant of 'Control.Arrow.|||'.+choose :: Conn k c a -> Conn k c b -> Conn k c (Either a b)+choose f g = Conn Left (either id id) Right >>> f `choice` g ------------------------------------------------------------------------- Connection R----------------------------------------------------------------------+infixr 4 `divide` --- | A specialization of /conn/ to right-side connections.------ This is a convenience function provided primarily to avoid needing--- to enable /DataKinds/.-connR :: Right a b => ConnR a b-connR = conn @ 'R+-- | A preorder variant of 'Control.Arrow.&&&'.+divide :: Connection k (c, c) c => Conn k a c -> Conn k b c -> Conn k (a, b) c+divide f g = f `strong` g >>> conn --- | Extract the center of a 'ConnK' or lower half of a 'ConnR'.-embedR :: Right a b => b -> a-embedR = embed connR+-- | A minimal element of a preorder.+--+-- > x /\ minimal = minimal+-- > x \/ minimal = x+--+-- 'minimal' needn't be unique, but it must obey:+--+-- > x <~ minimal => x ~~ minimal+minimal :: Left () a => a+minimal = ceiling conn ()  -- | A maximal element of a preorder. --+-- > x /\ maximal = x+-- > x \/ maximal = maximal+-- -- 'maximal' needn't be unique, but it must obey: -- -- > x >~ maximal => x ~~ maximal maximal :: Right () a => a-maximal = floor ()--infixr 6 `meet`---- | Semigroup operation on a meet-lattice.-meet :: Right (a, a) a => a -> a -> a-meet = curry floor+maximal = floor conn () --- | Extract the floor of a 'ConnK' or upper half of a 'ConnL'.------ > floor @a @a = id--- > floor (x1 `meet` x2) = floor x1 `meet` floor x2------ The latter law is the adjoint functor theorem for preorders.------ >>> Data.Connection.floor @Rational @Float (0 :% 0)--- NaN--- >>> Data.Connection.floor @Rational @Float (1 :% 0)--- Infinity--- >>> Data.Connection.floor @Rational @Float (13 :% 10)--- 1.3-floor :: Right a b => a -> b-floor = floorWith conn+-- | The canonical connection with a 'Bool'.+extremal :: Triple () a => Conn k a Bool+extremal = Conn f g h+  where+    g False = minimal+    g True = maximal --- | Lift a unary function over a 'ConnR'.-floor1 :: Right a b => (a -> a) -> b -> b-floor1 = floorWith1 conn+    f i+        | i ~~ minimal = False+        | otherwise = True --- | Lift a binary function over a 'ConnR'.-floor2 :: Right a b => (a -> a -> a) -> b -> b -> b-floor2 = floorWith2 conn+    h i+        | i ~~ maximal = True+        | otherwise = False  --------------------------------------------------------------------- -- Instances@@ -466,6 +374,35 @@     conn = Conn (const $ -1 :% 0) (const ()) (const $ 1 :% 0) instance Connection k (Rational, Rational) Rational where conn = latticeN5 +instance Connection k Deci Uni where conn = f01f00+instance Connection k Centi Uni where conn = f02f00+instance Connection k Milli Uni where conn = f03f00+instance Connection k Micro Uni where conn = f06f00+instance Connection k Nano Uni where conn = f09f00+instance Connection k Pico Uni where conn = f12f00++instance Connection k Centi Deci where conn = f02f01+instance Connection k Milli Deci where conn = f03f01+instance Connection k Micro Deci where conn = f06f01+instance Connection k Nano Deci where conn = f09f01+instance Connection k Pico Deci where conn = f12f01++instance Connection k Milli Centi where conn = f03f02+instance Connection k Micro Centi where conn = f06f02+instance Connection k Nano Centi where conn = f09f02+instance Connection k Pico Centi where conn = f12f02++instance Connection k Micro Milli where conn = f06f03+instance Connection k Nano Milli where conn = f09f03+instance Connection k Pico Milli where conn = f12f03++instance Connection k Nano Micro where conn = f09f06+instance Connection k Pico Micro where conn = f12f06++instance Connection k Pico Nano where conn = f12f09++instance Connection k (Fixed e, Fixed e) (Fixed e) where conn = latticeOrd+ instance Connection k () Float where conn = extremalN5 instance Connection k Double Float where conn = f64f32 instance Connection k Rational Float where conn = ratf32@@ -510,28 +447,51 @@ instance Connection 'L Int32 (Maybe Integer) where conn = i32int instance Connection 'L Int64 (Maybe Integer) where conn = i64int instance Connection 'L Int (Maybe Integer) where conn = ixxint--{- instance Connection 'L Integer (Maybe Integer) where-  -- | Provided as a shim for /RebindableSyntax/.-  -- Note that this instance will clip negative numbers to zero.-conn = swapR $ intnat >>> natint--}+    conn = c1 >>> intnat >>> natint >>> c2+      where+        c1 = Conn shiftR shiftL shiftR+        c2 = Conn (fmap shiftL) (fmap shiftR) (fmap shiftL) +        shiftR x = x + m+        shiftL x = x - m+        m = 9223372036854775808+ instance Connection k Rational (Extended Int8) where conn = rati08 instance Connection k Rational (Extended Int16) where conn = rati16 instance Connection k Rational (Extended Int32) where conn = rati32 instance Connection k Rational (Extended Int64) where conn = rati64 instance Connection k Rational (Extended Int) where conn = ratixx instance Connection k Rational (Extended Integer) where conn = ratint+instance HasResolution prec => Connection k Rational (Extended (Fixed prec)) where conn = ratfix --- | All 'Data.Int.Int08' values are exactly representable in a 'Float'.+instance Connection 'L Float (Extended Word8) where conn = f32i08 >>> mapped i08w08+instance Connection 'L Float (Extended Word16) where conn = f32i16 >>> mapped i16w16+instance Connection 'L Float (Extended Word32) where conn = f32i32 >>> mapped i32w32+instance Connection 'L Float (Extended Word64) where conn = f32i64 >>> mapped i64w64+instance Connection 'L Float (Extended Word) where conn = f32ixx >>> mapped ixxwxx+instance Connection 'L Float (Extended Natural) where conn = f32int >>> mapped intnat++-- | All 'Data.Int.Int8' values are exactly representable in a 'Float'. instance Connection k Float (Extended Int8) where conn = f32i08  -- | All 'Data.Int.Int16' values are exactly representable in a 'Float'. instance Connection k Float (Extended Int16) where conn = f32i16 --- | All 'Data.Int.Int08' values are exactly representable in a 'Double'.+instance Connection 'L Float (Extended Int32) where conn = f32i32+instance Connection 'L Float (Extended Int64) where conn = f32i64+instance Connection 'L Float (Extended Int) where conn = f32ixx+instance Connection 'L Float (Extended Integer) where conn = f32int+instance HasResolution res => Connection 'L Float (Extended (Fixed res)) where conn = connL ratf32 >>> ratfix++instance Connection 'L Double (Extended Word8) where conn = f64i08 >>> mapped i08w08+instance Connection 'L Double (Extended Word16) where conn = f64i16 >>> mapped i16w16+instance Connection 'L Double (Extended Word32) where conn = f64i32 >>> mapped i32w32+instance Connection 'L Double (Extended Word64) where conn = f64i64 >>> mapped i64w64+instance Connection 'L Double (Extended Word) where conn = f64ixx >>> mapped ixxwxx+instance Connection 'L Double (Extended Natural) where conn = f64int >>> mapped intnat++-- | All 'Data.Int.Int8' values are exactly representable in a 'Double'. instance Connection k Double (Extended Int8) where conn = f64i08  -- | All 'Data.Int.Int16' values are exactly representable in a 'Double'.@@ -540,6 +500,11 @@ -- | All 'Data.Int.Int32' values are exactly representable in a 'Double'. instance Connection k Double (Extended Int32) where conn = f64i32 +instance Connection 'L Double (Extended Int64) where conn = f64i64+instance Connection 'L Double (Extended Int) where conn = f64ixx+instance Connection 'L Double (Extended Integer) where conn = f64int+instance HasResolution res => Connection 'L Double (Extended (Fixed res)) where conn = connL ratf64 >>> ratfix+ instance Connection k a b => Connection k (Identity a) b where     conn = Conn runIdentity Identity runIdentity >>> conn @@ -586,19 +551,19 @@     conn = ConnL (const Map.empty) (const ())  instance (Total a, Left (b, b) b) => Connection 'L (Map.Map a b, Map.Map a b) (Map.Map a b) where-    conn = ConnL (uncurry $ Map.unionWith join) fork+    conn = ConnL (uncurry $ Map.unionWith (join conn)) fork  instance (Total a, Right (b, b) b) => Connection 'R (Map.Map a b, Map.Map a b) (Map.Map a b) where-    conn = ConnR fork (uncurry $ Map.intersectionWith meet)+    conn = ConnR fork (uncurry $ Map.intersectionWith (meet conn))  instance Preorder a => Connection 'L () (IntMap.IntMap a) where     conn = ConnL (const IntMap.empty) (const ())  instance Left (a, a) a => Connection 'L (IntMap.IntMap a, IntMap.IntMap a) (IntMap.IntMap a) where-    conn = ConnL (uncurry $ IntMap.unionWith join) fork+    conn = ConnL (uncurry $ IntMap.unionWith (join conn)) fork  instance Right (a, a) a => Connection 'R (IntMap.IntMap a, IntMap.IntMap a) (IntMap.IntMap a) where-    conn = ConnR fork (uncurry $ IntMap.intersectionWith meet)+    conn = ConnR fork (uncurry $ IntMap.intersectionWith (meet conn))  -- Internal @@ -666,7 +631,7 @@ joinMaybe _ u@(Just _) = u joinMaybe Nothing Nothing = Nothing -meetMaybe :: Connection 'R (a, a) a => Maybe a -> Maybe a -> Maybe a+meetMaybe :: Right (a, a) a => Maybe a -> Maybe a -> Maybe a meetMaybe Nothing Nothing = Nothing meetMaybe Nothing _ = Nothing meetMaybe _ Nothing = Nothing@@ -679,7 +644,7 @@ joinExtended Bottom       y            = y joinExtended x            Bottom       = x -meetExtended :: Connection 'R (a, a) a => Extended a -> Extended a -> Extended a+meetExtended :: Right (a, a) a => Extended a -> Extended a -> Extended a meetExtended Top          y            = y meetExtended x            Top          = x meetExtended (Extended x) (Extended y) = Extended (x `meet` y)@@ -692,7 +657,7 @@ joinEither _ u@(Right _) = u joinEither (Left x) (Left y) = Left (x `join` y) -meetEither :: (Connection 'R (a, a) a, Connection 'R (b, b) b) => Either a b -> Either a b -> Either a b+meetEither :: (Right (a, a) a, Right (b, b) b) => Either a b -> Either a b -> Either a b meetEither (Left x) (Left y) = Left (x `meet` y) meetEither l@(Left _) _ = l meetEither _ l@(Left _) = l@@ -701,6 +666,6 @@ joinTuple :: (Connection 'L (a, a) a, Connection 'L (b, b) b) => (a, b) -> (a, b) -> (a, b) joinTuple (x1, y1) (x2, y2) = (x1 `join` x2, y1 `join` y2) -meetTuple :: (Connection 'R (a, a) a, Connection 'R (b, b) b) => (a, b) -> (a, b) -> (a, b)+meetTuple :: (Right (a, a) a, Right (b, b) b) => (a, b) -> (a, b) -> (a, b) meetTuple (x1, y1) (x2, y2) = (x1 `meet` x2, y1 `meet` y2) -}

@@ -14,65 +14,66 @@     -- * Conn     Kan (..),     Conn (),-    pattern Conn,     embed,     range,     identity,--    -- * Connection k-    ConnK,-    half,-    midpoint,-    roundWith,-    roundWith1,-    roundWith2,-    truncateWith,-    truncateWith1,-    truncateWith2,+    (>>>),+    (<<<),+    mapped,+    choice,+    strong,      -- * Connection L     ConnL,     pattern ConnL,-    upL,-    downL,-    swapL,-    counit,+    connL,     upper,     upper1,     upper2,-    filterWith,-    ceilingWith,-    ceilingWith1,-    ceilingWith2,+    join,+    ceiling,+    ceiling1,+    ceiling2,      -- * Connection R     ConnR,     pattern ConnR,-    upR,-    downR,-    swapR,-    unit,+    connR,     lower,     lower1,     lower2,-    idealWith,-    floorWith,-    floorWith1,-    floorWith2,+    meet,+    floor,+    floor1,+    floor2, -    -- * Combinators-    (>>>),-    (<<<),-    choice,-    strong,+    -- * Connection k+    pattern Conn,+    half,+    midpoint,+    round,+    round1,+    round2,+    truncate,+    truncate1,+    truncate2,++    -- * Down+    upL,+    upR,+    downL,+    downR,+    filterL,+    filterR,+    Down (..), ) where -import safe Control.Arrow+import safe Control.Arrow ((&&&)) import safe Control.Category (Category, (<<<), (>>>)) import safe qualified Control.Category as C import safe Data.Bifunctor (bimap) import safe Data.Order-import safe Prelude hiding (Ord (..))+import safe Prelude hiding (Ord (..), ceiling, floor, round, truncate)  -- $setup -- >>> :set -XTypeApplications@@ -85,322 +86,411 @@  -- | A data kind distinguishing the directionality of a Galois connection: ----- * /L/-tagged types are low / increasing (e.g. 'Data.Connection.Class.minimal', 'Data.Connection.Class.upper', 'Data.Connection.Class.ceiling', 'Data.Connection.Class.join')+-- * /L/-tagged types are low / increasing (e.g. 'Data.Connection.Class.minimal', 'Data.Connection.Class.ceiling', 'Data.Connection.Class.join') ----- * /R/-tagged types are high / decreasing (e.g. 'Data.Connection.Class.maximal', 'Data.Connection.Class.lower', 'Data.Connection.Class.floor', 'Data.Connection.Class.meet')+-- * /R/-tagged types are high / decreasing (e.g. 'Data.Connection.Class.maximal', 'Data.Connection.Class.floor', 'Data.Connection.Class.meet') data Kan = L | R --- | An < https://ncatlab.org/nlab/show/adjoint+string adjoint string > of Galois connections of length 2 or 3.+-- | A (chain of) Galois connections. --+-- A [Galois connection](https://en.wikipedia.org/wiki/Galois_connection) between preorders P and Q+-- is a pair of monotone maps `f :: p -> q` and `g :: q -> p` such that:+--+-- > f x <= y iff x <= g y+--+-- We say that `f` is the left or right adjoint, and `g` is the right or left adjoint of the connection.+-- -- Connections have many nice properties wrt numerical conversion: -- -- >>> range (conn @_ @Rational @Float) (1 :% 8) -- eighths are exactly representable in a float -- (0.125,0.125) -- >>> range (conn @_ @Rational @Float) (1 :% 7) -- sevenths are not -- (0.14285713,0.14285715)-data Conn (k :: Kan) a b = Galois (a -> (b, b)) (b -> a)+--+-- See the /README/ file for a slightly more in-depth introduction.+data Conn (k :: Kan) a b = Conn_ (a -> (b, b)) (b -> a)  instance Category (Conn k) where     id = identity     {-# INLINE id #-} -    Galois f1 g1 . Galois f2 g2 = Galois ((fst . f1) . (fst . f2) &&& (snd . f1) . (snd . f2)) (g2 . g1)+    Conn_ f1 g1 . Conn_ f2 g2 = Conn_ ((fst . f1) . (fst . f2) &&& (snd . f1) . (snd . f2)) (g2 . g1)     {-# INLINE (.) #-} --- | Obtain a /Conn/ from an adjoint triple of monotone functions.------  This is a view pattern for an arbitrary 'Conn'. When applied to a 'ConnL'---  or 'ConnR', the two functions of type @a -> b@ returned will be identical.------  /Caution/: /Conn f g h/ must obey \(f \dashv g \dashv h\). This condition is not checked.------  For detailed properties see 'Data.Connection.Property'.-pattern Conn :: (a -> b) -> (b -> a) -> (a -> b) -> Conn k a b-pattern Conn f g h <- (embed &&& _1 &&& _2 -> (g, (h, f))) where Conn f g h = Galois (h &&& f) g--{-# COMPLETE Conn #-}- -- Internal floor function. When \(f \dashv g \dashv h \) this is h. _1 :: Conn k a b -> a -> b-_1 (Galois f _) = fst . f+_1 (Conn_ f _) = fst . f {-# INLINE _1 #-}  -- Internal ceiling function. When \(f \dashv g \dashv h \) this is f. _2 :: Conn k a b -> a -> b-_2 (Galois f _) = snd . f+_2 (Conn_ f _) = snd . f {-# INLINE _2 #-} --- | The identity 'Conn'.-identity :: Conn k a a-identity = Galois (id &&& id) id-{-# INLINE identity #-}---- | Obtain the center of a 'ConnK', upper adjoint of a 'ConnL', or lower adjoint of a 'ConnR'.+-- | Retrieve the upper adjoint of a 'ConnL', or lower adjoint of a 'ConnR'. embed :: Conn k a b -> b -> a-embed (Galois _ g) = g+embed (Conn_ _ g) = g {-# INLINE embed #-} --- | Obtain the upper and/or lower adjoints of a connection.+-- | Retrieve the left and/or right adjoints of a connection. ----- > range c = floorWith c &&& ceilingWith c+-- > range c = floor c &&& ceiling c -- -- >>> range f64f32 pi -- (3.1415925,3.1415927) -- >>> range f64f32 (0/0) -- (NaN,NaN) range :: Conn k a b -> a -> (b, b)-range (Galois f _) = f+range (Conn_ f _) = f {-# INLINE range #-} +-- | The identity 'Conn'.+identity :: Conn k a a+identity = Conn_ (id &&& id) id+{-# INLINE identity #-}++-- | Lift a 'Conn' into a functor.+--+-- /Caution/: This function will result in an invalid connection+-- if the functor alters the internal preorder (i.e. 'Data.Ord.Down').+mapped :: Functor f => Conn k a b -> Conn k (f a) (f b)+mapped (Conn f g h) = Conn (fmap f) (fmap g) (fmap h)+{-# INLINE mapped #-}++-- | Lift two 'Conn's into a 'Conn' on the <https://en.wikibooks.org/wiki/Category_Theory/Categories_of_ordered_sets coproduct order>+--+-- > (choice id) (ab >>> cd) = (choice id) ab >>> (choice id) cd+-- > (flip choice id) (ab >>> cd) = (flip choice id) ab >>> (flip choice id) cd+choice :: Conn k a b -> Conn k c d -> Conn k (Either a c) (Either b d)+choice (Conn ab ba ab') (Conn cd dc cd') = Conn f g h+  where+    f = either (Left . ab) (Right . cd)+    g = either (Left . ba) (Right . dc)+    h = either (Left . ab') (Right . cd')+{-# INLINE choice #-}++-- | Lift two 'Conn's into a 'Conn' on the <https://en.wikibooks.org/wiki/Order_Theory/Preordered_classes_and_poclasses#product_order product order>+--+-- > (strong id) (ab >>> cd) = (strong id) ab >>> (strong id) cd+-- > (flip strong id) (ab >>> cd) = (flip strong id) ab >>> (flip strong id) cd+strong :: Conn k a b -> Conn k c d -> Conn k (a, c) (b, d)+strong (Conn ab ba ab') (Conn cd dc cd') = Conn f g h+  where+    f = bimap ab cd+    g = bimap ba dc+    h = bimap ab' cd'+{-# INLINE strong #-}+ ------------------------------------------------------------------------ ConnK+-- Conn 'L --------------------------------------------------------------------- --- | An <https://ncatlab.org/nlab/show/adjoint+triple adjoint triple> of Galois connections.+type ConnL = Conn 'L++-- | A <https://ncatlab.org/nlab/show/Galois+connection Galois connection> between two monotone functions. ----- An adjoint triple is a chain of connections of length 3:+-- A Galois connection between /f/ and /g/, written \(f \dashv g \)+-- is an adjunction in the category of preorders. ----- \(f \dashv g \dashv h \)+-- Each side of the connection may be defined in terms of the other: ----- For detailed properties see 'Data.Connection.Property'.-type ConnK a b = forall k. Conn k a b---- | Determine which half of the interval between 2 representations of /a/ a particular value lies.+--  \( g(x) = \sup \{y \in E \mid f(y) \leq x \} \) ----- @ 'half' t x = 'pcompare' (x - 'lower' t x) ('upper' t x - x) @+--  \( f(x) = \inf \{y \in E \mid g(y) \geq x \} \) ----- >>> maybe False (== EQ) $ half f64f32 (midpoint f64f32 pi)--- True-half :: (Num a, Preorder a) => ConnK a b -> a -> Maybe Ordering-half c x = pcompare (x - lower c x) (upper c x - x)-{-# INLINE half #-}+-- /Caution/: /ConnL f g/ must obey \(f \dashv g \). This condition is not checked.+--+-- For further information see 'Data.Connection.Property'.+pattern ConnL :: (a -> b) -> (b -> a) -> ConnL a b+pattern ConnL f g <- (_2 &&& upper -> (f, g)) where ConnL f g = Conn_ (f &&& f) g --- | Return the midpoint of the interval containing x.+{-# COMPLETE ConnL #-}++-- | Witness to the symmetry between 'ConnL' and 'ConnR'. ----- >>> pi - midpoint f64f32 pi--- 3.1786509424591713e-8-midpoint :: Fractional a => ConnK a b -> a -> a-midpoint c x = lower c x / 2 + upper c x / 2-{-# INLINE midpoint #-}+-- > connL . connR = id+-- > connR . connL = id+connL :: ConnR a b -> ConnL b a+connL (ConnR f g) = ConnL f g+{-# INLINE connL #-} --- | Return the nearest value to x.+-- | Obtain the upper adjoint of a 'ConnL', or lower adjoint of a 'ConnR'.+upper :: ConnL a b -> b -> a+upper = embed+{-# INLINE upper #-}++-- | Map over a 'ConnL' from the right. ----- > roundWith identity = id+-- This is the unit of the resulting monad: ----- If x lies halfway between two finite values, then return the value--- with the larger absolute value (i.e. round away from zero).+-- > x <~ upper1 c id x ----- See <https://en.wikipedia.org/wiki/Rounding>.-roundWith :: forall a b. (Num a, Preorder a) => ConnK a b -> a -> b-roundWith c x = case half c x of-    Just GT -> ceilingWith c x-    Just LT -> floorWith c x-    _ -> truncateWith c x-{-# INLINE roundWith #-}+-- >>> compare pi $ upper1 f64f32 id pi+-- LT+upper1 :: ConnL a b -> (b -> b) -> a -> a+upper1 (ConnL f g) h a = g $ h (f a)+{-# INLINE upper1 #-} --- | Lift a unary function over a 'ConnK'.------ Results are rounded to the nearest value with ties away from 0.-roundWith1 :: (Num a, Preorder a) => ConnK a b -> (a -> a) -> b -> b-roundWith1 c f x = roundWith c $ f (g x) where Conn _ g _ = c-{-# INLINE roundWith1 #-}+-- | Zip over a 'ConnL' from the right.+upper2 :: ConnL a b -> (b -> b -> b) -> a -> a -> a+upper2 (ConnL f g) h a1 a2 = g $ h (f a1) (f a2)+{-# INLINE upper2 #-} --- | Lift a binary function over a 'ConnK'.+infixr 5 `join`++-- | Semigroup operation on a join-semilattice.+join :: ConnL (a, a) b -> a -> a -> b+join = curry . ceiling+{-# INLINE join #-}++-- | Extract the lower half of a 'ConnL'. ----- Results are rounded to the nearest value with ties away from 0.+-- > ceiling identity = id+-- > ceiling c (x \/ y) = ceiling c x \/ ceiling c y ----- Example avoiding loss-of-precision:+-- The latter law is the adjoint functor theorem for preorders. ----- >>> f x y = (x + y) - x--- >>> maxOdd32 = 1.6777215e7--- >>> f maxOdd32 2.0 :: Float--- 1.0--- >>> roundWith2 ratf32 f maxOdd32 2.0--- 2.0-roundWith2 :: (Num a, Preorder a) => ConnK a b -> (a -> a -> a) -> b -> b -> b-roundWith2 c f x y = roundWith c $ f (g x) (g y) where Conn _ g _ = c-{-# INLINE roundWith2 #-}+-- >>> Data.Connection.ceiling ratf32 (0 :% 0)+-- NaN+-- >>> Data.Connection.ceiling ratf32 (1 :% 0)+-- Infinity+-- >>> Data.Connection.ceiling ratf32 (13 :% 10)+-- 1.3000001+-- >>> Data.Connection.ceiling f64f32 pi+-- 3.1415927+ceiling :: ConnL a b -> a -> b+ceiling (ConnL f _) = f+{-# INLINE ceiling #-} --- | Truncate towards zero.+-- | Map over a 'ConnL' from the left. ----- > truncateWith identity = id-truncateWith :: (Num a, Preorder a) => ConnK a b -> a -> b-truncateWith c x = if x >~ 0 then floorWith c x else ceilingWith c x-{-# INLINE truncateWith #-}---- | Lift a unary function over a 'ConnK'.+-- This is the counit of the resulting comonad: ----- Results are truncated towards zero.+-- > x >~ ceiling1 c id x ----- > truncateWith1 identity = id-truncateWith1 :: (Num a, Preorder a) => ConnK a b -> (a -> a) -> b -> b-truncateWith1 c f x = truncateWith c $ f (g x) where Conn _ g _ = c-{-# INLINE truncateWith1 #-}+-- >>> ceiling1 (conn @_ @() @Ordering) id LT+-- LT+-- >>> ceiling1 (conn @_ @() @Ordering) id GT+-- LT+ceiling1 :: ConnL a b -> (a -> a) -> b -> b+ceiling1 (ConnL f g) h b = f $ h (g b)+{-# INLINE ceiling1 #-} -truncateWith2 :: (Num a, Preorder a) => ConnK a b -> (a -> a -> a) -> b -> b -> b-truncateWith2 c f x y = truncateWith c $ f (g x) (g y) where Conn _ g _ = c-{-# INLINE truncateWith2 #-}+-- | Zip over a 'ConnL' from the left.+ceiling2 :: ConnL a b -> (a -> a -> a) -> b -> b -> b+ceiling2 (ConnL f g) h b1 b2 = f $ h (g b1) (g b2)+{-# INLINE ceiling2 #-}  ------------------------------------------------------------------------ ConnL+-- Conn 'R --------------------------------------------------------------------- --- | A <https://ncatlab.org/nlab/show/Galois+connection Galois connection> between two monotone functions.+type ConnR = Conn 'R++-- | A Galois connection between two monotone functions. ----- A Galois connection between /f/ and /g/, written \(f \dashv g \)--- is an adjunction in the category of preorders.+-- 'ConnR' is the mirror image of 'ConnL': ----- Each side of the connection may be defined in terms of the other:+-- > connR :: ConnL a b -> ConnR b a -----  \( g(x) = \sup \{y \in E \mid f(y) \leq x \} \)+-- If you only require one connection there is no particular reason to+-- use one version over the other. However some use cases (e.g. rounding)+-- require an adjoint triple of connections that can lower into a standard+-- connection in either of two ways. -----  \( f(x) = \inf \{y \in E \mid g(y) \geq x \} \)+-- /Caution/: /ConnR f g/ must obey \(f \dashv g \). This condition is not checked. -- -- For further information see 'Data.Connection.Property'.------ /Caution/: Monotonicity is not checked.-type ConnL = Conn 'L+pattern ConnR :: (b -> a) -> (a -> b) -> ConnR a b+pattern ConnR f g <- (lower &&& _1 -> (f, g)) where ConnR f g = Conn_ (g &&& g) f --- | A view pattern for a 'ConnL'.+{-# COMPLETE ConnR #-}++-- | Witness to the symmetry between 'ConnL' and 'ConnR'. ----- /Caution/: /ConnL f g/ must obey \(f \dashv g \). This condition is not checked.-pattern ConnL :: (a -> b) -> (b -> a) -> ConnL a b-pattern ConnL f g <- (_2 &&& embed -> (f, g)) where ConnL f g = Galois (f &&& f) g+-- > connL . connR = id+-- > connR . connL = id+connR :: ConnL a b -> ConnR b a+connR (ConnL f g) = ConnR f g+{-# INLINE connR #-} -{-# COMPLETE ConnL #-}+-- | Obtain the  lower adjoint of a 'ConnR'.+lower :: ConnR a b -> b -> a+lower = embed+{-# INLINE lower #-} --- | Convert an inverted 'ConnL' to a 'ConnL'.+-- | Map over a 'ConnR' from the left. ----- > upL . downL = downL . upL = id-upL :: ConnL (Down a) (Down b) -> ConnL b a-upL (ConnL f g) = ConnL g' f'-  where-    f' x = let (Down y) = f (Down x) in y-    g' x = let (Down y) = g (Down x) in y-{-# INLINE upL #-}---- | Convert a 'ConnL' to an inverted 'ConnL'.+-- This is the counit of the resulting comonad: ----- >>> upper (downL $ conn @_ @() @Ordering) (Down LT)--- Down LT--- >>> upper (downL $ conn @_ @() @Ordering) (Down GT)--- Down LT-downL :: ConnL a b -> ConnL (Down b) (Down a)-downL (ConnL f g) = ConnL (\(Down x) -> Down $ g x) (\(Down x) -> Down $ f x)-{-# INLINE downL #-}---- | Witness to the symmetry between 'ConnL' and 'ConnR'.+-- > x >~ lower1 c id x ----- > swapL . swapR = id--- > swapR . swapL = id-swapL :: ConnR a b -> ConnL b a-swapL (ConnR f g) = ConnL f g-{-# INLINE swapL #-}+-- >>> compare pi $ lower1 f64f32 id pi+-- GT+lower1 :: ConnR a b -> (b -> b) -> a -> a+lower1 (ConnR f g) h a = f $ h (g a)+{-# INLINE lower1 #-} --- | Reverse round trip through a 'ConnK' or 'ConnL'.+-- | Zip over a 'ConnR' from the left.+lower2 :: ConnR a b -> (b -> b -> b) -> a -> a -> a+lower2 (ConnR f g) h a1 a2 = f $ h (g a1) (g a2)+{-# INLINE lower2 #-}++infixr 6 `meet`++-- | Semigroup operation on a meet-semilattice.+meet :: ConnR (a, a) b -> a -> a -> b+meet = curry . floor+{-# INLINE meet #-}++-- | Extract the upper half of a 'ConnR' ----- This is the counit of the resulting comonad:+-- > floor identity = id+-- > floor c (x /\ y) = floor c x /\ floor c y ----- > x >~ counit c x+-- The latter law is the adjoint functor theorem for preorders. ----- >>> counit (conn @_ @() @Ordering) LT--- LT--- >>> counit (conn @_ @() @Ordering) GT--- LT-counit :: ConnL a b -> b -> b-counit c = ceilingWith1 c id-{-# INLINE counit #-}+-- >>> Data.Connection.floor ratf32 (0 :% 0)+-- NaN+-- >>> Data.Connection.floor ratf32 (1 :% 0)+-- Infinity+-- >>> Data.Connection.floor ratf32 (13 :% 10)+-- 1.3+-- >>> Data.Connection.floor f64f32 pi+-- 3.1415925+floor :: ConnR a b -> a -> b+floor (ConnR _ g) = g+{-# INLINE floor #-} --- | Round trip through a 'ConnK' or 'ConnL'.+-- | Map over a 'ConnR' from the right. ----- > upper c = upper1 c id = embed c . ceilingWith c--- > x <= upper c x+-- This is the unit of the resulting monad: ----- >>> compare pi $ upper f64f32 pi--- LT-upper :: ConnL a b -> a -> a-upper c = upper1 c id-{-# INLINE upper #-}+-- > x <~ floor1 c id x+--+-- >>> floor1 (conn @_ @() @Ordering) id LT+-- GT+-- >>> floor1 (conn @_ @() @Ordering) id GT+-- GT+floor1 :: ConnR a b -> (a -> a) -> b -> b+floor1 (ConnR f g) h b = g $ h (f b)+{-# INLINE floor1 #-} --- | Map over a 'ConnK' or 'ConnL' from the right.-upper1 :: ConnL a b -> (b -> b) -> a -> a-upper1 (ConnL f g) h a = g $ h (f a)-{-# INLINE upper1 #-}+-- | Zip over a 'ConnR' from the right.+floor2 :: ConnR a b -> (a -> a -> a) -> b -> b -> b+floor2 (ConnR f g) h b1 b2 = g $ h (f b1) (f b2)+{-# INLINE floor2 #-} --- | Zip over a 'ConnK' or 'ConnL' from the right.-upper2 :: ConnL a b -> (b -> b -> b) -> a -> a -> a-upper2 (ConnL f g) h a1 a2 = g $ h (f a1) (f a2)-{-# INLINE upper2 #-}+---------------------------------------------------------------------+-- Conn k+--------------------------------------------------------------------- --- | Obtain the principal filter in /B/ generated by an element of /A/.------ A subset /B/ of a lattice is an filter if and only if it is an upper set--- that is closed under finite meets, i.e., it is nonempty and for all--- /x/, /y/ in /B/, the element @x `meet` y@ is also in /b/.+-- | An <https://ncatlab.org/nlab/show/adjoint+triple adjoint triple> of Galois connections. ----- /filterWith/ and /idealWith/ commute with /Down/:+-- An adjoint triple is a chain of connections of length 3: ----- > filterWith c a b <=> idealWith c (Down a) (Down b)+-- \(f \dashv g \dashv h \) ----- > filterWith c (Down a) (Down b) <=> idealWith c a b+-- When applied to a 'ConnL' or 'ConnR', the two functions of type @a -> b@ returned will be identical. ----- /filterWith c a/ is upward-closed for all /a/:+-- /Caution/: /Conn f g h/ must obey \(f \dashv g \dashv h\). This condition is not checked. ----- > a <= b1 && b1 <= b2 => a <= b2+-- For detailed properties see 'Data.Connection.Property'.+pattern Conn :: (a -> b) -> (b -> a) -> (a -> b) -> Conn k a b+pattern Conn f g h <- (embed &&& _1 &&& _2 -> (g, (h, f))) where Conn f g h = Conn_ (h &&& f) g++{-# COMPLETE Conn #-}++-- | Determine which half of the interval between 2 representations of /a/ a particular value lies. ----- > a1 <= b && inf a2 <= b => ceiling a1 `meet` ceiling a2 <= b+-- @ 'half' c x = 'pcompare' (x - 'lower1' c 'id' x) ('upper1' c 'id' x - x) @ ----- See <https://en.wikipedia.org/wiki/Filter_(mathematics)>-filterWith :: Preorder b => ConnL a b -> a -> b -> Bool-filterWith c a b = ceilingWith c a <~ b-{-# INLINE filterWith #-}+-- >>> maybe False (== EQ) $ half f64f32 (midpoint f64f32 pi)+-- True+half :: (Num a, Preorder a) => (forall k. Conn k a b) -> a -> Maybe Ordering+half c x = pcompare (x - lower1 c id x) (upper1 c id x - x)+{-# INLINE half #-} --- | Extract the left half of a 'ConnK' or 'ConnL'.+-- | Return the midpoint of the interval containing x. ----- >>> floorWith f64f32 pi--- 3.1415925--- >>> ceilingWith f64f32 pi--- 3.1415927-ceilingWith :: ConnL a b -> a -> b-ceilingWith (ConnL f _) = f-{-# INLINE ceilingWith #-}---- | Map over a 'ConnK' or 'ConnL' from the left.-ceilingWith1 :: ConnL a b -> (a -> a) -> b -> b-ceilingWith1 (ConnL f g) h b = f $ h (g b)-{-# INLINE ceilingWith1 #-}+-- >>> pi - midpoint f64f32 pi+-- 3.1786509424591713e-8+midpoint :: Fractional a => (forall k. Conn k a b) -> a -> a+midpoint c x = lower1 c id x / 2 + upper1 c id x / 2+{-# INLINE midpoint #-} --- | Zip over a 'ConnK' or 'ConnL' from the left.-ceilingWith2 :: ConnL a b -> (a -> a -> a) -> b -> b -> b-ceilingWith2 (ConnL f g) h b1 b2 = f $ h (g b1) (g b2)-{-# INLINE ceilingWith2 #-}+-- | Return the nearest value to x.+--+-- > round identity = id+--+-- If x lies halfway between two finite values, then return the value+-- with the larger absolute value (i.e. round away from zero).+--+-- See <https://en.wikipedia.org/wiki/Rounding>.+round :: (Num a, Preorder a) => (forall k. Conn k a b) -> a -> b+round c x = case half c x of+    Just GT -> ceiling c x+    Just LT -> floor c x+    _ -> truncate c x+{-# INLINE round #-} ------------------------------------------------------------------------- ConnR----------------------------------------------------------------------+-- | Lift a unary function over a 'Trip'.+--+-- Results are rounded to the nearest value with ties away from 0.+round1 :: (Num a, Preorder a) => (forall k. Conn k a b) -> (a -> a) -> b -> b+round1 c f x = round c $ f (g x) where Conn _ g _ = c+{-# INLINE round1 #-} --- | A Galois connection between two monotone functions.+-- | Lift a binary function over a 'Trip'. ----- 'ConnR' is the mirror image of 'ConnL':+-- Results are rounded to the nearest value with ties away from 0. ----- > swapR :: ConnL a b -> ConnR b a+-- Example avoiding loss-of-precision: ----- If you only require one connection there is no particular reason to--- use one version over the other.+-- >>> f x y = (x + y) - x+-- >>> maxOdd32 = 1.6777215e7+-- >>> f maxOdd32 2.0 :: Float+-- 1.0+-- >>> round2 ratf32 f maxOdd32 2.0+-- 2.0+round2 :: (Num a, Preorder a) => (forall k. Conn k a b) -> (a -> a -> a) -> b -> b -> b+round2 c f x y = round c $ f (g x) (g y) where Conn _ g _ = c+{-# INLINE round2 #-}++-- | Truncate towards zero. ----- However some use cases (e.g. rounding) require an adjoint triple--- of connections (i.e. a 'ConnK') that can lower into a standard--- connection in either of two ways.-type ConnR = Conn 'R+-- > truncate identity = id+truncate :: (Num a, Preorder a) => (forall k. Conn k a b) -> a -> b+truncate c x = if x >~ 0 then floor c x else ceiling c x+{-# INLINE truncate #-} --- | A view pattern for a 'ConnR'.+-- | Lift a unary function over a 'Trip'. ----- /Caution/: /ConnR f g/ must obey \(f \dashv g \). This condition is not checked.-pattern ConnR :: (b -> a) -> (a -> b) -> ConnR a b-pattern ConnR f g <- (embed &&& _1 -> (f, g)) where ConnR f g = Galois (g &&& g) f+-- Results are truncated towards zero.+--+-- > truncate1 identity = id+truncate1 :: (Num a, Preorder a) => (forall k. Conn k a b) -> (a -> a) -> b -> b+truncate1 c f x = truncate c $ f (g x) where Conn _ g _ = c+{-# INLINE truncate1 #-} -{-# COMPLETE ConnR #-}+truncate2 :: (Num a, Preorder a) => (forall k. Conn k a b) -> (a -> a -> a) -> b -> b -> b+truncate2 c f x y = truncate c $ f (g x) (g y) where Conn _ g _ = c+{-# INLINE truncate2 #-} +---------------------------------------------------------------------+-- Down+---------------------------------------------------------------------++-- | Convert an inverted 'ConnL' to a 'ConnL'.+--+-- > upL . downL = downL . upL = id+upL :: ConnL (Down a) (Down b) -> ConnL b a+upL (ConnL f g) = ConnL g' f'+  where+    f' x = let (Down y) = f (Down x) in y+    g' x = let (Down y) = g (Down x) in y+{-# INLINE upL #-}+ -- | Convert an inverted 'ConnR' to a 'ConnR'. -- -- > upR . downR = downR . upR = id@@ -411,122 +501,63 @@     g' x = let (Down y) = g (Down x) in y {-# INLINE upR #-} +-- | Convert a 'ConnL' to an inverted 'ConnL'.+--+-- >>> let counit = upper1 (downL $ conn @_ @() @Ordering) id+-- >>> counit (Down LT)+-- Down LT+-- >>> counit (Down GT)+-- Down LT+downL :: ConnL a b -> ConnL (Down b) (Down a)+downL (ConnL f g) = ConnL (\(Down x) -> Down $ g x) (\(Down x) -> Down $ f x)+{-# INLINE downL #-}+ -- | Convert a 'ConnR' to an inverted 'ConnR'. ----- >>> lower (downR $ conn @_ @() @Ordering) (Down LT)+-- >>> let unit = lower1 (downR $ conn @_ @() @Ordering) id+-- >>> unit (Down LT) -- Down GT--- >>> lower (downR $ conn @_ @() @Ordering) (Down GT)+-- >>> unit (Down GT) -- Down GT downR :: ConnR a b -> ConnR (Down b) (Down a) downR (ConnR f g) = ConnR (\(Down x) -> Down $ g x) (\(Down x) -> Down $ f x) {-# INLINE downR #-} --- | Witness to the symmetry between 'ConnL' and 'ConnR'.+-- | Obtain the principal filter in /B/ generated by an element of /A/. ----- > swapL . swapR = id--- > swapR . swapL = id-swapR :: ConnL a b -> ConnR b a-swapR (ConnL f g) = ConnR f g-{-# INLINE swapR #-}---- | Round trip through a 'ConnK' or 'ConnR'.+-- A subset /B/ of a lattice is an filter if and only if it is an upper set+-- that is closed under finite meets, i.e., it is nonempty and for all+-- /x/, /y/ in /B/, the element @meet c x y@ is also in /b/. ----- This is the unit of the resulting monad:+-- /filterL/ and /filterR/ commute with /Down/: ----- > x <~ unit c x--- > unit c = floorWith1 c id = floorWith c . embed c+-- > filterL c a b <=> ideal c (Down a) (Down b) ----- >>> unit (conn @_ @() @Ordering) LT--- GT--- >>> unit (conn @_ @() @Ordering) GT--- GT-unit :: ConnR a b -> b -> b-unit c = floorWith1 c id-{-# INLINE unit #-}---- | Reverse round trip through a 'ConnK' or 'ConnR'.+-- > filterL c (Down a) (Down b) <=> ideal c a b ----- > x >~ lower c x+-- /filterL c a/ is upward-closed for all /a/: ----- >>> compare pi $ lower f64f32 pi--- GT-lower :: ConnR a b -> a -> a-lower c = lower1 c id-{-# INLINE lower #-}---- | Map over a 'ConnK' or 'ConnR' from the left.-lower1 :: ConnR a b -> (b -> b) -> a -> a-lower1 (ConnR f g) h a = f $ h (g a)-{-# INLINE lower1 #-}---- | Zip over a 'ConnK' or 'ConnR' from the left.-lower2 :: ConnR a b -> (b -> b -> b) -> a -> a -> a-lower2 (ConnR f g) h a1 a2 = f $ h (g a1) (g a2)-{-# INLINE lower2 #-}+-- > a <= b1 && b1 <= b2 => a <= b2+-- > a1 <= b && a2 <= b => meet c (ceiling c a1) (ceiling c a2) <= b+--+-- See <https://en.wikipedia.org/wiki/Filter_(mathematics)>+filterL :: Preorder b => ConnL a b -> a -> b -> Bool+filterL c a b = ceiling c a <~ b+{-# INLINE filterL #-}  -- | Obtain the principal ideal in /B/ generated by an element of /A/. -- -- A subset /B/ of a lattice is an ideal if and only if it is a lower set -- that is closed under finite joins, i.e., it is nonempty and for all--- /x/, /y/ in /B/, the element /x `join` y/ is also in /B/.+-- /x/, /y/ in /B/, the element /join c x y/ is also in /B/. ----- /idealWith c a/ is downward-closed for all /a/:+-- /filterR c a/ is downward-closed for all /a/: -- -- > a >= b1 && b1 >= b2 => a >= b2 ----- > a1 >= b && a2 >= b => floor a1 `join` floor a2 >= b+-- > a1 >= b && a2 >= b => join c (floor c a1) (floor c a2) >= b -- -- See <https://en.wikipedia.org/wiki/Ideal_(order_theory)>-idealWith :: Preorder b => ConnR a b -> a -> b -> Bool-idealWith c a b = b <~ floorWith c a-{-# INLINE idealWith #-}---- | Extract the right half of a 'ConnK' or 'ConnR'------ This is the adjoint functor theorem for preorders.------ >>> floorWith f64f32 pi--- 3.1415925--- >>> ceilingWith f64f32 pi--- 3.1415927-floorWith :: ConnR a b -> a -> b-floorWith (ConnR _ g) = g-{-# INLINE floorWith #-}---- | Map over a 'ConnK' or 'ConnR' from the right.-floorWith1 :: ConnR a b -> (a -> a) -> b -> b-floorWith1 (ConnR f g) h b = g $ h (f b)-{-# INLINE floorWith1 #-}---- | Zip over a 'ConnK' or 'ConnR' from the right.-floorWith2 :: ConnR a b -> (a -> a -> a) -> b -> b -> b-floorWith2 (ConnR f g) h b1 b2 = g $ h (f b1) (f b2)-{-# INLINE floorWith2 #-}-------------------------------------------------------------------------- Combinators-------------------------------------------------------------------------- | Lift two 'Conn's into a 'Conn' on the <https://en.wikibooks.org/wiki/Category_Theory/Categories_of_ordered_sets coproduct order>------ > (choice id) (ab >>> cd) = (choice id) ab >>> (choice id) cd--- > (flip choice id) (ab >>> cd) = (flip choice id) ab >>> (flip choice id) cd-choice :: Conn k a b -> Conn k c d -> Conn k (Either a c) (Either b d)-choice (Conn ab ba ab') (Conn cd dc cd') = Conn f g h-  where-    f = either (Left . ab) (Right . cd)-    g = either (Left . ba) (Right . dc)-    h = either (Left . ab') (Right . cd')-{-# INLINE choice #-}---- | Lift two 'Conn's into a 'Conn' on the <https://en.wikibooks.org/wiki/Order_Theory/Preordered_classes_and_poclasses#product_order product order>------ > (strong id) (ab >>> cd) = (strong id) ab >>> (strong id) cd--- > (flip strong id) (ab >>> cd) = (flip strong id) ab >>> (flip strong id) cd-strong :: Conn k a b -> Conn k c d -> Conn k (a, c) (b, d)-strong (Conn ab ba ab') (Conn cd dc cd') = Conn f g h-  where-    f = bimap ab cd-    g = bimap ba dc-    h = bimap ab' cd'-{-# INLINE strong #-}+filterR :: Preorder b => ConnR a b -> a -> b -> Bool+filterR c a b = b <~ floor c a+{-# INLINE filterR #-}

@@ -0,0 +1,152 @@+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE Safe #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}++module Data.Connection.Fixed (+    Fixed (..),+    showFixed,+    shiftf,++    -- * Uni+    Uni,++    -- * Deci+    Deci,+    f01f00,++    -- * Centi+    Centi,+    f02f00,+    f02f01,++    -- * Milli+    Milli,+    f03f00,+    f03f01,+    f03f02,++    -- * Micro+    Micro,+    f06f00,+    f06f01,+    f06f02,+    f06f03,++    -- * Nano+    Nano,+    f09f00,+    f09f01,+    f09f02,+    f09f03,+    f09f06,++    -- * Pico+    Pico,+    f12f00,+    f12f01,+    f12f02,+    f12f03,+    f12f06,+    f12f09,++    -- * HasResolution+    HasResolution (..),+) where++import safe Data.Connection.Conn+import safe Data.Fixed+import safe Data.Order.Syntax+import safe Prelude hiding (Eq (..), Ord (..))++-- | Shift by n 'units of least precision' where the ULP is determined by the precision.+--+-- This is an analog of 'Data.Connection.Float.shift32' for fixed point numbers.+shiftf :: Integer -> Fixed a -> Fixed a+shiftf j (MkFixed i) = MkFixed (i + j)++-- Deci++f01f00 :: Conn k Deci Uni+f01f00 = triple 10++-- Centi++f02f00 :: Conn k Centi Uni+f02f00 = triple 100++f02f01 :: Conn k Centi Deci+f02f01 = triple 10++-- Milli++f03f00 :: Conn k Milli Uni+f03f00 = triple 1000++f03f01 :: Conn k Milli Deci+f03f01 = triple 100++f03f02 :: Conn k Milli Centi+f03f02 = triple 10++-- Micro++f06f00 :: Conn k Micro Uni+f06f00 = triple $ 10 ^ (6 :: Integer)++f06f01 :: Conn k Micro Deci+f06f01 = triple $ 10 ^ (5 :: Integer)++f06f02 :: Conn k Micro Centi+f06f02 = triple $ 10 ^ (4 :: Integer)++f06f03 :: Conn k Micro Milli+f06f03 = triple $ 10 ^ (3 :: Integer)++-- Nano++f09f00 :: Conn k Nano Uni+f09f00 = triple $ 10 ^ (9 :: Integer)++f09f01 :: Conn k Nano Deci+f09f01 = triple $ 10 ^ (8 :: Integer)++f09f02 :: Conn k Nano Centi+f09f02 = triple $ 10 ^ (7 :: Integer)++f09f03 :: Conn k Nano Milli+f09f03 = triple $ 10 ^ (6 :: Integer)++f09f06 :: Conn k Nano Micro+f09f06 = triple $ 10 ^ (3 :: Integer)++-- Pico++f12f00 :: Conn k Pico Uni+f12f00 = triple $ 10 ^ (12 :: Integer)++f12f01 :: Conn k Pico Deci+f12f01 = triple $ 10 ^ (11 :: Integer)++f12f02 :: Conn k Pico Centi+f12f02 = triple $ 10 ^ (10 :: Integer)++f12f03 :: Conn k Pico Milli+f12f03 = triple $ 10 ^ (9 :: Integer)++f12f06 :: Conn k Pico Micro+f12f06 = triple $ 10 ^ (6 :: Integer)++f12f09 :: Conn k Pico Nano+f12f09 = triple $ 10 ^ (3 :: Integer)++-- Internal++-------------------------++triple :: Integer -> Conn k (Fixed e1) (Fixed e2)+triple prec = Conn f g h+  where+    f (MkFixed i) = MkFixed $ let j = i `div` prec in if i `mod` prec == 0 then j else j + 1+    g (MkFixed i) = MkFixed $ i * prec+    h (MkFixed i) = MkFixed $ let j = i `div` prec in if i `mod` prec == 0 then j else j -1

@@ -1,34 +1,45 @@ {-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE Safe #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE ViewPatterns #-}  module Data.Connection.Float (-    -- * Connections-    f32i08,-    f32i16,-    f64i08,-    f64i16,-    f64i32,-    f64f32,-     -- * Float     min32,     max32,+    eps32,     ulp32,     near32,     shift32,+    f32i08,+    f32i16,+    f32i32,+    f32i64,+    f32ixx,+    f32int,      -- * Double     min64,     max64,+    eps64,     ulp64,     near64,     shift64,+    f64i08,+    f64i16,+    f64i32,+    f64i64,+    f64ixx,+    f64int,+    f64f32,     until, ) where  import safe Data.Bool-import safe Data.Connection.Conn+import safe Data.Connection.Conn hiding (ceiling, floor) import safe Data.Int import safe Data.Order import safe Data.Order.Extended@@ -39,56 +50,6 @@ import safe qualified Prelude as P  ------------------------------------------------------------------------ Connections-------------------------------------------------------------------------- | All 'Data.Int.Int08' values are exactly representable in a 'Float'.-f32i08 :: Conn k Float (Extended Int8)-f32i08 = triple 127---- | All 'Data.Int.Int16' values are exactly representable in a 'Float'.------  > ceilingWith f32i16 32767.0---  Extended 32767---  > ceilingWith f32i16 32767.1---  Top-f32i16 :: Conn k Float (Extended Int16)-f32i16 = triple 32767---- | All 'Data.Int.Int08' values are exactly representable in a 'Double'.-f64i08 :: Conn k Double (Extended Int8)-f64i08 = triple 127---- | All 'Data.Int.Int16' values are exactly representable in a 'Double'.-f64i16 :: Conn k Double (Extended Int16)-f64i16 = triple 32767---- | All 'Data.Int.Int32' values are exactly representable in a 'Double'.-f64i32 :: Conn k Double (Extended Int32)-f64i32 = triple 2147483647--f64f32 :: Conn k Double Float-f64f32 = Conn f1 g f2-  where-    f1 x =-        let est = F.double2Float x-         in if g est >~ x-                then est-                else ascend32 est g x--    f2 x =-        let est = F.double2Float x-         in if g est <~ x-                then est-                else descend32 est g x--    g = F.float2Double--    ascend32 z g1 y = until (\x -> g1 x >~ y) (<~) (shift32 1) z--    descend32 z h1 x = until (\y -> h1 y <~ x) (>~) (shift32 (-1)) z----------------------------------------------------------------------- -- Float --------------------------------------------------------------------- @@ -114,6 +75,12 @@     (True, False) -> y     (True, True) -> x +-- | Compute the difference between a float and its next largest neighbor.+--+-- See < https://en.wikipedia.org/wiki/Machine_epsilon >.+eps32 :: Float -> Float+eps32 x = shift32 1 x - x+ -- | Compute the signed distance between two floats in units of least precision. -- -- >>> ulp32 1.0 (shift32 1 1.0)@@ -133,7 +100,7 @@ -- -- Required accuracy is specified in units of least precision. ----- See also <https://randomascii.wordpress.com/2012/02/25/comparing-floating-point-numbers-2012-edition/>.+-- See <https://randomascii.wordpress.com/2012/02/25/comparing-floating-point-numbers-2012-edition/>. near32 :: Word32 -> Float -> Float -> Bool near32 tol x y = maybe False ((<= tol) . snd) $ ulp32 x y @@ -144,16 +111,45 @@ -- >>> shift32 1 1 - 1 -- 1.1920929e-7 -- >>> shift32 1 $ 0/0--- NaN+-- Infinity -- >>> shift32 (-1) $ 0/0--- NaN+-- -Infinity -- >>> shift32 1 $ 1/0 -- Infinity shift32 :: Int32 -> Float -> Float-shift32 n x-    | x ~~ 0 / 0 = x-    | otherwise = int32Float . clamp32 . (+ n) . floatInt32 $ x+shift32 n x =+    if isNaN x == True+        then case signum n of+            -1 -> -1 / 0+            1 -> 1 / 0+            _ -> 0 / 0+        else int32Float . clamp32 . (+ n) . floatInt32 $ x +-- | All 'Data.Int.Int08' values are exactly representable in a 'Float'.+f32i08 :: Conn k Float (Extended Int8)+f32i08 = fxxext++-- | All 'Data.Int.Int16' values are exactly representable in a 'Float'.+--+-- >>> Data.Connection.Conn.ceiling f32i16 32767.0+-- Extended 32767+-- >>> Data.Connection.Conn.ceiling f32i16 32767.1+-- Top+f32i16 :: Conn k Float (Extended Int16)+f32i16 = fxxext++f32i32 :: Conn 'L Float (Extended Int32)+f32i32 = f32ext++f32i64 :: Conn 'L Float (Extended Int64)+f32i64 = f32ext++f32ixx :: Conn 'L Float (Extended Int)+f32ixx = f32ext++f32int :: Conn 'L Float (Extended Integer)+f32int = f32ext+ --------------------------------------------------------------------- -- Double ---------------------------------------------------------------------@@ -180,6 +176,12 @@     (True, False) -> y     (True, True) -> x +-- | Compute the difference between a double and its next largest neighbor.+--+-- See < https://en.wikipedia.org/wiki/Machine_epsilon >.+eps64 :: Double -> Double+eps64 x = shift64 1 x - x+ -- | Compute the signed distance between two doubles in units of least precision. -- -- >>> ulp64 1.0 (shift64 1 1.0)@@ -210,16 +212,63 @@ -- >>> shift64 1 1 - 1 -- 2.220446049250313e-16 -- >>> shift64 1 $ 0/0--- NaN+-- Infinity -- >>> shift64 (-1) $ 0/0--- NaN+-- -Infinity -- >>> shift64 1 $ 1/0 -- Infinity shift64 :: Int64 -> Double -> Double-shift64 n x-    | x ~~ 0 / 0 = x-    | otherwise = int64Double . clamp64 . (+ n) . doubleInt64 $ x+shift64 n x =+    if isNaN x == True+        then case signum n of+            -1 -> -1 / 0+            1 -> 1 / 0+            _ -> 0 / 0+        else int64Double . clamp64 . (+ n) . doubleInt64 $ x +-- | All 'Data.Int.Int08' values are exactly representable in a 'Double'.+f64i08 :: Conn k Double (Extended Int8)+f64i08 = fxxext++-- | All 'Data.Int.Int16' values are exactly representable in a 'Double'.+f64i16 :: Conn k Double (Extended Int16)+f64i16 = fxxext++-- | All 'Data.Int.Int32' values are exactly representable in a 'Double'.+f64i32 :: Conn k Double (Extended Int32)+f64i32 = fxxext++f64i64 :: Conn 'L Double (Extended Int64)+f64i64 = f64ext++f64ixx :: Conn 'L Double (Extended Int)+f64ixx = f64ext++f64int :: Conn 'L Double (Extended Integer)+f64int = f64ext++f64f32 :: Conn k Double Float+f64f32 = Conn f g h+  where+    f x =+        let est = double2Float x+         in if g est >~ x+                then est+                else ascend32 est g x++    g = float2Double++    h x =+        let est = double2Float x+         in if g est <~ x+                then est+                else descend32 est g x++    ascend32 z g1 y = until (\x -> g1 x >~ y) (<~) (shift32 1) z++    descend32 z h1 x = until (\y -> h1 y <~ x) (>~) (shift32 (-1)) z+{-# INLINE f64f32 #-}+ --------------------------------------------------------------------- -- Internal ---------------------------------------------------------------------@@ -245,7 +294,7 @@ signed64 :: Word64 -> Int64 signed64 x     | x < 0x8000000000000000 = fromIntegral x-    | otherwise = fromIntegral (maxBound P.- (x P.- 0x8000000000000000))+    | otherwise = fromIntegral (maxBound - (x - 0x8000000000000000))  -- Non-monotonic function converting from 2s-complement format. unsigned32 :: Int32 -> Word32@@ -256,20 +305,21 @@ -- Non-monotonic function converting from 2s-complement format. unsigned64 :: Int64 -> Word64 unsigned64 x-    | x >~ 0 = fromIntegral x-    | otherwise = 0x8000000000000000 + (maxBound P.- (fromIntegral x))+    | x >= 0 = fromIntegral x+    | otherwise = 0x8000000000000000 + (maxBound - (fromIntegral x))  int32Float :: Int32 -> Float-int32Float = F.castWord32ToFloat . unsigned32+int32Float = castWord32ToFloat . unsigned32 +-- NB: I needed these zeros to avoid some error floatInt32 :: Float -> Int32-floatInt32 = signed32 . (+ 0) . F.castFloatToWord32+floatInt32 = signed32 . (+ 0) . castFloatToWord32  int64Double :: Int64 -> Double-int64Double = F.castWord64ToDouble . unsigned64+int64Double = castWord64ToDouble . unsigned64  doubleInt64 :: Double -> Int64-doubleInt64 = signed64 . (+ 0) . F.castDoubleToWord64+doubleInt64 = signed64 . (+ 0) . castDoubleToWord64  -- Clamp between the int representations of -1/0 and 1/0 clamp32 :: Int32 -> Int32@@ -279,51 +329,59 @@ clamp64 :: Int64 -> Int64 clamp64 = P.max (-9218868437227405313) . P.min 9218868437227405312 -triple :: (RealFrac a, Preorder a, Bounded b, Integral b) => a -> Conn k a (Extended b)-triple high = Conn f g h+f32ext :: Integral a => Conn 'L Float (Extended a)+f32ext = ConnL f g   where-    f = liftExtended (~~ -1 / 0) (\x -> x ~~ 0 / 0 || x > high) $ \x -> if x < low then minBound else P.ceiling x+    prec = 24 :: Int -- Float loses integer precision beyond 2^prec+    f x+        | abs x <= 2 ** 24 -1 = Extended (ceiling x)+        | otherwise = case pcompare x 0 of+            Just LT -> Bottom+            _ -> Extended (2 ^ prec) -    g = extended (-1 / 0) (1 / 0) P.fromIntegral+    g Bottom = -2 ** 24+    g Top = 1 / 0+    g (Extended i)+        | abs i P.<= 2 ^ prec -1 = fromIntegral i+        | otherwise = if i P.>= 0 then 1 / 0 else -2 ** 24+{-# INLINE f32ext #-} -    h = liftExtended (\x -> x ~~ 0 / 0 || x < low) (~~ 1 / 0) $ \x -> if x > high then maxBound else P.floor x+f64ext :: Integral a => Conn 'L Double (Extended a)+f64ext = ConnL f g+  where+    prec = 53 :: Int -- Double loses integer precision beyond 2^prec+    f x+        | abs x <= 2 ** 53 -1 = Extended (ceiling x)+        | otherwise = case pcompare x 0 of+            Just LT -> Bottom+            _ -> Extended (2 ^ prec) -    low = -1 - high+    g Bottom = -2 ** 53+    g Top = 1 / 0+    g (Extended i)+        | abs i P.<= 2 ^ prec -1 = fromIntegral i+        | otherwise = if i P.>= 0 then 1 / 0 else -2 ** 53+{-# INLINE f64ext #-} -{---- | Exact embedding up to the largest representable 'Int32'.-f32i32 :: ConnL Float (Maybe Int32)-f32i32 = Conn (nanf f) (nan g) where-  f x | abs x <~ 2**24-1 = P.ceiling x-      | otherwise = if x >~ 0 then 2^24 else minBound+fxxext :: forall a b k. (RealFrac a, Preorder a, Bounded b, Integral b) => Conn k a (Extended b)+fxxext = Conn f g h+  where+    f = liftExtended (~~ -1 / 0) (\x -> x ~~ 0 / 0 || x > high) $ \x -> if x < low then minBound else ceiling x -  g i | abs' i <~ 2^24-1 = fromIntegral i-      | otherwise = if i >~ 0 then 1/0 else -2**24+    g = extended (-1 / 0) (1 / 0) fromIntegral --- | Exact embedding up to the largest representable 'Int32'.-i32f32 :: ConnL (Maybe Int32) Float-i32f32 = Conn (nan g) (nanf f) where-  f x | abs x <~ 2**24-1 = P.floor x-      | otherwise = if x >~ 0 then maxBound else -2^24+    h = liftExtended (\x -> x ~~ 0 / 0 || x < low) (~~ 1 / 0) $ \x -> if x > high then maxBound else floor x -  g i | abs i <~ 2^24-1 = fromIntegral i-      | otherwise = if i >~ 0 then 2**24 else -1/0+    low = fromIntegral $ minBound @b --- | Exact embedding up to the largest representable 'Int64'.-f64i64 :: Conn Double (Maybe Int64)-f64i64 = Conn (nanf f) (nan g) where-  f x | abs x <~ 2**53-1 = P.ceiling x-      | otherwise = if x >~ 0 then 2^53 else minBound+    high = fromIntegral $ maxBound @b+{-# INLINE fxxext #-} -  g i | abs' i <~ 2^53-1 = fromIntegral i-      | otherwise = if i >~ 0 then 1/0 else -2**53+{- --- | Exact embedding up to the largest representable 'Int64'.-f64ixx :: Conn Double (Maybe Int)-f64ixx = Conn (nanf f) (nan g) where-  f x | abs x <~ 2**53-1 = P.ceiling x-      | otherwise = if x >~ 0 then 2^53 else minBound+frac2fixed :: (RealFrac a, HasResolution b) => a -> Fixed b+frac2fixed (flip approxRational 0 -> (n :% d)) = fromInteger n / fromInteger d -  g i | abs' i <~ 2^53-1 = fromIntegral i-      | otherwise = if i >~ 0 then 1/0 else -2**53+--fixed2Float :: forall a . HasResolution a => Fixed a -> Float+--fixed2Float (MkFixed i) = rationalToFloat i $ resolution (Proxy :: Proxy a) -}

@@ -1,4 +1,5 @@ {-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-} {-# LANGUAGE Safe #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-}@@ -54,61 +55,61 @@ import safe Prelude  -- Int16-w08i16 :: ConnL Word8 (Maybe Int16)+w08i16 :: Conn 'L Word8 (Maybe Int16) w08i16 = signed -i08i16 :: ConnL Int8 (Maybe Int16)+i08i16 :: Conn 'L Int8 (Maybe Int16) i08i16 = signed  -- Int32-w08i32 :: ConnL Word8 (Maybe Int32)+w08i32 :: Conn 'L Word8 (Maybe Int32) w08i32 = signed -w16i32 :: ConnL Word16 (Maybe Int32)+w16i32 :: Conn 'L Word16 (Maybe Int32) w16i32 = signed -i08i32 :: ConnL Int8 (Maybe Int32)+i08i32 :: Conn 'L Int8 (Maybe Int32) i08i32 = signed -i16i32 :: ConnL Int16 (Maybe Int32)+i16i32 :: Conn 'L Int16 (Maybe Int32) i16i32 = signed  -- Int64-w08i64 :: ConnL Word8 (Maybe Int64)+w08i64 :: Conn 'L Word8 (Maybe Int64) w08i64 = signed -w16i64 :: ConnL Word16 (Maybe Int64)+w16i64 :: Conn 'L Word16 (Maybe Int64) w16i64 = signed -w32i64 :: ConnL Word32 (Maybe Int64)+w32i64 :: Conn 'L Word32 (Maybe Int64) w32i64 = signed -i08i64 :: ConnL Int8 (Maybe Int64)+i08i64 :: Conn 'L Int8 (Maybe Int64) i08i64 = signed -i16i64 :: ConnL Int16 (Maybe Int64)+i16i64 :: Conn 'L Int16 (Maybe Int64) i16i64 = signed -i32i64 :: ConnL Int32 (Maybe Int64)+i32i64 :: Conn 'L Int32 (Maybe Int64) i32i64 = signed  -- Int-w08ixx :: ConnL Word8 (Maybe Int)+w08ixx :: Conn 'L Word8 (Maybe Int) w08ixx = signed -w16ixx :: ConnL Word16 (Maybe Int)+w16ixx :: Conn 'L Word16 (Maybe Int) w16ixx = signed -w32ixx :: ConnL Word32 (Maybe Int)+w32ixx :: Conn 'L Word32 (Maybe Int) w32ixx = signed -i08ixx :: ConnL Int8 (Maybe Int)+i08ixx :: Conn 'L Int8 (Maybe Int) i08ixx = signed -i16ixx :: ConnL Int16 (Maybe Int)+i16ixx :: Conn 'L Int16 (Maybe Int) i16ixx = signed -i32ixx :: ConnL Int32 (Maybe Int)+i32ixx :: Conn 'L Int32 (Maybe Int) i32ixx = signed  -- | /Caution/: This assumes that 'Int' on your system is 64 bits.@@ -116,37 +117,37 @@ i64ixx = Conn fromIntegral fromIntegral fromIntegral  -- Integer-w08int :: ConnL Word8 (Maybe Integer)+w08int :: Conn 'L Word8 (Maybe Integer) w08int = signed -w16int :: ConnL Word16 (Maybe Integer)+w16int :: Conn 'L Word16 (Maybe Integer) w16int = signed -w32int :: ConnL Word32 (Maybe Integer)+w32int :: Conn 'L Word32 (Maybe Integer) w32int = signed -w64int :: ConnL Word64 (Maybe Integer)+w64int :: Conn 'L Word64 (Maybe Integer) w64int = signed -wxxint :: ConnL Word (Maybe Integer)+wxxint :: Conn 'L Word (Maybe Integer) wxxint = signed -natint :: ConnL Natural (Maybe Integer)+natint :: Conn 'L Natural (Maybe Integer) natint = ConnL (fmap fromIntegral . fromPred (/= 0)) (maybe 0 $ fromInteger . max 0) -i08int :: ConnL Int8 (Maybe Integer)+i08int :: Conn 'L Int8 (Maybe Integer) i08int = signed -i16int :: ConnL Int16 (Maybe Integer)+i16int :: Conn 'L Int16 (Maybe Integer) i16int = signed -i32int :: ConnL Int32 (Maybe Integer)+i32int :: Conn 'L Int32 (Maybe Integer) i32int = signed -i64int :: ConnL Int64 (Maybe Integer)+i64int :: Conn 'L Int64 (Maybe Integer) i64int = signed -ixxint :: ConnL Int (Maybe Integer)+ixxint :: Conn 'L Int (Maybe Integer) ixxint = signed  ---------------------------------------------------------------------@@ -156,7 +157,7 @@ fromPred :: (a -> Bool) -> a -> Maybe a fromPred p a = a <$ guard (p a) -signed :: forall a b. (Bounded a, Integral a, Integral b) => ConnL a (Maybe b)+signed :: forall a b. (Bounded a, Integral a, Integral b) => Conn 'L a (Maybe b) signed = ConnL f g   where     f = fmap fromIntegral . fromPred (/= minBound)

@@ -8,117 +8,138 @@ -- --  \( \forall x, y : f \dashv g \Rightarrow f (x) \leq b \Leftrightarrow x \leq g (y) \) -----  \( \forall x, y : x \leq y \Rightarrow f (x) \leq f (y) \)------  \( \forall x, y : x \leq y \Rightarrow g (x) \leq g (y) \)--- --  \( \forall x : f \dashv g \Rightarrow x \leq g \circ f (x) \) -- --  \( \forall x : f \dashv g \Rightarrow f \circ g (x) \leq x \)------  \( \forall x : unit \circ unit (x) \sim unit (x) \)------  \( \forall x : counit \circ counit (x) \sim counit (x) \)------  \( \forall x : counit \circ f (x) \sim f (x) \)------  \( \forall x : unit \circ g (x) \sim g (x) \)-module Data.Connection.Property where+module Data.Connection.Property (+    -- * Adjointness+    adjointL,+    adjointR,+    adjoint,+    adjunction, +    -- * Closure+    closedL,+    closedR,+    closed,+    kernelL,+    kernelR,+    kernel,+    invertible,++    -- * Monotonicity+    monotonicR,+    monotonicL,+    monotonic,+    monotone,++    -- * Idempotence+    idempotentL,+    idempotentR,+    idempotent,+    projective,+) where+ import Data.Connection import Data.Order import Data.Order.Property import Prelude hiding (Num (..), Ord (..), ceiling, floor) +-- Adjointness++-------------------------+ -- | \( \forall x, y : f \dashv g \Rightarrow f (x) \leq y \Leftrightarrow x \leq g (y) \) -- -- A Galois connection is an adjunction of preorders. This is a required property.-adjoint :: (Preorder a, Preorder b) => ConnK a b -> a -> b -> Bool-adjoint t a b =-    adjointL t a b-        && adjointR t a b-        && adjointL (swapL t) b a-        && adjointR (swapR t) b a- adjointL :: (Preorder a, Preorder b) => ConnL a b -> a -> b -> Bool adjointL (ConnL f g) = adjunction (<~) (<~) f g  adjointR :: (Preorder a, Preorder b) => ConnR a b -> a -> b -> Bool adjointR (ConnR f g) = adjunction (>~) (>~) g f +adjoint :: (Preorder a, Preorder b) => (forall k. Conn k a b) -> a -> b -> Bool+adjoint t a b =+    adjointL t a b+        && adjointR t a b+        && adjointL (connL t) b a+        && adjointR (connR t) b a++-- | \( \forall a: f a \leq b \Leftrightarrow a \leq g b \)+--+-- A monotone Galois connection is defined by @adjunction (<~) (<~)@,+-- while an antitone Galois connection is defined by @adjunction (>~) (<~)@.+adjunction :: Rel r Bool -> Rel s Bool -> (s -> r) -> (r -> s) -> s -> r -> Bool+adjunction (#) (%) f g a b = f a # b <=> a % g b++-- Closure++-------------------------+ -- | \( \forall x : f \dashv g \Rightarrow x \leq g \circ f (x) \) -- -- This is a required property.-closed :: (Preorder a, Preorder b) => ConnK a b -> a -> Bool-closed t a = closedL t a && closedR t a- closedL :: (Preorder a, Preorder b) => ConnL a b -> a -> Bool closedL (ConnL f g) = invertible (>~) f g  closedR :: (Preorder a, Preorder b) => ConnR a b -> a -> Bool closedR (ConnR f g) = invertible (<~) g f +closed :: (Preorder a, Preorder b) => (forall k. Conn k a b) -> a -> Bool+closed t a = closedL t a && closedR t a+ -- | \( \forall x : f \dashv g \Rightarrow x \leq g \circ f (x) \) -- -- This is a required property.-kernel :: (Preorder a, Preorder b) => ConnK a b -> b -> Bool-kernel t b = kernelL t b && kernelR t b- kernelL :: (Preorder a, Preorder b) => ConnL a b -> b -> Bool kernelL (ConnL f g) = invertible (<~) g f  kernelR :: (Preorder a, Preorder b) => ConnR a b -> b -> Bool kernelR (ConnR f g) = invertible (>~) f g +kernel :: (Preorder a, Preorder b) => (forall k. Conn k a b) -> b -> Bool+kernel t b = kernelL t b && kernelR t b++-- | \( \forall a: f (g a) \sim a \)+invertible :: Rel s b -> (s -> r) -> (r -> s) -> s -> b+invertible (#) f g a = g (f a) # a++-- Monotonicity++-------------------------+ -- | \( \forall x, y : x \leq y \Rightarrow f (x) \leq f (y) \) -- -- This is a required property.-monotonic :: (Preorder a, Preorder b) => ConnK a b -> a -> a -> b -> b -> Bool-monotonic t a1 a2 b1 b2 = monotonicL t a1 a2 b1 b2 && monotonicR t a1 a2 b1 b2- monotonicR :: (Preorder a, Preorder b) => ConnR a b -> a -> a -> b -> b -> Bool monotonicR (ConnR f g) a1 a2 b1 b2 = monotone (<~) (<~) g a1 a2 && monotone (<~) (<~) f b1 b2  monotonicL :: (Preorder a, Preorder b) => ConnL a b -> a -> a -> b -> b -> Bool monotonicL (ConnL f g) a1 a2 b1 b2 = monotone (<~) (<~) f a1 a2 && monotone (<~) (<~) g b1 b2 --- | \( \forall x: f \dashv g \Rightarrow counit \circ f (x) \sim f (x) \wedge unit \circ g (x) \sim g (x) \)------ See <https://ncatlab.org/nlab/show/idempotent+adjunction>-idempotent :: (Preorder a, Preorder b) => ConnK a b -> a -> b -> Bool-idempotent t a b = idempotentL t a b && idempotentR t a b--idempotentL :: (Preorder a, Preorder b) => ConnL a b -> a -> b -> Bool-idempotentL c@(ConnL f g) a b = projective (~~) g (upper c) b && projective (~~) f (counit c) a--idempotentR :: (Preorder a, Preorder b) => ConnR a b -> a -> b -> Bool-idempotentR c@(ConnR f g) a b = projective (~~) g (unit c) a && projective (~~) f (lower c) b-------------------------------------------------------------------------- Properties of general relations----------------------------------------------------------------------+monotonic :: (Preorder a, Preorder b) => (forall k. Conn k a b) -> a -> a -> b -> b -> Bool+monotonic t a1 a2 b1 b2 = monotonicL t a1 a2 b1 b2 && monotonicR t a1 a2 b1 b2  -- | \( \forall a, b: a \leq b \Rightarrow f(a) \leq f(b) \) monotone :: Rel r Bool -> Rel s Bool -> (r -> s) -> r -> r -> Bool monotone (#) (%) f a b = a # b ==> f a % f b --- | \( \forall a, b: a \leq b \Rightarrow f(b) \leq f(a) \)-antitone :: Rel r Bool -> Rel s Bool -> (r -> s) -> r -> r -> Bool-antitone (#) (%) f a b = a # b ==> f b % f a+-- Idempotence --- | \( \forall a: f a \leq b \Leftrightarrow a \leq g b \)+-------------------------++-- | \( \forall x: f \dashv g \Rightarrow counit \circ f (x) \sim f (x) \wedge unit \circ g (x) \sim g (x) \) ----- For example, a monotone Galois connection is defined by @adjunction (<~) (<~)@,--- and an antitone Galois connection is defined by @adjunction (>~) (<~)@.-adjunction :: Rel r Bool -> Rel s Bool -> (s -> r) -> (r -> s) -> s -> r -> Bool-adjunction (#) (%) f g a b = f a # b <=> a % g b+-- See <https://ncatlab.org/nlab/show/idempotent+adjunction>+idempotentL :: (Preorder a, Preorder b) => ConnL a b -> a -> b -> Bool+idempotentL c@(ConnL f g) a b = projective (~~) g (upper1 c id) b && projective (~~) f (ceiling1 c id) a --- | \( \forall a: f (g a) \sim a \)-invertible :: Rel s b -> (s -> r) -> (r -> s) -> s -> b-invertible (#) f g a = g (f a) # a+idempotentR :: (Preorder a, Preorder b) => ConnR a b -> a -> b -> Bool+idempotentR c@(ConnR f g) a b = projective (~~) g (floor1 c id) a && projective (~~) f (lower1 c id) b +idempotent :: (Preorder a, Preorder b) => (forall k. Conn k a b) -> a -> b -> Bool+idempotent t a b = idempotentL t a b && idempotentR t a b+ -- | \( \forall a: g \circ f (a) \sim f (a) \)------ > idempotent (#) f = projective (#) f f projective :: Rel s b -> (r -> s) -> (s -> s) -> r -> b projective (#) f g r = g (f r) # f r

@@ -2,21 +2,23 @@ {-# LANGUAGE Safe #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-}+{-# LANGUAGE ViewPatterns #-}  module Data.Connection.Ratio (     Ratio (..),     reduce,-    shiftd,+    shiftr,      -- * Rational-    ratf32,-    ratf64,     rati08,     rati16,     rati32,     rati64,     ratixx,     ratint,+    ratfix,+    ratf32,+    ratf64,      -- * Positive     posw08,@@ -27,18 +29,19 @@     posnat, ) where -import safe Data.Connection.Conn-import safe qualified Data.Connection.Float as Float+import safe Data.Connection.Conn hiding (ceiling, floor)+import safe Data.Connection.Fixed+import safe Data.Connection.Float as Float import safe Data.Int import safe Data.Order import safe Data.Order.Extended import safe Data.Order.Syntax+import safe Data.Proxy import safe Data.Ratio import safe Data.Word import safe GHC.Real (Ratio (..), Rational) import safe Numeric.Natural-import safe Prelude hiding (Ord (..), until)-import safe qualified Prelude as P+import safe Prelude hiding (Eq (..), Ord (..), until)  -- | A total version of 'GHC.Real.reduce'. reduce :: Integral a => Ratio a -> Ratio a@@ -48,74 +51,89 @@ -- | Shift by n 'units of least precision' where the ULP is determined by the denominator -- -- This is an analog of 'Data.Connection.Float.shift32' for rationals.-shiftd :: Num a => a -> Ratio a -> Ratio a-shiftd n (x :% y) = (n + x) :% y+shiftr :: Num a => a -> Ratio a -> Ratio a+shiftr n (x :% y) = (n + x) :% y  --------------------------------------------------------------------- -- Ratio Integer ---------------------------------------------------------------------  rati08 :: Conn k Rational (Extended Int8)-rati08 = signedTriple+rati08 = tripleI  rati16 :: Conn k Rational (Extended Int16)-rati16 = signedTriple+rati16 = tripleI  rati32 :: Conn k Rational (Extended Int32)-rati32 = signedTriple+rati32 = tripleI  rati64 :: Conn k Rational (Extended Int64)-rati64 = signedTriple+rati64 = tripleI  ratixx :: Conn k Rational (Extended Int)-ratixx = signedTriple+ratixx = tripleI  ratint :: Conn k Rational (Extended Integer) ratint = Conn f g h   where-    f = liftExtended (~~ ninf) (\x -> x ~~ nan || x ~~ pinf) P.ceiling+    f = liftExtended (~~ ninf) (\x -> x ~~ nan || x ~~ pinf) ceiling -    g = extended ninf pinf P.fromIntegral+    g = extended ninf pinf fromIntegral -    h = liftExtended (\x -> x ~~ nan || x ~~ ninf) (~~ pinf) P.floor+    h = liftExtended (\x -> x ~~ nan || x ~~ ninf) (~~ pinf) floor +ratfix :: forall e k. HasResolution e => Conn k Rational (Extended (Fixed e))+ratfix = Conn f' g h'+  where+    prec = resolution (Proxy :: Proxy e)++    f (reduce . (* (toRational prec)) -> n :% d) = MkFixed $ let i = n `div` d in if n `mod` d == 0 then i else i + 1++    f' = liftExtended (~~ ninf) (\x -> x ~~ nan || x ~~ pinf) f++    g = extended ninf pinf toRational++    h (reduce . (* (toRational prec)) -> n :% d) = MkFixed $ n `div` d++    h' = liftExtended (\x -> x ~~ nan || x ~~ ninf) (~~ pinf) h+ ratf32 :: Conn k Rational Float-ratf32 = Conn (toFloating f) (fromFloating g) (toFloating h)+ratf32 = Conn (toFractional f) (fromFractional g) (toFractional h)   where     f x =-        let est = P.fromRational x-         in if fromFloating g est >~ x+        let est = fromRational x+         in if fromFractional g est >~ x                 then est-                else ascendf est (fromFloating g) x+                else ascendf est (fromFractional g) x      g = flip approxRational 0      h x =-        let est = P.fromRational x-         in if fromFloating g est <~ x+        let est = fromRational x+         in if fromFractional g est <~ x                 then est-                else descendf est (fromFloating g) x+                else descendf est (fromFractional g) x      ascendf z g1 y = Float.until (\x -> g1 x >~ y) (<~) (Float.shift32 1) z      descendf z f1 x = Float.until (\y -> f1 y <~ x) (>~) (Float.shift32 (-1)) z  ratf64 :: Conn k Rational Double-ratf64 = Conn (toFloating f) (fromFloating g) (toFloating h)+ratf64 = Conn (toFractional f) (fromFractional g) (toFractional h)   where     f x =-        let est = P.fromRational x-         in if fromFloating g est >~ x+        let est = fromRational x+         in if fromFractional g est >~ x                 then est-                else ascendf est (fromFloating g) x+                else ascendf est (fromFractional g) x      g = flip approxRational 0      h x =-        let est = P.fromRational x-         in if fromFloating g est <~ x+        let est = fromRational x+         in if fromFractional g est <~ x                 then est-                else descendf est (fromFloating g) x+                else descendf est (fromFractional g) x      ascendf z g1 y = Float.until (\x -> g1 x >~ y) (<~) (Float.shift64 1) z @@ -126,28 +144,28 @@ ---------------------------------------------------------------------  posw08 :: Conn k Positive (Lowered Word8)-posw08 = unsignedTriple+posw08 = tripleW  posw16 :: Conn k Positive (Lowered Word16)-posw16 = unsignedTriple+posw16 = tripleW  posw32 :: Conn k Positive (Lowered Word32)-posw32 = unsignedTriple+posw32 = tripleW  posw64 :: Conn k Positive (Lowered Word64)-posw64 = unsignedTriple+posw64 = tripleW  poswxx :: Conn k Positive (Lowered Word)-poswxx = unsignedTriple+poswxx = tripleW  posnat :: Conn k Positive (Lowered Natural) posnat = Conn f g h   where-    f = liftEitherR (\x -> x ~~ nan || x ~~ pinf) P.ceiling+    f = liftEitherR (\x -> x ~~ nan || x ~~ pinf) ceiling -    g = either P.fromIntegral (const pinf)+    g = either fromIntegral (const pinf) -    h = liftEitherR (~~ pinf) $ \x -> if x ~~ nan then 0 else P.floor x+    h = liftEitherR (~~ pinf) $ \x -> if x ~~ nan then 0 else floor x  --------------------------------------------------------------------- -- Internal@@ -162,45 +180,45 @@ nan :: Num a => Ratio a nan = 0 :% 0 -unsignedTriple :: forall a k. (Bounded a, Integral a) => Conn k Positive (Lowered a)-unsignedTriple = Conn f g h+tripleW :: forall a k. (Bounded a, Integral a) => Conn k Positive (Lowered a)+tripleW = Conn f g h   where     f x         | x ~~ nan = Right maxBound         | x > high = Right maxBound-        | otherwise = Left $ P.ceiling x+        | otherwise = Left $ ceiling x -    g = either P.fromIntegral (const pinf)+    g = either fromIntegral (const pinf)      h x         | x ~~ nan = Left minBound         | x ~~ pinf = Right maxBound         | x > high = Left maxBound-        | otherwise = Left $ P.floor x+        | otherwise = Left $ floor x -    high = P.fromIntegral @a maxBound+    high = fromIntegral @a maxBound -signedTriple :: forall a k. (Bounded a, Integral a) => Conn k Rational (Extended a)-signedTriple = Conn f g h+tripleI :: forall a k. (Bounded a, Integral a) => Conn k Rational (Extended a)+tripleI = Conn f g h   where-    f = liftExtended (~~ ninf) (\x -> x ~~ nan || x > high) $ \x -> if x < low then minBound else P.ceiling x+    f = liftExtended (~~ ninf) (\x -> x ~~ nan || x > high) $ \x -> if x < low then minBound else ceiling x -    g = extended ninf pinf P.fromIntegral+    g = extended ninf pinf fromIntegral -    h = liftExtended (\x -> x ~~ nan || x < low) (~~ pinf) $ \x -> if x > high then maxBound else P.floor x+    h = liftExtended (\x -> x ~~ nan || x < low) (~~ pinf) $ \x -> if x > high then maxBound else floor x -    high = P.fromIntegral @a maxBound+    high = fromIntegral @a maxBound     low = -1 - high -toFloating :: Fractional a => (Rational -> a) -> Rational -> a-toFloating f x+toFractional :: Fractional a => (Rational -> a) -> Rational -> a+toFractional f x     | x ~~ nan = 0 / 0     | x ~~ ninf = (-1) / 0     | x ~~ pinf = 1 / 0     | otherwise = f x -fromFloating :: (Order a, Fractional a) => (a -> Rational) -> a -> Rational-fromFloating f x+fromFractional :: (Order a, Fractional a) => (a -> Rational) -> a -> Rational+fromFractional f x     | x ~~ 0 / 0 = nan     | x ~~ (-1) / 0 = ninf     | x ~~ 1 / 0 = pinf@@ -221,9 +239,9 @@ ratpos :: Conn k Rational Positive ratpos = Conn k f g h where -  f = liftExtended (~~ ninf) (\x -> x ~~ nan || x ~~ pinf) P.ceiling+  f = liftExtended (~~ ninf) (\x -> x ~~ nan || x ~~ pinf) ceiling -  g = extended minBound maxBound P.fromIntegral+  g = extended minBound maxBound fromIntegral -  h = liftExtended (\x -> x ~~ nan || x ~~ ninf) (~~ pinf) P.floor+  h = liftExtended (\x -> x ~~ nan || x ~~ ninf) (~~ pinf) floor -}

@@ -60,7 +60,7 @@  import safe Data.Bifunctor (bimap) import safe Data.Bool hiding (not)-import safe Data.Connection.Class+import safe Data.Connection.Class hiding ((/\), (\/)) import safe Data.Connection.Conn import safe Data.Either import safe Data.Int@@ -72,7 +72,7 @@ import safe Data.Order.Syntax import safe qualified Data.Set as Set import safe Data.Word-import safe Prelude hiding (Eq (..), Ord (..), not)+import safe Prelude hiding (Eq (..), Ord (..), ceiling, floor, not) import safe qualified Prelude as P  -------------------------------------------------------------------------------@@ -161,31 +161,31 @@  -- | Lattice meet. ----- > (/\) = curry $ floorWith semilattice+-- > (/\) = curry $ floor semilattice (/\) :: Meet a => a -> a -> a-(/\) = curry $ floorWith semilattice+(/\) = curry $ floor semilattice  -- | The unique top element of a bounded lattice -- -- > x /\ top = x -- > x \/ top = top top :: Meet a => a-top = floorWith bounded ()+top = floor bounded ()  infixr 5 \/  -- | Lattice join. ----- > (\/) = curry $ ceilingWith semilattice+-- > (\/) = curry $ lower semilattice (\/) :: Join a => a -> a -> a-(\/) = curry $ ceilingWith semilattice+(\/) = curry $ ceiling semilattice  -- | The unique bottom element of a bounded lattice -- -- > x /\ bottom = bottom -- > x \/ bottom = x bottom :: Join a => a-bottom = ceilingWith bounded ()+bottom = ceiling bounded ()  ------------------------------------------------------------------------------- -- Heyting algebras@@ -278,7 +278,7 @@ -- >>> True // True -- True (//) :: Algebra 'R a => a -> a -> a-(//) = floorWith . algebra+(//) = floor . algebra  -- | Intuitionistic equivalence. --@@ -363,7 +363,7 @@ -- >>> [GT,EQ] \\ [LT] -- fromList [EQ,GT] (\\) :: Algebra 'L a => a -> a -> a-(\\) = flip $ ceilingWith . algebra+(\\) = flip $ ceiling . algebra  -- | Intuitionistic co-equivalence. equiv :: Algebra 'L a => a -> a -> a@@ -513,7 +513,6 @@     not LT = GT     not EQ = EQ     not GT = LT-instance Boolean Ordering  instance Semilattice k Word8 instance Algebra 'L Word8 where algebra = coheyting impliesL@@ -678,7 +677,7 @@      semilattice = ConnL f fork       where-        f = uncurry $ Map.unionWith (curry $ ceilingWith semilattice)+        f = uncurry $ Map.unionWith (curry $ ceiling semilattice)  instance (Total k, Join a) => Algebra 'L (Map.Map k a) where     algebra = coheyting (Map.\\)@@ -688,7 +687,7 @@      semilattice = ConnL f fork       where-        f = uncurry $ IntMap.unionWith (curry $ ceilingWith semilattice)+        f = uncurry $ IntMap.unionWith (curry $ ceiling semilattice)  instance (Join a) => Algebra 'L (IntMap.IntMap a) where     algebra = coheyting (IntMap.\\)

@@ -36,6 +36,7 @@ import safe Data.Complex import safe Data.Either import safe qualified Data.Eq as Eq+import safe Data.Fixed import safe Data.Functor.Identity import safe Data.Int import safe qualified Data.IntMap as IntMap@@ -287,7 +288,20 @@ deriving via (Base Int64) instance Preorder Int64 deriving via (Base Integer) instance Preorder Integer ---TODO move to Order and derive Preorder as well+deriving via (Base (Fixed e)) instance Preorder (Fixed e)++-- | An < https://en.wikipedia.org/wiki/Modular_lattice#Examples /N5/ > lattice.+--+--  A non-modular lattice formed by the < https://en.wikipedia.org/wiki/Extended_real_number_line affine extended >+--  reals along with a /NaN/ value that is incomparable to any finite number, i.e.:+--+--  > pcompare (N5 NaN) (N5 x) = pcompare (N5 x) (N5 NaN) = Nothing+--+--  for any finite /x/.+--+--  > N5 NaN == N5 NaN = True+--  > N5 NaN < N5 (1/0) = True+--  > N5 NaN > N5 (-1/0) = True newtype N5 a = N5 {getN5 :: a}     deriving stock (Eq, Show, Functor)     deriving (Applicative) via Identity

@@ -11,6 +11,7 @@ import Data.Lattice import Data.Int import Data.Word+import Data.Fixed import Data.Order import Data.Order.Extended import Data.Order.Interval@@ -53,9 +54,11 @@ f64 = gen_flt $ G.double rd  rat :: Gen (Ratio Integer)-rat = G.frequency [(49, gen), (1, G.element [-1 :% 0, 1 :% 0, 0 :% 0])]-  where gen = G.realFrac_ (R.linearFracFrom 0 (- 2^127) (2^127))+rat = G.realFrac_ $ R.linearFracFrom 0 (- 2^(127 :: Integer)) (2^(127 :: Integer)) +rat' :: Gen (Ratio Integer)+rat' = G.frequency [(49, rat), (1, G.element [-1 :% 0, 1 :% 0, 0 :% 0])]+ pos :: Gen (Ratio Natural) pos = G.frequency [(49, gen), (1, G.element [1 :% 0, 0 :% 0])]   where gen = G.realFrac_ (R.linearFracFrom 0 0 (2^127))@@ -85,8 +88,8 @@   x' <- forAll f32   o <- forAll ord   o' <- forAll ord-  r <- forAll rat-  r' <- forAll rat+  r <- forAll rat'+  r' <- forAll rat'    assert $ Prop.adjoint (conn @_ @() @Ordering) () o   assert $ Prop.closed (conn @_ @() @Ordering) ()

@@ -0,0 +1,153 @@+{-# LANGUAGE TemplateHaskell #-}++module Test.Data.Connection.Fixed where++import Data.Connection.Fixed+import qualified Data.Connection.Property as Prop+import Hedgehog+import qualified Hedgehog.Gen as G+import Test.Data.Connection++fxx :: Gen (Fixed k)+fxx = MkFixed <$> G.integral ri'++prop_connections_micro :: Property+prop_connections_micro = withTests 1000 . property $ do+    f00 <- forAll fxx+    f01 <- forAll fxx+    f02 <- forAll fxx+    f03 <- forAll fxx+    f06 <- forAll fxx++    f00' <- forAll fxx+    f01' <- forAll fxx+    f02' <- forAll fxx+    f03' <- forAll fxx+    f06' <- forAll fxx++    assert $ Prop.adjoint f06f00 f06 f00+    assert $ Prop.closed f06f00 f06+    assert $ Prop.kernel f06f00 f00+    assert $ Prop.monotonic f06f00 f06 f06' f00 f00'+    assert $ Prop.idempotent f06f00 f06 f00++    assert $ Prop.adjoint f06f01 f06 f01+    assert $ Prop.closed f06f01 f06+    assert $ Prop.kernel f06f01 f01+    assert $ Prop.monotonic f06f01 f06 f06' f01 f01'+    assert $ Prop.idempotent f06f01 f06 f01++    assert $ Prop.adjoint f06f02 f06 f02+    assert $ Prop.closed f06f02 f06+    assert $ Prop.kernel f06f02 f02+    assert $ Prop.monotonic f06f02 f06 f06' f02 f02'+    assert $ Prop.idempotent f06f02 f06 f02++    assert $ Prop.adjoint f06f03 f06 f03+    assert $ Prop.closed f06f03 f06+    assert $ Prop.kernel f06f03 f03+    assert $ Prop.monotonic f06f03 f06 f06' f03 f03'+    assert $ Prop.idempotent f06f03 f06 f03++prop_connections_nano :: Property+prop_connections_nano = withTests 1000 . property $ do+    f00 <- forAll fxx+    f01 <- forAll fxx+    f02 <- forAll fxx+    f03 <- forAll fxx+    f06 <- forAll fxx+    f09 <- forAll fxx++    f00' <- forAll fxx+    f01' <- forAll fxx+    f02' <- forAll fxx+    f03' <- forAll fxx+    f06' <- forAll fxx+    f09' <- forAll fxx++    assert $ Prop.adjoint f09f00 f09 f00+    assert $ Prop.closed f09f00 f09+    assert $ Prop.kernel f09f00 f00+    assert $ Prop.monotonic f09f00 f09 f09' f00 f00'+    assert $ Prop.idempotent f09f00 f09 f00++    assert $ Prop.adjoint f09f01 f09 f01+    assert $ Prop.closed f09f01 f09+    assert $ Prop.kernel f09f01 f01+    assert $ Prop.monotonic f09f01 f09 f09' f01 f01'+    assert $ Prop.idempotent f09f01 f09 f01++    assert $ Prop.adjoint f09f02 f09 f02+    assert $ Prop.closed f09f02 f09+    assert $ Prop.kernel f09f02 f02+    assert $ Prop.monotonic f09f02 f09 f09' f02 f02'+    assert $ Prop.idempotent f09f02 f09 f02++    assert $ Prop.adjoint f09f03 f09 f03+    assert $ Prop.closed f09f03 f09+    assert $ Prop.kernel f09f03 f03+    assert $ Prop.monotonic f09f03 f09 f09' f03 f03'+    assert $ Prop.idempotent f09f03 f09 f03++    assert $ Prop.adjoint f09f06 f09 f06+    assert $ Prop.closed f09f06 f09+    assert $ Prop.kernel f09f06 f06+    assert $ Prop.monotonic f09f06 f09 f09' f06 f06'+    assert $ Prop.idempotent f09f06 f09 f06++prop_connections_pico :: Property+prop_connections_pico = withTests 1000 . property $ do+    f00 <- forAll fxx+    f01 <- forAll fxx+    f02 <- forAll fxx+    f03 <- forAll fxx+    f06 <- forAll fxx+    f09 <- forAll fxx+    f12 <- forAll fxx++    f00' <- forAll fxx+    f01' <- forAll fxx+    f02' <- forAll fxx+    f03' <- forAll fxx+    f06' <- forAll fxx+    f09' <- forAll fxx+    f12' <- forAll fxx++    assert $ Prop.adjoint f12f00 f12 f00+    assert $ Prop.closed f12f00 f12+    assert $ Prop.kernel f12f00 f00+    assert $ Prop.monotonic f12f00 f12 f12' f00 f00'+    assert $ Prop.idempotent f12f00 f12 f00++    assert $ Prop.adjoint f12f01 f12 f01+    assert $ Prop.closed f12f01 f12+    assert $ Prop.kernel f12f01 f01+    assert $ Prop.monotonic f12f01 f12 f12' f01 f01'+    assert $ Prop.idempotent f12f01 f12 f01++    assert $ Prop.adjoint f12f02 f12 f02+    assert $ Prop.closed f12f02 f12+    assert $ Prop.kernel f12f02 f02+    assert $ Prop.monotonic f12f02 f12 f12' f02 f02'+    assert $ Prop.idempotent f12f02 f12 f02++    assert $ Prop.adjoint f12f03 f12 f03+    assert $ Prop.closed f12f03 f12+    assert $ Prop.kernel f12f03 f03+    assert $ Prop.monotonic f12f03 f12 f12' f03 f03'+    assert $ Prop.idempotent f12f03 f12 f03++    assert $ Prop.adjoint f12f06 f12 f06+    assert $ Prop.closed f12f06 f12+    assert $ Prop.kernel f12f06 f06+    assert $ Prop.monotonic f12f06 f12 f12' f06 f06'+    assert $ Prop.idempotent f12f06 f12 f06++    assert $ Prop.adjoint f12f09 f12 f09+    assert $ Prop.closed f12f09 f12+    assert $ Prop.kernel f12f09 f09+    assert $ Prop.monotonic f12f09 f12 f12' f09 f09'+    assert $ Prop.idempotent f12f09 f12 f09++tests :: IO Bool+tests = checkParallel $$(discover)

@@ -1,93 +1,188 @@ {-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE ViewPatterns #-}+ module Test.Data.Connection.Float where  import Data.Connection.Conn import Data.Connection.Float+import Data.Fixed import Data.Int-import Hedgehog-import Prelude hiding (Ord(..),Bounded, until)-import Test.Data.Connection+import Data.Order+ import qualified Data.Connection.Property as Prop+import Hedgehog import qualified Hedgehog.Gen as G-+import Test.Data.Connection  prop_connection_f32i08 :: Property prop_connection_f32i08 = withTests 1000 . property $ do-  x <- forAll f32-  x' <- forAll f32-  y <- forAll $ gen_extended $ G.integral (ri @Int8)-  y' <- forAll $ gen_extended $ G.integral (ri @Int8)+    x <- forAll f32+    x' <- forAll f32+    y <- forAll $ gen_extended $ G.integral (ri @Int8)+    y' <- forAll $ gen_extended $ G.integral (ri @Int8) -  assert $ Prop.adjoint (f32i08) x y-  assert $ Prop.closed (f32i08) x-  assert $ Prop.kernel (f32i08) y-  assert $ Prop.monotonic (f32i08) x x' y y'-  assert $ Prop.idempotent (f32i08) x y+    assert $ Prop.adjoint f32i08 x y+    assert $ Prop.closed f32i08 x+    assert $ Prop.kernel f32i08 y+    assert $ Prop.monotonic f32i08 x x' y y'+    assert $ Prop.idempotent f32i08 x y  prop_connection_f32i16 :: Property prop_connection_f32i16 = withTests 1000 . property $ do-  x <- forAll f32-  x' <- forAll f32-  y <- forAll $ gen_extended $ G.integral (ri @Int16)-  y' <- forAll $ gen_extended $ G.integral (ri @Int16)+    x <- forAll f32+    x' <- forAll f32+    y <- forAll $ gen_extended $ G.integral (ri @Int16)+    y' <- forAll $ gen_extended $ G.integral (ri @Int16) -  assert $ Prop.adjoint (f32i16) x y-  assert $ Prop.closed (f32i16) x-  assert $ Prop.kernel (f32i16) y-  assert $ Prop.monotonic (f32i16) x x' y y'-  assert $ Prop.idempotent (f32i16) x y+    assert $ Prop.adjoint f32i16 x y+    assert $ Prop.closed f32i16 x+    assert $ Prop.kernel f32i16 y+    assert $ Prop.monotonic f32i16 x x' y y'+    assert $ Prop.idempotent f32i16 x y +prop_connection_f32i32 :: Property+prop_connection_f32i32 = withTests 1000 . property $ do+    x <- forAll f32+    x' <- forAll f32+    y <- forAll $ gen_extended $ G.integral (ri @Int32)+    y' <- forAll $ gen_extended $ G.integral (ri @Int32)++    assert $ Prop.adjointL f32i32 x y+    assert $ Prop.closedL f32i32 x+    assert $ Prop.kernelL f32i32 y+    assert $ Prop.monotonicL f32i32 x x' y y'+    assert $ Prop.idempotentL f32i32 x y++prop_connection_f32i64 :: Property+prop_connection_f32i64 = withTests 1000 . property $ do+    x <- forAll f32+    x' <- forAll f32+    y <- forAll $ gen_extended $ G.integral (ri @Int64)+    y' <- forAll $ gen_extended $ G.integral (ri @Int64)++    assert $ Prop.adjointL f32i64 x y+    assert $ Prop.closedL f32i64 x+    assert $ Prop.kernelL f32i64 y+    assert $ Prop.monotonicL f32i64 x x' y y'+    assert $ Prop.idempotentL f32i64 x y++prop_connection_f32ixx :: Property+prop_connection_f32ixx = withTests 1000 . property $ do+    x <- forAll f32+    x' <- forAll f32+    y <- forAll $ gen_extended $ G.integral (ri @Int)+    y' <- forAll $ gen_extended $ G.integral (ri @Int)++    assert $ Prop.adjointL f32ixx x y+    assert $ Prop.closedL f32ixx x+    assert $ Prop.kernelL f32ixx y+    assert $ Prop.monotonicL f32ixx x x' y y'+    assert $ Prop.idempotentL f32ixx x y++prop_connection_f32int :: Property+prop_connection_f32int = withTests 1000 . property $ do+    x <- forAll f32+    x' <- forAll f32+    y <- forAll $ gen_extended $ G.integral ri'+    y' <- forAll $ gen_extended $ G.integral ri'++    assert $ Prop.adjointL f32int x y+    assert $ Prop.closedL f32int x+    assert $ Prop.kernelL f32int y+    assert $ Prop.monotonicL f32int x x' y y'+    assert $ Prop.idempotentL f32int x y+ prop_connection_f64i08 :: Property prop_connection_f64i08 = withTests 1000 . property $ do-  x <- forAll f64-  x' <- forAll f64-  y <- forAll $ gen_extended $ G.integral (ri @Int8)-  y' <- forAll $ gen_extended $ G.integral (ri @Int8)+    x <- forAll f64+    x' <- forAll f64+    y <- forAll $ gen_extended $ G.integral (ri @Int8)+    y' <- forAll $ gen_extended $ G.integral (ri @Int8) -  assert $ Prop.adjoint (f64i08) x y-  assert $ Prop.closed (f64i08) x-  assert $ Prop.kernel (f64i08) y-  assert $ Prop.monotonic (f64i08) x x' y y'-  assert $ Prop.idempotent (f64i08) x y+    assert $ Prop.adjoint f64i08 x y+    assert $ Prop.closed f64i08 x+    assert $ Prop.kernel f64i08 y+    assert $ Prop.monotonic f64i08 x x' y y'+    assert $ Prop.idempotent f64i08 x y  prop_connection_f64i16 :: Property prop_connection_f64i16 = withTests 1000 . property $ do-  x <- forAll f64-  x' <- forAll f64-  y <- forAll $ gen_extended $ G.integral (ri @Int16)-  y' <- forAll $ gen_extended $ G.integral (ri @Int16)+    x <- forAll f64+    x' <- forAll f64+    y <- forAll $ gen_extended $ G.integral (ri @Int16)+    y' <- forAll $ gen_extended $ G.integral (ri @Int16) -  assert $ Prop.adjoint (f64i16) x y-  assert $ Prop.closed (f64i16) x-  assert $ Prop.kernel (f64i16) y-  assert $ Prop.monotonic (f64i16) x x' y y'-  assert $ Prop.idempotent (f64i16) x y+    assert $ Prop.adjoint f64i16 x y+    assert $ Prop.closed f64i16 x+    assert $ Prop.kernel f64i16 y+    assert $ Prop.monotonic f64i16 x x' y y'+    assert $ Prop.idempotent f64i16 x y  prop_connection_f64i32 :: Property prop_connection_f64i32 = withTests 1000 . property $ do-  x <- forAll f64-  x' <- forAll f64-  y <- forAll $ gen_extended $ G.integral (ri @Int32)-  y' <- forAll $ gen_extended $ G.integral (ri @Int32)+    x <- forAll f64+    x' <- forAll f64+    y <- forAll $ gen_extended $ G.integral (ri @Int32)+    y' <- forAll $ gen_extended $ G.integral (ri @Int32) -  assert $ Prop.adjoint (f64i32) x y-  assert $ Prop.closed (f64i32) x-  assert $ Prop.kernel (f64i32) y-  assert $ Prop.monotonic (f64i32) x x' y y'-  assert $ Prop.idempotent (f64i32) x y+    assert $ Prop.adjoint f64i32 x y+    assert $ Prop.closed f64i32 x+    assert $ Prop.kernel f64i32 y+    assert $ Prop.monotonic f64i32 x x' y y'+    assert $ Prop.idempotent f64i32 x y +prop_connection_f64i64 :: Property+prop_connection_f64i64 = withTests 1000 . property $ do+    x <- forAll f64+    x' <- forAll f64+    y <- forAll $ gen_extended $ G.integral (ri @Int64)+    y' <- forAll $ gen_extended $ G.integral (ri @Int64)++    assert $ Prop.adjointL f64i64 x y+    assert $ Prop.closedL f64i64 x+    assert $ Prop.kernelL f64i64 y+    assert $ Prop.monotonicL f64i64 x x' y y'+    assert $ Prop.idempotentL f64i64 x y++prop_connection_f64ixx :: Property+prop_connection_f64ixx = withTests 1000 . property $ do+    x <- forAll f64+    x' <- forAll f64+    y <- forAll $ gen_extended $ G.integral (ri @Int)+    y' <- forAll $ gen_extended $ G.integral (ri @Int)++    assert $ Prop.adjointL f64ixx x y+    assert $ Prop.closedL f64ixx x+    assert $ Prop.kernelL f64ixx y+    assert $ Prop.monotonicL f64ixx x x' y y'+    assert $ Prop.idempotentL f64ixx x y++prop_connection_f64int :: Property+prop_connection_f64int = withTests 1000 . property $ do+    x <- forAll f64+    x' <- forAll f64+    y <- forAll $ gen_extended $ G.integral ri'+    y' <- forAll $ gen_extended $ G.integral ri'++    assert $ Prop.adjointL f64int x y+    assert $ Prop.closedL f64int x+    assert $ Prop.kernelL f64int y+    assert $ Prop.monotonicL f64int x x' y y'+    assert $ Prop.idempotentL f64int x y+ prop_connection_f64f32 :: Property prop_connection_f64f32 = withTests 1000 . property $ do-  x <- forAll f64-  x' <- forAll f64-  y <- forAll f32-  y' <- forAll f32+    x <- forAll f64+    x' <- forAll f64+    y <- forAll f32+    y' <- forAll f32 -  assert $ Prop.adjoint (f64f32) x y-  assert $ Prop.closed (f64f32) x-  assert $ Prop.kernel (f64f32) y-  assert $ Prop.monotonic (f64f32) x x' y y'-  assert $ Prop.idempotent (f64f32) x y+    assert $ Prop.adjoint (f64f32) x y+    assert $ Prop.closed (f64f32) x+    assert $ Prop.kernel (f64f32) y+    assert $ Prop.monotonic (f64f32) x x' y y'+    assert $ Prop.idempotent (f64f32) x y  tests :: IO Bool tests = checkParallel $$(discover)

@@ -1,170 +1,218 @@ {-# LANGUAGE TemplateHaskell #-}-{-# Language AllowAmbiguousTypes #-}+{-# LANGUAGE TypeApplications #-}+ module Test.Data.Connection.Ratio where +import qualified Data.Connection.Property as Prop+import Data.Connection.Ratio+import Data.Fixed import Data.Int+import Data.Order.Extended import Data.Word-import Data.Connection.Ratio+import GHC.Real hiding (Fractional (..), div, (^), (^^)) import Hedgehog-import Test.Data.Connection-import qualified Data.Connection.Property as Prop import qualified Hedgehog.Gen as G+import qualified Hedgehog.Range as R+import Numeric.Natural+import Test.Data.Connection +fxx :: Gen (Extended (Fixed k))+fxx = gen_extended $ MkFixed <$> G.integral ri'++prop_connection_ratf06 :: Property+prop_connection_ratf06 = withTests 1000 . property $ do+    x <- forAll rat+    x' <- forAll rat+    y <- forAll fxx+    y' <- forAll fxx++    assert $ Prop.adjoint (ratfix @E6) x y+    assert $ Prop.closed (ratfix @E6) x+    assert $ Prop.kernel (ratfix @E6) y+    assert $ Prop.monotonic (ratfix @E6) x x' y y'+    assert $ Prop.idempotent (ratfix @E6) x y++prop_connection_ratf09 :: Property+prop_connection_ratf09 = withTests 1000 . property $ do+    x <- forAll rat+    x' <- forAll rat+    y <- forAll fxx+    y' <- forAll fxx++    assert $ Prop.adjoint (ratfix @E9) x y+    assert $ Prop.closed (ratfix @E9) x+    assert $ Prop.kernel (ratfix @E9) y+    assert $ Prop.monotonic (ratfix @E9) x x' y y'+    assert $ Prop.idempotent (ratfix @E9) x y++prop_connection_ratf12 :: Property+prop_connection_ratf12 = withTests 1000 . property $ do+    x <- forAll rat+    x' <- forAll rat+    y <- forAll fxx+    y' <- forAll fxx++    assert $ Prop.adjoint (ratfix @E12) x y+    assert $ Prop.closed (ratfix @E12) x+    assert $ Prop.kernel (ratfix @E12) y+    assert $ Prop.monotonic (ratfix @E12) x x' y y'+    assert $ Prop.idempotent (ratfix @E12) x y+ prop_connection_ratf32 :: Property prop_connection_ratf32 = withTests 1000 . property $ do-  x <- forAll rat-  x' <- forAll rat-  y <- forAll f32-  y' <- forAll f32+    x <- forAll rat'+    x' <- forAll rat'+    y <- forAll f32+    y' <- forAll f32 -  assert $ Prop.adjoint (ratf32) x y-  assert $ Prop.closed (ratf32) x-  assert $ Prop.kernel (ratf32) y-  assert $ Prop.monotonic (ratf32) x x' y y'-  assert $ Prop.idempotent (ratf32) x y+    assert $ Prop.adjoint (ratf32) x y+    assert $ Prop.closed (ratf32) x+    assert $ Prop.kernel (ratf32) y+    assert $ Prop.monotonic (ratf32) x x' y y'+    assert $ Prop.idempotent (ratf32) x y  prop_connection_ratf64 :: Property prop_connection_ratf64 = withTests 1000 . property $ do-  x <- forAll rat-  x' <- forAll rat-  y <- forAll f64-  y' <- forAll f64+    x <- forAll rat'+    x' <- forAll rat'+    y <- forAll f64+    y' <- forAll f64 -  assert $ Prop.adjoint (ratf64) x y-  assert $ Prop.closed (ratf64) x-  assert $ Prop.kernel (ratf64) y-  assert $ Prop.monotonic (ratf64) x x' y y'-  assert $ Prop.idempotent (ratf64) x y+    assert $ Prop.adjoint (ratf64) x y+    assert $ Prop.closed (ratf64) x+    assert $ Prop.kernel (ratf64) y+    assert $ Prop.monotonic (ratf64) x x' y y'+    assert $ Prop.idempotent (ratf64) x y  prop_connection_rati08 :: Property prop_connection_rati08 = withTests 1000 . property $ do-  x <- forAll rat-  x' <- forAll rat-  y <- forAll $ gen_extended $ G.integral (ri @Int8)-  y' <- forAll $ gen_extended $ G.integral (ri @Int8)+    x <- forAll rat'+    x' <- forAll rat'+    y <- forAll $ gen_extended $ G.integral (ri @Int8)+    y' <- forAll $ gen_extended $ G.integral (ri @Int8) -  assert $ Prop.adjoint (rati08) x y-  assert $ Prop.closed (rati08) x-  assert $ Prop.kernel (rati08) y-  assert $ Prop.monotonic (rati08) x x' y y'-  assert $ Prop.idempotent (rati08) x y+    assert $ Prop.adjoint (rati08) x y+    assert $ Prop.closed (rati08) x+    assert $ Prop.kernel (rati08) y+    assert $ Prop.monotonic (rati08) x x' y y'+    assert $ Prop.idempotent (rati08) x y  prop_connection_rati16 :: Property prop_connection_rati16 = withTests 1000 . property $ do-  x <- forAll rat-  x' <- forAll rat-  y <- forAll $ gen_extended $ G.integral (ri @Int16)-  y' <- forAll $ gen_extended $ G.integral (ri @Int16)+    x <- forAll rat'+    x' <- forAll rat'+    y <- forAll $ gen_extended $ G.integral (ri @Int16)+    y' <- forAll $ gen_extended $ G.integral (ri @Int16) -  assert $ Prop.adjoint (rati16) x y-  assert $ Prop.closed (rati16) x-  assert $ Prop.kernel (rati16) y-  assert $ Prop.monotonic (rati16) x x' y y'-  assert $ Prop.idempotent (rati16) x y+    assert $ Prop.adjoint (rati16) x y+    assert $ Prop.closed (rati16) x+    assert $ Prop.kernel (rati16) y+    assert $ Prop.monotonic (rati16) x x' y y'+    assert $ Prop.idempotent (rati16) x y  prop_connection_rati32 :: Property prop_connection_rati32 = withTests 1000 . property $ do-  x <- forAll rat-  x' <- forAll rat-  y <- forAll $ gen_extended $ G.integral (ri @Int32)-  y' <- forAll $ gen_extended $ G.integral (ri @Int32)+    x <- forAll rat'+    x' <- forAll rat'+    y <- forAll $ gen_extended $ G.integral (ri @Int32)+    y' <- forAll $ gen_extended $ G.integral (ri @Int32) -  assert $ Prop.adjoint (rati32) x y-  assert $ Prop.closed (rati32) x-  assert $ Prop.kernel (rati32) y-  assert $ Prop.monotonic (rati32) x x' y y'-  assert $ Prop.idempotent (rati32) x y+    assert $ Prop.adjoint (rati32) x y+    assert $ Prop.closed (rati32) x+    assert $ Prop.kernel (rati32) y+    assert $ Prop.monotonic (rati32) x x' y y'+    assert $ Prop.idempotent (rati32) x y  prop_connection_rati64 :: Property prop_connection_rati64 = withTests 1000 . property $ do-  x <- forAll rat-  x' <- forAll rat-  y <- forAll $ gen_extended $ G.integral (ri @Int64)-  y' <- forAll $ gen_extended $ G.integral (ri @Int64)+    x <- forAll rat'+    x' <- forAll rat'+    y <- forAll $ gen_extended $ G.integral (ri @Int64)+    y' <- forAll $ gen_extended $ G.integral (ri @Int64) -  assert $ Prop.adjoint (rati64) x y-  assert $ Prop.closed (rati64) x-  assert $ Prop.kernel (rati64) y-  assert $ Prop.monotonic (rati64) x x' y y'-  assert $ Prop.idempotent (rati64) x y+    assert $ Prop.adjoint (rati64) x y+    assert $ Prop.closed (rati64) x+    assert $ Prop.kernel (rati64) y+    assert $ Prop.monotonic (rati64) x x' y y'+    assert $ Prop.idempotent (rati64) x y  prop_connection_ratint :: Property prop_connection_ratint = withTests 1000 . property $ do-  x <- forAll rat-  x' <- forAll rat-  y <- forAll $ gen_extended $ G.integral ri'-  y' <- forAll $ gen_extended $ G.integral ri'+    x <- forAll rat'+    x' <- forAll rat'+    y <- forAll $ gen_extended $ G.integral ri'+    y' <- forAll $ gen_extended $ G.integral ri' -  assert $ Prop.adjoint (ratint) x y-  assert $ Prop.closed (ratint) x-  assert $ Prop.kernel (ratint) y-  assert $ Prop.monotonic (ratint) x x' y y'-  assert $ Prop.idempotent (ratint) x y+    assert $ Prop.adjoint (ratint) x y+    assert $ Prop.closed (ratint) x+    assert $ Prop.kernel (ratint) y+    assert $ Prop.monotonic (ratint) x x' y y'+    assert $ Prop.idempotent (ratint) x y  prop_connection_posw08 :: Property prop_connection_posw08 = withTests 1000 . property $ do-  x <- forAll pos-  x' <- forAll pos-  y <- forAll $ gen_lowered $ G.integral (ri @Word8)-  y' <- forAll $ gen_lowered $ G.integral (ri @Word8)+    x <- forAll pos+    x' <- forAll pos+    y <- forAll $ gen_lowered $ G.integral (ri @Word8)+    y' <- forAll $ gen_lowered $ G.integral (ri @Word8) -  assert $ Prop.adjoint (posw08) x y-  assert $ Prop.closed (posw08) x-  assert $ Prop.kernel (posw08) y-  assert $ Prop.monotonic (posw08) x x' y y'-  assert $ Prop.idempotent (posw08) x y+    assert $ Prop.adjoint (posw08) x y+    assert $ Prop.closed (posw08) x+    assert $ Prop.kernel (posw08) y+    assert $ Prop.monotonic (posw08) x x' y y'+    assert $ Prop.idempotent (posw08) x y  prop_connection_posw16 :: Property prop_connection_posw16 = withTests 1000 . property $ do-  x <- forAll pos-  x' <- forAll pos-  y <- forAll $ gen_lowered $ G.integral (ri @Word16)-  y' <- forAll $ gen_lowered $ G.integral (ri @Word16)+    x <- forAll pos+    x' <- forAll pos+    y <- forAll $ gen_lowered $ G.integral (ri @Word16)+    y' <- forAll $ gen_lowered $ G.integral (ri @Word16) -  assert $ Prop.adjoint (posw16) x y-  assert $ Prop.closed (posw16) x-  assert $ Prop.kernel (posw16) y-  assert $ Prop.monotonic (posw16) x x' y y'-  assert $ Prop.idempotent (posw16) x y+    assert $ Prop.adjoint (posw16) x y+    assert $ Prop.closed (posw16) x+    assert $ Prop.kernel (posw16) y+    assert $ Prop.monotonic (posw16) x x' y y'+    assert $ Prop.idempotent (posw16) x y  prop_connection_posw32 :: Property prop_connection_posw32 = withTests 1000 . property $ do-  x <- forAll pos-  x' <- forAll pos-  y <- forAll $ gen_lowered $ G.integral (ri @Word32)-  y' <- forAll $ gen_lowered $ G.integral (ri @Word32)+    x <- forAll pos+    x' <- forAll pos+    y <- forAll $ gen_lowered $ G.integral (ri @Word32)+    y' <- forAll $ gen_lowered $ G.integral (ri @Word32) -  assert $ Prop.adjoint (posw32) x y-  assert $ Prop.closed (posw32) x-  assert $ Prop.kernel (posw32) y-  assert $ Prop.monotonic (posw32) x x' y y'-  assert $ Prop.idempotent (posw32) x y+    assert $ Prop.adjoint (posw32) x y+    assert $ Prop.closed (posw32) x+    assert $ Prop.kernel (posw32) y+    assert $ Prop.monotonic (posw32) x x' y y'+    assert $ Prop.idempotent (posw32) x y  prop_connection_posw64 :: Property prop_connection_posw64 = withTests 1000 . property $ do-  x <- forAll pos-  x' <- forAll pos-  y <- forAll $ gen_lowered $ G.integral (ri @Word64)-  y' <- forAll $ gen_lowered $ G.integral (ri @Word64)+    x <- forAll pos+    x' <- forAll pos+    y <- forAll $ gen_lowered $ G.integral (ri @Word64)+    y' <- forAll $ gen_lowered $ G.integral (ri @Word64) -  assert $ Prop.adjoint (posw64) x y-  assert $ Prop.closed (posw64) x-  assert $ Prop.kernel (posw64) y-  assert $ Prop.monotonic (posw64) x x' y y'-  assert $ Prop.idempotent (posw64) x y+    assert $ Prop.adjoint (posw64) x y+    assert $ Prop.closed (posw64) x+    assert $ Prop.kernel (posw64) y+    assert $ Prop.monotonic (posw64) x x' y y'+    assert $ Prop.idempotent (posw64) x y  prop_connection_posnat :: Property prop_connection_posnat = withTests 1000 . property $ do-  x <- forAll pos-  x' <- forAll pos-  y <- forAll $ gen_lowered $ G.integral rn-  y' <- forAll $ gen_lowered $ G.integral rn+    x <- forAll pos+    x' <- forAll pos+    y <- forAll $ gen_lowered $ G.integral rn+    y' <- forAll $ gen_lowered $ G.integral rn -  assert $ Prop.adjoint (posnat) x y-  assert $ Prop.closed (posnat) x-  assert $ Prop.kernel (posnat) y-  assert $ Prop.monotonic (posnat) x x' y y'-  assert $ Prop.idempotent (posnat) x y+    assert $ Prop.adjoint (posnat) x y+    assert $ Prop.closed (posnat) x+    assert $ Prop.kernel (posnat) y+    assert $ Prop.monotonic (posnat) x x' y y'+    assert $ Prop.idempotent (posnat) x y  tests :: IO Bool tests = checkParallel $$(discover)

@@ -250,10 +250,10 @@  prop_order_rat :: Property prop_order_rat = withTests 1000 . property $ do-  x <- forAll rat-  y <- forAll rat-  z <- forAll rat-  w <- forAll rat+  x <- forAll rat'+  y <- forAll rat'+  z <- forAll rat'+  w <- forAll rat'   assert $ Prop.preorder x y   assert $ Prop.order z w   assert $ Prop.reflexive_eq x

@@ -3,6 +3,7 @@ import System.IO (BufferMode (..), hSetBuffering, stderr, stdout)  import qualified Test.Data.Connection as C+import qualified Test.Data.Connection.Fixed as CX import qualified Test.Data.Connection.Float as CF import qualified Test.Data.Connection.Int as CI import qualified Test.Data.Connection.Ratio as CR@@ -19,6 +20,7 @@         , CI.tests         , CW.tests         , CF.tests+        , CX.tests         , CR.tests         ]