connections 0.1.0 → 0.2.0

raw patch · 25 files changed

+3608/−3735 lines, 25 filesdep +doctestdep −finite-typelitsdep −transformersdep −universe-basedep ~basenew-component:exe:doctestPVP ok

version bump matches the API change (PVP)

Dependencies added: doctest

Dependencies removed: finite-typelits, transformers, universe-base

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• ChangeLog.md +17/−2
• connections.cabal +21/−14
• src/Data/Connection.hs +4/−182
• src/Data/Connection/Class.hs +705/−814
• src/Data/Connection/Conn.hs +363/−208
• src/Data/Connection/Double.hs +0/−322
• src/Data/Connection/Float.hs +249/−136
• src/Data/Connection/Int.hs +122/−123
• src/Data/Connection/Property.hs +19/−38
• src/Data/Connection/Ratio.hs +140/−133
• src/Data/Connection/Word.hs +141/−101
• src/Data/Lattice.hs +517/−388
• src/Data/Lattice/Property.hs +168/−136
• src/Data/Order.hs +184/−311
• src/Data/Order/Extended.hs +46/−39
• src/Data/Order/Interval.hs +24/−157
• src/Data/Order/Property.hs +87/−112
• src/Data/Order/Syntax.hs +69/−28
• test/Test/Data/Connection.hs +4/−9
• test/Test/Data/Connection/Float.hs +7/−146
• test/Test/Data/Connection/Int.hs +232/−96
• test/Test/Data/Connection/Word.hs +308/−69
• test/Test/Data/Lattice.hs +148/−153
• test/doctest.hs +14/−0
• test/test.hs +19/−18

@@ -2,6 +2,21 @@  ## 0.0.3  -- 2020-02-17 -* `Data.Float` : add cmath utils+* `Data.Connection.Float` : float utils * `Data.Connection.Ratio` : add rational connections-* `Numeric.Prelude` : add numeric prelude++## 0.1.0  -- 2020-07-07++* Unify `Connection` and `Triple` into a single class+* Add `Heyting`, `Symmetric`, and `Boolean` algebras+* Add misc new instances++## 0.2.0  -- 2021-02-21++* Change integral connection instances to non-shifting behavior.+* Move all one-sided `Connection` instances to `Connection 'L`.+* Consolidate floating point utilities into one module.+* Rename some functions in `Class.hs` and `Conn.hs` for clarity.+* Move `<` and `>` to `Syntax.hs`.+* Remove niche instances w/ upstream dependencies.+* Add misc new instances.

@@ -1,5 +1,5 @@ name:                connections-version:             0.1.0+version:             0.2.0 synopsis:            Orders, Galois connections, and lattices. description:         A library for order manipulation using Galois connections. homepage:            https://github.com/cmk/connections@@ -26,7 +26,6 @@     , Data.Connection.Word     , Data.Connection.Ratio     , Data.Connection.Float-    , Data.Connection.Double     , Data.Connection.Property      , Data.Lattice@@ -41,19 +40,7 @@   build-depends:              base            >= 4.10  && < 5.0     , containers      >= 0.4.0 && < 1.0-    , transformers    >= 0.5.5 && < 0.6-    , universe-base   >= 1.1.1 && < 2.0-    , finite-typelits >= 0.1.4.2 && < 0.1.5 -  default-extensions:-      ScopedTypeVariables-    , TypeApplications-    , MultiParamTypeClasses-    , UndecidableInstances-    , FlexibleInstances-    , FlexibleContexts-    , TypeOperators- test-suite test   type: exitcode-stdio-1.0   other-modules:@@ -76,3 +63,23 @@   hs-source-dirs: test   default-language: Haskell2010   ghc-options: -threaded -rtsopts -with-rtsopts=-N -Wall++executable doctest+  main-is:           doctest.hs+  ghc-options:       -Wall -threaded+  hs-source-dirs:    test+  default-language:  Haskell2010+  x-doctest-options: --fast++  build-depends:+      base+    , doctest                >= 0.8+    , connections -any++  default-extensions: +      ScopedTypeVariables+    , TypeApplications+    , MultiParamTypeClasses+    , UndecidableInstances+    , FlexibleInstances+    , FlexibleContexts

@@ -1,187 +1,9 @@-{-# Language TypeApplications    #-}-{-# Language AllowAmbiguousTypes #-}-{-# Language ConstraintKinds     #-}-{-# Language DataKinds           #-}-{-# Language Safe                #-}-{-# Language ViewPatterns        #-}-{-# Language PatternSynonyms     #-}-{-# Language RankNTypes          #-}-{-# Language QuantifiedConstraints #-}+{-# LANGUAGE Safe #-}  module Data.Connection (-  -- * Types-    Kan(..)-  , Semilattice-  , Extremal-  , ConnFloat-  , ConnDouble-  , ConnInteger-  , ConnRational-  , ConnExtended-  -- * Connection L-  , type ConnL-  , pattern ConnL-  , connL-  , swapL-  , embedL-  , ceiling-  , ceiling1-  , ceiling2-  , filterL-  , minimal-  , (\/)-  , glb-  -- * Connection R-  , type ConnR-  , pattern ConnR-  , connR-  , swapR-  , floor-  , floor1-  , floor2-  , embedR-  , filterR-  , maximal-  , (/\)-  , lub-  -- * Connection-  , type Trip-  , pattern Conn-  , half-  , midpoint-  , round-  , round1-  , round2-  , truncate-  , truncate1-  , truncate2-  , maybeL-  , maybeR-  , choice-  , strong-  , fmapped-  -- * Connection-  , Conn()-  , Triple-  , Connection(..)+    module Data.Connection.Conn,+    module Data.Connection.Class, ) where -import safe Data.Connection.Conn import safe Data.Connection.Class-import safe Data.Order-import safe Prelude hiding-  (Bounded,fromInteger, fromRational, floor, ceiling, round, truncate)---- $setup--- >>> :set -XTypeApplications--- >>> import Data.Int--- >>> import Prelude hiding (Ord(..), Bounded, fromInteger, fromRational, RealFrac(..))--- >>> import qualified Prelude as P--- >>> :load Data.Connection---- | Determine which half of the interval between 2 representations of /a/ a particular value lies.--- --- @ 'half' t x = 'pcompare' (x - 'counitR' t x) ('unitL' t x - x) @----half :: (Num a, Preorder a) => Trip a b -> a -> Maybe Ordering-half t x = pcompare (x - counitR t x) (unitL t x - x) ---- | Return the midpoint of the interval containing x.------ >>> midpoint f32i08 4.3--- 4.5--- >>> midpoint f64i08 4.3--- 4.5--- >>> pi - midpoint f64f32 pi--- 3.1786509424591713e-8------ >>> maybe False (~~ EQ) $ half f64f32 (midpoint f64f32 pi)--- True----midpoint :: Fractional a => Trip a b -> a -> a-midpoint t x = counitR t x / 2 + unitL t x / 2-------------------------------------------------------------------------- Rounding-------------------------------------------------------------------------- | Return the nearest value to x.------ > round @a @a = 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>.------ Usable in conjunction with /RebindableSyntax/:------ >>> fromRational = round--- >>> fromRational @Float 1.3--- 1.3--- >>> fromRational @Float (1 :% 0)--- Infinity--- >>> fromRational @Float (0 :% 0)--- NaN----round :: forall a b. (Num a, Triple a b) => a -> b-round x = case pcompare halfR halfL of-  Just GT -> ceiling x-  Just LT -> floor x-  _       -> truncate x--  where-    halfR = x - counitR (connR @a @b) x -- dist from lower bound--    halfL = unitL (connL @a @b) x - x -- dist from upper bound---- | Lift a unary function over a 'Trip'.------ Results are rounded to the nearest value with ties away from 0.----round1 :: forall a b. (Num a, Triple a b) => (a -> a) -> b -> b-round1 f x = round $ f (g x) where Conn _ g _ = connL-{-# INLINE round1 #-}---- | Lift a binary function over a 'Trip'.------ Results are rounded to the nearest value with ties away from 0.------ >>> f x y = (x + y) - x --- >>> maxOdd32 = 1.6777215e7--- >>> maxOdd64 = 9.007199254740991e15--- >>> f maxOdd32 2.0 :: Float--- 1.0--- >>> round2 @Rational @Float f maxOdd32 2.0--- 2.0--- >>> f maxOdd64 2.0 :: Double--- 1.0--- >>> round2 @Rational @Double f maxOdd64 2.0--- 2.0----round2 :: (Num a, Triple a b) => (a -> a -> a) -> b -> b -> b-round2 f x y = round $ f (g x) (g y) where Conn _ g _ = connL-{-# INLINE round2 #-}---- | Truncate towards zero.------ > truncate @a @a = id----truncate :: (Num a, Triple a b) => a -> b-truncate x = if x >~ 0 then floor x else ceiling x---- | Lift a unary function over a 'Trip'.------ Results are truncated towards 0.----truncate1 :: (Num a, Triple a b) => (a -> a) -> b -> b-truncate1 f x = truncate $ f (g x) where Conn _ g _ = connL-{-# INLINE truncate1 #-}---- | Lift a binary function over a 'Trip'.------ Results are truncated towards 0.----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 #-}+import safe Data.Connection.Conn

@@ -1,815 +1,706 @@-{-# Language TypeApplications    #-}-{-# Language AllowAmbiguousTypes #-}-{-# Language ConstraintKinds     #-}-{-# Language DataKinds           #-}-{-# Language Safe                #-}-{-# Language ViewPatterns        #-}-{-# Language PatternSynonyms     #-}-{-# Language RankNTypes          #-}-{-# LANGUAGE DerivingVia         #-}-{-# LANGUAGE StandaloneDeriving  #-}--module Data.Connection.Class (-  -- * Types-    Kan(..)-  , Conn()-  , Semilattice-  , Extremal-  , ConnFloat-  , ConnDouble-  , ConnInteger-  , ConnRational-  , ConnExtended-  -- * Connection L-  , ConnL-  , pattern ConnL-  , connL-  , swapL-  , embedL-  , ceiling-  , ceiling1-  , ceiling2-  , filterL-  , minimal-  , (\/)-  , glb-  -- * Connection R-  , ConnR-  , pattern ConnR-  , connR-  , swapR-  , floor-  , floor1-  , floor2-  , embedR-  , filterR-  , maximal-  , (/\)-  , lub-  -- * Connection k-  , Trip-  , pattern Conn-  , maybeL-  , maybeR-  , choice-  , strong-  , fmapped-  -- * Connection-  , Connection(..)-  , Triple-) where--import safe Control.Applicative (liftA2)-import safe Control.Category ((>>>))-import safe Data.Bool (bool)-import safe Data.Connection.Conn-import safe Data.Connection.Int-import safe Data.Connection.Word-import safe Data.Connection.Float-import safe Data.Connection.Double-import safe Data.Connection.Ratio-import safe Data.Functor.Contravariant-import safe Data.Functor.Identity-import safe Data.Monoid-import safe Data.Order-import safe Data.Order.Extended-import safe Data.Order.Interval-import safe Data.Word-import safe Data.Int-import safe GHC.TypeNats-import safe Numeric.Natural-import safe Prelude hiding (Bounded, floor, ceiling, fromInteger, fromRational)-import safe qualified Control.Category as C-import safe qualified Data.IntMap as IntMap-import safe qualified Data.IntSet as IntSet-import safe qualified Data.Map as Map-import safe qualified Data.Set as Set-import safe qualified Data.Finite as F-import safe qualified Data.Universe.Class as U-import safe qualified Prelude as P---- $setup--- >>> :set -XTypeApplications--- >>> import Data.Int--- >>> import Prelude hiding (Ord(..), Bounded, fromInteger, fromRational, RealFrac(..))--- >>> import qualified Prelude as P--- >>> :load Data.Connection----- | Semilattices.------ A complete is a partially ordered set in which every two elements have a unique join --- (least upper bound or supremum) and a unique meet (greatest lower bound or infimum). ------ These operations may in turn be defined by the lower and upper adjoints to the unique--- function /a -> (a, a)/.------ /Associativity/------ @--- x '\/' (y '\/' z) = (x '\/' y) '\/' z--- x '/\' (y '/\' z) = (x '/\' y) '/\' z--- @------ /Commutativity/------ @--- x '\/' y = y '\/' x--- x '/\' y = y '/\' x--- @------ /Idempotency/------ @--- x '\/' x = x--- x '/\' x = x--- @------ /Absorption/------ @--- (x '\/' y) '/\' y = y--- (x '/\' y) '\/' y = y--- @------ See < https://en.wikipedia.org/wiki/Absorption_law Absorption >.------ Note that distributivity is _not_ a requirement for a complete.--- However when /a/ is distributive we have;--- --- @--- 'glb' x y z = 'lub' x y z--- @------ See < https://en.wikipedia.org/wiki/Lattice_(order) >.----type Semilattice k a = Connection k (a, a) a--type Extremal k = Connection k ()--type ConnInteger k = Connection k (Maybe Integer)--type ConnFloat k = Connection k Float--type ConnDouble k = Connection k Double--type ConnRational k = Connection k Rational--type ConnExtended k a b = Connection k 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--    -- |-    ---    -- >>> range (conn @_ @Double @Float) pi-    -- (3.1415925,3.1415927)-    -- >>> range (conn @_ @Rational @Float) (1 :% 7)-    -- (0.14285713,0.14285715)-    -- >>> range (conn @_ @Rational @Float) (1 :% 8)-    -- (0.125,0.125)-    ---    conn :: Conn k a b---- | A constraint kind representing an <https://ncatlab.org/nlab/show/adjoint+triple adjoint triple> of Galois connections.----type Triple a b = (Connection 'L a b, Connection 'R a b)---------------------------------------------------------------------------- Connection L-------------------------------------------------------------------------- | A specialization of /conn/ to left-side connections.------ This is a convenience function provided primarily to avoid needing--- to enable /DataKinds/.----connL :: Connection 'L a b => ConnL a b-connL = conn @'L---- | Extract the center of a 'Trip' or upper half of a 'ConnL'.----embedL :: Connection 'L a b => b -> a-embedL = embed connL---- | Extract the ceiling of a 'Trip' or lower half of a 'ConnL'.------ > ceiling @a @a = id------ >>> ceiling @Rational @Float (0 :% 0)--- NaN--- >>> ceiling @Rational @Float (1 :% 0)--- Infinity--- >>> ceiling @Rational @Float (13 :% 10)--- 1.3000001----ceiling :: Connection 'L a b => a -> b-ceiling = lowerL connL---- | Lift a unary function over a 'ConnL'.----ceiling1 :: Connection 'L a b => (a -> a) -> b -> b-ceiling1 = lowerL1 connL---- | Lift a binary function over a 'ConnL'.----ceiling2 :: Connection 'L a b => (a -> a -> a) -> b -> b -> b-ceiling2 = lowerL2 connL---- | 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 /\ y@ is also in /b/.------ /filterL/ and /filterR/ commute with /Down/:------ > filterL a b <=> filterR (Down a) (Down b)------ > filterL (Down a) (Down b) <=> filterR a b------ /filterL a/ is upward-closed for all /a/:------ > a <= b1 && b1 <= b2 => a <= b2------ > a1 <= b && inf a2 <= b => ceiling a1 /\ ceiling a2 <= b------ See <https://en.wikipedia.org/wiki/Filter_(mathematics)>----filterL :: Connection 'L a b => a -> b -> Bool-filterL a b = ceiling a <~ b---- | A minimal element of a preorder defined by a connection with '()'.------ 'minimal' needn't be unique, but we must have:------ > x <~ minimal => x ~~ minimal----minimal :: Extremal 'L a => a-minimal = lowerL connL ()--infixr 5 \/---- | Semigroup operation on a join-semilattice.------ > (\/) = curry $ lowerL forked----(\/) :: Semilattice 'L a => a -> a -> a-(\/) = curry $ lowerL connL---- | Greatest lower bound operator.------ > glb x x y = x--- > glb x y z = glb z x y--- > glb x x y = x--- > 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)-------------------------------------------------------------------------- Connection R-------------------------------------------------------------------------- | A specialization of /conn/ to right-side connections.------ This is a convenience function provided primarily to avoid needing--- to enable /DataKinds/.----connR :: Connection 'R a b => ConnR a b-connR = conn @'R---- | Extract the floor of a 'Trip' or upper half of a 'ConnL'.------ > floor @a @a = id------ >>> floor @Rational @Float (0 :% 0)--- NaN--- >>> floor @Rational @Float (1 :% 0)--- Infinity--- >>> floor @Rational @Float (13 :% 10)--- 1.3----floor :: Connection 'R a b => a -> b-floor = upperR connR---- | Lift a unary function over a 'ConnR'.----floor1 :: Connection 'R a b => (a -> a) -> b -> b-floor1 = upperR1 connR---- | Lift a binary function over a 'ConnR'.----floor2 :: Connection 'R a b => (a -> a -> a) -> b -> b -> b-floor2 = upperR2 connR---- | Extract the center of a 'Trip' or lower half of a 'ConnR'.----embedR :: Connection 'R a b => b -> a-embedR = embed connR---- | 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 \/ y/ is also in /B/.------ /filterR a/ is downward-closed for all /a/:------ > a >= b1 && b1 >= b2 => a >= b2------ > a1 >= b && a2 >= b => floor a1 \/ floor a2 >= b------ See <https://en.wikipedia.org/wiki/Ideal_(order_theory)>----filterR :: Connection 'R a b => a -> b -> Bool-filterR a b = b <~ floor a---- | A maximal element of a preorder defined by a connection with '()'.------ 'maximal' needn't be unique, but we must have:------ > x >~ maximal => x ~~ maximal----maximal :: Extremal 'R a => a-maximal = upperR connR ()--infixr 6 /\ -- comment for the parser---- | Semigroup operation on a meet-semilattice.------ > (/\) = curry $ upperR forked----(/\) :: Semilattice 'R a => a -> a -> a-(/\) = curry $ upperR connR---- | 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 /\ y) \/ (y /\ z) \/ (z /\ x)-------------------------------------------------------------------------- Connection------------------------------------------------------------------------maybeL :: Triple () b => Trip (Maybe a) (Either a b)-maybeL = trip f g h where-  f = maybe (Right minimal) Left-  g = either Just (const Nothing)-  h = maybe (Right maximal) Left--maybeR :: Triple () a => Trip (Maybe b) (Either a b)-maybeR = trip f g h where-  f = maybe (Left minimal) Right-  g = either (const Nothing) Just-  h = maybe (Left maximal) Right-------------------------------------------------------------------------- Instances------------------------------------------------------------------------instance Preorder a => Connection k a a where-  conn = C.id--instance Connection 'R Word16 Word8 where-  conn = swapR w08w16--instance Connection 'R Word32 Word8 where-  conn = swapR w08w32--instance Connection 'R Word32 Word16 where-  conn = swapR w16w32--instance Connection 'R Word64 Word8 where-  conn = swapR w08w64--instance Connection 'R Word64 Word16 where-  conn = swapR w16w64--instance Connection 'R Word64 Word32 where-  conn = swapR w32w64--instance Connection k Word Word64 where-  conn = wxxw64--instance Connection 'R Natural Word8 where-  conn = swapR w08nat--instance Connection 'R Natural Word16 where-  conn = swapR w16nat--instance Connection 'R Natural Word32 where-  conn = swapR w32nat--instance Connection 'R Natural Word64 where-  conn = swapR w64nat--instance Connection 'R Natural Word where-  conn = swapR wxxnat--instance Connection 'R Natural Integer where-  conn = swapR intnat--instance Connection 'R Int32 Int8 where-  conn = swapR i08i32--instance Connection 'R Int32 Int16 where-  conn = swapR i16i32--instance Connection 'R Int64 Int8 where-  conn = swapR i08i64--instance Connection 'R Int64 Int16 where-  conn = swapR i16i64--instance Connection 'R Int64 Int32 where-  conn = swapR i32i64--instance Connection k Int Int64 where-  conn = ixxi64--instance Connection 'R (Maybe Integer) Word8 where-  conn = swapR $ w08nat >>> natint--instance Connection 'R (Maybe Integer) Word16 where-  conn = swapR $ w16nat >>> natint--instance Connection 'R (Maybe Integer) Word32 where-  conn = swapR $ w32nat >>> natint--instance Connection 'R (Maybe Integer) Word64 where-  conn = swapR $ w64nat >>> natint--instance Connection 'R (Maybe Integer) Word where-  conn = swapR $ wxxnat >>> natint--instance Connection 'R (Maybe Integer) Natural where-  conn = swapR natint--instance Connection 'R (Maybe Integer) Int8 where-  conn = swapR i08int--instance Connection 'R (Maybe Integer) Int16 where-  conn = swapR i16int--instance Connection 'R (Maybe Integer) Int32 where-  conn = swapR i32int--instance Connection 'R (Maybe Integer) Int64 where-  conn = swapR i64int--instance Connection 'R (Maybe Integer) Int where-  conn = swapR ixxint--instance Connection 'R (Maybe Integer) Integer where-  -- | Provided as a shim for /RebindableSyntax/.-  -- Note that this instance will clip negative numbers to zero.-  conn = swapR $ intnat >>> natint--instance Connection k Int8 Word8 where-  conn = i08w08--instance Connection k Int16 Word16 where-  conn = i16w16--instance Connection k Int32 Word32 where-  conn = i32w32--instance Connection k Int64 Word64 where-  conn = i64w64--instance Connection k Int Word where-  conn = ixxwxx--instance Connection k Double Float where-  conn = f64f32--instance Connection k Rational Float where-  conn = ratf32--instance Connection k Rational Double where-  conn = ratf64--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 Connection k Float (Extended Int8) where-  conn = f32i08--instance Connection k Float (Extended Int16) where-  conn = f32i16--instance Connection 'L Float (Extended Int32) where-  conn = conn >>> fmapped (i16w16 >>> w16w32 >>> w32i32)--instance Connection 'L Float (Extended Int64) where-  conn = conn >>> fmapped (i16w16 >>> w16w64 >>> w64i64)--instance Connection 'L Float (Extended Int) where-  conn = conn >>> fmapped (i16w16 >>> w16wxx >>> swapL ixxwxx)--instance Connection k Double (Extended Int8) where-  conn = f64i08--instance Connection k Double (Extended Int16) where-  conn = f64i16--instance Connection k Double (Extended Int32) where-  conn = f64i32--instance Connection 'L Double (Extended Int64) where-  conn = conn >>> fmapped (i32w32 >>> w32w64 >>> w64i64)--instance Connection 'L Double (Extended Int) where-  conn = conn >>> fmapped (i32w32 >>> w32wxx >>> swapL ixxwxx)--instance Connection k a b => Connection k (Identity a) b where-  conn = Conn runIdentity Identity runIdentity >>> conn--instance Connection k a b => Connection k a (Identity b) where-  conn = conn >>> Conn Identity runIdentity Identity-------------------------------------------------------------------------- ------------------------------------------------------------------------fork :: a -> (a, a)-fork x = (x, x)--semilatticeN5 :: (Total a, Fractional a) => Conn k (a, a) a-semilatticeN5 = Conn (uncurry joinN5) fork (uncurry meetN5) where-  joinN5 x y = maybe (1 / 0) (bool y x . (>= EQ)) (pcompare x y)--  meetN5 x y = maybe (-1 / 0) (bool y x . (<= EQ)) (pcompare x y)--extremalN5 :: (Total a, Fractional a) => Conn k () a-extremalN5 = Conn (const $ -1/0) (const ()) (const $ 1/0)--semilatticeOrd :: (Total a) => Conn k (a, a) a-semilatticeOrd = Conn (uncurry max) fork (uncurry min)--extremalOrd :: (Total a, P.Bounded a) => Conn k () a-extremalOrd = Conn (const minBound) (const ()) (const maxBound)--instance Connection k ((),()) () where conn = semilatticeOrd-instance Connection k (Bool, Bool) Bool where conn = semilatticeOrd-instance Connection k () Bool where conn = extremalOrd-instance Connection k (Ordering, Ordering) Ordering  where conn = semilatticeOrd-instance Connection k () Ordering where conn = extremalOrd--instance Connection k (Word8, Word8) Word8 where conn = semilatticeOrd-instance Connection k () Word8 where conn = extremalOrd-instance Connection k (Word16, Word16) Word16 where conn = semilatticeOrd-instance Connection k () Word16 where conn = extremalOrd-instance Connection k (Word32, Word32) Word32 where conn = semilatticeOrd-instance Connection k () Word32 where conn = extremalOrd-instance Connection k (Word64, Word64) Word64 where conn = semilatticeOrd-instance Connection k () Word64 where conn = extremalOrd-instance Connection k (Word, Word) Word where conn = semilatticeOrd-instance Connection k () Word where conn = extremalOrd-instance Connection k (Natural, Natural) Natural where conn = semilatticeOrd--instance Connection k (Positive, Positive) Positive where conn = semilatticeN5-instance Connection k () Positive where-  conn = Conn (const $ 0 :% 1) (const ()) (const $ 1 :% 0)--instance Connection k (Int8, Int8) Int8 where conn = semilatticeOrd-instance Connection k () Int8 where conn = extremalOrd-instance Connection k (Int16, Int16) Int16 where conn = semilatticeOrd-instance Connection k () Int16 where conn = extremalOrd-instance Connection k (Int32, Int32) Int32 where conn = semilatticeOrd-instance Connection k () Int32 where conn = extremalOrd-instance Connection k (Int64, Int64) Int64 where conn = semilatticeOrd-instance Connection k () Int64 where conn = extremalOrd-instance Connection k (Int, Int) Int where conn = semilatticeOrd-instance Connection k () Int where conn = extremalOrd-instance Connection k (Integer, Integer) Integer where conn = semilatticeOrd--instance Connection k (Rational, Rational) Rational where conn = semilatticeN5-instance Connection k () Rational where-  conn = Conn (const $ -1 :% 0) (const ()) (const $ 1 :% 0)--instance Connection k (F.Finite n, F.Finite n) (F.Finite n) where conn = semilatticeOrd-instance KnownNat n => Connection k () (F.Finite n) where conn = extremalOrd--instance Connection k (Float, Float) Float where conn = semilatticeN5-instance Connection k () Float where conn = extremalN5--instance Connection k (Double, Double) Double where conn = semilatticeN5-instance Connection k () Double where conn = extremalN5--instance Total a => Connection k (Set.Set a, Set.Set a) (Set.Set a) where-  conn = Conn (uncurry Set.union) fork (uncurry Set.intersection)----instance (Total a, U.Finite a) => Connection k () (Set.Set a) where---  conn = Conn (const Set.empty) (const ()) (const $ Set.fromList U.universeF)-instance (Total a) => Connection 'L () (Set.Set a) where-  conn = ConnL (const Set.empty) (const ())--instance (Total a, U.Finite a) => Connection 'R () (Set.Set a) where-  conn = ConnR (const ()) (const $ Set.fromList U.universeF)--instance Connection k (IntSet.IntSet, IntSet.IntSet) IntSet.IntSet where-  conn = Conn (uncurry IntSet.union) fork (uncurry IntSet.intersection)--instance Connection k () IntSet.IntSet where-  conn = Conn (const IntSet.empty) (const ()) (const $ IntSet.fromList U.universeF)--instance (Total a, Connection 'L (b,b) b) => Connection 'L (Map.Map a b, Map.Map a b) (Map.Map a b) where-  conn = ConnL (uncurry $ Map.unionWith (\/)) fork--instance (Total a, Connection 'R (b,b) b) => Connection 'R (Map.Map a b, Map.Map a b) (Map.Map a b) where-  conn = ConnR fork (uncurry $ Map.intersectionWith (/\))--instance (Total a, Preorder b) => Connection 'L () (Map.Map a b) where-  conn = ConnL (const Map.empty) (const ()) --instance (Total a, U.Finite a, Connection 'R () b) => Connection 'R () (Map.Map a b) where-  conn = ConnR (const ()) (const . Map.fromList $ U.universeF `zip` repeat maximal)--instance Connection 'L (a,a) a => Connection 'L (IntMap.IntMap a, IntMap.IntMap a) (IntMap.IntMap a) where-  conn = ConnL (uncurry $ IntMap.unionWith (\/)) fork--instance Connection 'R (a,a) a => Connection 'R (IntMap.IntMap a, IntMap.IntMap a) (IntMap.IntMap a) where-  conn = ConnR fork (uncurry $ IntMap.intersectionWith (/\))--instance Preorder a => Connection 'L () (IntMap.IntMap a) where-  conn = ConnL (const IntMap.empty) (const ())--instance Connection 'R () a => Connection 'R () (IntMap.IntMap a) where-  conn = ConnR (const ()) (const . IntMap.fromList $ U.universeF `zip` repeat maximal)--joinMaybe :: Connection 'L (a, a) a => Maybe a -> Maybe a -> Maybe a-joinMaybe (Just x) (Just y) = Just (x \/ y)-joinMaybe u@(Just _) _ = u-joinMaybe _ u@(Just _) = u-joinMaybe Nothing Nothing = Nothing--meetMaybe :: Connection 'R (a, a) a => Maybe a -> Maybe a -> Maybe a-meetMaybe Nothing Nothing = Nothing-meetMaybe Nothing _ = Nothing-meetMaybe _ Nothing = Nothing-meetMaybe (Just x) (Just y) = Just (x /\ y)--instance Connection 'L (a, a) a => Connection 'L (Maybe a, Maybe a) (Maybe a) where-  conn = ConnL (uncurry joinMaybe) fork--instance Connection 'R (a, a) a => Connection 'R (Maybe a, Maybe a) (Maybe a) where-  conn = ConnR fork (uncurry meetMaybe)--instance Preorder a => Connection 'L () (Maybe a) where-  conn = ConnL (const Nothing) (const ())--instance Connection 'R () a => Connection 'R () (Maybe a) where-  conn = ConnR (const ()) (const $ Just maximal)--joinExtended :: Connection 'L (a, a) a => Extended a -> Extended a -> Extended a-joinExtended Top          _            = Top-joinExtended _            Top          = Top-joinExtended (Extended x) (Extended y) = Extended (x \/ y)-joinExtended Bottom       y            = y-joinExtended x            Bottom       = x--meetExtended :: Connection 'R (a, a) a => Extended a -> Extended a -> Extended a-meetExtended Top          y            = y-meetExtended x            Top          = x-meetExtended (Extended x) (Extended y) = Extended (x /\ y)-meetExtended Bottom       _            = Bottom-meetExtended _            Bottom       = Bottom--instance Connection 'L (a, a) a => Connection 'L (Extended a, Extended a) (Extended a) where-  conn = ConnL (uncurry joinExtended) fork--instance Connection 'R (a, a) a => Connection 'R (Extended a, Extended a) (Extended a) where-  conn = ConnR fork (uncurry meetExtended)--instance Preorder a => Connection k () (Extended a) where-  conn = Conn (const Bottom) (const ()) (const Top)--joinEither :: (Connection 'L (a, a) a, Connection 'L (b, b) b) => Either a b -> Either a b -> Either a b-joinEither (Right x) (Right y) = Right (x \/ y)-joinEither u@(Right _) _ = u-joinEither _ u@(Right _) = u-joinEither (Left x) (Left y) = Left (x \/ y)--meetEither :: (Connection 'R (a, a) a, Connection 'R (b, b) b) => Either a b -> Either a b -> Either a b-meetEither (Left x) (Left y) = Left (x /\ y)-meetEither l@(Left _) _ = l-meetEither _ l@(Left _) = l-meetEither (Right x) (Right y) = Right (x /\ y)---- | All minimal elements of the upper lattice cover all maximal elements of the lower lattice.-instance (Connection 'L (a,a) a, Connection 'L (b,b) b) => Connection 'L (Either a b, Either a b) (Either a b) where-  conn = ConnL (uncurry joinEither) fork--instance (Connection 'R (a,a) a, Connection 'R (b,b) b) => Connection 'R (Either a b, Either a b) (Either a b) where-  conn = ConnR fork (uncurry meetEither)--instance (Connection 'L () a, Preorder b) => Connection 'L () (Either a b) where-  conn = ConnL (const $ Left minimal) (const ())--instance (Preorder a, Connection 'R () b) => Connection 'R () (Either a b) where-  conn = ConnR (const ()) (const $ Right maximal)--joinTuple :: (Connection 'L (a, a) a, Connection 'L (b, b) b) => (a, b) -> (a, b) -> (a, b)-joinTuple (x1, y1) (x2, y2) = (x1 \/ x2, y1 \/ y2)--meetTuple :: (Connection 'R (a, a) a, Connection 'R (b, b) b) => (a, b) -> (a, b) -> (a, b)-meetTuple (x1, y1) (x2, y2) = (x1 /\ x2, y1 /\ y2)--instance (Triple (a, a) a, Triple (b, b) b) => Connection k ((a, b), (a, b)) (a, b) where-  conn = Conn (uncurry joinTuple) fork (uncurry meetTuple)--instance (Triple () a, Triple () b) => Connection k () (a, b) where-  conn = Conn (const (minimal, minimal)) (const ()) (const (maximal, maximal))--instance (U.Finite a, Triple (b, b) b) => Connection k (a -> b, a -> b) (a -> b) where-  conn = Conn (uncurry $ liftA2 (\/)) fork (uncurry $ liftA2 (/\))--instance (U.Finite a, Triple () b) => Connection k () (a -> b) where-  conn = Conn (const $ pure minimal) (const ()) (const $ pure maximal)--instance (U.Finite a, Triple (a, a) a) => Connection k (Endo a, Endo a) (Endo a) where-  conn = Conn (\(Endo x, Endo y) -> Endo $ x\/y) fork (\(Endo x, Endo y) -> Endo $ x/\y)--instance (U.Finite a, Triple () a) => Connection k () (Endo a) where-  conn = Conn (const $ Endo minimal) (const ()) (const $ Endo maximal)--instance (U.Finite a, Triple (b, b) b) => Connection k (Op b a, Op b a) (Op b a) where-  conn = Conn (\(Op x, Op y) -> Op $ x\/y) fork (\(Op x, Op y) -> Op $ x/\y)--instance (U.Finite a, Triple () b) => Connection k () (Op b a) where-  conn = Conn (const $ Op minimal) (const ()) (const $ Op maximal)--instance U.Finite a => Connection k (Predicate a, Predicate a) (Predicate a) where-  conn = Conn (\(Predicate x, Predicate y) -> Predicate $ x\/y) fork (\(Predicate x, Predicate y) -> Predicate $ x/\y)--instance U.Finite a => Connection k () (Predicate a) where-  conn = Conn (const $ Predicate minimal) (const ()) (const $ Predicate maximal)--{--instance (Applicative m, Connection k r) => Connection k (ContT r m a) where-  (<>) = liftA2 joinCont--instance (Applicative m, Connection k () r) => Connection k () (ContT r m a) where-  mempty = pure . ContT . const $ pure bottom--instance Monad m => Connection k (SelectT r m a) where-  (<>) = liftA2 joinSelect--instance MonadPlus m => Connection k () (SelectT r m a)) where-  bottom = pure empty-instance (Ord.Ord a, Preorder a, Preorder r, Finite r) => Preorder (Cont r a) where-  (ContT x) <~ (ContT y) = x `contLe` y--instance (Ord.Ord a, Preorder a, Preorder r, Finite r) => Preorder (Select r a) where-  (SelectT x) <~ (SelectT y) = x `contLe` y-instance (Applicative m, Total a, Preorder r, Finite r, Connection 'L r) => Connection 'L (ContT r m a, ContT r m a) (ContT r m a) where-  conn = ConnL (uncurry joinCont) fork--joinCont :: (Applicative m, Connection 'L (r,r) r) => ContT r m a -> ContT r m a -> ContT r m a-joinCont (ContT f) (ContT g) = ContT $ \p -> liftA2 join (f p) (g p) --instance (Monad m, Total a, Preorder r, Finite r, Extremal 'L r) => Connection 'L (SelectT r m a, SelectT r m a) (SelectT r m a) where-  conn = ConnL (uncurry joinSelect) fork--joinSelect :: (Monad m, Extremal 'L r) => SelectT r m b -> SelectT r m b -> SelectT r m b-joinSelect x y = branch x y >>= id-  where-    ifM c x y = c >>= \b -> if b then x else y-    branch x y = SelectT $ \p -> ifM ((~~ maximal) <$> p x) (pure x) (pure y)-  +{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE Safe #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE ViewPatterns #-}++module Data.Connection.Class (+    -- * Conn+    Conn (),+    identity,++    -- * Connection k+    Triple,+    pattern Conn,+    ConnK,+    embed,+    extremal,+    lub,+    glb,+    half,+    midpoint,+    range,+    round,+    round1,+    round2,+    truncate,+    truncate1,+    truncate2,++    -- * Connection L+    Left,+    pattern ConnL,+    ConnL,+    connL,+    embedL,+    minimal,+    join,+    ceiling,+    ceiling1,+    ceiling2,++    -- * Connection R+    Right,+    pattern ConnR,+    ConnR,+    connR,+    embedR,+    maximal,+    meet,+    floor,+    floor1,+    floor2,++    -- * Combinators+    (>>>),+    (<<<),+    (/|\),+    (\|/),+    choice,+    strong,++    -- * Connection+    Kan (..),+    ConnInteger,+    ConnRational,+    ConnExtended,+    Connection (..),+) where++import safe Control.Category ((>>>))+import safe Data.Bool (bool)+import safe Data.Connection.Conn+import safe Data.Connection.Float+import safe Data.Connection.Int+import safe Data.Connection.Ratio+import safe Data.Connection.Word+import safe Data.Functor.Identity+import safe Data.Int+import safe qualified Data.IntMap as IntMap+import safe qualified Data.IntSet as IntSet+import safe qualified Data.Map as Map+import safe Data.Order+import safe Data.Order.Extended+import safe qualified Data.Set as Set+import safe Data.Word+import safe Numeric.Natural+import safe Prelude hiding (ceiling, floor, round, truncate)++-- $setup+-- >>> :set -XTypeApplications+-- >>> :set -XFlexibleContexts+-- >>> import GHC.Real (Ratio(..))+-- >>> import Data.Set (Set,fromList)+-- >>> :load Data.Connection+-- >>> import Prelude hiding (round, floor, ceiling, truncate)++type Left = Connection 'L++type Right = Connection '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)++-- | A constraint kind for 'Integer' conversions.+--+--  Usable in conjunction with /RebindableSyntax/:+--+--  > fromInteger = embedL . 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+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+    -- |+    --+    -- >>> range (conn @_ @Rational @Float) (22 :% 7)+    -- (3.142857,3.1428573)+    -- >>> range (conn @_ @Double @Float) pi+    -- (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+--+-- 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 :: forall a b. (Num a, Triple a b) => a -> b+round x = case pcompare halfR halfL of+    Just GT -> ceiling x+    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++-- | Lift a unary function over a 'Conn'.+--+-- Results are rounded to the nearest value with ties away from 0.+round1 :: (Num a, Triple a b) => (a -> a) -> b -> b+round1 f x = round $ f (g x) where Conn _ g _ = connL+{-# INLINE round1 #-}++-- | Lift a binary function over a 'Conn'.+--+-- Results are rounded to the nearest value with ties away from 0.+--+-- Example avoiding loss-of-precision:+--+-- >>> f x y = (x + y) - x+-- >>> maxOdd32 = 1.6777215e7+-- >>> f maxOdd32 2.0 :: Float+-- 1.0+-- >>> round2 @Rational @Float f maxOdd32 2.0+-- 2.0+-- >>> maxOdd64 = 9.007199254740991e15+-- >>> f maxOdd64 2.0 :: Double+-- 1.0+-- >>> round2 @Rational @Double f maxOdd64 2.0+-- 2.0+round2 :: (Num a, Triple a b) => (a -> a -> a) -> b -> b -> b+round2 f x y = round $ f (g x) (g y) where Conn _ g _ = connL+{-# INLINE round2 #-}++-- | Truncate towards zero.+--+-- > truncate @a @a = id+truncate :: (Num a, Triple a b) => a -> b+truncate x = if x >~ 0 then floor x else ceiling x++-- | Lift a unary function over a 'Conn'.+--+-- Results are truncated towards 0.+truncate1 :: (Num a, Triple a b) => (a -> a) -> b -> b+truncate1 f x = truncate $ f (g x) where Conn _ g _ = connL+{-# INLINE truncate1 #-}++-- | Lift a binary function over a 'Conn'.+--+-- Results are truncated towards 0.+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+---------------------------------------------------------------------++-- | 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++-- | A minimal element of a preorder.+--+-- 'minimal' needn't be unique, but it must obey:+--+-- > x <~ minimal => x ~~ minimal+minimal :: Left () a => a+minimal = ceiling ()++infixr 5 `join`++-- | Semigroup operation on a join-lattice.+join :: Left (a, a) a => a -> a -> a+join = curry ceiling++-- | Extract the ceiling of a 'Conn' or lower half of a 'ConnL'.+--+-- > ceiling @a @a = id+-- > ceiling (x1 `join` a2) = ceiling x1 `join` ceiling x2+--+-- The latter law is the adjoint functor theorem for preorders.+--+-- >>> 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++-- | Lift a unary function over a 'ConnL'.+ceiling1 :: Left a b => (a -> a) -> b -> b+ceiling1 = ceilingWith1 conn++-- | Lift a binary function over a 'ConnL'.+ceiling2 :: Left a b => (a -> a -> a) -> b -> b -> b+ceiling2 = ceilingWith2 conn++---------------------------------------------------------------------+-- Connection R+---------------------------------------------------------------------++-- | 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++-- | Extract the center of a 'ConnK' or lower half of a 'ConnR'.+embedR :: Right a b => b -> a+embedR = embed connR++-- | A maximal element of a preorder.+--+-- '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++-- | 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++-- | Lift a unary function over a 'ConnR'.+floor1 :: Right a b => (a -> a) -> b -> b+floor1 = floorWith1 conn++-- | Lift a binary function over a 'ConnR'.+floor2 :: Right a b => (a -> a -> a) -> b -> b -> b+floor2 = floorWith2 conn++---------------------------------------------------------------------+-- Instances+---------------------------------------------------------------------++instance Preorder a => Connection k a a where conn = identity++instance Connection k ((), ()) () where conn = latticeOrd++instance Connection k () Bool where conn = bounded+instance Connection k Ordering Bool where conn = extremal+instance Connection k Word8 Bool where conn = extremal+instance Connection k Word16 Bool where conn = extremal+instance Connection k Word32 Bool where conn = extremal+instance Connection k Word64 Bool where conn = extremal+instance Connection k Word Bool where conn = extremal+instance Connection k Positive Bool where conn = extremal+instance Connection k Int8 Bool where conn = extremal+instance Connection k Int16 Bool where conn = extremal+instance Connection k Int32 Bool where conn = extremal+instance Connection k Int64 Bool where conn = extremal+instance Connection k Int Bool where conn = extremal+instance Connection k Rational Bool where conn = extremal+instance Connection k Float Bool where conn = extremal+instance Connection k Double Bool where conn = extremal+instance Connection k (Bool, Bool) Bool where conn = latticeOrd++instance Connection k () Ordering where conn = bounded+instance Connection k (Ordering, Ordering) Ordering where conn = latticeOrd++instance Connection k () Word8 where conn = bounded+instance Connection 'L Int8 Word8 where conn = i08w08+instance Connection k (Word8, Word8) Word8 where conn = latticeOrd++instance Connection k () Word16 where conn = bounded+instance Connection 'L Word8 Word16 where conn = w08w16+instance Connection 'L Int8 Word16 where conn = i08w16+instance Connection 'L Int16 Word16 where conn = i16w16+instance Connection k (Word16, Word16) Word16 where conn = latticeOrd++instance Connection k () Word32 where conn = bounded+instance Connection 'L Word8 Word32 where conn = w08w32+instance Connection 'L Word16 Word32 where conn = w16w32+instance Connection 'L Int8 Word32 where conn = i08w32+instance Connection 'L Int16 Word32 where conn = i16w32+instance Connection 'L Int32 Word32 where conn = i32w32+instance Connection k (Word32, Word32) Word32 where conn = latticeOrd++instance Connection k () Word64 where conn = bounded+instance Connection 'L Word8 Word64 where conn = w08w64+instance Connection 'L Word16 Word64 where conn = w16w64+instance Connection 'L Word32 Word64 where conn = w32w64+instance Connection 'L Int8 Word64 where conn = i08w64+instance Connection 'L Int16 Word64 where conn = i16w64+instance Connection 'L Int32 Word64 where conn = i32w64+instance Connection 'L Int64 Word64 where conn = i64w64+instance Connection 'L Int Word64 where conn = ixxw64+instance Connection k (Word64, Word64) Word64 where conn = latticeOrd++instance Connection k () Word where conn = bounded+instance Connection 'L Word8 Word where conn = w08wxx+instance Connection 'L Word16 Word where conn = w16wxx+instance Connection 'L Word32 Word where conn = w32wxx+instance Connection k Word64 Word where conn = w64wxx+instance Connection 'L Int8 Word where conn = i08wxx+instance Connection 'L Int16 Word where conn = i16wxx+instance Connection 'L Int32 Word where conn = i32wxx+instance Connection 'L Int64 Word where conn = i64wxx+instance Connection 'L Int Word where conn = ixxwxx+instance Connection k (Word, Word) Word where conn = latticeOrd++instance Connection 'L () Natural where conn = ConnL (const 0) (const ())+instance Connection 'L Word8 Natural where conn = w08nat+instance Connection 'L Word16 Natural where conn = w16nat+instance Connection 'L Word32 Natural where conn = w32nat+instance Connection 'L Word64 Natural where conn = w64nat+instance Connection 'L Word Natural where conn = wxxnat+instance Connection 'L Int8 Natural where conn = i08nat+instance Connection 'L Int16 Natural where conn = i16nat+instance Connection 'L Int32 Natural where conn = i32nat+instance Connection 'L Int64 Natural where conn = i64nat+instance Connection 'L Int Natural where conn = ixxnat+instance Connection 'L Integer Natural where conn = intnat+instance Connection k (Natural, Natural) Natural where conn = latticeOrd++instance Connection k () Positive where+    conn = Conn (const $ 0 :% 1) (const ()) (const $ 1 :% 0)+instance Connection k (Positive, Positive) Positive where conn = latticeN5++instance Connection k () Int8 where conn = bounded+instance Connection k (Int8, Int8) Int8 where conn = latticeOrd+instance Connection k () Int16 where conn = bounded+instance Connection k (Int16, Int16) Int16 where conn = latticeOrd+instance Connection k () Int32 where conn = bounded+instance Connection k (Int32, Int32) Int32 where conn = latticeOrd+instance Connection k () Int64 where conn = bounded+instance Connection k (Int64, Int64) Int64 where conn = latticeOrd+instance Connection k () Int where conn = bounded+instance Connection k (Int, Int) Int where conn = latticeOrd+instance Connection k (Integer, Integer) Integer where conn = latticeOrd++instance Connection k () Rational where+    conn = Conn (const $ -1 :% 0) (const ()) (const $ 1 :% 0)+instance Connection k (Rational, Rational) Rational where conn = latticeN5++instance Connection k () Float where conn = extremalN5+instance Connection k Double Float where conn = f64f32+instance Connection k Rational Float where conn = ratf32+instance Connection k (Float, Float) Float where conn = latticeN5++instance Connection k () Double where conn = extremalN5+instance Connection k Rational Double where conn = ratf64+instance Connection k (Double, Double) Double where conn = latticeN5++instance Connection 'L Word8 (Maybe Int16) where conn = w08i16+instance Connection 'L Int8 (Maybe Int16) where conn = i08i16++instance Connection 'L Word8 (Maybe Int32) where conn = w08i32+instance Connection 'L Word16 (Maybe Int32) where conn = w16i32+instance Connection 'L Int8 (Maybe Int32) where conn = i08i32+instance Connection 'L Int16 (Maybe Int32) where conn = i16i32++instance Connection 'L Word8 (Maybe Int64) where conn = w08i64+instance Connection 'L Word16 (Maybe Int64) where conn = w16i64+instance Connection 'L Word32 (Maybe Int64) where conn = w32i64+instance Connection 'L Int8 (Maybe Int64) where conn = i08i64+instance Connection 'L Int16 (Maybe Int64) where conn = i16i64+instance Connection 'L Int32 (Maybe Int64) where conn = i32i64++instance Connection 'L Word8 (Maybe Int) where conn = w08ixx+instance Connection 'L Word16 (Maybe Int) where conn = w16ixx+instance Connection 'L Word32 (Maybe Int) where conn = w32ixx+instance Connection 'L Int8 (Maybe Int) where conn = i08ixx+instance Connection 'L Int16 (Maybe Int) where conn = i16ixx+instance Connection 'L Int32 (Maybe Int) where conn = i32ixx+instance Connection k Int64 Int where conn = i64ixx++instance Connection 'L Word8 (Maybe Integer) where conn = w08int+instance Connection 'L Word16 (Maybe Integer) where conn = w16int+instance Connection 'L Word32 (Maybe Integer) where conn = w32int+instance Connection 'L Word64 (Maybe Integer) where conn = w64int+instance Connection 'L Word (Maybe Integer) where conn = wxxint+instance Connection 'L Natural (Maybe Integer) where conn = natint++instance Connection 'L Int8 (Maybe Integer) where conn = i08int+instance Connection 'L Int16 (Maybe Integer) where conn = i16int+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+-}++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++-- | All 'Data.Int.Int08' 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 k Double (Extended Int8) where conn = f64i08++-- | All 'Data.Int.Int16' values are exactly representable in a 'Double'.+instance Connection k Double (Extended Int16) where conn = f64i16++-- | All 'Data.Int.Int32' values are exactly representable in a 'Double'.+instance Connection k Double (Extended Int32) where conn = f64i32++instance Connection k a b => Connection k (Identity a) b where+    conn = Conn runIdentity Identity runIdentity >>> conn++instance Connection k a b => Connection k a (Identity b) where+    conn = conn >>> Conn Identity runIdentity Identity++instance (Triple () a, Triple () b) => Connection k () (a, b) where+    conn = Conn (const (minimal, minimal)) (const ()) (const (maximal, maximal))++instance Preorder a => Connection 'L () (Maybe a) where+    conn = ConnL (const Nothing) (const ())++instance Right () a => Connection 'R () (Maybe a) where+    conn = ConnR (const ()) (const $ Just maximal)++instance Preorder a => Connection k () (Extended a) where+    conn = Conn (const Bottom) (const ()) (const Top)++instance (Left () a, Preorder b) => Connection 'L () (Either a b) where+    conn = ConnL (const $ Left minimal) (const ())++instance (Preorder a, Right () b) => Connection 'R () (Either a b) where+    conn = ConnR (const ()) (const $ Right maximal)++instance (Preorder a, Triple () b) => Connection k (Maybe a) (Either a b) where+    conn = maybeL++instance (Triple () a, Preorder b) => Connection k (Maybe b) (Either a b) where+    conn = maybeR++instance (Total a) => Connection 'L () (Set.Set a) where+    conn = ConnL (const Set.empty) (const ())++instance Total a => Connection k (Set.Set a, Set.Set a) (Set.Set a) where+    conn = Conn (uncurry Set.union) fork (uncurry Set.intersection)++instance Connection 'L () IntSet.IntSet where+    conn = ConnL (const IntSet.empty) (const ())++instance Connection k (IntSet.IntSet, IntSet.IntSet) IntSet.IntSet where+    conn = Conn (uncurry IntSet.union) fork (uncurry IntSet.intersection)++instance (Total a, Preorder b) => Connection 'L () (Map.Map a b) where+    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++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)++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++instance Right (a, a) a => Connection 'R (IntMap.IntMap a, IntMap.IntMap a) (IntMap.IntMap a) where+    conn = ConnR fork (uncurry $ IntMap.intersectionWith meet)++-- Internal++-------------------------++fork :: a -> (a, a)+fork x = (x, x)++bounded :: Bounded a => Conn k () a+bounded = Conn (const minBound) (const ()) (const maxBound)++latticeN5 :: (Total a, Fractional a) => Conn k (a, a) a+latticeN5 = Conn (uncurry joinN5) fork (uncurry meetN5)+  where+    joinN5 x y = maybe (1 / 0) (bool y x . (>= EQ)) (pcompare x y)++    meetN5 x y = maybe (-1 / 0) (bool y x . (<= EQ)) (pcompare x y)++extremalN5 :: (Total a, Fractional a) => Conn k () a+extremalN5 = Conn (const $ -1 / 0) (const ()) (const $ 1 / 0)++latticeOrd :: (Total a) => Conn k (a, a) a+latticeOrd = Conn (uncurry max) fork (uncurry min)++maybeL :: Triple () b => Conn k (Maybe a) (Either a b)+maybeL = Conn f g h+  where+    f = maybe (Right minimal) Left+    g = either Just (const Nothing)+    h = maybe (Right maximal) Left++maybeR :: Triple () a => Conn k (Maybe b) (Either a b)+maybeR = Conn f g h+  where+    f = maybe (Left minimal) Right+    g = either (const Nothing) Just+    h = maybe (Left maximal) Right++{-+instance (Triple (a, a) a, Triple (b, b) b) => Connection k ((a, b), (a, b)) (a, b) where+  conn = Conn (uncurry joinTuple) fork (uncurry meetTuple)++instance Left (a, a) a => Connection 'L (Maybe a, Maybe a) (Maybe a) where+  conn = ConnL (uncurry joinMaybe) fork++instance Right (a, a) a => Connection 'R (Maybe a, Maybe a) (Maybe a) where+  conn = ConnR fork (uncurry meetMaybe)++instance Left (a, a) a => Connection 'L (Extended a, Extended a) (Extended a) where+  conn = ConnL (uncurry joinExtended) fork++instance Right (a, a) a => Connection 'R (Extended a, Extended a) (Extended a) where+  conn = ConnR fork (uncurry meetExtended)++-- | All minimal elements of the upper lattice cover all maximal elements of the lower lattice.+instance (Left (a, a) a, Left (b, b) b) => Connection 'L (Either a b, Either a b) (Either a b) where+  conn = ConnL (uncurry joinEither) fork++instance (Right (a, a) a, Right (b, b) b) => Connection 'R (Either a b, Either a b) (Either a b) where+  conn = ConnR fork (uncurry meetEither)++joinMaybe :: Connection 'L (a, a) a => Maybe a -> Maybe a -> Maybe a+joinMaybe (Just x) (Just y) = Just (x `join` y)+joinMaybe u@(Just _) _ = u+joinMaybe _ u@(Just _) = u+joinMaybe Nothing Nothing = Nothing++meetMaybe :: Connection 'R (a, a) a => Maybe a -> Maybe a -> Maybe a+meetMaybe Nothing Nothing = Nothing+meetMaybe Nothing _ = Nothing+meetMaybe _ Nothing = Nothing+meetMaybe (Just x) (Just y) = Just (x `meet` y)++joinExtended :: Connection 'L (a, a) a => Extended a -> Extended a -> Extended a+joinExtended Top          _            = Top+joinExtended _            Top          = Top+joinExtended (Extended x) (Extended y) = Extended (x `join` y)+joinExtended Bottom       y            = y+joinExtended x            Bottom       = x++meetExtended :: Connection 'R (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)+meetExtended Bottom       _            = Bottom+meetExtended _            Bottom       = Bottom++joinEither :: (Connection 'L (a, a) a, Connection 'L (b, b) b) => Either a b -> Either a b -> Either a b+joinEither (Right x) (Right y) = Right (x `join` y)+joinEither u@(Right _) _ = u+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 (Left x) (Left y) = Left (x `meet` y)+meetEither l@(Left _) _ = l+meetEither _ l@(Left _) = l+meetEither (Right x) (Right y) = Right (x `meet` y)++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 (x1, y1) (x2, y2) = (x1 `meet` x2, y1 `meet` y2) -}

@@ -1,137 +1,246 @@-{-# Language TypeFamilies        #-}-{-# Language TypeApplications    #-}-{-# Language AllowAmbiguousTypes #-}-{-# Language ConstraintKinds     #-}-{-# Language Safe                #-}-{-# Language DeriveFunctor       #-}-{-# Language DeriveGeneric       #-}-{-# Language DataKinds           #-}-{-# Language ViewPatterns        #-}-{-# Language PatternSynonyms     #-}-{-# Language RankNTypes          #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE Safe #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE ViewPatterns #-}+ module Data.Connection.Conn (-  -- * Conn-    Kan(..)-  , Conn()-  , embed-  -- ** Trip-  , type Trip-  , pattern Conn-  , trip-  , range-  -- ** ConnL-  , type ConnL-  , pattern ConnL-  , swapL-  , downL-  , unitL-  , counitL-  , lowerL-  , lowerL1-  , lowerL2-  , upperL1-  , upperL2-  -- ** ConnR-  , type ConnR-  , pattern ConnR-  , swapR-  , downR-  , unitR-  , counitR-  , upperR-  , upperR1-  , upperR2-  , lowerR1-  , lowerR2-  -- * Connections-  , choice-  , strong-  , fmapped+    -- * Conn+    Kan (..),+    Conn (),+    pattern Conn,+    embed,+    range,+    identity,++    -- * Connection k+    ConnK,+    half,+    midpoint,+    roundWith,+    roundWith1,+    roundWith2,+    truncateWith,+    truncateWith1,+    truncateWith2,++    -- * Connection L+    ConnL,+    pattern ConnL,+    upL,+    downL,+    swapL,+    counit,+    upper,+    upper1,+    upper2,+    filterWith,+    ceilingWith,+    ceilingWith1,+    ceilingWith2,++    -- * Connection R+    ConnR,+    pattern ConnR,+    upR,+    downR,+    swapR,+    unit,+    lower,+    lower1,+    lower2,+    idealWith,+    floorWith,+    floorWith1,+    floorWith2,++    -- * Combinators+    (>>>),+    (<<<),+    choice,+    strong, ) where  import safe Control.Arrow-import safe Control.Category (Category)+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(..), Bounded)-import safe qualified Control.Category as C+import safe Prelude hiding (Ord (..)) --- | A data kind distinguishing the chirality of a Kan extension.------ Here it serves to distinguish the directionality of a preorder:------ * /L/-tagged types are 'upwards-directed'+-- $setup+-- >>> :set -XTypeApplications+-- >>> import Data.Int+-- >>> import Data.Ord (Down(..))+-- >>> import GHC.Real (Ratio(..))+-- >>> :load Data.Connection+-- >>> ratf32 = conn @_ @Rational @Float+-- >>> f64f32 = conn @_ @Double @Float++-- | A data kind distinguishing the directionality of a Galois connection: ----- * /R/-tagged types are 'downwards-directed'+-- * /L/-tagged types are low / increasing (e.g. 'Data.Connection.Class.minimal', 'Data.Connection.Class.upper', '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') data Kan = L | R  -- | An < https://ncatlab.org/nlab/show/adjoint+string adjoint string > of Galois connections of length 2 or 3. ---data Conn (k :: Kan) a b = Conn_ (a -> (b , b)) (b -> a)+-- 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)  instance Category (Conn k) where-  id = Conn_ (id &&& id) id+    id = identity+    {-# INLINE id #-} -  Conn_ f1 g1 . Conn_ f2 g2 = Conn_ ((fst.f1).(fst.f2) &&& (snd.f1).(snd.f2)) (g2 . g1)+    Galois f1 g1 . Galois f2 g2 = Galois ((fst . f1) . (fst . f2) &&& (snd . f1) . (snd . f2)) (g2 . g1)+    {-# INLINE (.) #-} --- | Obtain the center of a /Trip/, upper half of a /ConnL/, or the lower half of a /ConnR/.+-- | Obtain a /Conn/ from an adjoint triple of monotone functions. ---embed :: Conn k a b -> b -> a-embed (Conn_ _ g) = g+--  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 (Conn_ f _) = fst . f+_1 (Galois 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 (Conn_ f _) = snd . f+_2 (Galois 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'.+embed :: Conn k a b -> b -> a+embed (Galois _ g) = g+{-# INLINE embed #-}++-- | Obtain the upper and/or lower adjoints of a connection.+--+-- > range c = floorWith c &&& ceilingWith 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+{-# INLINE range #-}+ ------------------------------------------------------------------------ Trip+-- ConnK ---------------------------------------------------------------------  -- | An <https://ncatlab.org/nlab/show/adjoint+triple adjoint triple> of Galois connections. -- -- An adjoint triple is a chain of connections of length 3: ----- \(f \dashv g \dashv h \) +-- \(f \dashv g \dashv h \) -- -- 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. ---type Trip a b = forall k. Conn k a b+-- @ 'half' t x = 'pcompare' (x - 'lower' t x) ('upper' t x - 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 #-} --- | A view pattern for an arbitrary (left or right) 'Conn'.+-- | Return the midpoint of the interval containing x. ----- /Caution/: /Conn f g h/ must obey \(f \dashv g \dashv h\). This condition is not checked.+-- >>> 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 #-}++-- | Return the nearest value to x. ----- For detailed properties see 'Data.Connection.Property'.+-- > roundWith identity = id ---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 #-}+-- 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>.+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 #-} --- | Obtain a /forall k. Conn k/ from an adjoint triple of monotone functions.+-- | Lift a unary function over a 'ConnK'. ----- /Caution/: @Conn f g h@ must obey \(f \dashv g \dashv h\). This condition is not checked.+-- 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 #-}++-- | Lift a binary function over a 'ConnK'. ---trip :: (a -> b) -> (b -> a) -> (a -> b) -> Trip a b-trip f g h = Conn_ (h &&& f) g+-- Results are rounded to the nearest value with ties away from 0.+--+-- Example avoiding loss-of-precision:+--+-- >>> 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 #-} --- | Obtain the lower and upper functions from a 'Trip'.+-- | Truncate towards zero. ----- > range c = upperR c &&& lowerL c+-- > 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'. ----- >>> range f64f32 pi--- (3.1415925,3.1415927)--- >>> range f64f32 (0/0)--- (NaN,NaN)+-- Results are truncated towards zero. ---range :: Trip a b -> a -> (b, b)-range c = upperR c &&& lowerL c +-- > 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 #-} +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 #-}+ --------------------------------------------------------------------- -- ConnL ---------------------------------------------------------------------@@ -142,7 +251,7 @@ -- is an adjunction in the category of preorders. -- -- Each side of the connection may be defined in terms of the other:--- +-- --  \( g(x) = \sup \{y \in E \mid f(y) \leq x \} \) -- --  \( f(x) = \inf \{y \in E \mid g(y) \geq x \} \)@@ -150,94 +259,122 @@ -- For further information see 'Data.Connection.Property'. -- -- /Caution/: Monotonicity is not checked.--- type ConnL = Conn 'L  -- | A view pattern for a 'ConnL'. -- -- /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 = Conn_ (f &&& f) g+pattern ConnL f g <- (_2 &&& embed -> (f, g)) where ConnL f g = Galois (f &&& f) g+ {-# COMPLETE ConnL #-} --- | Witness to the symmetry between 'ConnL' and 'ConnR'.------ > swapL . swapR = id--- > swapR . swapL = id+-- | Convert an inverted 'ConnL' to a 'ConnL'. ---swapL :: ConnR a b -> ConnL b a-swapL (ConnR f g) = ConnL f g+-- > 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 arbitrary 'Conn' to an inverted 'ConnL'.+-- | Convert a 'ConnL' to an inverted 'ConnL'. ----- >>> unitL (downL $ conn @_ @() @Ordering) (Down LT)+-- >>> upper (downL $ conn @_ @() @Ordering) (Down LT) -- Down LT--- >>> unitL (downL $ conn @_ @() @Ordering) (Down GT)+-- >>> 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 #-} --- | Round trip through a connection.------ > unitL c = upperL1 c id = embed c . lowerL c--- > x <= unitL c x--- --- >>> compare pi $ unitL f64f32 pi--- LT+-- | Witness to the symmetry between 'ConnL' and 'ConnR'. ---unitL :: ConnL a b -> a -> a-unitL c = upperL1 c id+-- > swapL . swapR = id+-- > swapR . swapL = id+swapL :: ConnR a b -> ConnL b a+swapL (ConnR f g) = ConnL f g+{-# INLINE swapL #-} --- | Reverse round trip through a connection.+-- | Reverse round trip through a 'ConnK' or 'ConnL'. ----- > x >= counitL c x+-- This is the counit of the resulting comonad: ----- >>> counitL (conn @_ @() @Ordering) LT+-- > x >~ counit c x+--+-- >>> counit (conn @_ @() @Ordering) LT -- LT--- >>> counitL (conn @_ @() @Ordering) GT+-- >>> counit (conn @_ @() @Ordering) GT -- LT+counit :: ConnL a b -> b -> b+counit c = ceilingWith1 c id+{-# INLINE counit #-}++-- | Round trip through a 'ConnK' or 'ConnL'. ---counitL :: ConnL a b -> b -> b-counitL c = lowerL1 c id+-- > upper c = upper1 c id = embed c . ceilingWith c+-- > x <= upper c x+--+-- >>> compare pi $ upper f64f32 pi+-- LT+upper :: ConnL a b -> a -> a+upper c = upper1 c id+{-# INLINE upper #-} --- | Extract the lower half of a 'Trip' or 'ConnL'.+-- | 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 '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 #-}++-- | Obtain the principal filter in /B/ generated by an element of /A/. ----- When /a/ and /b/ are lattices we have:+-- 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/. ----- > lowerL c (x1 \/ a2) = lowerL c x1 \/ lowerL c x2+-- /filterWith/ and /idealWith/ commute with /Down/: ----- This is the adjoint functor theorem for preorders.+-- > filterWith c a b <=> idealWith c (Down a) (Down b) ----- >>> upperR f64f32 pi--- 3.1415925--- >>> lowerL f64f32 pi--- 3.1415927+-- > filterWith c (Down a) (Down b) <=> idealWith c a b ---lowerL :: ConnL a b -> a -> b-lowerL (ConnL f _) = f---- | Map over a connection from the left.+-- /filterWith c a/ is upward-closed for all /a/: ---lowerL1 :: ConnL a b -> (a -> a) -> b -> b-lowerL1 (ConnL f g) h b = f $ h (g b)---- | Zip over a connection from the left.+-- > a <= b1 && b1 <= b2 => a <= b2 ---lowerL2 :: ConnL a b -> (a -> a -> a) -> b -> b -> b-lowerL2 (ConnL f g) h b1 b2 = f $ h (g b1) (g b2)---- | Map over a connection from the left.+-- > a1 <= b && inf a2 <= b => ceiling a1 `meet` ceiling a2 <= b ---upperL1 :: ConnL a b -> (b -> b) -> a -> a-upperL1 (ConnL f g) h a = g $ h (f a)+-- 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 #-} --- | Zip over a connection from the left.+-- | Extract the left half of a 'ConnK' or 'ConnL'. ---upperL2 :: ConnL a b -> (b -> b -> b) -> a -> a -> a-upperL2 (ConnL f g) h a1 a2 = g $ h (f a1) (f a2)+-- >>> 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 #-}++-- | 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 #-}+ --------------------------------------------------------------------- -- ConnR ---------------------------------------------------------------------@@ -252,126 +389,144 @@ -- use one version over the other. -- -- However some use cases (e.g. rounding) require an adjoint triple--- of connections (i.e. a 'Trip') that can lower into a standard+-- of connections (i.e. a 'ConnK') that can lower into a standard -- connection in either of two ways.--- type ConnR = Conn 'R  -- | A view pattern for a 'ConnR'. -- -- /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 = Conn_ (g &&& g) f+pattern ConnR f g <- (embed &&& _1 -> (f, g)) where ConnR f g = Galois (g &&& g) f+ {-# COMPLETE ConnR #-} --- | Convert an arbitrary 'Conn' to an inverted 'ConnR'.+-- | Convert an inverted 'ConnR' to a 'ConnR'. ----- >>> counitR (downR $ conn @_ @() @Ordering) (Down LT)+-- > upR . downR = downR . upR = id+upR :: ConnR (Down a) (Down b) -> ConnR b a+upR (ConnR f g) = ConnR g' f'+  where+    f' x = let (Down y) = f (Down x) in y+    g' x = let (Down y) = g (Down x) in y+{-# INLINE upR #-}++-- | Convert a 'ConnR' to an inverted 'ConnR'.+--+-- >>> lower (downR $ conn @_ @() @Ordering) (Down LT) -- Down GT--- >>> counitR (downR $ conn @_ @() @Ordering) (Down GT)+-- >>> lower (downR $ conn @_ @() @Ordering) (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'. -- -- > 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 connection.+-- | Round trip through a 'ConnK' or 'ConnR'. ----- > unitR c = upperR1 c id = upperR c . embed c--- > x <= unitR c x+-- This is the unit of the resulting monad: ----- >>> unitR (conn @_ @() @Ordering) LT+-- > x <~ unit c x+-- > unit c = floorWith1 c id = floorWith c . embed c+--+-- >>> unit (conn @_ @() @Ordering) LT -- GT--- >>> unitR (conn @_ @() @Ordering) GT+-- >>> unit (conn @_ @() @Ordering) GT -- GT----unitR :: ConnR a b -> b -> b-unitR c = upperR1 c id+unit :: ConnR a b -> b -> b+unit c = floorWith1 c id+{-# INLINE unit #-} --- | Reverse round trip through a connection.+-- | Reverse round trip through a 'ConnK' or 'ConnR'. ----- > x >= counitR c x+-- > x >~ lower c x ----- >>> compare pi $ counitR f64f32 pi+-- >>> compare pi $ lower f64f32 pi -- GT----counitR :: ConnR a b -> a -> a-counitR c = lowerR1 c id+lower :: ConnR a b -> a -> a+lower c = lower1 c id+{-# INLINE lower #-} --- | Extract the upper half of a connection.+-- | 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 #-}++-- | Obtain the principal ideal in /B/ generated by an element of /A/. ----- When /a/ and /b/ are lattices we have:+-- 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/. ----- > upperR c (x1 /\ x2) = upperR c x1 /\ upperR c x2+-- /idealWith c a/ is downward-closed for all /a/: ----- This is the adjoint functor theorem for preorders.+-- > a >= b1 && b1 >= b2 => a >= b2 ----- >>> upperR f64f32 pi--- 3.1415925--- >>> lowerL f64f32 pi--- 3.1415927+-- > a1 >= b && a2 >= b => floor a1 `join` floor a2 >= b ---upperR :: ConnR a b -> a -> b-upperR (ConnR _ g) = g+-- 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 #-} --- | Map over a connection from the left.+-- | Extract the right half of a 'ConnK' or 'ConnR' ---upperR1 :: ConnR a b -> (a -> a) -> b -> b-upperR1 (ConnR f g) h b = g $ h (f b)---- | Zip over a connection from the left.+-- This is the adjoint functor theorem for preorders. ---upperR2 :: ConnR a b -> (a -> a -> a) -> b -> b -> b-upperR2 (ConnR f g) h b1 b2 = g $ h (f b1) (f b2)+-- >>> 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 connection from the right.----lowerR1 :: ConnR a b -> (b -> b) -> a -> a-lowerR1 (ConnR f g) h a = f $ h (g a)+-- | 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 connection from the right.----lowerR2 :: ConnR a b -> (b -> b -> b) -> a -> a -> a-lowerR2 (ConnR f g) h a1 a2 = f $ h (g a1) (g a2)+-- | 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 #-}  ------------------------------------------------------------------------ Connections+-- 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')+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'---- | 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').----fmapped :: Functor f => Conn k a b -> Conn k (f a) (f b)-fmapped (Conn f g h) = Conn (fmap f) (fmap g) (fmap h)+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 #-}

@@ -1,322 +0,0 @@-{-# Language ConstraintKinds #-}-{-# Language Safe            #-}-{-# Language RankNTypes      #-}-module Data.Connection.Double (-    f64f32-  , f64i08-  , f64i16-  , f64i32-  , min64-  , max64-  , ulp-  , covers-  , shift-  , within-  , epsilon-  , until-) where-----import safe Data.Universe.Class-import safe Data.Bool-import safe Data.Connection.Conn-import safe Data.Int-import safe Data.Order-import safe Data.Order.Extended-import safe Data.Order.Syntax hiding (min, max)-import safe Data.Word-import safe GHC.Float as F-import safe Prelude hiding (Eq(..), Ord(..), until)-import safe qualified Data.Connection.Float as F32-import safe qualified Prelude as P-------------------------------------------------------------------------- Connections------------------------------------------------------------------------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) (<~) (F32.shift 1) z--  descend32 z h1 x = until (\y -> h1 y <~ x) (>~) (F32.shift (-1)) z---- | 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--------------------------------------------------------------------------- Double-------------------------------------------------------------------------- | A /NaN/-handling min function.------ > min64 x NaN = x--- > min64 NaN y = y----min64 :: Double -> Double -> Double-min64 x y = case (isNaN x, isNaN y) of-  (False, False) -> if x <= y then x else y-  (False, True) -> x-  (True, False) -> y-  (True, True)  -> x---- | A /NaN/-handling max function.------ > max64 x NaN = x--- > max64 NaN y = y----max64 :: Double -> Double -> Double-max64 x y = case (isNaN x, isNaN y) of-  (False, False) -> if x >= y then x else y-  (False, True) -> x-  (True, False) -> y-  (True, True)  -> x---- | Covering relation on the /N5/ lattice of doubles.------ < https://en.wikipedia.org/wiki/Covering_relation >------ >>> covers 1 (shift 1 1)--- True--- >>> covers 1 (shift 2 1)--- False----covers :: Double -> Double -> Bool-covers x y = x ~~ shift (-1) y---- | Compute the signed distance between two doubles in units of least precision.------ >>> ulp 1.0 (shift 1 1.0)--- Just (LT,1)--- >>> ulp (0.0/0.0) 1.0--- Nothing----ulp :: Double -> Double -> Maybe (Ordering, Word64)-ulp x y = fmap f $ pcompare x y-  where  x' = doubleInt64 x-         y' = doubleInt64 y-         f LT = (LT, fromIntegral . abs $ y' - x')-         f EQ = (EQ, 0)-         f GT = (GT, fromIntegral . abs $ x' - y')---- | Shift by /n/ units of least precision.------ >>> shift 1 0--- 1.0e-45--- >>> shift 1 $ 0/0--- NaN--- >>> shift (-1) $ 0/0--- NaN--- >>> shift 1 $ 1/0--- Infinity----shift :: Int64 -> Double -> Double-shift n x | x ~~ 0/0 = x-          | otherwise = int64Double . clamp64 . (+ n) . doubleInt64 $ x---- | Compare two double-precision floats for approximate equality.------ Required accuracy is specified in units of least precision.------ See also <https://randomascii.wordpress.com/2012/02/25/comparing-floating-point-numbers-2012-edition/>.--- -within :: Word64 -> Double -> Double -> Bool-within tol x y = maybe False ((<= tol) . snd) $ ulp x y---- | Difference between 1 and the smallest representable value greater than 1.------ > epsilon = shift 1 1 - 1------ >>> epsilon--- 2.220446049250313e-16----epsilon :: Double-epsilon = shift 1 1.0 - 1.0--{----- | Minimal positive value.------ >>> minimal64--- 5.0e-324--- >>> shift (-1) minimal64--- 0----minimal64 :: Double-minimal64 = shift 1 0.0---- | Maximum finite value.------ >>> maximal64--- 1.7976931348623157e308--- >>> shift 1 maximal64--- Infinity--- >>> shift (-1) $ negate maximal64--- -Infinity--- -maximal64 :: Double-maximal64 = shift (-1) maxBound --}------------------------------------------------------------------------------------ Orphans-----------------------------------------------------------------------{--instance Universe Double where-  universe = 0/0 : indexFromTo (minBound ... maxBound)--instance Finite Double--}------------------------------------------------------------------------- Internal------------------------------------------------------------------------{-# INLINE until #-}-until :: (a -> Bool) -> (a -> a -> Bool) -> (a -> a) -> a -> a-until pre rel f seed = go seed-  where go x | x' `rel` x = x-             | pre x = x-             | otherwise = go x'-          where x' = f x------- Non-monotonic function -signed64 :: Word64 -> Int64-signed64 x | x < 0x8000000000000000 = fromIntegral x-           | otherwise      = fromIntegral (maxBound P.- (x P.- 0x8000000000000000))---- Non-monotonic function converting from 2s-complement format.-unsigned64 :: Int64 -> Word64-unsigned64 x | x >~ 0  = fromIntegral x-             | otherwise = 0x8000000000000000 + (maxBound P.- (fromIntegral x))---- Clamp between the int representations of -1/0 and 1/0 -clamp64 :: Int64 -> Int64-clamp64 = P.max (-9218868437227405313) . P.min 9218868437227405312 --int64Double :: Int64 -> Double-int64Double = word64Double . unsigned64--doubleInt64 :: Double -> Int64-doubleInt64 = signed64 . doubleWord64 ---- Bit-for-bit conversion.-word64Double :: Word64 -> Double-word64Double = F.castWord64ToDouble---- TODO force to pos representation?--- Bit-for-bit conversion.-doubleWord64 :: Double -> Word64-doubleWord64 = (+0) . F.castDoubleToWord64--{----- | 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--  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'.-i64f64 :: Conn (Maybe Int64) Double-i64f64 = Conn (nan g) (nanf f) where-  f x | abs x <~ 2**53-1 = P.floor x-      | otherwise = if x >~ 0 then maxBound else -2^53--  g i | abs i <~ 2^53-1 = fromIntegral i-      | otherwise = if i >~ 0 then 2**53 else -1/0---- | 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--  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'.-ixxf64 :: Conn (Maybe Int) Double-ixxf64 = Conn (nan g) (nanf f) where-  f x | abs x <~ 2**53-1 = P.floor x-      | otherwise = if x >~ 0 then maxBound else -2^53--  g i | abs i <~ 2^53-1 = fromIntegral i-      | otherwise = if i >~ 0 then 2**53 else -1/0---}---{---- |------ @'lower64' x@ is the least element /y/ in the descending--- chain such that @not $ f y '<~' x@.----lower :: Preorder a => Double -> (Double -> a) -> a -> Double-lower z f x = until (\y -> f y <~ x) (>~) (shift $ -1) z---- |------ @'upper64' y@ is the greatest element /x/ in the ascending--- chain such that @g x '<~' y@.----upper :: Preorder a => Double -> (Double -> a) -> a -> Double-upper z g y = until (\x -> g x >~ y) (<~) (shift 1) z---- |------ @'lower' x@ is the least element /y/ in the descending--- chain such that @not $ f y '<~' x@.----lower :: Preorder a => Float -> (Float -> a) -> a -> Float-lower z f x = until (\y -> f y <~ x) (>~) (F32.shift $ -1) z---- |------ @'upper' y@ is the greatest element /x/ in the ascending--- chain such that @not $ g x '>~' y@.----upper :: Preorder a => Float -> (Float -> a) -> a -> Float-upper z g y = until (\x -> g x >~ y) (<~) (F32.shift 1) z--}--------------------------------------------------------------------------- Internal------------------------------------------------------------------------triple :: (Bounded a, Integral a) => Double -> Conn k Double (Extended a)-triple high = Conn f1 g f2 where-  f1 = liftExtended (~~ -1/0) (\x -> x ~~ 0/0 || x > high) $ \x -> if x < low then minBound else P.ceiling x--  f2 = liftExtended (\x -> x ~~ 0/0 || x < low) (~~ 1/0) $ \x -> if x > high then maxBound else P.floor x--  g = extended (-1/0) (1/0) P.fromIntegral- -  low = -1 - high

@@ -1,17 +1,30 @@-{-# Language ConstraintKinds #-}-{-# Language Safe            #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE Safe #-}+ module Data.Connection.Float (-  -- * Connections-    f32i08-  , f32i16-  --, f32i32-  , min32-  , max32-  , covers-  , ulp-  , shift-  , within-  , epsilon+    -- * Connections+    f32i08,+    f32i16,+    f64i08,+    f64i16,+    f64i32,+    f64f32,++    -- * Float+    min32,+    max32,+    ulp32,+    near32,+    shift32,++    -- * Double+    min64,+    max64,+    ulp64,+    near64,+    shift64,+    until, ) where  import safe Data.Bool@@ -19,13 +32,63 @@ import safe Data.Int import safe Data.Order import safe Data.Order.Extended-import safe Data.Order.Syntax+import safe Data.Order.Syntax hiding (max, min) import safe Data.Word import safe GHC.Float as F-import safe Prelude hiding (Eq(..), Ord(..), until)-import safe qualified Prelude as P +import safe Prelude hiding (Eq (..), Ord (..), until)+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 --------------------------------------------------------------------- @@ -33,124 +96,200 @@ -- -- > min32 x NaN = x -- > min32 NaN y = y--- min32 :: Float -> Float -> Float min32 x y = case (isNaN x, isNaN y) of-  (False, False) -> if x <= y then x else y-  (False, True) -> x-  (True, False) -> y-  (True, True)  -> x+    (False, False) -> if x <= y then x else y+    (False, True) -> x+    (True, False) -> y+    (True, True) -> x  -- | A /NaN/-handling max32 function. -- -- > max32 x NaN = x -- > max32 NaN y = y--- max32 :: Float -> Float -> Float max32 x y = case (isNaN x, isNaN y) of-  (False, False) -> if x >= y then x else y-  (False, True) -> x-  (True, False) -> y-  (True, True)  -> x---- | Covering relation on the /N5/ lattice of floats.------ < https://en.wikipedia.org/wiki/Covering_relation >------ >>> covers 1 (shift 1 1)--- True--- >>> covers 1 (shift 2 1)--- False----covers :: Float -> Float -> Bool-covers x y = x ~~ shift (-1) y+    (False, False) -> if x >= y then x else y+    (False, True) -> x+    (True, False) -> y+    (True, True) -> x  -- | Compute the signed distance between two floats in units of least precision. ----- >>> ulp 1.0 (shift 1 1.0)+-- >>> ulp32 1.0 (shift32 1 1.0) -- Just (LT,1)--- >>> ulp (0.0/0.0) 1.0+-- >>> ulp32 (0.0/0.0) 1.0 -- Nothing+ulp32 :: Float -> Float -> Maybe (Ordering, Word32)+ulp32 x y = fmap f $ pcompare x y+  where+    x' = floatInt32 x+    y' = floatInt32 y+    f LT = (LT, fromIntegral . abs $ y' - x')+    f EQ = (EQ, 0)+    f GT = (GT, fromIntegral . abs $ x' - y')++-- | Compare two floats for approximate equality. ---ulp :: Float -> Float -> Maybe (Ordering, Word32)-ulp x y = fmap f $ pcompare x y-  where  x' = floatInt32 x-         y' = floatInt32 y-         f LT = (LT, fromIntegral . abs $ y' - x')-         f EQ = (EQ, 0)-         f GT = (GT, fromIntegral . abs $ x' - y')+-- Required accuracy is specified in units of least precision.+--+-- See also <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  -- | Shift a float by /n/ units of least precision. ----- >>> shift 1 0+-- >>> shift32 1 0 -- 1.0e-45--- >>> shift 1 $ 0/0+-- >>> shift32 1 1 - 1+-- 1.1920929e-7+-- >>> shift32 1 $ 0/0 -- NaN--- >>> shift (-1) $ 0/0+-- >>> shift32 (-1) $ 0/0 -- NaN--- >>> shift 1 $ 1/0+-- >>> shift32 1 $ 1/0 -- Infinity----shift :: Int32 -> Float -> Float-shift n x | x ~~ 0/0 = x-          | otherwise = int32Float . clamp32 . (+ n) . floatInt32 $ x+shift32 :: Int32 -> Float -> Float+shift32 n x+    | x ~~ 0 / 0 = x+    | otherwise = int32Float . clamp32 . (+ n) . floatInt32 $ x --- | Compare two floats for approximate equality.------ Required accuracy is specified in units of least precision.------ See also <https://randomascii.wordpress.com/2012/02/25/comparing-floating-point-numbers-2012-edition/>.--- -within :: Word32 -> Float -> Float -> Bool-within tol x y = maybe False ((<= tol) . snd) $ ulp x y+---------------------------------------------------------------------+-- Double+--------------------------------------------------------------------- --- | Difference between 1 and the smallest representable value greater than 1.+-- | A /NaN/-handling min function. ----- > epsilon = shift 1 1 - 1+-- > min64 x NaN = x+-- > min64 NaN y = y+min64 :: Double -> Double -> Double+min64 x y = case (isNaN x, isNaN y) of+    (False, False) -> if x <= y then x else y+    (False, True) -> x+    (True, False) -> y+    (True, True) -> x++-- | A /NaN/-handling max function. ----- >>> epsilon--- 1.1920929e-7+-- > max64 x NaN = x+-- > max64 NaN y = y+max64 :: Double -> Double -> Double+max64 x y = case (isNaN x, isNaN y) of+    (False, False) -> if x >= y then x else y+    (False, True) -> x+    (True, False) -> y+    (True, True) -> x++-- | Compute the signed distance between two doubles in units of least precision. ---epsilon :: Float-epsilon = shift 1 1.0 - 1.0+-- >>> ulp64 1.0 (shift64 1 1.0)+-- Just (LT,1)+-- >>> ulp64 (0.0/0.0) 1.0+-- Nothing+ulp64 :: Double -> Double -> Maybe (Ordering, Word64)+ulp64 x y = fmap f $ pcompare x y+  where+    x' = doubleInt64 x+    y' = doubleInt64 y+    f LT = (LT, fromIntegral . abs $ y' - x')+    f EQ = (EQ, 0)+    f GT = (GT, fromIntegral . abs $ x' - y') -{---- | Minimal32 positive value.+-- | Compare two double-precision floats for approximate equality. ----- >>> minimal32--- 1.0e-45--- >>> shift (-1) minimal32--- 0+-- Required accuracy is specified in units of least precision. ---minimal32 :: Float-minimal32 = shift 1 0.0+-- See also <https://randomascii.wordpress.com/2012/02/25/comparing-floating-point-numbers-2012-edition/>.+near64 :: Word64 -> Double -> Double -> Bool+near64 tol x y = maybe False ((<= tol) . snd) $ ulp64 x y --- | Maximum finite value.+-- | Shift by /n/ units of least precision. ----- >>> maximal32--- 3.4028235e38--- >>> shift 1 maximal32+-- >>> shift64 1 0+-- 5.0e-324+-- >>> shift64 1 1 - 1+-- 2.220446049250313e-16+-- >>> shift64 1 $ 0/0+-- NaN+-- >>> shift64 (-1) $ 0/0+-- NaN+-- >>> shift64 1 $ 1/0 -- Infinity--- >>> shift (-1) $ negate maximal32--- -Infinity----maximal32 :: Float-maximal32 = shift (-1) (1/0) ---}+shift64 :: Int64 -> Double -> Double+shift64 n x+    | x ~~ 0 / 0 = x+    | otherwise = int64Double . clamp64 . (+ n) . doubleInt64 $ x  ------------------------------------------------------------------------ Float+-- Internal --------------------------------------------------------------------- --- | All 'Data.Int.Int08' values are exactly representable in a 'Float'.-f32i08 :: Conn k Float (Extended Int8)-f32i08 = signedTriple 127+{-# INLINE until #-}+until :: (a -> Bool) -> (a -> a -> Bool) -> (a -> a) -> a -> a+until pre rel f seed = go seed+  where+    go x+        | x' `rel` x = x+        | pre x = x+        | otherwise = go x'+      where+        x' = f x --- | All 'Data.Int.Int16' values are exactly representable in a 'Float'.-f32i16 :: Conn k Float (Extended Int16)-f32i16 = signedTriple 32767+-- Non-monotonic function+signed32 :: Word32 -> Int32+signed32 x+    | x < 0x80000000 = fromIntegral x+    | otherwise = fromIntegral (maxBound - (x - 0x80000000)) +-- Non-monotonic function+signed64 :: Word64 -> Int64+signed64 x+    | x < 0x8000000000000000 = fromIntegral x+    | otherwise = fromIntegral (maxBound P.- (x P.- 0x8000000000000000))++-- Non-monotonic function converting from 2s-complement format.+unsigned32 :: Int32 -> Word32+unsigned32 x+    | x >= 0 = fromIntegral x+    | otherwise = 0x80000000 + (maxBound - (fromIntegral x))++-- Non-monotonic function converting from 2s-complement format.+unsigned64 :: Int64 -> Word64+unsigned64 x+    | x >~ 0 = fromIntegral x+    | otherwise = 0x8000000000000000 + (maxBound P.- (fromIntegral x))++int32Float :: Int32 -> Float+int32Float = F.castWord32ToFloat . unsigned32++floatInt32 :: Float -> Int32+floatInt32 = signed32 . (+ 0) . F.castFloatToWord32++int64Double :: Int64 -> Double+int64Double = F.castWord64ToDouble . unsigned64++doubleInt64 :: Double -> Int64+doubleInt64 = signed64 . (+ 0) . F.castDoubleToWord64++-- Clamp between the int representations of -1/0 and 1/0+clamp32 :: Int32 -> Int32+clamp32 = P.max (-2139095041) . P.min 2139095040++-- Clamp between the int representations of -1/0 and 1/0+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+  where+    f = liftExtended (~~ -1 / 0) (\x -> x ~~ 0 / 0 || x > high) $ \x -> if x < low then minBound else P.ceiling x++    g = extended (-1 / 0) (1 / 0) P.fromIntegral++    h = liftExtended (\x -> x ~~ 0 / 0 || x < low) (~~ 1 / 0) $ \x -> if x > high then maxBound else P.floor x++    low = -1 - high+ {- -- | Exact embedding up to the largest representable 'Int32'. f32i32 :: ConnL Float (Maybe Int32)@@ -161,7 +300,6 @@   g i | abs' i <~ 2^24-1 = fromIntegral i       | otherwise = if i >~ 0 then 1/0 else -2**24 - -- | Exact embedding up to the largest representable 'Int32'. i32f32 :: ConnL (Maybe Int32) Float i32f32 = Conn (nan g) (nanf f) where@@ -170,47 +308,22 @@    g i | abs i <~ 2^24-1 = fromIntegral i       | otherwise = if i >~ 0 then 2**24 else -1/0--} ------------------------------------------------------------------------- Internal------------------------------------------------------------------------signedTriple :: (Bounded a, Integral a) => Float -> Conn k Float (Extended a)-signedTriple high = Conn f g h where--  f = liftExtended (~~ -1/0) (\x -> x ~~ 0/0 || x > high) $ \x -> if x < low then minBound else P.ceiling x--  g = extended (-1/0) (1/0) P.fromIntegral- -  h = liftExtended (\x -> x ~~ 0/0 || x < low) (~~ 1/0) $ \x -> if x > high then maxBound else P.floor x--  low = -1 - high---- Non-monotonic function -signed32 :: Word32 -> Int32-signed32 x | x < 0x80000000 = fromIntegral x-           | otherwise      = fromIntegral (maxBound - (x - 0x80000000))---- Non-monotonic function converting from 2s-complement format.-unsigned32 :: Int32 -> Word32-unsigned32 x | x >= 0  = fromIntegral x-             | otherwise = 0x80000000 + (maxBound - (fromIntegral x))---- Clamp between the int representations of -1/0 and 1/0 -clamp32 :: Int32 -> Int32-clamp32 = P.max (-2139095041) . P.min 2139095040--int32Float :: Int32 -> Float-int32Float = word32Float . unsigned32+-- | 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 -floatInt32 :: Float -> Int32-floatInt32 = signed32 . floatWord32 +  g i | abs' i <~ 2^53-1 = fromIntegral i+      | otherwise = if i >~ 0 then 1/0 else -2**53 --- Bit-for-bit conversion.-word32Float :: Word32 -> Float-word32Float = F.castWord32ToFloat+-- | 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 --- Bit-for-bit conversion.-floatWord32 :: Float -> Word32-floatWord32 = (+0) .  F.castFloatToWord32+  g i | abs' i <~ 2^53-1 = fromIntegral i+      | otherwise = if i >~ 0 then 1/0 else -2**53+-}

@@ -1,164 +1,163 @@-{-# Language ConstraintKinds #-}-{-# Language Safe            #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE Safe #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+ module Data.Connection.Int (-  -- * Int8-    i08c08-  , i08w08-  , i08i16-  , i08i32-  , i08i64-  , i08int-  -- * Int16-  , i16c16-  , i16w16-  , i16i32-  , i16i64-  , i16int-  -- * Int32-  , i32c32-  , i32w32-  , i32i64-  , i32int-  -- * Int64-  , i64c64-  , i64w64-  , i64int-  -- * Int-  , ixxwxx-  , ixxi64-  , ixxint-  -- * Integer-  , intnat-  , natint-  ) where+    -- * Int16+    w08i16,+    i08i16, -import safe Control.Category ((>>>))+    -- * Int32+    w08i32,+    w16i32,+    i08i32,+    i16i32,++    -- * Int64+    w08i64,+    w16i64,+    w32i64,+    i08i64,+    i16i64,+    i32i64,++    -- * Int+    w08ixx,+    w16ixx,+    w32ixx,+    i08ixx,+    i16ixx,+    i32ixx,+    i64ixx,++    -- * Integer+    w08int,+    w16int,+    w32int,+    w64int,+    wxxint,+    natint,+    i08int,+    i16int,+    i32int,+    i64int,+    ixxint,+) where+ import safe Control.Applicative import safe Control.Monad import safe Data.Connection.Conn-import safe Data.Connection.Word import safe Data.Int-import safe Data.Order.Syntax import safe Data.Word-import safe Foreign.C.Types import safe Numeric.Natural-import safe Prelude hiding (Eq(..), Ord(..), Bounded)-import safe qualified Prelude as P--i08c08 :: ConnL Int8 CChar-i08c08 = ConnL CChar $ \(CChar x) -> x--i08w08 :: Conn k Int8 Word8-i08w08 = unsigned--i08int :: ConnL Int8 (Maybe Integer)-i08int = signed--i16c16 :: ConnL Int16 CShort-i16c16 = ConnL CShort $ \(CShort x) -> x--i16w16 :: Conn k Int16 Word16-i16w16 = unsigned+import safe Prelude -i16int :: ConnL Int16 (Maybe Integer)-i16int = signed+-- Int16+w08i16 :: ConnL Word8 (Maybe Int16)+w08i16 = signed -i32c32 :: ConnL Int32 CInt-i32c32 = ConnL CInt $ \(CInt x) -> x+i08i16 :: ConnL Int8 (Maybe Int16)+i08i16 = signed -i32w32 :: Conn k Int32 Word32-i32w32 = unsigned+-- Int32+w08i32 :: ConnL Word8 (Maybe Int32)+w08i32 = signed -i32int :: ConnL Int32 (Maybe Integer)-i32int = signed+w16i32 :: ConnL Word16 (Maybe Int32)+w16i32 = signed -i64c64 :: ConnL Int64 CLong-i64c64 = ConnL CLong $ \(CLong x) -> x+i08i32 :: ConnL Int8 (Maybe Int32)+i08i32 = signed -i64w64 :: Conn k Int64 Word64-i64w64 = unsigned+i16i32 :: ConnL Int16 (Maybe Int32)+i16i32 = signed --- | /Caution/: This assumes that 'Int' on your system is 64 bits.-ixxi64 :: Conn k Int Int64-ixxi64 = Conn fromIntegral fromIntegral fromIntegral+-- Int64+w08i64 :: ConnL Word8 (Maybe Int64)+w08i64 = signed -i64int :: ConnL Int64 (Maybe Integer)-i64int = signed+w16i64 :: ConnL Word16 (Maybe Int64)+w16i64 = signed -ixxwxx :: Conn k Int Word-ixxwxx = unsigned+w32i64 :: ConnL Word32 (Maybe Int64)+w32i64 = signed --- | /Caution/: This assumes that 'Int' on your system is 64 bits.-ixxint :: ConnL Int (Maybe Integer)-ixxint = signed+i08i64 :: ConnL Int8 (Maybe Int64)+i08i64 = signed -intnat :: ConnL Integer Natural-intnat = ConnL (fromIntegral . max 0) fromIntegral+i16i64 :: ConnL Int16 (Maybe Int64)+i16i64 = signed -natint :: ConnL Natural (Maybe Integer)-natint = ConnL (fmap fromIntegral . fromPred (==0)) (maybe 0 $ P.fromInteger . max 0)+i32i64 :: ConnL Int32 (Maybe Int64)+i32i64 = signed -i08i16 :: ConnL Int8 Int16-i08i16 = i08w08 >>> w08w16 >>> w16i16+-- Int+w08ixx :: ConnL Word8 (Maybe Int)+w08ixx = signed -i08i32 :: ConnL Int8 Int32-i08i32 = i08w08 >>> w08w32 >>> w32i32+w16ixx :: ConnL Word16 (Maybe Int)+w16ixx = signed -i08i64 :: ConnL Int8 Int64-i08i64 = i08w08 >>> w08w64 >>> w64i64+w32ixx :: ConnL Word32 (Maybe Int)+w32ixx = signed -i16i32 :: ConnL Int16 Int32-i16i32 = i16w16 >>> w16w32 >>> w32i32+i08ixx :: ConnL Int8 (Maybe Int)+i08ixx = signed -i16i64 :: ConnL Int16 Int64-i16i64 = i16w16 >>> w16w64 >>> w64i64+i16ixx :: ConnL Int16 (Maybe Int)+i16ixx = signed -i32i64 :: ConnL Int32 Int64-i32i64 = i32w32 >>> w32w64 >>> w64i64+i32ixx :: ConnL Int32 (Maybe Int)+i32ixx = signed ------------------------------------------------------------------------- Internal----------------------------------------------------------------------+-- | /Caution/: This assumes that 'Int' on your system is 64 bits.+i64ixx :: Conn k Int64 Int+i64ixx = Conn fromIntegral fromIntegral fromIntegral +-- Integer+w08int :: ConnL Word8 (Maybe Integer)+w08int = signed -fromPred :: Alternative f => (t -> Bool) -> t -> f t-fromPred p a = a <$ guard (p a)+w16int :: ConnL Word16 (Maybe Integer)+w16int = signed -unsigned :: (P.Bounded a, Integral a, Integral b) => Conn k a b-unsigned = Conn f g f where-  f y = fromIntegral (y + P.maxBound + 1)-  g x = fromIntegral x - P.minBound+w32int :: ConnL Word32 (Maybe Integer)+w32int = signed -signed :: forall a. (P.Bounded a, Integral a) => ConnL a (Maybe Integer)-signed = ConnL f g where-  f = fmap fromIntegral . fromPred (==P.minBound)-  g = maybe P.minBound $ P.fromInteger . min (fromIntegral @a P.maxBound) . max (fromIntegral @a P.minBound)+w64int :: ConnL Word64 (Maybe Integer)+w64int = signed -{-+wxxint :: ConnL Word (Maybe Integer)+wxxint = signed +natint :: ConnL Natural (Maybe Integer)+natint = ConnL (fmap fromIntegral . fromPred (/= 0)) (maybe 0 $ fromInteger . max 0) -clip08 :: Integer -> Integer-clip08 = min 127 . max (-128)+i08int :: ConnL Int8 (Maybe Integer)+i08int = signed -clip16 :: Integer -> Integer-clip16 = min 32767 . max (-32768)+i16int :: ConnL Int16 (Maybe Integer)+i16int = signed -clip32 :: Integer -> Integer-clip32 = min 2147483647 . max (-2147483648)+i32int :: ConnL Int32 (Maybe Integer)+i32int = signed -clip64 :: Integer -> Integer-clip64 = min 9223372036854775807 . max (-9223372036854775808)+i64int :: ConnL Int64 (Maybe Integer)+i64int = signed -unsigned :: (Bounded a, Preorder b, Integral a, Integral b) => ConnL a b-unsigned = ConnL f g where-  f = fromIntegral . max 0-  g = fromIntegral . min (f P.maxBound)+ixxint :: ConnL Int (Maybe Integer)+ixxint = signed -signed' :: forall a k. (Bounded a, Integral a) => Conn k a (Extended Integer)-signed' = Conn f g h where-  f = liftExtended (~~ P.minBound) (const False) fromIntegral-  g = extended P.minBound P.maxBound $ P.fromInteger . min (fromIntegral @a P.maxBound) . max (fromIntegral @a P.minBound)-  h = liftExtended (const False) (~~ P.maxBound) fromIntegral--}+---------------------------------------------------------------------+-- Internal+--------------------------------------------------------------------- +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 = ConnL f g+  where+    f = fmap fromIntegral . fromPred (/= minBound)+    g = maybe minBound $ fromIntegral @b . min (fromIntegral @a maxBound) . max (fromIntegral @a minBound)

@@ -1,8 +1,8 @@-{-# Language DataKinds #-}-{-# Language TypeFamilies #-}-{-# Language TypeApplications #-}-{-# Language ConstraintKinds #-}-{-# Language RankNTypes #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}  -- | Galois connections have the same properties as adjunctions defined over other categories: --@@ -23,24 +23,22 @@ --  \( \forall x : counit \circ f (x) \sim f (x) \) -- --  \( \forall x : unit \circ g (x) \sim g (x) \)--- module Data.Connection.Property where +import Data.Connection import Data.Order import Data.Order.Property-import Data.Connection-import Data.Connection.Conn-import Prelude hiding (Num(..),Ord(..), floor, ceiling)+import Prelude hiding (Num (..), Ord (..), ceiling, floor)  -- | \( \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) => Trip 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+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@@ -51,8 +49,7 @@ -- | \( \forall x : f \dashv g \Rightarrow x \leq g \circ f (x) \) -- -- This is a required property.----closed :: (Preorder a, Preorder b) => Trip a b -> a -> Bool+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@@ -64,8 +61,7 @@ -- | \( \forall x : f \dashv g \Rightarrow x \leq g \circ f (x) \) -- -- This is a required property.----kernel :: (Preorder a, Preorder b) => Trip a b -> b -> Bool+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@@ -77,8 +73,7 @@ -- | \( \forall x, y : x \leq y \Rightarrow f (x) \leq f (y) \) -- -- This is a required property.----monotonic :: (Preorder a, Preorder b) => Trip a b -> a -> a -> b -> b -> Bool+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@@ -90,27 +85,24 @@ -- | \( \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) => Trip a b -> a -> b -> Bool+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 (unitL c) b && projective (~~) f (counitL c) a+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 (unitR c) a && projective (~~) f (counitR c) b+idempotentR c@(ConnR f g) a b = projective (~~) g (unit c) a && projective (~~) f (lower c) b  --------------------------------------------------------------------- -- Properties of general relations ---------------------------------------------------------------------  -- | \( \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 @@ -118,26 +110,15 @@ -- -- 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 -range' :: Triple () a => (a, a)-range' = (floor (), ceiling ())--ordering :: Trip () Ordering-ordering = trip (const GT) (const ()) (const LT)---extremalOrd :: (Total a, P.Bounded a) => Conn k () a---extremalOrd = Conn (const minBound) (const ()) (const maxBound)- -- | \( \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  -- | \( \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

@@ -1,163 +1,158 @@-{-# Language AllowAmbiguousTypes #-}-{-# Language ConstraintKinds     #-}-{-# Language Safe                #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE Safe #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+ module Data.Connection.Ratio (-    Ratio(..) -  , reduce-  , shiftd-  -- * Rational-  , ratf32-  , ratf64-  , rati08-  , rati16-  , rati32-  , rati64-  , ratixx-  , ratint-  -- * Positive-  , posw08-  , posw16-  , posw32-  , posw64-  , poswxx-  , posnat+    Ratio (..),+    reduce,+    shiftd,++    -- * Rational+    ratf32,+    ratf64,+    rati08,+    rati16,+    rati32,+    rati64,+    ratixx,+    ratint,++    -- * Positive+    posw08,+    posw16,+    posw32,+    posw64,+    poswxx,+    posnat, ) where  import safe Data.Connection.Conn+import safe qualified 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.Ratio import safe Data.Word-import safe GHC.Real (Ratio(..), Rational)+import safe GHC.Real (Ratio (..), Rational) import safe Numeric.Natural-import safe Prelude hiding (Ord(..), until)+import safe Prelude hiding (Ord (..), until) import safe qualified Prelude as P-import safe qualified Data.Connection.Float as F32-import safe qualified Data.Connection.Double as F64  -- | A total version of 'GHC.Real.reduce'.--- reduce :: Integral a => Ratio a -> Ratio a reduce (x :% 0) = x :% 0 reduce (x :% y) = (x `quot` d) :% (y `quot` d) where d = gcd x y  -- | Shift by n 'units of least precision' where the ULP is determined by the denominator--- --- This is an analog of 'Data.Connection.Float.shift' for rationals. --+-- 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  ------------------------------------------------------------------------ Rational+-- Ratio Integer ---------------------------------------------------------------------  rati08 :: Conn k Rational (Extended Int8)-rati08 = signedTriple 127+rati08 = signedTriple  rati16 :: Conn k Rational (Extended Int16)-rati16 = signedTriple 32767+rati16 = signedTriple  rati32 :: Conn k Rational (Extended Int32)-rati32 = signedTriple 2147483647+rati32 = signedTriple  rati64 :: Conn k Rational (Extended Int64)-rati64 = signedTriple 9223372036854775807+rati64 = signedTriple  ratixx :: Conn k Rational (Extended Int)-ratixx = signedTriple 9223372036854775807+ratixx = signedTriple  ratint :: Conn k Rational (Extended Integer)-ratint = Conn f g h where-  -  f = liftExtended (~~ ninf) (\x -> x ~~ nan || x ~~ pinf) P.ceiling+ratint = Conn f g h+  where+    f = liftExtended (~~ ninf) (\x -> x ~~ nan || x ~~ pinf) P.ceiling -  g = extended ninf pinf P.fromIntegral+    g = extended ninf pinf P.fromIntegral -  h = liftExtended (\x -> x ~~ nan || x ~~ ninf) (~~ pinf) P.floor+    h = liftExtended (\x -> x ~~ nan || x ~~ ninf) (~~ pinf) P.floor  ratf32 :: Conn k Rational Float-ratf32 = Conn (toFloating f) (fromFloating g) (toFloating h) where-  f x = let est = P.fromRational x in --F.fromRat'-          if fromFloating g est >~ x-          then est-          else ascendf est (fromFloating g) x-    -  g = flip approxRational 0 +ratf32 = Conn (toFloating f) (fromFloating g) (toFloating h)+  where+    f x =+        let est = P.fromRational x+         in if fromFloating g est >~ x+                then est+                else ascendf est (fromFloating g) x -  h x = let est = P.fromRational x in-          if fromFloating g est <~ x-          then est-          else descendf est (fromFloating g) x+    g = flip approxRational 0 -  ascendf z g1 y = F64.until (\x -> g1 x >~ y) (<~) (F32.shift 1) z+    h x =+        let est = P.fromRational x+         in if fromFloating g est <~ x+                then est+                else descendf est (fromFloating g) x -  descendf z f1 x = F64.until (\y -> f1 y <~ x) (>~) (F32.shift (-1)) z+    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) where-  f x = let est = P.fromRational x in-          if fromFloating g est >~ x-          then est-          else ascendf est (fromFloating g) x-    -  g = flip approxRational 0 +ratf64 = Conn (toFloating f) (fromFloating g) (toFloating h)+  where+    f x =+        let est = P.fromRational x+         in if fromFloating g est >~ x+                then est+                else ascendf est (fromFloating g) x -  h x = let est = P.fromRational x in-          if fromFloating g est <~ x-          then est-          else descendf est (fromFloating g) x+    g = flip approxRational 0 -  ascendf z g1 y = F64.until (\x -> g1 x >~ y) (<~) (F64.shift 1) z+    h x =+        let est = P.fromRational x+         in if fromFloating g est <~ x+                then est+                else descendf est (fromFloating g) x -  descendf z f1 x = F64.until (\y -> f1 y <~ x) (>~) (F64.shift (-1)) z+    ascendf z g1 y = Float.until (\x -> g1 x >~ y) (<~) (Float.shift64 1) z +    descendf z f1 x = Float.until (\y -> f1 y <~ x) (>~) (Float.shift64 (-1)) z+ --------------------------------------------------------------------- -- Ratio Natural --------------------------------------------------------------------- -posw08 :: Conn k Positive (Lowered Word8) -posw08 = unsignedTriple 255+posw08 :: Conn k Positive (Lowered Word8)+posw08 = unsignedTriple -posw16 :: Conn k Positive (Lowered Word16) -posw16 = unsignedTriple 65535+posw16 :: Conn k Positive (Lowered Word16)+posw16 = unsignedTriple -posw32 :: Conn k Positive (Lowered Word32) -posw32 = unsignedTriple 4294967295+posw32 :: Conn k Positive (Lowered Word32)+posw32 = unsignedTriple -posw64 :: Conn k Positive (Lowered Word64) -posw64 = unsignedTriple 18446744073709551615+posw64 :: Conn k Positive (Lowered Word64)+posw64 = unsignedTriple -poswxx :: Conn k Positive (Lowered Word) -poswxx = unsignedTriple 18446744073709551615+poswxx :: Conn k Positive (Lowered Word)+poswxx = unsignedTriple  posnat :: Conn k Positive (Lowered Natural)-posnat = Conn f g h where-  -  f = liftEitherR (\x -> x ~~ nan || x ~~ pinf) P.ceiling+posnat = Conn f g h+  where+    f = liftEitherR (\x -> x ~~ nan || x ~~ pinf) P.ceiling -  g = either P.fromIntegral (const pinf)+    g = either P.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 P.floor x  --------------------------------------------------------------------- -- Internal --------------------------------------------------------------------- -{--pabs :: (Lattice a, Eq a, Num a) => a -> a-pabs x = if 0 <~ x then x else negate x--cancel :: (Lattice a, Eq a, Num a) => Ratio a -> Ratio a-cancel (x :% y) = if x < 0 && y < 0 then (pabs x) :% (pabs y) else x :% y---- | An exception-safe version of 'nanf' for rationals.----nanr :: Integral b => (a -> Ratio b) -> Maybe a -> Ratio b-nanr f = maybe (0 :% 0) f--}- pinf :: Num a => Ratio a pinf = 1 :% 0 @@ -167,56 +162,68 @@ nan :: Num a => Ratio a nan = 0 :% 0 -{--intnat :: Conn Integer Natural-intnat = Conn (fromIntegral . max 0) fromIntegral+unsignedTriple :: forall a k. (Bounded a, Integral a) => Conn k Positive (Lowered a)+unsignedTriple = Conn f g h+  where+    f x+        | x ~~ nan = Right maxBound+        | x > high = Right maxBound+        | otherwise = Left $ P.ceiling x -natint :: Conn Natural (Lifted Integer)-natint = Conn (lifts P.fromIntegral) (lifted $ P.fromInteger . max 0)+    g = either P.fromIntegral (const pinf) -ratpos :: Conn k Rational Positive-ratpos = Conn k f g h where-  -  f = liftExtended (~~ ninf) (\x -> x ~~ nan || x ~~ pinf) P.ceiling+    h x+        | x ~~ nan = Left minBound+        | x ~~ pinf = Right maxBound+        | x > high = Left maxBound+        | otherwise = Left $ P.floor x -  g = extended minBound maxBound P.fromIntegral+    high = P.fromIntegral @a maxBound -  h = liftExtended (\x -> x ~~ nan || x ~~ ninf) (~~ pinf) P.floor--}+signedTriple :: forall a k. (Bounded a, Integral a) => Conn k Rational (Extended a)+signedTriple = Conn f g h+  where+    f = liftExtended (~~ ninf) (\x -> x ~~ nan || x > high) $ \x -> if x < low then minBound else P.ceiling x -unsignedTriple :: (Bounded a, Integral a) => Ratio Natural -> Conn k Positive (Lowered a) -unsignedTriple high = Conn f g h where-  f x | x ~~ nan = Right maxBound-      | x > high = Right maxBound-      | otherwise = Left $ P.ceiling x+    g = extended ninf pinf P.fromIntegral -  g = either P.fromIntegral (const pinf)+    h = liftExtended (\x -> x ~~ nan || x < low) (~~ pinf) $ \x -> if x > high then maxBound else P.floor x -  h x | x ~~ nan = Left minBound-      | x ~~ pinf = Right maxBound-      | x > high = Left maxBound-      | otherwise = Left $ P.floor x+    high = P.fromIntegral @a maxBound+    low = -1 - high -signedTriple :: (Bounded a, Integral a) => Rational -> Conn k Rational (Extended a)-signedTriple high = Conn f g h where+toFloating :: Fractional a => (Rational -> a) -> Rational -> a+toFloating f x+    | x ~~ nan = 0 / 0+    | x ~~ ninf = (-1) / 0+    | x ~~ pinf = 1 / 0+    | otherwise = f x -  f = liftExtended (~~ ninf) (\x -> x ~~ nan || x > high) $ \x -> if x < low then minBound else P.ceiling x+fromFloating :: (Order a, Fractional a) => (a -> Rational) -> a -> Rational+fromFloating f x+    | x ~~ 0 / 0 = nan+    | x ~~ (-1) / 0 = ninf+    | x ~~ 1 / 0 = pinf+    | otherwise = f x -  g = extended ninf pinf P.fromIntegral- -  h = liftExtended (\x -> x ~~ nan || x < low) (~~ pinf) $ \x -> if x > high then maxBound else P.floor x+{-+pabs :: (Lattice a, Eq a, Num a) => a -> a+pabs x = if 0 <~ x then x else negate x -  low = -1 - high+cancel :: (Lattice a, Eq a, Num a) => Ratio a -> Ratio a+cancel (x :% y) = if x < 0 && y < 0 then (pabs x) :% (pabs y) else x :% y +-- | An exception-safe version of 'nanf' for rationals.+--+nanr :: Integral b => (a -> Ratio b) -> Maybe a -> Ratio b+nanr f = maybe (0 :% 0) f -toFloating :: (Order (Ratio a), Fractional b, Num a) => (Ratio a -> b) -> Ratio a -> b-toFloating f x | x ~~ nan = 0/0-         | x ~~ ninf = (-1)/0-         | x ~~ pinf = 1/0-         | otherwise = f x+ratpos :: Conn k Rational Positive+ratpos = Conn k f g h where -fromFloating :: (Order a, Eq a, Fractional a, Num b) => (a -> Ratio b) -> a -> Ratio b-fromFloating f x | x ~~ 0/0 = nan-                 | x ~~ (-1)/0 = ninf-                 | x ~~ 1/0 = pinf-                 | otherwise = f x+  f = liftExtended (~~ ninf) (\x -> x ~~ nan || x ~~ pinf) P.ceiling++  g = extended minBound maxBound P.fromIntegral++  h = liftExtended (\x -> x ~~ nan || x ~~ ninf) (~~ pinf) P.floor+-}

@@ -1,145 +1,185 @@-{-# Language Safe                #-}+{-# LANGUAGE Safe #-}+ module Data.Connection.Word (-  -- * Bool-    c08bin-  , binc08-  -- * Word8-  , w08c08-  , w08i08-  , w08w16-  , w08w32-  , w08w64-  , w08wxx-  , w08nat-  -- * Word16-  , w16c16-  , w16i16-  , w16w32-  , w16w64-  , w16wxx-  , w16nat-  -- * Word32-  , w32c32-  , w32i32-  , w32w64-  , w32wxx-  , w32nat-  -- * Word64-  , w64c64-  , w64i64-  , w64nat-  -- * Word-  , wxxw64-  , wxxnat+    -- * Word8+    i08w08,++    -- * Word16+    w08w16,+    i08w16,+    i16w16,++    -- * Word32+    w08w32,+    w16w32,+    i08w32,+    i16w32,+    i32w32,++    -- * Word64+    w08w64,+    w16w64,+    w32w64,+    i08w64,+    i16w64,+    i32w64,+    i64w64,+    ixxw64,++    -- * Word+    w08wxx,+    w16wxx,+    w32wxx,+    w64wxx,+    i08wxx,+    i16wxx,+    i32wxx,+    i64wxx,+    ixxwxx,++    -- * Natural+    w08nat,+    w16nat,+    w32nat,+    w64nat,+    wxxnat,+    i08nat,+    i16nat,+    i32nat,+    i64nat,+    ixxnat,+    intnat, ) where  import safe Data.Connection.Conn import safe Data.Int-import safe Data.Order-import safe Data.Order.Syntax import safe Data.Word-import safe Foreign.C.Types import safe Numeric.Natural-import safe Prelude hiding (Ord(..), Eq(..)) -c08bin :: ConnL CBool Bool-c08bin = ConnL f g where-  f (CBool i) | i == 255 = True-              | otherwise = False-  -  g True = CBool 255-  g _ = CBool 254+-- Word8+i08w08 :: ConnL Int8 Word8+i08w08 = unsigned -binc08 :: ConnL Bool CBool-binc08 = ConnL f g where-  f False = CBool 0-  f _ = CBool 1+-- Word16+w08w16 :: ConnL Word8 Word16+w08w16 = unsigned -  g (CBool i) | i == 0 = False-              | otherwise = True+i08w16 :: ConnL Int8 Word16+i08w16 = unsigned -w08c08 :: ConnL Word8 CUChar-w08c08 = ConnL CUChar $ \(CUChar x) -> x+i16w16 :: ConnL Int16 Word16+i16w16 = unsigned -w08i08 :: ConnL Word8 Int8-w08i08 = signed+-- Word32+w08w32 :: ConnL Word8 Word32+w08w32 = unsigned -w08nat :: ConnL Word8 Natural-w08nat = unsigned+w16w32 :: ConnL Word16 Word32+w16w32 = unsigned -w08w16 :: ConnL Word8 Word16-w08w16 = unsigned+i08w32 :: ConnL Int8 Word32+i08w32 = unsigned --- w08w32 = w08w16 >>> w16w32-w08w32 :: ConnL Word8 Word32-w08w32 = unsigned+i16w32 :: ConnL Int16 Word32+i16w32 = unsigned --- w08w64 = w08w32 >>> w32w64 = w08w16 >>> w16w64+i32w32 :: ConnL Int32 Word32+i32w32 = unsigned++-- Word64 w08w64 :: ConnL Word8 Word64 w08w64 = unsigned -w08wxx :: ConnL Word8 Word-w08wxx = unsigned+w16w64 :: ConnL Word16 Word64+w16w64 = unsigned -w16c16 :: ConnL Word16 CUShort-w16c16 = ConnL CUShort $ \(CUShort x) -> x+w32w64 :: ConnL Word32 Word64+w32w64 = unsigned -w16i16 :: ConnL Word16 Int16-w16i16 = signed+i08w64 :: ConnL Int8 Word64+i08w64 = unsigned -w16w32 :: ConnL Word16 Word32-w16w32 = unsigned+i16w64 :: ConnL Int16 Word64+i16w64 = unsigned --- w16w64 = w16w32 >>> w32w64-w16w64 :: ConnL Word16 Word64-w16w64 = unsigned+i32w64 :: ConnL Int32 Word64+i32w64 = unsigned +i64w64 :: ConnL Int64 Word64+i64w64 = unsigned++ixxw64 :: ConnL Int Word64+ixxw64 = unsigned++-- Word+w08wxx :: ConnL Word8 Word+w08wxx = unsigned+ w16wxx :: ConnL Word16 Word w16wxx = unsigned -w16nat :: ConnL Word16 Natural-w16nat = unsigned+w32wxx :: ConnL Word32 Word+w32wxx = unsigned -w32c32 :: ConnL Word32 CUInt-w32c32 = ConnL CUInt $ \(CUInt x) -> x+-- | /Caution/: This assumes that 'Word' on your system is 64 bits.+w64wxx :: Conn k Word64 Word+w64wxx = Conn fromIntegral fromIntegral fromIntegral -w32i32 :: ConnL Word32 Int32-w32i32 = signed+i08wxx :: ConnL Int8 Word+i08wxx = unsigned -w32w64 :: ConnL Word32 Word64-w32w64 = unsigned+i16wxx :: ConnL Int16 Word+i16wxx = unsigned -w32wxx :: ConnL Word32 Word-w32wxx = unsigned+i32wxx :: ConnL Int32 Word+i32wxx = unsigned -w32nat :: ConnL Word32 Natural-w32nat = unsigned+i64wxx :: ConnL Int64 Word+i64wxx = unsigned -w64c64 :: ConnL Word64 CULong-w64c64 = ConnL CULong $ \(CULong x) -> x+ixxwxx :: ConnL Int Word+ixxwxx = unsigned -w64i64 :: ConnL Word64 Int64-w64i64 = signed+-- Natural+w08nat :: ConnL Word8 Natural+w08nat = unsigned +w16nat :: ConnL Word16 Natural+w16nat = unsigned++w32nat :: ConnL Word32 Natural+w32nat = unsigned+ w64nat :: ConnL Word64 Natural w64nat = unsigned --- | /Caution/: This assumes that 'Word' on your system is 64 bits.-wxxw64 :: Conn k Word Word64-wxxw64 = Conn fromIntegral fromIntegral fromIntegral---- | /Caution/: This assumes that 'Word' on your system is 64 bits. wxxnat :: ConnL Word Natural-wxxnat = ConnL fromIntegral (fromIntegral . min 18446744073709551615)+wxxnat = unsigned +i08nat :: ConnL Int8 Natural+i08nat = unsigned++i16nat :: ConnL Int16 Natural+i16nat = unsigned++i32nat :: ConnL Int32 Natural+i32nat = unsigned++i64nat :: ConnL Int64 Natural+i64nat = unsigned++ixxnat :: ConnL Int Natural+ixxnat = unsigned++intnat :: ConnL Integer Natural+intnat = ConnL (fromIntegral . max 0) fromIntegral+ --------------------------------------------------------------------- -- Internal ----------------------------------------------------------------------signed :: (Bounded b, Integral a, Integral b) => ConnL a b-signed = ConnL (\x -> fromIntegral x - minBound)-               (\y -> fromIntegral (y + maxBound + 1)) -unsigned :: (Bounded a, Preorder b, Integral a, Integral b) => ConnL a b-unsigned = ConnL f g where-  f = fromIntegral-  g = fromIntegral . min (f maxBound)+unsigned :: (Bounded a, Integral a, Integral b) => ConnL a b+unsigned = ConnL f g+  where+    f = fromIntegral . max 0+    g = fromIntegral . min (f maxBound)

@@ -1,121 +1,202 @@-{-# LANGUAGE Safe                       #-}-{-# LANGUAGE PolyKinds                  #-}-{-# LANGUAGE DataKinds                  #-}-{-# LANGUAGE ConstraintKinds            #-}-{-# LANGUAGE DefaultSignatures          #-}-{-# LANGUAGE DeriveFunctor              #-}-{-# LANGUAGE DeriveGeneric              #-}-{-# LANGUAGE DerivingVia                #-}-{-# LANGUAGE FlexibleContexts           #-}-{-# LANGUAGE FlexibleInstances          #-}-{-# LANGUAGE StandaloneDeriving         #-}-{-# LANGUAGE TypeOperators              #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE Safe #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+ -- | Lattices & algebras module Data.Lattice (-  -- * Types-    Lattice-  , Semilattice-  -- * HeytingL-  , type HeytingL-  , (\\)-  , non-  , equiv-  , boundary-  , booleanL-  , heytingL-  -- * HeytingR-  , type HeytingR-  , (//)-  , neg-  , iff-  , middle-  , booleanR-  , heytingR-  -- * Heyting-  , (\/)-  , (/\)-  , glb-  , lub-  , true-  , false-  , Heyting(..)-  -- * Symmetric-  , Biheyting-  , Symmetric(..)-  , symmetricL-  , symmetricR-  -- * Boolean-  , Boolean(..)+    -- * Semilattice+    Lattice,+    Semilattice (..),++    -- ** Meet+    Meet,+    (/\),+    top,++    -- ** Join+    Join,+    (\/),+    bottom,++    -- * Algebra+    Biheyting,+    Algebra (..),++    -- ** Heyting+    Heyting,+    (//),+    iff,+    neg,+    middle,+    heyting,+    booleanR,++    -- ** Coheyting+    Coheyting,+    (\\),+    equiv,+    non,+    boundary,+    coheyting,+    booleanL,++    -- ** Symmetric+    Symmetric (..),+    converseL,+    converseR,+    symmetricL,+    symmetricR,++    -- ** Boolean+    Boolean (..), ) where -import safe Control.Applicative import safe Data.Bifunctor (bimap) import safe Data.Bool hiding (not)-import safe Data.Connection.Conn import safe Data.Connection.Class+import safe Data.Connection.Conn import safe Data.Either-import safe Data.Functor.Contravariant-import safe Data.Foldable-import safe Data.Order-import safe Data.Order.Extended-import safe Data.Order.Interval-import safe Data.Order.Syntax import safe Data.Int-import safe Data.Maybe-import safe Data.Monoid-import safe Data.Word-import safe GHC.TypeNats---import safe Numeric.Natural-import safe Prelude hiding (Eq(..),Ord(..),Bounded, not) import safe qualified Data.IntMap as IntMap import safe qualified Data.IntSet as IntSet import safe qualified Data.Map as Map-import safe qualified Data.Map.Merge.Lazy as Map+import safe Data.Order+import safe Data.Order.Extended+import safe Data.Order.Syntax import safe qualified Data.Set as Set-import safe qualified Data.Finite as F-import safe qualified Data.Universe.Class as U+import safe Data.Word+import safe Prelude hiding (Eq (..), Ord (..), not) import safe qualified Prelude as P  ------------------------------------------------------------------------------- -- Lattices ------------------------------------------------------------------------------- +type Lattice a = (Join a, Meet a)++-- | A convenience alias for a join semilattice+type Join = Semilattice 'L++-- | A convenience alias for a meet semilattice+type Meet = Semilattice 'R+ -- | Bounded < https://ncatlab.org/nlab/show/lattice lattices >. --+-- A lattice is a partially ordered set in which every two elements have a unique join+-- (least upper bound or supremum) and a unique meet (greatest lower bound or infimum).+--+-- A bounded lattice adds unique elements 'top' and 'bottom', which serve as+-- identities to '\/' and '/\', respectively.+-- -- /Neutrality/: ----- The least and greatest elements of a complete /a/ are given by the unique--- upper and lower adjoints to the function /a -> ()/.+-- @+-- x '\/' 'bottom' = x+-- x '/\' 'top' = x+-- 'glb' 'bottom' x 'top' = x+-- 'lub' 'bottom' x 'top' = x+-- @ --+-- /Associativity/+-- -- @--- x '\/' 'false' = x--- x '/\' 'true' = x--- 'glb' 'false' x 'true' = x--- 'lub' 'false' x 'true' = x+-- x '\/' (y '\/' z) = (x '\/' y) '\/' z+-- x '/\' (y '/\' z) = (x '/\' y) '/\' z -- @ ---type Lattice a = (Eq a, Semilattice 'L a, Extremal 'L a, Semilattice 'R a, Extremal 'R a)+-- /Commutativity/+--+-- @+-- x '\/' y = y '\/' x+-- x '/\' y = y '/\' x+-- @+--+-- /Idempotency/+--+-- @+-- x '\/' x = x+-- x '/\' x = x+-- @+--+-- /Absorption/+--+-- @+-- (x '\/' y) '/\' y = y+-- (x '/\' y) '\/' y = y+-- @+--+-- See < https://en.wikipedia.org/wiki/Absorption_law Absorption >.+--+-- Note that distributivity is _not_ a requirement for a complete.+-- However when /a/ is distributive we have:+--+-- @+-- 'glb' x y z = 'lub' x y z+-- @+--+-- See < https://en.wikipedia.org/wiki/Lattice_(order) >.+class Order a => Semilattice (k :: Kan) a where+    -- | The defining connection of a bounded semilattice.+    --+    -- 'bottom' and 'top' are defined by the left and right adjoints to /a -> ()/.+    bounded :: Conn k () a+    default bounded :: Connection k () a => Conn k () a+    bounded = conn +    -- | The defining connection of a semilattice.+    --+    -- '\/' and '/\' are defined by the left and right adjoints to /a -> (a, a)/.+    semilattice :: Conn k (a, a) a+    default semilattice :: Connection k (a, a) a => Conn k (a, a) a+    semilattice = conn++infixr 6 /\ -- comment for the parser++-- | Lattice meet.+--+-- > (/\) = curry $ floorWith semilattice+(/\) :: Meet a => a -> a -> a+(/\) = curry $ floorWith semilattice+ -- | The unique top element of a bounded lattice ----- > x /\ true = x--- > x \/ true = true+-- > x /\ top = x+-- > x \/ top = top+top :: Meet a => a+top = floorWith bounded ()++infixr 5 \/++-- | Lattice join. ---true :: Lattice a => a-true = maximal+-- > (\/) = curry $ ceilingWith semilattice+(\/) :: Join a => a -> a -> a+(\/) = curry $ ceilingWith semilattice  -- | The unique bottom element of a bounded lattice ----- > x /\ false = false--- > x \/ false = x----false :: Lattice a => a-false = minimal+-- > x /\ bottom = bottom+-- > x \/ bottom = x+bottom :: Join a => a+bottom = ceilingWith bounded ()  ------------------------------------------------------------------------------- -- Heyting algebras ------------------------------------------------------------------------------- +-- | A convenience alias for a Heyting algebra.+type Heyting a = (Lattice a, Algebra 'R a)++-- | A convenience alias for a < https://ncatlab.org/nlab/show/co-Heyting+algebra co-Heyting algebra >.+type Coheyting a = (Lattice a, Algebra 'L a)+ -- | A < https://ncatlab.org/nlab/show/co-Heyting+algebra bi-Heyting algebra >. -- -- /Laws/:@@ -123,30 +204,21 @@ -- > neg x <= non x -- -- with equality occurring iff /a/ is a 'Boolean' algebra.----type Biheyting a = (HeytingL a, HeytingR a)---- | A convenience alias for a < https://ncatlab.org/nlab/show/co-Heyting+algebra co-Heyting algebra >.----type HeytingL = Heyting 'L---- | A convenience alias for a Heyting algebra.----type HeytingR = Heyting 'R+type Biheyting a = (Coheyting a, Heyting a) --- | Heyting algebras+-- | Heyting and co-Heyting algebras ----- A Heyting algebra is a bounded, distributive complete equipped with an+-- A Heyting algebra is a bounded, distributive lattice equipped with an -- implication operation. ----- * The complete of closed subsets of a trueological space is the primordial--- example of a /HeytingL/ (co-Heyting) algebra.+-- * The complete of closed subsets of a topological space is the primordial+-- example of a /Coheyting/ (co-Algebra) algebra. ----- * The dual complete of open subsets of a trueological space is likewise--- the primordial example of a /HeytingR/ algebra.+-- * The dual complete of open subsets of a topological space is likewise+-- the primordial example of a /Heyting/ algebra. ----- /Heyting 'L/:--- +-- /Coheyting/:+-- -- Co-implication to /a/ is the lower adjoint of disjunction with /a/: -- -- > x \\ a <= y <=> x <= y \/ a@@ -155,12 +227,12 @@ -- -- > EQ /\ non EQ = EQ /\ GT \\ EQ = EQ /\ GT = EQ /= LT ----- See < https://ncatlab.org/nlab/show/co-Heyting+algebra >+-- See < https://ncatlab.org/nlab/show/co-Algebra+algebra > ----- /Heyting 'R/:+-- /Heyting/: -- -- Implication from /a/ is the upper adjoint of conjunction with /a/:--- +-- -- > x <= a // y <=> a /\ x <= y -- -- Similarly, Heyting algebras needn't obey the law of the excluded middle:@@ -168,20 +240,94 @@ -- > EQ \/ neg EQ = EQ \/ EQ // LT = EQ \/ LT = EQ /= GT -- -- See < https://ncatlab.org/nlab/show/Heyting+algebra >----class Lattice a => Heyting k a where-    +class Semilattice k a => Algebra k a where     -- | The defining connection of a (co-)Heyting algebra.     ---    -- > heyting @'L x = ConnL (\\ x) (\/ x) -    -- > heyting @'R x = ConnR (x /\) (x //)-    ---    heyting :: a -> Conn k a a+    -- > algebra @'L x = ConnL (\\ x) (\/ x)+    -- > algebra @'R x = ConnR (x /\) (x //)+    algebra :: a -> Conn k a a  ---------------------------------------------------------------------------------- HeytingL+-- Heyting ------------------------------------------------------------------------------- +infixr 8 // -- same as ^++-- | Logical implication:+--+-- \( a \Rightarrow b = \vee \{x \mid x \wedge a \leq b \} \)+--+-- /Laws/:+--+-- > x /\ y <= z <=> x <= y // z+-- > x // y <= x // (y \/ z)+-- > x <= y => z // x <= z // y+-- > y <= x // (x /\ y)+-- > x <= y <=> x // y = top+-- > (x \/ z) // y <= x // y+-- > (x /\ y) // z = x // y // z+-- > x // (y /\ z) = x // y /\ x // z+-- > x /\ x // y = x /\ y+--+-- >>> False // False+-- True+-- >>> False // True+-- True+-- >>> True // False+-- False+-- >>> True // True+-- True+(//) :: Algebra 'R a => a -> a -> a+(//) = floorWith . algebra++-- | Intuitionistic equivalence.+--+-- When @a@ is /Bool/ this is 'if-and-only-if'.+iff :: Algebra 'R a => a -> a -> a+iff x y = (x // y) /\ (y // x)++-- | Logical negation.+--+-- @ 'neg' x = x '//' 'bottom' @+--+-- /Laws/:+--+-- > neg bottom = top+-- > neg top = bottom+-- > x <= neg (neg x)+-- > neg (x \/ y) <= neg x+-- > neg (x // y) = neg (neg x) /\ neg y+-- > neg (x \/ y) = neg x /\ neg y+-- > x /\ neg x = bottom+-- > neg (neg (neg x)) = neg x+-- > neg (neg (x \/ neg x)) = top+--+-- Some logics may in addition obey < https://ncatlab.org/nlab/show/De+Morgan+Algebra+algebra De Morgan conditions >.+neg :: Heyting a => a -> a+neg x = x // bottom++-- | The Algebra (< https://ncatlab.org/nlab/show/excluded+middle not necessarily excluded>) middle operator.+middle :: Heyting a => a -> a+middle x = x \/ neg x++-- | Default constructor for a Algebra algebra.+heyting :: Meet a => (a -> a -> a) -> a -> ConnR a a+heyting f a = ConnR (a /\) (a `f`)++-- | An adjunction between a Algebra algebra and its Boolean sub-algebra.+--+-- Double negation is a meet-preserving monad.+booleanR :: Heyting a => ConnR a a+booleanR =+    let -- Check that /x/ is a regular element+        -- See https://ncatlab.org/nlab/show/regular+element+        inj x = if x ~~ (neg . neg) x then x else bottom+     in ConnR (neg . neg) inj++-------------------------------------------------------------------------------+-- Coheyting+-------------------------------------------------------------------------------+ infixl 8 \\  -- | Logical co-implication:@@ -189,12 +335,12 @@ -- \( a \Rightarrow b = \wedge \{x \mid a \leq b \vee x \} \) -- -- /Laws/:--- +-- -- > x \\ y <= z <=> x <= y \/ z -- > x \\ y >= (x /\ z) \\ y -- > x >= y => x \\ z >= y \\ z -- > x >= x \\ y--- > x >= y <=> y \\ x = false+-- > x >= y <=> y \\ x = bottom -- > x \\ (y /\ z) >= x \\ y -- > z \\ (x \/ y) = z \\ x \\ y -- > (y \/ z) \\ x = y \\ x \/ z \\ x@@ -216,147 +362,52 @@ -- fromList [EQ,GT] -- >>> [GT,EQ] \\ [LT] -- fromList [EQ,GT]--- -(\\) :: Heyting 'L a => a -> a -> a-(\\) = flip $ lowerL . heyting+(\\) :: Algebra 'L a => a -> a -> a+(\\) = flip $ ceilingWith . algebra +-- | Intuitionistic co-equivalence.+equiv :: Algebra 'L a => a -> a -> a+equiv x y = (x \\ y) \/ (y \\ x)+ -- | Logical < https://ncatlab.org/nlab/show/co-Heyting+negation co-negation >. ----- @ 'non' x = 'true' '\\' x @+-- @ 'non' x = 'top' '\\' x @ -- -- /Laws/:--- --- > non false = true--- > non true = false+--+-- > non bottom = top+-- > non top = bottom -- > x >= non (non x) -- > non (x /\ y) >= non x -- > non (y \\ x) = non (non x) \/ non y -- > non (x /\ y) = non x \/ non y--- > x \/ non x = true+-- > x \/ non x = top -- > non (non (non x)) = non x--- > non (non (x /\ non x)) = false----non :: Heyting 'L a => a -> a-non x = true \\ x---- | Intuitionistic co-equivalence.----equiv :: Heyting 'L a => a -> a -> a-equiv x y = (x \\ y) \/ (y \\ x)+-- > non (non (x /\ non x)) = bottom+non :: Coheyting a => a -> a+non x = top \\ x --- | The co-Heyting < https://ncatlab.org/nlab/show/co-Heyting+boundary boundary > operator.    +-- | The co-Heyting < https://ncatlab.org/nlab/show/co-Heyting+boundary boundary > operator. -- -- > x = boundary x \/ (non . non) x -- > boundary (x /\ y) = (boundary x /\ y) \/ (x /\ boundary y)  -- (Leibniz rule) -- > boundary (x \/ y) \/ boundary (x /\ y) = boundary x \/ boundary y----boundary :: Heyting 'L a => a -> a+boundary :: Coheyting a => a -> a boundary x = x /\ non x +-- | Default constructor for a co-Heyting algebra.+coheyting :: Join a => (a -> a -> a) -> a -> ConnL a a+coheyting f a = ConnL (`f` a) (\/ a)+ -- | An adjunction between a co-Heyting algebra and its Boolean sub-algebra. -- -- Double negation is a join-preserving comonad.----booleanL :: Heyting 'L a => Conn 'L a a+booleanL :: Coheyting a => ConnL a a booleanL =-  let -    -- Check that /x/ is a regular element-    -- See https://ncatlab.org/nlab/show/regular+element-    inj x = if x == (non . non) x then x else true--  in-    ConnL inj (non . non)---- | Default constructor for a co-Heyting algebra.----heytingL :: Lattice a => (a -> a -> a) -> a -> Conn 'L a a-heytingL f a = ConnL (`f` a) (\/ a)------------------------------------------------------------------------------------ HeytingR----------------------------------------------------------------------------------infixr 8 // -- same as ^---- | Logical implication:------ \( a \Rightarrow b = \vee \{x \mid x \wedge a \leq b \} \)------ /Laws/:------ > x /\ y <= z <=> x <= y // z--- > x // y <= x // (y \/ z)--- > x <= y => z // x <= z // y--- > y <= x // (x /\ y)--- > x <= y <=> x // y = true--- > (x \/ z) // y <= x // y--- > (x /\ y) // z = x // y // z--- > x // (y /\ z) = x // y /\ x // z--- > x /\ x // y = x /\ y------ >>> False // False--- True--- >>> False // True--- True--- >>> True // False--- False--- >>> True // True--- True----(//) :: Heyting 'R a => a -> a -> a-(//) x = upperR $ heyting x---- | Logical negation.------ @ 'neg' x = x '//' 'false' @------ /Laws/:------ > neg false = true--- > neg true = false--- > x <= neg (neg x)--- > neg (x \/ y) <= neg x--- > neg (x // y) = neg (neg x) /\ neg y--- > neg (x \/ y) = neg x /\ neg y--- > x /\ neg x = false--- > neg (neg (neg x)) = neg x--- > neg (neg (x \/ neg x)) = true------ Some logics may in addition obey < https://ncatlab.org/nlab/show/De+Morgan+Heyting+algebra De Morgan conditions >.----neg :: Heyting 'R a => a -> a-neg x = x // false---- | Intuitionistic equivalence.------ When /a=Bool/ this is 'if-and-only-if'.----iff :: Heyting 'R a => a -> a -> a-iff x y = (x // y) /\ (y // x)---- | The Heyting (< https://ncatlab.org/nlab/show/excluded+middle not necessarily excluded>) middle operator.----middle :: Heyting 'R a => a -> a-middle x = x \/ neg x---- | An adjunction between a Heyting algebra and its Boolean sub-algebra.------ Double negation is a meet-preserving monad.----booleanR :: Heyting 'R a => Conn 'R a a-booleanR = -  let-    -- Check that /x/ is a regular element-    -- See https://ncatlab.org/nlab/show/regular+element-    inj x = if x == (neg . neg) x then x else false--  in -    ConnR (neg . neg) inj---- | Default constructor for a Heyting algebra.----heytingR :: Lattice a => (a -> a -> a) -> a -> Conn 'R a a-heytingR f a = ConnR (a /\) (a `f`)+    let -- Check that /x/ is a regular element+        -- See https://ncatlab.org/nlab/show/regular+element+        inj x = if x ~~ (non . non) x then x else top+     in ConnL inj (non . non)  ------------------------------------------------------------------------------- -- Symmetric@@ -364,8 +415,8 @@  -- | Symmetric Heyting algebras ----- A symmetric Heyting algebra is a <https://ncatlab.org/nlab/show/De+Morgan+Heyting+algebra De Morgan >--- bi-Heyting algebra with an idempotent, antitone negation operator.+-- A symmetric Heyting algebra is a <https://ncatlab.org/nlab/show/De+Morgan+Algebra+algebra De Morgan >+-- bi-Algebra algebra with an idempotent, antitone negation operator. -- -- /Laws/: --@@ -379,9 +430,7 @@ -- > converseR x <= converseL x -- -- with equality occurring iff /a/ is a 'Boolean' algebra.--- class Biheyting a => Symmetric a where-     -- | Symmetric negation.     --     -- > not . not = id@@ -394,7 +443,6 @@     -- > non = not . converseR = converseL . not     -- > x \\ y = not (not y // not x)     -- > x // y = not (not y \\ not x)-    --     not :: a -> a      infixl 4 `xor`@@ -402,226 +450,254 @@     -- | Exclusive or.     --     -- > xor x y = (x \/ y) /\ (not x \/ not y)-    --     xor :: a -> a -> a     xor x y = (x \/ y) /\ not (x /\ y) -    -- | Left converse operator.-    --    -    converseL :: a -> a-    converseL x = true \\ not x--    -- | Right converse operator.-    --    -    converseR :: a -> a-    converseR x = not x // false+-- | Left converse operator.+converseL :: Symmetric a => a -> a+converseL x = top \\ not x --- | Default constructor for a co-Heyting algebra.----symmetricL :: Symmetric a => a -> ConnL a a-symmetricL = heytingL $ \x y -> not (not y // not x)+-- | Right converse operator.+converseR :: Symmetric a => a -> a+converseR x = not x // bottom  -- | Default constructor for a Heyting algebra.--- symmetricR :: Symmetric a => a -> ConnR a a-symmetricR = heytingR $ \x y -> not (not y \\ not x)+symmetricR = heyting $ \x y -> not (not y \\ not x) +-- | Default constructor for a co-Heyting algebra.+symmetricL :: Symmetric a => a -> ConnL a a+symmetricL = coheyting $ \x y -> not (not y // not x)+ ------------------------------------------------------------------------------- -- Boolean -------------------------------------------------------------------------------  -- | Boolean algebras. ----- < https://ncatlab.org/nlab/show/Boolean+algebra Boolean algebras > are --- symmetric Heyting algebras that satisfy both the law of excluded middle+-- < https://ncatlab.org/nlab/show/Boolean+algebra Boolean algebras > are+-- symmetric Algebra algebras that satisfy both the law of excluded middle -- and the law of law of non-contradiction: ----- > x \/ neg x = true--- > x /\ non x = false+-- > x \/ neg x = top+-- > x /\ non x = bottom -- -- If /a/ is Boolean we also have: -- -- > non = not = neg--- class Symmetric a => Boolean a where-     -- | A witness to the lawfulness of a boolean algebra.-    ---    boolean :: Trip a a+    boolean :: Conn k a a     boolean = Conn (converseR . converseL) id (converseL . converseR)  ------------------------------------------------------------------------------- -- Instances ------------------------------------------------------------------------------- --impliesL :: (Total a, P.Bounded a) => a -> a -> a-impliesL x y = if y < x then x else P.minBound--impliesR :: (Total a, P.Bounded a) => a -> a -> a-impliesR x y = if x > y then y else P.maxBound--instance Heyting 'L () where heyting = heytingL impliesL-instance Heyting 'L Bool where heyting = heytingL impliesL-instance Heyting 'L Ordering where heyting = heytingL impliesL-instance Heyting 'L Word8 where heyting = heytingL impliesL-instance Heyting 'L Word16 where heyting = heytingL impliesL-instance Heyting 'L Word32 where heyting = heytingL impliesL-instance Heyting 'L Word64 where heyting = heytingL impliesL-instance Heyting 'L Word where heyting = heytingL impliesL-instance KnownNat n => Heyting 'L (F.Finite n) where heyting = heytingL impliesL--instance Heyting 'R () where heyting = heytingR impliesR-instance Heyting 'R Bool where heyting = heytingR impliesR---instance Heyting 'R Ordering where heyting = heytingR impliesR-instance Heyting 'R Word8 where heyting = heytingR impliesR-instance Heyting 'R Word16 where heyting = heytingR impliesR-instance Heyting 'R Word32 where heyting = heytingR impliesR-instance Heyting 'R Word64 where heyting = heytingR impliesR-instance Heyting 'R Word where heyting = heytingR impliesR-instance KnownNat n => Heyting 'R (F.Finite n) where heyting = heytingR impliesR--instance Heyting 'L Int8 where heyting = heytingL impliesL-instance Heyting 'L Int16 where heyting = heytingL impliesL-instance Heyting 'L Int32 where heyting = heytingL impliesL-instance Heyting 'L Int64 where heyting = heytingL impliesL-instance Heyting 'L Int where heyting = heytingL impliesL-instance Heyting 'R Int8 where heyting = heytingR impliesR-instance Heyting 'R Int16 where heyting = heytingR impliesR-instance Heyting 'R Int32 where heyting = heytingR impliesR-instance Heyting 'R Int64 where heyting = heytingR impliesR-instance Heyting 'R Int where heyting = heytingR impliesR+instance Semilattice k ()+instance Algebra 'L () where algebra = coheyting impliesL+instance Algebra 'R () where algebra = heyting impliesR+instance Symmetric () where not = id+instance Boolean () -instance Symmetric () where not _ = ()+instance Semilattice k Bool+instance Algebra 'L Bool where algebra = coheyting impliesL+instance Algebra 'R Bool where algebra = heyting impliesR instance Symmetric Bool where not = P.not-instance Symmetric Ordering where-  not LT = GT-  not EQ = EQ-  not GT = LT- -instance Heyting 'R Ordering where heyting = symmetricR--instance Boolean () instance Boolean Bool ----------------------------------------------------------------------------------- Instances: sum types--------------------------------------------------------------------------------+instance Semilattice k Ordering+instance Algebra 'L Ordering where algebra = coheyting impliesL+instance Algebra 'R Ordering where algebra = heyting impliesR+instance Symmetric Ordering where+    not LT = GT+    not EQ = EQ+    not GT = LT+instance Boolean Ordering +instance Semilattice k Word8+instance Algebra 'L Word8 where algebra = coheyting impliesL+instance Algebra 'R Word8 where algebra = heyting impliesR +instance Semilattice k Word16+instance Algebra 'L Word16 where algebra = coheyting impliesL+instance Algebra 'R Word16 where algebra = heyting impliesR --- |--- Subdirectly irreducible Heyting algebra.-instance Heyting 'R a => Heyting 'R (Lowered a) where-  heyting = heytingR f where+instance Semilattice k Word32+instance Algebra 'L Word32 where algebra = coheyting impliesL+instance Algebra 'R Word32 where algebra = heyting impliesR -    (Left a)  `f` (Left b) | a <= b    = true-                           | otherwise = Left (a // b)-    (Right _) `f` a                    = a-    _         `f` (Right _)            = true+instance Semilattice k Word64+instance Algebra 'L Word64 where algebra = coheyting impliesL+instance Algebra 'R Word64 where algebra = heyting impliesR -instance Heyting 'R a => Heyting 'R (Lifted a) where-  heyting = heytingR f where-    f (Right a) (Right b) = Right (a // b)-    f (Left _)   _        = Right true-    f _         (Left _)  = false+instance Semilattice k Word+instance Algebra 'L Word where algebra = coheyting impliesL+instance Algebra 'R Word where algebra = heyting impliesR -instance Heyting 'R a => Heyting 'R (Maybe a) where-  heyting = heytingR f where-    f (Just a) (Just b)   = Just (a // b)-    f Nothing  _          = Just true-    f _        Nothing    = Nothing+instance Semilattice k Int8+instance Algebra 'L Int8 where algebra = coheyting impliesL+instance Algebra 'R Int8 where algebra = heyting impliesR ---instance Complete k a => Complete k (Extended a)-instance Heyting 'R a => Heyting 'R (Extended a) where-  heyting = heytingR f where+instance Semilattice k Int16+instance Algebra 'L Int16 where algebra = coheyting impliesL+instance Algebra 'R Int16 where algebra = heyting impliesR -    Extended a `f` Extended b | a <= b    = Top-                              | otherwise = Extended (a // b)-    Top        `f` a          = a-    _          `f` Top        = Top-    Bottom     `f` _          = Top-    _          `f` Bottom     = Bottom+instance Semilattice k Int32+instance Algebra 'L Int32 where algebra = coheyting impliesL+instance Algebra 'R Int32 where algebra = heyting impliesR ---instance Symmetric a => Symmetric (Extended a) where+instance Semilattice k Int64+instance Algebra 'L Int64 where algebra = coheyting impliesL+instance Algebra 'R Int64 where algebra = heyting impliesR +instance Semilattice k Int+instance Algebra 'L Int where algebra = coheyting impliesL+instance Algebra 'R Int where algebra = heyting impliesR+ ------------------------------------------------------------------------------- -- Instances: product types ------------------------------------------------------------------------------- -instance (Heyting k a, Heyting k b) => Heyting k (a, b) where-  heyting (a,b) = heyting a `strong` heyting b+instance (Lattice a, Lattice b) => Semilattice k (a, b) where+    bounded = Conn (const (bottom, bottom)) (const ()) (const (top, top))+    semilattice = Conn (uncurry joinTuple) fork (uncurry meetTuple) +instance (Heyting a, Heyting b) => Algebra 'R (a, b) where+    algebra (a, b) = algebra a `strong` algebra b++instance (Coheyting a, Coheyting b) => Algebra 'L (a, b) where+    algebra (a, b) = algebra a `strong` algebra b+ instance (Symmetric a, Symmetric b) => Symmetric (a, b) where-  not = bimap not not+    not = bimap not not -instance (Boolean a, Boolean b) => Boolean (a, b) where+instance (Boolean a, Boolean b) => Boolean (a, b)  ---------------------------------------------------------------------------------- Instances: function types+-- Instances: sum types ------------------------------------------------------------------------------- +instance Join a => Semilattice 'L (Maybe a) where+    bounded = ConnL (const Nothing) (const ())+    semilattice = ConnL (uncurry joinMaybe) fork -instance (U.Finite a, Biheyting b) => Heyting 'L (a -> b) where-  heyting = heytingL $ liftA2 (\\)+instance Meet a => Semilattice 'R (Maybe a) where+    bounded = ConnR (const ()) (const $ Just top)+    semilattice = ConnR fork (uncurry meetMaybe) -instance (U.Finite a, Biheyting b) => Heyting 'R (a -> b) where-  heyting = heytingR $ liftA2 (//)+instance Heyting a => Algebra 'R (Maybe a) where+    algebra = heyting f+      where+        f (Just a) (Just b) = Just (a // b)+        f Nothing _ = Just top+        f _ Nothing = Nothing -instance (U.Finite a, Symmetric b) => Symmetric (a -> b) where not = fmap not+instance Join a => Semilattice 'L (Extended a) where+    bounded = Conn (const Bottom) (const ()) (const Top)+    semilattice = ConnL (uncurry joinExtended) fork -instance (U.Finite a, Boolean b) => Boolean (a -> b)+instance Meet a => Semilattice 'R (Extended a) where+    bounded = Conn (const Bottom) (const ()) (const Top)+    semilattice = ConnR fork (uncurry meetExtended) -deriving via (a -> a) instance (U.Finite a, Biheyting a) => Heyting 'L (Endo a)-deriving via (a -> a) instance (U.Finite a, Biheyting a) => Heyting 'R (Endo a)-instance (U.Finite a, Symmetric a) => Symmetric (Endo a)-instance (U.Finite a, Boolean a) => Boolean (Endo a)+instance Heyting a => Algebra 'R (Extended a) where+    algebra = heyting f+      where+        Extended a `f` Extended b+            | a <~ b = Top+            | otherwise = Extended (a // b)+        Top `f` a = a+        _ `f` Top = Top+        Bottom `f` _ = Top+        _ `f` Bottom = Bottom -deriving via (a -> b) instance (U.Finite a, Biheyting b) => Heyting 'L (Op b a)-deriving via (a -> b) instance (U.Finite a, Biheyting b) => Heyting 'R (Op b a)-instance (U.Finite a, Symmetric b) => Symmetric (Op b a)-instance (U.Finite a, Boolean b) => Boolean (Op b a)+-- | All minimal elements of the upper lattice cover all maximal elements of the lower lattice.+instance (Join a, Join b) => Semilattice 'L (Either a b) where+    bounded = ConnL (const $ Left bottom) (const ())+    semilattice = ConnL (uncurry joinEither) fork -deriving via (Op Bool a) instance (U.Finite a) => Heyting 'L (Predicate a)-deriving via (Op Bool a) instance (U.Finite a) => Heyting 'R (Predicate a)-instance (U.Finite a) => Symmetric (Predicate a)-instance (U.Finite a) => Boolean (Predicate a)+instance (Meet a, Meet b) => Semilattice 'R (Either a b) where+    bounded = ConnR (const ()) (const $ Right top)+    semilattice = ConnR fork (uncurry meetEither) +-- |+-- Subdirectly irreducible Algebra algebra.+instance Heyting a => Algebra 'R (Lowered a) where+    algebra = heyting f+      where+        (Left a) `f` (Left b)+            | a <~ b = top+            | otherwise = Left (a // b)+        (Right _) `f` a = a+        _ `f` (Right _) = top++instance Heyting a => Algebra 'R (Lifted a) where+    algebra = heyting f+      where+        f (Right a) (Right b) = Right (a // b)+        f (Left _) _ = Right top+        f _ (Left _) = bottom+ ------------------------------------------------------------------------------- -- Instances: collections ------------------------------------------------------------------------------- +instance Total a => Semilattice 'L (Set.Set a) -instance (Total a, U.Finite a) => Heyting 'L (Set.Set a) where-  heyting = heytingL (Set.\\)+instance Total a => Algebra 'L (Set.Set a) where+    algebra = coheyting (Set.\\) -instance (Total a, U.Finite a) => Heyting 'R (Set.Set a) where-  heyting = symmetricR+--instance (Total a, U.Finite a) => Algebra 'R (Set.Set a) where+--  algebra = symmetricR -instance (Total a, U.Finite a) => Symmetric (Set.Set a) where-  not = non --(U.universe Set.\\)+--instance (Total a, U.Finite a) => Symmetric (Set.Set a) where+--  not = non --(U.universe Set.\\) -instance (Total a, U.Finite a) => Boolean (Set.Set a) where+--instance (Total a, U.Finite a) => Boolean (Set.Set a) where -instance Heyting 'L IntSet.IntSet where-  heyting = heytingL (IntSet.\\)+instance Semilattice 'L IntSet.IntSet -instance Heyting 'R IntSet.IntSet where-  --heyting = heytingR $ \x y -> non x \/ y-  heyting = symmetricR+instance Algebra 'L IntSet.IntSet where+    algebra = coheyting (IntSet.\\) +{-+instance Algebra 'R IntSet.IntSet where+  --heyting = heyting $ \x y -> non x \/ y+  algebra = symmetricR+ instance Symmetric IntSet.IntSet where   not = non --(U.universe IntSet.\\)  instance Boolean IntSet.IntSet where +-}++instance (Total k, Join a) => Semilattice 'L (Map.Map k a) where+    bounded = ConnL (const Map.empty) (const ())++    semilattice = ConnL f fork+      where+        f = uncurry $ Map.unionWith (curry $ ceilingWith semilattice)++instance (Total k, Join a) => Algebra 'L (Map.Map k a) where+    algebra = coheyting (Map.\\)++instance (Join a) => Semilattice 'L (IntMap.IntMap a) where+    bounded = ConnL (const IntMap.empty) (const ())++    semilattice = ConnL f fork+      where+        f = uncurry $ IntMap.unionWith (curry $ ceilingWith semilattice)++instance (Join a) => Algebra 'L (IntMap.IntMap a) where+    algebra = coheyting (IntMap.\\)+ {- TODO pick an instance either key-aware or no-instance (Total a, U.Finite a, Lattice b) => Heyting 'L (Map.Map a b) where-  heyting = heytingL (Map.\\) -instance (Total a, U.Finite a, Heyting 'R b) => Heyting 'R (Map.Map a b) where+instance (Total a, U.Finite a, Heyting b) => Algebra 'R (Map.Map a b) where -  heyting = heytingR $ \a b ->+  algebra = heyting $ \a b ->     let       x = Map.merge             Map.dropMissing                    -- drop if an element is missing in @b@@@ -634,30 +710,29 @@         -- a @true@ key     in       Map.union x y-{-+ -- TODO: compare performance impliesMap a b =   Map.intersection (`implies`) a b     `Map.union` Map.map (const true) (Map.difference b a)     `Map.union` Map.fromList [(k, true) | k <- universeF, not (Map.member k a), not (Map.member k b)]--}--} +-}  {-  -- A symmetric Heyting algebra--- +-- -- λ> implies (False ... True) (False ... True) -- Interval True True -- λ> implies (False ... True) (singleton False) -- Interval False False -- λ> implies (singleton True) (False ... True) -- Interval False True--- +-- -- λ> implies ([EQ,GT] ... [EQ,GT]) ([LT] ... [LT,EQ])  :: Interval (Set.Set Ordering) -- Interval (fromList [LT]) (fromList [LT,EQ])--- +-- -- TODO: may need /a/ to be boolean here. implies :: Symmetric a => Interval a -> Interval a -> Interval a implies i1 i2 = maybe iempty (uncurry (...)) $ liftA2 f (endpts i1) (endpts i2) where@@ -669,11 +744,11 @@ coimplies i1 i2 = not (not i1 `implies` not i2)  -- The symmetry--- neg x = true \\ not x--- non x = not x // false+-- neg x = top \\ not x+-- non x = not x // bottom -- λ> not ([LT] ... [LT,GT]) :: Interval (Set.Set Ordering) -- Interval (fromList [EQ]) (fromList [EQ,GT])--- +-- not :: Symmetric a => Interval a -> Interval a not = maybe iempty (\(x1, x2) -> neg x2 ... neg x1) . endpts @@ -681,16 +756,70 @@ -- Interval False False -- λ> (False ... True) `implies` (singleton False) -- Interval False False--- -neg' x = (false ... true) `coimplies` (not x)+--+neg' x = (bottom ... top) `coimplies` (not x)  -- λ> non' (False ... True) -- Interval False False -- λ> (singleton True) `coimplies` (False ... True) -- Interval False False--- -non' x = not x `implies` (singleton false)+--+non' x = not x `implies` (singleton bottom)  -} +-- Internal +-------------------------+fork :: a -> (a, a)+fork x = (x, x)++impliesL :: (Total a, P.Bounded a) => a -> a -> a+impliesL x y = if y < x then x else P.minBound++impliesR :: (Total a, P.Bounded a) => a -> a -> a+impliesR x y = if x > y then y else P.maxBound++joinTuple :: (Semilattice 'L a, Semilattice 'L b) => (a, b) -> (a, b) -> (a, b)+joinTuple (x1, y1) (x2, y2) = (x1 \/ x2, y1 \/ y2)++meetTuple :: (Semilattice 'R a, Semilattice 'R b) => (a, b) -> (a, b) -> (a, b)+meetTuple (x1, y1) (x2, y2) = (x1 /\ x2, y1 /\ y2)++joinMaybe :: Join a => Maybe a -> Maybe a -> Maybe a+joinMaybe (Just x) (Just y) = Just (x \/ y)+joinMaybe u@(Just _) _ = u+joinMaybe _ u@(Just _) = u+joinMaybe Nothing Nothing = Nothing++meetMaybe :: Meet a => Maybe a -> Maybe a -> Maybe a+meetMaybe Nothing Nothing = Nothing+meetMaybe Nothing _ = Nothing+meetMaybe _ Nothing = Nothing+meetMaybe (Just x) (Just y) = Just (x /\ y)++joinExtended :: Join a => Extended a -> Extended a -> Extended a+joinExtended Top _ = Top+joinExtended _ Top = Top+joinExtended (Extended x) (Extended y) = Extended (x \/ y)+joinExtended Bottom y = y+joinExtended x Bottom = x++meetExtended :: Meet a => Extended a -> Extended a -> Extended a+meetExtended Top y = y+meetExtended x Top = x+meetExtended (Extended x) (Extended y) = Extended (x /\ y)+meetExtended Bottom _ = Bottom+meetExtended _ Bottom = Bottom++joinEither :: (Join a, Join b) => Either a b -> Either a b -> Either a b+joinEither (Right x) (Right y) = Right (x \/ y)+joinEither u@(Right _) _ = u+joinEither _ u@(Right _) = u+joinEither (Left x) (Left y) = Left (x \/ y)++meetEither :: (Meet a, Meet b) => Either a b -> Either a b -> Either a b+meetEither (Left x) (Left y) = Left (x /\ y)+meetEither l@(Left _) _ = l+meetEither _ l@(Left _) = l+meetEither (Right x) (Right y) = Right (x /\ y)

@@ -1,178 +1,212 @@-{-# LANGUAGE DataKinds                  #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+ module Data.Lattice.Property where -import Data.Connection.Conn-import Data.Connection.Property-import Data.Order+import Data.Lattice import Data.Order.Property import Data.Order.Syntax-import Data.Lattice-import Prelude hiding (Eq(..), Ord(..), Bounded, not)+import Prelude hiding (Bounded, Eq (..), Ord (..), not) ---foo x y z = x // y <= x // y /\ z---foo x z y = x /\ z // y <= x // y--- --- x '\\' x           = 'true'--- x '/\' (x '\\' y)  = x '/\' y--- y '/\' (x '\\' y)  = y--- x '\\' (y '\\' z) = (x '/\' y) '\\' z--- x '\\' (y '/\' z)  = (x '\\' y) '/\' (x '\\' z)--- 'neg' (x '/\' y)    = 'neg' (x '\/' y)--- 'neg' (x '\/' y)    = 'neg' x '/\' 'neg' y--- (x '\\' y) '\/' x '<=' y--- y '<=' (x '\\' x '/\' y)--- x '<=' y => (z '\\' x) '<=' (z '\\' y)--- x '<=' y => (x '\\' z) '<=' (y '\\' z)--- x '<=' y <=> x '\\' y '==' 'true'--- x '/\' y '<=' z <=> x '<=' (y '\\' z) <=> y '<=' (x '\\' z)--- ---+coheyting0 :: Coheyting a => a -> a -> a -> Bool+coheyting0 x y z = x \\ y <= z <=> x <= y \/ z +coheyting1 :: Coheyting a => a -> a -> a -> Bool+coheyting1 x y z = x \\ y >= (x /\ z) \\ y --- adjointL $ ConnL (\x -> y \\ not x) (\z -> not z // not y)-symmetric1 x = neg x <= non x-symmetric2 x = (neg . neg) x == (converseR . converseL) x-symmetric3 x = (non . non) x == (converseL . converseR) x-symmetric4 x = non x == (converseL . not) x && neg x == (not . converseL) x-symmetric5 x = non x == (not . converseR) x && neg x == (converseR . not) x-symmetric6 x = neg x \/ neg (neg x) == true-symmetric7 x y = not (x /\ y) == not x \/ not y-symmetric8 x y = (not . not) (x \/ y) == not (not x) \/ not (not y)-symmetric9 x y = not (x \/ y) == not x /\ not y-symmetric10 x y = converseL (x \/ y) == converseL x \/ converseL y-symmetric11 x y = converseR (x /\ y) == converseR x /\ converseR y-symmetric12 x y = converseL (x /\ y) == (non . non) (converseL x /\ converseL y)-symmetric13 x y = converseR (x \/ y) == (neg . neg) (converseR x \/ converseR y)- -boolean0 x = neg x == non x-boolean1 x = neg (neg x) == x-boolean2 x = x \/ neg x == true-boolean3 x = x /\ non x == false -boolean4 x y = (x <= y) // (neg y <= neg x)-boolean5 x y = x \\ y == neg (neg y // neg x)-boolean6 x y = x // y == non (non y \\ non x)+coheyting2 :: Coheyting a => a -> a -> a -> Bool+coheyting2 x y z = x \\ (y /\ z) >= x \\ y +coheyting3 :: Coheyting a => a -> a -> a -> Bool+coheyting3 x y z = x >= y ==> x \\ z >= y \\ z -heytingL0 :: Heyting 'L a => a -> a -> a -> Bool-heytingL0 x y z = x \\ y <= z <=> x <= y \/ z+coheyting4 :: Coheyting a => a -> a -> a -> Bool+coheyting4 x y z = z \\ (x \/ y) == z \\ x \\ y -heytingL1 :: Heyting 'L a => a -> a -> a -> Bool-heytingL1 x y z = x \\ y >= (x /\ z) \\ y+coheyting5 :: Coheyting a => a -> a -> a -> Bool+coheyting5 x y z = (y \/ z) \\ x == y \\ x \/ z \\ x -heytingL2 :: Heyting 'L a => a -> a -> a -> Bool-heytingL2 x y z = x \\ (y /\ z) >= x \\ y+coheyting6 :: Coheyting a => a -> a -> Bool+coheyting6 x y = x >= x \\ y -heytingL3 :: Heyting 'L a => a -> a -> a -> Bool-heytingL3 x y z = x >= y ==> x \\ z >= y \\ z+coheyting7 :: Coheyting a => a -> a -> Bool+coheyting7 x y = x \/ y \\ x == x \/ y -heytingL4 :: Heyting 'L a => a -> a -> a -> Bool-heytingL4 x y z = z \\ (x \/ y) == z \\ x \\ y+coheyting8 :: forall a. Coheyting a => a -> Bool+coheyting8 _ = non bottom == top @a && non top == bottom @a -heytingL5 :: Heyting 'L a => a -> a -> a -> Bool-heytingL5 x y z = (y \/ z) \\ x == y \\ x \/ z \\ x+-- Double co-negation is a co-monad.+coheyting9 :: Coheyting a => a -> a -> Bool+coheyting9 x y = x /\ non y >= x \\ y -heytingL6 :: Heyting 'L a => a -> a -> Bool-heytingL6 x y = x >= x \\ y+coheyting10 :: Coheyting a => a -> a -> Bool+coheyting10 x y = x >= y <=> y \\ x == bottom -heytingL7 :: Heyting 'L a => a -> a -> Bool-heytingL7 x y = x \/ y \\ x == x \/ y+coheyting11 :: Coheyting a => a -> a -> Bool+coheyting11 x y = non (x /\ y) >= non x -heytingL8 :: forall a. Heyting 'L a => a -> Bool-heytingL8 _ = non false == true @a && non true == false @a+coheyting12 :: Coheyting a => a -> a -> Bool+coheyting12 x y = non (y \\ x) == non (non x) \/ non y --- Double co-negation is a co-monad.-heytingL9 :: Heyting 'L a => a -> a -> Bool-heytingL9 x y = x /\ non y >= x \\ y+coheyting13 :: Coheyting a => a -> a -> Bool+coheyting13 x y = non (x /\ y) == non x \/ non y -heytingL10 :: Heyting 'L a => a -> a -> Bool-heytingL10 x y = x >= y <=> y \\ x == false+coheyting14 :: Coheyting a => a -> Bool+coheyting14 x = x \/ non x == top -heytingL11 :: Heyting 'L a => a -> a -> Bool-heytingL11 x y = non (x /\ y) >= non x+coheyting15 :: Coheyting a => a -> Bool+coheyting15 x = non (non (non x)) == non x -heytingL12 :: Heyting 'L a => a -> a -> Bool-heytingL12 x y = non (y \\ x) == non (non x) \/ non y+coheyting16 :: Coheyting a => a -> Bool+coheyting16 x = non (non (x /\ non x)) == bottom -heytingL13 :: Heyting 'L a => a -> a -> Bool-heytingL13 x y = non (x /\ y) == non x \/ non y+coheyting17 :: Coheyting a => a -> Bool+coheyting17 x = x >= non (non x) -heytingL14 :: Heyting 'L a => a -> Bool-heytingL14 x = x \/ non x == true+coheyting18 :: Coheyting c => c -> Bool+coheyting18 x = x == boundary x \/ (non . non) x -heytingL15 :: Heyting 'L a => a -> Bool-heytingL15 x = non (non (non x)) == non x+coheyting19 :: Coheyting a => a -> a -> Bool+coheyting19 x y = boundary (x /\ y) == (boundary x /\ y) \/ (x /\ boundary y) -- (Leibniz rule) -heytingL16 :: Heyting 'L a => a -> Bool-heytingL16 x = non (non (x /\ non x)) == false+coheyting20 :: Coheyting a => a -> a -> Bool+coheyting20 x y = boundary (x \/ y) \/ boundary (x /\ y) == boundary x \/ boundary y -heytingL17 :: Heyting 'L a => a -> Bool-heytingL17 x = x >= non (non x)+heyting0 :: Heyting a => a -> a -> a -> Bool+heyting0 x y z = x /\ y <= z <=> x <= y // z -heytingL18 :: Heyting 'L c => c -> Bool-heytingL18 x = x == boundary x \/ (non . non) x+heyting1 :: Heyting a => a -> a -> a -> Bool+heyting1 x y z = x // y <= x // (y \/ z) -heytingL19 :: Heyting 'L a => a -> a -> Bool-heytingL19 x y = boundary (x /\ y) == (boundary x /\ y) \/ (x /\ boundary y)  -- (Leibniz rule)+heyting2 :: Heyting a => a -> a -> a -> Bool+heyting2 x y z = (x \/ z) // y <= x // y -heytingL20 :: Heyting 'L a => a -> a -> Bool-heytingL20 x y = boundary (x \/ y) \/ boundary (x /\ y) == boundary x \/ boundary y+heyting3 :: Heyting a => a -> a -> a -> Bool+heyting3 x y z = x <= y ==> z // x <= z // y +heyting4 :: Heyting a => a -> a -> a -> Bool+heyting4 x y z = (x /\ y) // z == x // y // z -heytingR0 :: Heyting 'R a => a -> a -> a -> Bool-heytingR0 x y z = x /\ y <= z <=> x <= y // z+heyting5 :: Heyting a => a -> a -> a -> Bool+heyting5 x y z = x // (y /\ z) == x // y /\ x // z -heytingR1 :: Heyting 'R a => a -> a -> a -> Bool-heytingR1 x y z = x // y <= x // (y \/ z)+heyting6 :: Heyting a => a -> a -> Bool+heyting6 x y = y <= x // (x /\ y) -heytingR2 :: Heyting 'R a => a -> a -> a -> Bool-heytingR2 x y z = (x \/ z) // y <= x // y+heyting7 :: Heyting a => a -> a -> Bool+heyting7 x y = x /\ x // y == x /\ y -heytingR3 :: Heyting 'R a => a -> a -> a -> Bool-heytingR3 x y z = x <= y ==> z // x <= z // y+heyting8 :: forall a. Heyting a => a -> Bool+heyting8 _ = neg bottom == top @a && neg top == bottom @a -heytingR4 :: Heyting 'R a => a -> a -> a -> Bool-heytingR4 x y z = (x /\ y) // z == x // y // z+-- Double negation is a monad.+heyting9 :: Heyting a => a -> a -> Bool+heyting9 x y = neg x \/ y <= x // y -heytingR5 :: Heyting 'R a => a -> a -> a -> Bool-heytingR5 x y z = x // (y /\ z) == x // y /\ x // z+heyting10 :: Heyting a => a -> a -> Bool+heyting10 x y = x <= y <=> x // y == top -heytingR6 :: Heyting 'R a => a -> a -> Bool-heytingR6 x y = y <= x // (x /\ y)+heyting11 :: Heyting a => a -> a -> Bool+heyting11 x y = neg (x \/ y) <= neg x -heytingR7 :: Heyting 'R a => a -> a -> Bool-heytingR7 x y = x /\ x // y == x /\ y+heyting12 :: Heyting a => a -> a -> Bool+heyting12 x y = neg (x // y) == neg (neg x) /\ neg y -heytingR8 :: forall a. Heyting 'R a => a -> Bool-heytingR8 _ = neg false == true @a && neg true == false @a+heyting13 :: Heyting a => a -> a -> Bool+heyting13 x y = neg (x \/ y) == neg x /\ neg y --- Double negation is a monad.-heytingR9 :: Heyting 'R a => a -> a -> Bool-heytingR9 x y = neg x \/ y <= x // y+heyting14 :: Heyting a => a -> Bool+heyting14 x = x /\ neg x == bottom -heytingR10 :: Heyting 'R a => a -> a -> Bool-heytingR10 x y = x <= y <=> x // y == true+heyting15 :: Heyting a => a -> Bool+heyting15 x = neg (neg (neg x)) == neg x -heytingR11 :: Heyting 'R a => a -> a -> Bool-heytingR11 x y = neg (x \/ y) <= neg x+heyting16 :: Heyting a => a -> Bool+heyting16 x = neg (neg (x \/ neg x)) == top -heytingR12 :: Heyting 'R a => a -> a -> Bool-heytingR12 x y = neg (x // y) == neg (neg x) /\ neg y+heyting17 :: Heyting a => a -> Bool+heyting17 x = x <= neg (neg x) -heytingR13 :: Heyting 'R a => a -> a -> Bool-heytingR13 x y = neg (x \/ y) == neg x /\ neg y+--+-- x '\\' x           = 'top'+-- x '/\' (x '\\' y)  = x '/\' y+-- y '/\' (x '\\' y)  = y+-- x '\\' (y '\\' z) = (x '/\' y) '\\' z+-- x '\\' (y '/\' z)  = (x '\\' y) '/\' (x '\\' z)+-- 'neg' (x '/\' y)    = 'neg' (x '\/' y)+-- 'neg' (x '\/' y)    = 'neg' x '/\' 'neg' y+-- (x '\\' y) '\/' x '<=' y+-- y '<=' (x '\\' x '/\' y)+-- x '<=' y => (z '\\' x) '<=' (z '\\' y)+-- x '<=' y => (x '\\' z) '<=' (y '\\' z)+-- x '<=' y <=> x '\\' y '==' 'top'+-- x '/\' y '<=' z <=> x '<=' (y '\\' z) <=> y '<=' (x '\\' z)+--+-- -heytingR14 :: Heyting 'R a => a -> Bool-heytingR14 x = x /\ neg x == false+-- adjointL $ ConnL (\x -> y \\ not x) (\z -> not z // not y)+symmetric1 :: Biheyting a => a -> Bool+symmetric1 x = neg x <= non x -heytingR15 :: Heyting 'R a => a -> Bool-heytingR15 x = neg (neg (neg x)) == neg x+symmetric2 :: Symmetric a => a -> Bool+symmetric2 x = (neg . neg) x == (converseR . converseL) x -heytingR16 :: Heyting 'R a => a -> Bool-heytingR16 x = neg (neg (x \/ neg x)) == true+symmetric3 :: Symmetric a => a -> Bool+symmetric3 x = (non . non) x == (converseL . converseR) x -heytingR17 :: Heyting 'R a => a -> Bool-heytingR17 x = x <= neg (neg x)+symmetric4 :: Symmetric a => a -> Bool+symmetric4 x = non x == (converseL . not) x && neg x == (not . converseL) x +symmetric5 :: Symmetric a => a -> Bool+symmetric5 x = non x == (not . converseR) x && neg x == (converseR . not) x++symmetric6 :: Heyting a => a -> Bool+symmetric6 x = neg x \/ neg (neg x) == top++symmetric7 :: Symmetric a => a -> a -> Bool+symmetric7 x y = not (x /\ y) == not x \/ not y++symmetric8 :: Symmetric a => a -> a -> Bool+symmetric8 x y = (not . not) (x \/ y) == not (not x) \/ not (not y)++symmetric9 :: Symmetric a => a -> a -> Bool+symmetric9 x y = not (x \/ y) == not x /\ not y++symmetric10 :: Symmetric a => a -> a -> Bool+symmetric10 x y = converseL (x \/ y) == converseL x \/ converseL y++symmetric11 :: Symmetric a => a -> a -> Bool+symmetric11 x y = converseR (x /\ y) == converseR x /\ converseR y++symmetric12 :: Symmetric a => a -> a -> Bool+symmetric12 x y = converseL (x /\ y) == (non . non) (converseL x /\ converseL y)++symmetric13 :: Symmetric a => a -> a -> Bool+symmetric13 x y = converseR (x \/ y) == (neg . neg) (converseR x \/ converseR y)++boolean0 :: Biheyting a => a -> Bool+boolean0 x = neg x == non x++boolean1 :: Heyting a => a -> Bool+boolean1 x = neg (neg x) == x++boolean2 :: Heyting a => a -> Bool+boolean2 x = x \/ neg x == top++boolean3 :: Coheyting a => a -> Bool+boolean3 x = x /\ non x == bottom++boolean4 :: Heyting a => a -> a -> Bool+boolean4 x y = (x <= y) // (neg y <= neg x)++boolean5 :: Biheyting a => a -> a -> Bool+boolean5 x y = x \\ y == neg (neg y // neg x)++boolean6 :: Biheyting a => a -> a -> Bool+boolean6 x y = x // y == non (non y \\ non x)+ {- infix 4 `joinLe` -- | The partial ordering induced by the join-semilattice structure.@@ -237,8 +271,8 @@  -- | \( \forall a \in R: a \/ a = a \) ----- @ 'idempotent_join' = 'absorbative' 'true' @--- +-- @ 'idempotent_join' = 'absorbative' 'top' @+-- -- See < https:\\en.wikipedia.org/wiki/Band_(mathematics) >. -- -- This is a required property.@@ -254,10 +288,10 @@ -- This is a required property. -- associative_join :: Lattice r => r -> r -> r -> Bool-associative_join = associative_on (~~) (\/) +associative_join = associative_on (~~) (\/)  associative_join_on :: Semilattice 'L r => Rel r b -> r -> r -> r -> b-associative_join_on (=~) = associative_on (=~) (\/) +associative_join_on (=~) = associative_on (=~) (\/)  -- | \( \forall a, b, c: (a \# b) \# c \doteq a \# (b \# c) \) --@@ -272,8 +306,7 @@ commutative_join = commutative_join_on (~~)  commutative_join_on :: Semilattice 'L r => Rel r b -> r -> r -> b-commutative_join_on (=~) = commutative_on (=~) (\/) -+commutative_join_on (=~) = commutative_on (=~) (\/)  -- | \( \forall a, b: a \# b \doteq b \# a \) --@@ -285,7 +318,7 @@ -- Absorbativity is a generalized form of idempotency: -- -- @--- 'absorbative' 'true' a = a \/ a = a+-- 'absorbative' 'top' a = a \/ a = a -- @ -- -- This is a required property.@@ -298,7 +331,7 @@ -- Absorbativity is a generalized form of idempotency: -- -- @--- 'absorbative'' 'false' a = a \/ a = a+-- 'absorbative'' 'bottom' a = a \/ a = a -- @ -- -- This is a required property.@@ -350,7 +383,6 @@ -- See < https:\\en.wikipedia.org/wiki/Distributivity_(order_theory)#Distributivity_for_semilattices > -- modular :: Lattice r => r -> r -> r -> Bool-modular a b c = a \/ (c /\ b) ~~ (a \/ c) /\ b -+modular a b c = a \/ (c /\ b) ~~ (a \/ c) /\ b  -}

@@ -1,60 +1,57 @@-{-# LANGUAGE Safe                       #-}-{-# LANGUAGE PolyKinds                  #-}-{-# LANGUAGE ConstraintKinds            #-}-{-# Language DataKinds                  #-}-{-# LANGUAGE DefaultSignatures          #-}-{-# LANGUAGE DeriveFunctor              #-}-{-# LANGUAGE DeriveGeneric              #-}-{-# LANGUAGE DerivingVia                #-}-{-# LANGUAGE FlexibleContexts           #-}-{-# LANGUAGE FlexibleInstances          #-}-{-# LANGUAGE StandaloneDeriving         #-}-{-# LANGUAGE TypeOperators              #-}-{-# LANGUAGE TypeFamilies               #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DerivingVia #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE Safe #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}  module Data.Order (-  -- * Constraint kinds-    Order-  , Total-  -- * Preorders-  , Preorder(..)-  , pcomparing-  -- * DerivingVia-  , Base(..), N5(..) -  -- * Re-exports-  , Ordering(..)-  , Down(..)-  , Positive+    -- * Constraint kinds+    Order,+    Total,++    -- * Preorders+    Preorder (..),+    pcomparing,++    -- * DerivingVia+    Base (..),+    N5 (..),++    -- * Re-exports+    Ordering (..),+    Down (..),+    Positive, ) where  import safe Control.Applicative-import safe Control.Monad.Trans.Select-import safe Control.Monad.Trans.Cont import safe Data.Bool import safe Data.Complex import safe Data.Either-import safe Data.Foldable (foldl')+import safe qualified Data.Eq as Eq import safe Data.Functor.Identity-import safe Data.Functor.Contravariant import safe Data.Int+import safe qualified Data.IntMap as IntMap+import safe qualified Data.IntSet as IntSet import safe Data.List.NonEmpty+import safe qualified Data.Map as Map import safe Data.Maybe-import safe Data.Ord (Down(..))+import safe Data.Ord (Down (..))+import safe qualified Data.Ord as Ord import safe Data.Semigroup-import safe Data.Universe.Class (Finite(..))-import safe Data.Word+import safe qualified Data.Set as Set import safe Data.Void+import safe Data.Word import safe GHC.Real import safe Numeric.Natural-import safe Prelude hiding (Ord(..), Bounded, until)-import safe qualified Data.IntMap as IntMap-import safe qualified Data.IntSet as IntSet-import safe qualified Data.Map as Map-import safe qualified Data.Set as Set-import safe qualified Data.Ord as Ord-import safe qualified Data.Eq as Eq-import safe qualified Data.Finite as F-+import safe Prelude hiding (Bounded, Ord (..), until)  -- | An < https://en.wikipedia.org/wiki/Order_theory#Partially_ordered_sets order > on /a/. --@@ -62,17 +59,15 @@ -- -- We instead use a constraint kind in order to retain compatibility with the -- downstream users of /Eq/.--- type Order a = (Eq.Eq a, Preorder a)  -- | A < https://en.wikipedia.org/wiki/Total_order total order > on /a/.--- --- Note: ideally this would be a subclass of /PartialOrder/, without instances+--+-- Note: ideally this would be a subclass of /Order/, without instances -- for /Float/, /Double/, /Rational/, etc. -- -- We instead use a constraint kind in order to retain compatibility with the -- downstream users of /Ord/.---  type Total a = (Ord.Ord a, Preorder a)  -------------------------------------------------------------------------------@@ -84,7 +79,7 @@ -- A preorder relation '<~' must satisfy the following two axioms: -- -- \( \forall x: x \leq x \) (reflexivity)--- +-- -- \( \forall a, b, c: ((a \leq b) \wedge (b \leq c)) \Rightarrow (a \leq c) \) (transitivity) -- -- Given a preorder on /a/ one may define an equivalence relation '~~' such that@@ -101,25 +96,21 @@ -- -- Minimal complete definition: either 'pcompare' or '<~'. Using 'pcompare' can -- be more efficient for complex types.--- class Preorder a where-    {-# MINIMAL (<~) | pcompare #-} +    {-# MINIMAL (<~) | pcompare #-} -    infix 4 <~, >~, <, >, ?~, ~~, /~, `pcompare`, `pmax`, `pmin`+    infix 4 <~, >~, ?~, ~~, /~, `plt`, `pgt`, `pmax`, `pmin`, `pcompare`      -- | A non-strict preorder order relation on /a/.     --     -- Is /x/ less than or equal to /y/?     ---    -- Is /x/ less than or equal to /y/?-    --     -- '<~' is reflexive, anti-symmetric, and transitive.     --     -- > x <~ y = x < y || x ~~ y     -- > x <~ y = maybe False (<~ EQ) (pcompare x y)     --     -- for all /x/, /y/ in /a/.-    --     (<~) :: a -> a -> Bool     x <~ y = maybe False (Ord.<= EQ) (pcompare x y) @@ -127,79 +118,29 @@     --     -- Is /x/ greater than or equal to /y/?     ---    -- Is /x/ greater than or equal to /y/?-    --     -- '>~' is reflexive, anti-symmetric, and transitive.     --     -- > x >~ y = x > y || x ~~ y     -- > x >~ y = maybe False (>~ EQ) (pcompare x y)     --     -- for all /x/, /y/ in /a/.-    --     (>~) :: a -> a -> Bool     (>~) = flip (<~) -    -- | A strict preorder relation on /a/.-    ---    -- Is /x/ less than /y/?-    ---    -- Is /x/ less than /y/?-    ---    -- '<' is irreflexive, asymmetric, and transitive.-    ---    -- > x < y = x <~ y && not (y <~ x)-    -- > x < y = maybe False (< EQ) (pcompare x y)-    ---    -- When '<~' is antisymmetric then /a/ is a partial -    -- order and we have:-    -- -    -- > x < y = x <~ y && x /~ y-    ---    -- for all /x/, /y/ in /a/.-    ---    (<) :: a -> a -> Bool-    x < y = maybe False (Ord.< EQ) (pcompare x y)--    -- | A converse strict preorder relation on /a/.-    ---    -- Is /x/ greater than /y/?-    ---    -- Is /x/ greater than /y/?-    ---    -- '>' is irreflexive, asymmetric, and transitive.-    ---    -- > x > y = x >~ y && not (y >~ x)-    -- > x > y = maybe False (> EQ) (pcompare x y)-    -- -    -- When '<~' is antisymmetric then /a/ is a partial -    -- order and we have:-    -- -    -- > x > y = x >~ y && x /~ y-    ---    -- for all /x/, /y/ in /a/.-    ---    (>) :: a -> a -> Bool-    (>) = flip (<)--    -- | An equivalence relation on /a/. -    ---    -- Are /x/ and /y/ comparable?+    -- | An equivalence relation on /a/.     --     -- Are /x/ and /y/ comparable?     --     -- '?~' is reflexive, symmetric, and transitive.     --     -- If /a/ implements 'Ord' then we should have @x ?~ y = True@.-    --     (?~) :: a -> a -> Bool     x ?~ y = maybe False (const True) (pcompare x y)-    +     -- | An equivalence relation on /a/.     --     -- Are /x/ and /y/ equivalent?     ---    -- Are /x/ and /y/ equivalent?-    --     -- '~~' is reflexive, symmetric, and transitive.     --     -- > x ~~ y = x <~ y && y <~ x@@ -207,19 +148,53 @@     --     -- Use this as a lawful substitute for '==' when comparing     -- floats, doubles, or rationals.-    --     (~~) :: a -> a -> Bool     x ~~ y = maybe False (Eq.== EQ) (pcompare x y)      -- | Negation of '~~'.     --     -- Are /x/ and /y/ not equivalent?-    --     (/~) :: a -> a -> Bool     x /~ y = not $ x ~~ y-    -    -- | A similarity relation on /a/. ++    -- | A strict preorder relation on /a/.     --+    -- Is /x/ less than /y/?+    --+    -- 'plt' is irreflexive, asymmetric, and transitive.+    --+    -- > x `plt` y = x <~ y && not (y <~ x)+    -- > x `plt` y = maybe False (< EQ) (pcompare x y)+    --+    -- When '<~' is antisymmetric then /a/ is a partial+    -- order and we have:+    --+    -- > x `plt` y = x <~ y && x /~ y+    --+    -- for all /x/, /y/ in /a/.+    plt :: a -> a -> Bool+    plt x y = maybe False (Ord.< EQ) (pcompare x y)++    -- | A converse strict preorder relation on /a/.+    --+    -- Is /x/ greater than /y/?+    --+    -- 'pgt' is irreflexive, asymmetric, and transitive.+    --+    -- > x `pgt` y = x >~ y && not (y >~ x)+    -- > x `pgt` y = maybe False (> EQ) (pcompare x y)+    --+    -- When '<~' is antisymmetric then /a/ is a partial+    -- order and we have:+    --+    -- > x `pgt` y = x >~ y && x /~ y+    --+    -- for all /x/, /y/ in /a/.+    pgt :: a -> a -> Bool+    pgt = flip plt++    -- | A similarity relation on /a/.+    --     -- Are /x/ and /y/ either equivalent or incomparable?     --     -- 'similar' is reflexive and symmetric, but not necessarily transitive.@@ -229,10 +204,31 @@     -- > similar (0/0 :: Float) 5 = True     --     -- If /a/ implements 'Ord' then we should have @('~~') = 'similar' = ('==')@.-    --     similar :: a -> a -> Bool     similar x y = maybe True (Eq.== EQ) (pcompare x y) +    -- | A partial version of 'Data.Ord.max'.+    --+    -- Returns the left-hand argument in the case of equality.+    pmax :: a -> a -> Maybe a+    pmax x y = do+        o <- pcompare x y+        case o of+            GT -> Just x+            EQ -> Just x+            LT -> Just y++    -- | A partial version of 'Data.Ord.min'.+    --+    -- Returns the left-hand argument in the case of equality.+    pmin :: a -> a -> Maybe a+    pmin x y = do+        o <- pcompare x y+        case o of+            GT -> Just y+            EQ -> Just x+            LT -> Just x+     -- | A partial version of 'Data.Ord.compare'.     --     -- > x <  y = maybe False (<  EQ) $ pcompare x y@@ -242,46 +238,20 @@     -- > x ~~ y = maybe False (~~ EQ) $ pcompare x y     -- > x ?~ y = maybe False (const True) $ pcompare x y     -- > similar x y = maybe True (~~ EQ) $ pcompare x y-    -- -    -- If /a/ implements 'Ord' then we should have @'pcompare' x y = 'Just' '$' 'compare' x y@.     --+    -- If /a/ implements 'Ord' then we should have @'pcompare' x y = 'Just' '$' 'compare' x y@.     pcompare :: a -> a -> Maybe Ordering-    pcompare x y -      | x <~ y    = Just $ if y <~ x then EQ else LT-      | y <~ x    = Just GT-      | otherwise = Nothing--    -- | A partial version of 'Data.Ord.max'. -    ---    -- Returns the left-hand argument in the case of equality.-    ---    pmax :: a -> a -> Maybe a-    pmax x y = do-      o <- pcompare x y-      case o of-        GT -> Just x-        EQ -> Just x-        LT -> Just y--    -- | A partial version of 'Data.Ord.min'. -    ---    -- Returns the left-hand argument in the case of equality.-    ---    pmin :: a -> a -> Maybe a-    pmin x y = do-      o <- pcompare x y-      case o of-        GT -> Just y-        EQ -> Just x-        LT -> Just x+    pcompare x y+        | x <~ y = Just $ if y <~ x then EQ else LT+        | y <~ x = Just GT+        | otherwise = Nothing  -- | A partial version of 'Data.Order.Total.comparing'. -- -- > pcomparing p x y = pcompare (p x) (p y) ----- The partial application /pcomparing f/ induces a lawful preorder for +-- The partial application /pcomparing f/ induces a lawful preorder for -- any total function /f/.--- pcomparing :: Preorder a => (b -> a) -> b -> b -> Maybe Ordering pcomparing p x y = pcompare (p x) (p y) @@ -289,14 +259,14 @@ -- DerivingVia --------------------------------------------------------------------- -newtype Base a = Base { getBase :: a } deriving stock (Eq.Eq, Ord.Ord, Show, Functor)-  deriving Applicative via Identity-+newtype Base a = Base {getBase :: a}+    deriving stock (Eq.Eq, Ord.Ord, Show, Functor)+    deriving (Applicative) via Identity  instance Ord.Ord a => Preorder (Base a) where-  x <~ y = getBase $ liftA2 (Ord.<=) x y-  x >~ y = getBase $ liftA2 (Ord.>=) x y-  pcompare x y = Just . getBase $ liftA2 Ord.compare x y+    x <~ y = getBase $ liftA2 (Ord.<=) x y+    x >~ y = getBase $ liftA2 (Ord.>=) x y+    pcompare x y = Just . getBase $ liftA2 Ord.compare x y  --instance Preorder Void where  _ <~ _ = True deriving via (Base Void) instance Preorder Void@@ -316,32 +286,30 @@ deriving via (Base Int32) instance Preorder Int32 deriving via (Base Int64) instance Preorder Int64 deriving via (Base Integer) instance Preorder Integer-deriving via (Base (F.Finite n)) instance Preorder (F.Finite n)  --TODO move to Order and derive Preorder as well-newtype N5 a = N5 { getN5 :: a } deriving stock (Eq, Show, Functor)-  deriving Applicative via Identity+newtype N5 a = N5 {getN5 :: a}+    deriving stock (Eq, Show, Functor)+    deriving (Applicative) via Identity  instance (Ord.Ord a, Fractional a) => Preorder (N5 a) where-  x <~ y = getN5 $ liftA2 n5Le x y+    x <~ y = getN5 $ liftA2 n5Le x y  -- N5 lattice ordering: NInf <= NaN <= PInf n5Le :: (Ord.Ord a, Fractional a) => a -> a -> Bool-n5Le x y | x Eq./= x && y Eq./= y = True-       | x Eq./= x = y == 1/0-       | y Eq./= y = x == -1/0-       | otherwise = x Ord.<= y+n5Le x y+    | x Eq./= x && y Eq./= y = True+    | x Eq./= x = y == 1 / 0+    | y Eq./= y = x == -1 / 0+    | otherwise = x Ord.<= y  deriving via (N5 Float) instance Preorder Float deriving via (N5 Double) instance Preorder Double - --------------------------------------------------------------------- -- Instances --------------------------------------------------------------------- -- -- N5 lattice ordering: NInf <= NaN <= PInf {- pinf = 1 :% 0@@ -358,206 +326,111 @@ Nothing -} pcompareRat :: Rational -> Rational -> Maybe Ordering-pcompareRat (0:%0) (x:%0) = Just $ Ord.compare 0 x-pcompareRat (x:%0) (0:%0) = Just $ Ord.compare x 0-pcompareRat (x:%0) (y:%0) = Just $ Ord.compare (signum x) (signum y)-pcompareRat (0:%0) _ = Nothing-pcompareRat _ (0:%0) = Nothing-pcompareRat _ (x:%0) = Just $ Ord.compare 0 x -- guard against div-by-zero exceptions-pcompareRat (x:%0) _ = Just $ Ord.compare x 0+pcompareRat (0 :% 0) (x :% 0) = Just $ Ord.compare 0 x+pcompareRat (x :% 0) (0 :% 0) = Just $ Ord.compare x 0+pcompareRat (x :% 0) (y :% 0) = Just $ Ord.compare (signum x) (signum y)+pcompareRat (0 :% 0) _ = Nothing+pcompareRat _ (0 :% 0) = Nothing+pcompareRat _ (x :% 0) = Just $ Ord.compare 0 x -- guard against div-by-zero exceptions+pcompareRat (x :% 0) _ = Just $ Ord.compare x 0 pcompareRat x y = Just $ Ord.compare x y  -- | Positive rationals, extended with an absorbing zero. -- -- 'Positive' is the canonical < https://en.wikipedia.org/wiki/Semifield#Examples semifield >.--- type Positive = Ratio Natural  -- N5 lattice comparison pcomparePos :: Positive -> Positive -> Maybe Ordering-pcomparePos (0:%0) (x:%0) = Just $ Ord.compare 0 x-pcomparePos (x:%0) (0:%0) = Just $ Ord.compare x 0-pcomparePos (_:%0) (_:%0) = Just EQ -- all non-nan infs are equal-pcomparePos (0:%0) (0:%_) = Just $ GT-pcomparePos (0:%_) (0:%0) = Just $ LT-pcomparePos (0:%0) _ = Nothing-pcomparePos _ (0:%0) = Nothing-pcomparePos (x:%y) (x':%y') = Just $ Ord.compare (x*y') (x'*y)+pcomparePos (0 :% 0) (x :% 0) = Just $ Ord.compare 0 x+pcomparePos (x :% 0) (0 :% 0) = Just $ Ord.compare x 0+pcomparePos (_ :% 0) (_ :% 0) = Just EQ -- all non-nan infs are equal+pcomparePos (0 :% 0) (0 :% _) = Just $ GT+pcomparePos (0 :% _) (0 :% 0) = Just $ LT+pcomparePos (0 :% 0) _ = Nothing+pcomparePos _ (0 :% 0) = Nothing+pcomparePos (x :% y) (x' :% y') = Just $ Ord.compare (x * y') (x' * y)  instance Preorder Rational where-  pcompare = pcompareRat+    pcompare = pcompareRat  instance Preorder Positive where-  pcompare = pcomparePos+    pcompare = pcomparePos  instance (Preorder a, Num a) => Preorder (Complex a) where-  pcompare = pcomparing $ \(x :+ y) -> x^2 + y^2+    pcompare = pcomparing $ \(x :+ y) -> x * x + y * y  instance Preorder a => Preorder (Down a) where-  (Down x) <~ (Down y) = y <~ x-  pcompare (Down x) (Down y) = pcompare y x+    (Down x) <~ (Down y) = y <~ x+    pcompare (Down x) (Down y) = pcompare y x  instance Preorder a => Preorder (Dual a) where-  (Dual x) <~ (Dual y) = y <~ x-  pcompare (Dual x) (Dual y) = pcompare y x+    (Dual x) <~ (Dual y) = y <~ x+    pcompare (Dual x) (Dual y) = pcompare y x  instance Preorder a => Preorder (Max a) where-  Max a <~ Max b = a <~ b+    Max a <~ Max b = a <~ b  instance Preorder a => Preorder (Min a) where-  Min a <~ Min b = a <~ b+    Min a <~ Min b = a <~ b  instance Preorder Any where-  Any x <~ Any y = x <~ y+    Any x <~ Any y = x <~ y  instance Preorder All where-  All x <~ All y = y <~ x+    All x <~ All y = y <~ x  instance Preorder a => Preorder (Identity a) where-  pcompare (Identity x) (Identity y) = pcompare x y+    pcompare (Identity x) (Identity y) = pcompare x y  instance Preorder a => Preorder (Maybe a) where-  Nothing <~ _ = True-  Just{} <~ Nothing = False-  Just a <~ Just b = a <~ b+    Nothing <~ _ = True+    Just{} <~ Nothing = False+    Just a <~ Just b = a <~ b  instance Preorder a => Preorder [a] where-  {-# SPECIALISE instance Preorder [Char] #-}-  --[] <~ _     = True-  --(_:_) <~ [] = False-  --(x:xs) <~ (y:ys) = x <~ y && xs <~ ys+    {-# SPECIALIZE instance Preorder [Char] #-} -  pcompare []     []     = Just EQ-  pcompare []     (_:_)  = Just LT-  pcompare (_:_)  []     = Just GT-  pcompare (x:xs) (y:ys) = case pcompare x y of-                              Just EQ -> pcompare xs ys-                              other   -> other+    --[] <~ _     = True+    --(_:_) <~ [] = False+    --(x:xs) <~ (y:ys) = x <~ y && xs <~ ys +    pcompare [] [] = Just EQ+    pcompare [] (_ : _) = Just LT+    pcompare (_ : _) [] = Just GT+    pcompare (x : xs) (y : ys) = case pcompare x y of+        Just EQ -> pcompare xs ys+        other -> other+ instance Preorder a => Preorder (NonEmpty a) where-  (x :| xs) <~ (y :| ys) = x <~ y && xs <~ ys+    (x :| xs) <~ (y :| ys) = x <~ y && xs <~ ys  instance (Preorder a, Preorder b) => Preorder (Either a b) where-  Right a <~ Right b  = a <~ b-  Right _ <~ _        = False--  Left a <~ Left b   = a <~ b-  Left _ <~ _        = True- -instance (Preorder a, Preorder b) => Preorder (a, b) where -  (a,b) <~ (i,j) = a <~ i && b <~ j+    Right a <~ Right b = a <~ b+    Right _ <~ _ = False+    Left a <~ Left b = a <~ b+    Left _ <~ _ = True -instance (Preorder a, Preorder b, Preorder c) => Preorder (a, b, c) where -  (a,b,c) <~ (i,j,k) = a <~ i && b <~ j && c <~ k+instance (Preorder a, Preorder b) => Preorder (a, b) where+    (a, b) <~ (i, j) = a <~ i && b <~ j -instance (Preorder a, Preorder b, Preorder c, Preorder d) => Preorder (a, b, c, d) where -  (a,b,c,d) <~ (i,j,k,l) = a <~ i && b <~ j && c <~ k && d <~ l+instance (Preorder a, Preorder b, Preorder c) => Preorder (a, b, c) where+    (a, b, c) <~ (i, j, k) = a <~ i && b <~ j && c <~ k -instance (Preorder a, Preorder b, Preorder c, Preorder d, Preorder e) => Preorder (a, b, c, d, e) where -  (a,b,c,d,e) <~ (i,j,k,l,m) = a <~ i && b <~ j && c <~ k && d <~ l && e <~ m+instance (Preorder a, Preorder b, Preorder c, Preorder d) => Preorder (a, b, c, d) where+    (a, b, c, d) <~ (i, j, k, l) = a <~ i && b <~ j && c <~ k && d <~ l ---instance (Foldable1 f, Representable f, Preorder a) => Preorder (Co f a) where---  Co f <~ Co g = and $ liftR2 (<~) f g+instance (Preorder a, Preorder b, Preorder c, Preorder d, Preorder e) => Preorder (a, b, c, d, e) where+    (a, b, c, d, e) <~ (i, j, k, l, m) = a <~ i && b <~ j && c <~ k && d <~ l && e <~ m  instance (Ord.Ord k, Preorder a) => Preorder (Map.Map k a) where-  (<~) = Map.isSubmapOfBy (<~)+    (<~) = Map.isSubmapOfBy (<~)  instance Ord.Ord a => Preorder (Set.Set a) where-  (<~) = Set.isSubsetOf+    (<~) = Set.isSubsetOf  instance Preorder a => Preorder (IntMap.IntMap a) where-  (<~) = IntMap.isSubmapOfBy (<~)+    (<~) = IntMap.isSubmapOfBy (<~)  instance Preorder IntSet.IntSet where-  (<~) = IntSet.isSubsetOf---- | TODO: short-circuiting version.------ >>> const 3 <~ (const 4 :: Int8 -> Int8)--- True--- >>> const 3 <~ (id :: Int8 -> Int8)--- False-instance (Finite a, Preorder b) => Preorder (a -> b) where-  pcompare f g = foldl' acc (Just EQ) [f x `pcompare` g x | x <- universeF]-    where acc old new = do-            m' <- new-            n' <- old-            case (m', n') of-              (x , EQ) -> Just x-              (EQ, y ) -> Just y-              (x , y ) -> if x == y then Just x else Nothing--instance (Finite a, Preorder a) => Preorder (Endo a) where-  pcompare (Endo f) (Endo g) = pcompare f g--instance (Finite a, Preorder b) => Preorder (Op b a) where-  --universe = coerce (universe :: [b -> a])-  --universe = map Op universe-  pcompare (Op f) (Op g) = pcompare f g--instance (Finite a) => Preorder (Predicate a) where-  --universe = map (Predicate . flip S.member) universe-  --universe = map Op universe-  pcompare (Predicate f) (Predicate g) = pcompare f g---- |--- >>> cont ($ 1) == (cont ($ 2) :: Cont Bool Int8)--- False--- >>> cont ($ 1) == (cont ($ 2) :: Cont () Int8)--- True-instance (Total a, Preorder r, Finite r) => Preorder (Cont r a) where-  (ContT x) <~ (ContT y) = x `contLe` y--instance (Total a, Preorder r, Finite r) => Preorder (Select r a) where-  (SelectT x) <~ (SelectT y) = x `contLe` y--contLe :: forall a b c. (Finite b, Ord.Ord a, Preorder a, Preorder b, Preorder c) => ((a -> b) -> c) -> ((a -> b) -> c) -> Bool-contLe x y = if (universeF :: [b]) ~~ [] then True else point $ counter Map.empty-  where-    --point :: Preorder b => a -> Bool-    point ar = x ar <~ y ar--    --counter :: (Finite b, Ord.Ord a, Preorder c) => Map.Map a b -> a -> b-    counter acc a = case Map.lookup a acc of-      Just b -> b--      Nothing -> case [b | b <- universeF -                         , let acc' = Map.insert a b acc-                               func a' | a' < a = counter acc a'-                                 | otherwise = counter acc' a'-                         , not . point $ func-                      ] of-                   (b:_) -> b-                   [] -> Prelude.head universeF -- Return a failed counter-example to be pruned by 'point'---{--exm1, exm2, exm3 :: Cont Bool Integer-exm1 = cont $ \ib -> (ib 7 && ib 4) || ib 8-exm2 = cont $ \ib -> (ib 7 || ib 8) && (ib 4 || ib 8)-exm3 = cont $ \ib -> (ib 7 || ib 8) && ib 4---- exm1 ~~ exm2 >~ exm3-ex1 = (exm1 ~~ exm2, exm1 ~~ exm3, exm2 ~~ exm3) --(True, False, False)-ex2 = (exm1 ~~ exm2, exm1 >~ exm3, exm2 >~ exm3) --(True, True, True)-ex3 = (exm1 ~~ exm2 \/ exm3) -- True---- exm2 >~ exm3--- λ> runCont exm2 diff--- True--- λ> runCont exm3 diff--- False-diff :: Integer -> Bool-diff i = if i ~~ 7 || i ~~ 8 then True else False--}-------------------------------------------------------------------------- Orphan Instances------------------------------------------------------------------------instance (Finite a, Eq b) => Eq (a -> b) where-  f == g = and [f x == g x | x <- universeF]--deriving via (a -> a) instance (Finite a, Eq a) => Eq (Endo a)-deriving via (a -> b) instance (Finite a, Eq b) => Eq (Op b a)-deriving via (Op Bool a) instance (Finite a) => Eq (Predicate a)+    (<~) = IntSet.isSubsetOf

@@ -1,25 +1,26 @@-{-# Language Safe                #-}-{-# Language DeriveFunctor       #-}-{-# Language DeriveGeneric       #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE Safe #-}  module Data.Order.Extended (-  -- * Lattice extensions-    type Lifted-  , type Lowered-  , Extended(..)-  , extended-  --, retract-  -- * Lattice Extensions-  , liftMaybe-  , liftEitherL-  , liftEitherR-  , liftExtended+    -- * Lattice extensions+    Lifted,+    Lowered,+    Extended (..),+    extended,+    --, retract++    -- * Lattice Extensions+    liftMaybe,+    liftEitherL,+    liftEitherR,+    liftExtended, ) where  import safe Data.Order import safe Data.Order.Syntax import safe GHC.Generics-import safe Prelude hiding (Eq(..), Ord(..),Bounded)+import safe Prelude hiding (Bounded, Eq (..), Ord (..))  type Lifted = Either () @@ -29,21 +30,19 @@ -- -- The top is the absorbing element for the join, and the bottom is the absorbing -- element for the meet.--- data Extended a = Bottom | Extended a | Top-  deriving ( Eq, Ord, Show, Generic, Functor, Generic1 )+    deriving (Eq, Ord, Show, Generic, Functor, Generic1)  -- | Eliminate an 'Extended'. extended :: b -> b -> (a -> b) -> Extended a -> b-extended b _ _ Bottom       = b-extended _ t _ Top          = t+extended b _ _ Bottom = b+extended _ t _ Top = t extended _ _ f (Extended x) = f x  ------------------------------------------------------------------------------- -- Lattice extensions ------------------------------------------------------------------------------- - {- lifts :: Minimal a => Eq a => (a -> b) -> a -> Lifted b lifts = liftEitherL (== minimal)@@ -55,40 +54,48 @@ lowered f = either f (const maximal)  lowers :: Maximal a => Eq a => (a -> b) -> a -> Lowered b-lowers = liftEitherR (== maximal) +lowers = liftEitherR (== maximal) -}  liftMaybe :: (a -> Bool) -> (a -> b) -> a -> Maybe b-liftMaybe p f = g where-  g i | p i = Nothing-      | otherwise = Just $ f i+liftMaybe p f = g+  where+    g i+        | p i = Nothing+        | otherwise = Just $ f i  liftEitherL :: (a -> Bool) -> (a -> b) -> a -> Lifted b-liftEitherL p f = g where-  g i | p i = Left ()-      | otherwise = Right $ f i+liftEitherL p f = g+  where+    g i+        | p i = Left ()+        | otherwise = Right $ f i  liftEitherR :: (a -> Bool) -> (a -> b) -> a -> Lowered b-liftEitherR p f = g where-  g i | p i = Right ()-      | otherwise = Left $ f i+liftEitherR p f = g+  where+    g i+        | p i = Right ()+        | otherwise = Left $ f i  liftExtended :: (a -> Bool) -> (a -> Bool) -> (a -> b) -> a -> Extended b-liftExtended p q f = g where-  g i | p i = Bottom-      | q i = Top-      | otherwise = Extended $ f i+liftExtended p q f = g+  where+    g i+        | p i = Bottom+        | q i = Top+        | otherwise = Extended $ f i  --------------------------------------------------------------------- -- Instances ---------------------------------------------------------------------  instance Preorder a => Preorder (Extended a) where-  _ <~ Top = True-  Top <~ _ = False-  Bottom <~ _ = True-  _ <~ Bottom = False-  Extended x <~ Extended y = x <~ y+    _ <~ Top = True+    Top <~ _ = False+    Bottom <~ _ = True+    _ <~ Bottom = False+    Extended x <~ Extended y = x <~ y  {- instance Universe a => Universe (Extended a) where

@@ -1,33 +1,21 @@-{-# LANGUAGE DeriveFunctor              #-}-{-# LANGUAGE Safe              #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE Safe #-}  module Data.Order.Interval (-    Interval()-  , imap-  , (...)-  , iempty-  , singleton-  , contains-  , endpts-  --, above-  --, below-  --, interval-  -- * Floating point intervals-  , open32-  , open32L-  , open32R-  , open64-  , open64L-  , open64R+    Interval (),+    imap,+    (...),+    iempty,+    singleton,+    contains,+    endpts, ) where  import safe Data.Bifunctor (bimap)+import safe qualified Data.Eq as Eq import safe Data.Order import safe Data.Order.Syntax-import safe Prelude hiding (Ord(..), Eq(..), Bounded, until)-import safe qualified Data.Eq as Eq-import safe qualified Data.Connection.Float as F32-import safe qualified Data.Connection.Double as F64+import safe Prelude hiding (Bounded, Eq (..), Ord (..), until)  --------------------------------------------------------------------- -- Intervals@@ -38,14 +26,12 @@ -- An interval in a poset /P/ is a subset /I/ of /P/ with the following property: -- -- \( \forall x, y \in I, z \in P: x \leq z \leq y \Rightarrow z \in I \)----data Interval a = Empty | Interval !a !a deriving Show+data Interval a = Empty | Interval !a !a deriving (Show)  -- | Map over an interval. -- -- /Note/ this is not a functor, as a non-monotonic map -- may cause the interval to collapse to the iempty interval.--- imap :: Preorder b => (a -> b) -> Interval a -> Interval b imap f = maybe iempty (uncurry (...)) . fmap (bimap f f) . endpts @@ -55,19 +41,17 @@ -- -- /Note/: Endpoints are preorder-sorted. If /pcompare x y = Nothing/ -- then the resulting interval will be empty.---  (...) :: Preorder a => a -> a -> Interval a x ... y = case pcompare x y of-  Just LT -> Interval x y-  Just EQ -> Interval x y-  _ -> Empty+    Just LT -> Interval x y+    Just EQ -> Interval x y+    _ -> Empty {-# INLINE (...) #-}  -- | The iempty interval. -- -- >>> iempty -- Empty--- iempty :: Interval a iempty = Empty {-# INLINE iempty #-}@@ -76,13 +60,11 @@ -- -- >>> singleton 1 -- 1 ... 1--- singleton :: a -> Interval a singleton a = Interval a a {-# INLINE singleton #-}  -- | Obtain the endpoints of an interval.--- endpts :: Interval a -> Maybe (a, a) endpts Empty = Nothing endpts (Interval x y) = Just (x, y)@@ -92,132 +74,21 @@ contains Empty _ = False contains (Interval x y) p = x <~ p && p <~ y -{------ | \( X_\geq(x) = \{ y \in X | y \geq x \} \)------ Construct the upper set of an element /x/.------ This function is monotone:------ > x <~ y <=> above x <~ above y------ by the Yoneda lemma for preorders.----above :: Maximal a => a -> Interval a-above x = x ... maximal-{-# INLINE above #-}---- | \( X_\leq(x) = \{ y \in X | y \leq x \} \)------ Construct the lower set of an element /x/.------ This function is antitone:------ > x <~ y <=> below x >~ below y----below :: Minimal a => a -> Interval a-below x = minimal ... x-{-# INLINE below #-}----}- ------------------------------------------------------------------------ Floating point intervals--------------------------------------------------------------------------- | Construnct an open interval.------ >>> contains 1 $ open32 1 2--- False--- >>> contains 2 $ open32 1 2--- False----open32 :: Float -> Float -> Interval Float-open32 x y = F32.shift 1 x ... F32.shift (-1) y---- | Construnct a half-open interval.------ >>> contains 1 $ open32L 1 2--- False--- >>> contains 2 $ open32L 1 2--- True----open32L :: Float -> Float -> Interval Float-open32L x y = F32.shift 1 x ... y---- | Construnct a half-open interval.------ >>> contains 1 $ open32R 1 2--- True--- >>> contains 2 $ open32R 1 2--- False----open32R :: Float -> Float -> Interval Float-open32R x y = x ... F32.shift (-1) y---- | Construnct an open interval.------ >>> contains 1 $ open64 1 2--- False--- >>> contains 2 $ open64 1 2--- False----open64 :: Double -> Double -> Interval Double-open64 x y = F64.shift 1 x ... F64.shift (-1) y---- | Construnct a half-open interval.------ >>> contains 1 $ open64L 1 2--- False--- >>> contains 2 $ open64L 1 2--- True----open64L :: Double -> Double -> Interval Double-open64L x y = F64.shift 1 x ... y---- | Construnct a half-open interval.------ >>> contains 1 $ open64R 1 2--- True--- >>> contains 2 $ open64R 1 2--- False----open64R :: Double -> Double -> Interval Double-open64R x y = x ... F64.shift (-1) y--{---- | Generate a list of the contents on an interval.------ Returns the list of values in the interval defined by a bounding pair.------ Lawful variant of 'enumFromTo'.----indexFromTo :: Interval Float -> [Float]-indexFromTo i = case endpts i of-  Nothing -> []-  Just (x, y) -> flip unfoldr x $ \i -> if i ~~ y then Nothing else Just (i, shift 1 i)--}----------------------------------------------------------------------- -- Instances ---------------------------------------------------------------------  instance Eq a => Eq (Interval a) where-  Empty == Empty = True-  Empty == _ = False-  _ == Empty = False-  Interval x y == Interval x' y' = x == x' && y == y'+    Empty == Empty = True+    Empty == _ = False+    _ == Empty = False+    Interval x y == Interval x' y' = x == x' && y == y'  -- | A < https://en.wikipedia.org/wiki/Containment_order containment order >--- instance Preorder a => Preorder (Interval a) where-  Empty <~ _ = True-  _ <~ Empty = False-  Interval x y <~ Interval x' y' = x' <~ x && y <~ y'+    Empty <~ _ = True+    _ <~ Empty = False+    Interval x y <~ Interval x' y' = x' <~ x && y <~ y'  {- instance Bounded 'L a => Connection k (Maybe a) (Interval a) where@@ -231,19 +102,15 @@     f = maybe Nothing (Just . uncurry (\/)) . endpts     g = maybe iempty singleton     h = maybe Nothing (Just . uncurry (/\)) . endpts--} --{- instance Lattice a => Lattice (Interval a) where   (\/) = joinInterval   (/\) = meetInterval +bottom = Empty+top = bottom ... top joinInterval Empty i = i joinInterval i Empty = i joinInterval (I x y) (I x' y') = I (x /\ x') (y \/ y') -instance Bounded a => Bounded (Interval a) where-  bottom = Empty-  top = bottom ... top -}