connections 0.0.3 → 0.1.0

raw patch · 39 files changed

+5874/−5980 lines, 39 filesdep +finite-typelitsdep +transformersdep +universe-basedep −lawzdep −ringsdep −semigroupoidsdep ~containersPVP ok

version bump matches the API change (PVP)

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

Dependencies removed: lawz, rings, semigroupoids

Dependency ranges changed: containers

API changes (from Hackage documentation)

Files

• connections.cabal +26/−27
• src/Data/Connection.hs +150/−244
• src/Data/Connection/Class.hs +815/−0
• src/Data/Connection/Conn.hs +377/−0
• src/Data/Connection/Double.hs +322/−0
• src/Data/Connection/Float.hs +178/−135
• src/Data/Connection/Int.hs +104/−101
• src/Data/Connection/Property.hs +104/−49
• src/Data/Connection/Ratio.hs +163/−233
• src/Data/Connection/Round.hs +0/−249
• src/Data/Connection/Word.hs +103/−32
• src/Data/Float.hsc +0/−875
• src/Data/Lattice.hs +696/−0
• src/Data/Lattice/Property.hs +356/−0
• src/Data/Order.hs +563/−0
• src/Data/Order/Extended.hs +99/−0
• src/Data/Order/Interval.hs +249/−0
• src/Data/Order/Property.hs +376/−0
• src/Data/Order/Syntax.hs +109/−0
• src/Data/Prd.hs +0/−690
• src/Data/Prd/Nan.hs +0/−126
• src/Data/Prd/Property.hs +0/−193
• src/Data/Semigroup/Join.hs +0/−272
• src/Data/Semigroup/Meet.hs +0/−267
• src/Data/Semilattice.hs +0/−347
• src/Data/Semilattice/MaxMin.hs +0/−34
• src/Data/Semilattice/N5.hs +0/−135
• src/Data/Semilattice/Property.hs +0/−348
• src/Data/Semilattice/Top.hs +0/−148
• src/Numeric/Prelude.hs +0/−182
• test/Test/Data/Connection.hs +65/−35
• test/Test/Data/Connection/Float.hs +104/−403
• test/Test/Data/Connection/Int.hs +109/−182
• test/Test/Data/Connection/Ratio.hs +92/−225
• test/Test/Data/Connection/Word.hs +72/−104
• test/Test/Data/Lattice.hs +285/−0
• test/Test/Data/Order.hs +348/−0
• test/Test/Data/Prd.hs +0/−337
• test/test.hs +9/−7

@@ -1,7 +1,7 @@ name:                connections-version:             0.0.3-synopsis:            Partial orders, Galois connections, and lattices.-description:         A library for numerical conversions using Galois connections.+version:             0.1.0+synopsis:            Orders, Galois connections, and lattices.+description:         A library for order manipulation using Galois connections. homepage:            https://github.com/cmk/connections license:             BSD3 license-file:        LICENSE@@ -18,33 +18,32 @@   default-language: Haskell2010   ghc-options:      -Wall -optc-std=c99   exposed-modules:-      Data.Prd-    , Data.Prd.Nan-    , Data.Prd.Property-    , Data.Float-    , Data.Semigroup.Join-    , Data.Semigroup.Meet-    , Data.Connection++      Data.Connection+    , Data.Connection.Conn+    , Data.Connection.Class     , Data.Connection.Int     , Data.Connection.Word-    , Data.Connection.Float     , Data.Connection.Ratio-    , Data.Connection.Round+    , Data.Connection.Float+    , Data.Connection.Double     , Data.Connection.Property-    , Data.Semilattice-    , Data.Semilattice.N5-    , Data.Semilattice.Top-    , Data.Semilattice.MaxMin-    , Data.Semilattice.Property -    , Numeric.Prelude+    , Data.Lattice+    , Data.Lattice.Property +    , Data.Order+    , Data.Order.Extended+    , Data.Order.Interval+    , Data.Order.Property+    , Data.Order.Syntax+       build-depends:       -      base              >= 4.10    && < 5.0-    , lawz              >= 0.1.1   && < 1.0-    , rings             >= 0.0.3.1 && < 0.0.4-    , containers        >= 0.4.0   && < 0.7-    , semigroupoids     >= 5.0     && < 6.0+      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@@ -58,7 +57,8 @@ test-suite test   type: exitcode-stdio-1.0   other-modules:-      Test.Data.Prd+      Test.Data.Order+    , Test.Data.Lattice     , Test.Data.Connection     , Test.Data.Connection.Int     , Test.Data.Connection.Word@@ -68,11 +68,10 @@       base == 4.*     , connections -any      , hedgehog-    , rings-    , lawz   default-extensions:       ScopedTypeVariables,-      TypeApplications+      TypeApplications,+      FlexibleContexts   main-is: test.hs   hs-source-dirs: test   default-language: Haskell2010

@@ -1,281 +1,187 @@-{-# Language TypeFamilies #-}-{-# Language TypeApplications #-}+{-# Language TypeApplications    #-} {-# Language AllowAmbiguousTypes #-}-{-# Language ConstraintKinds #-}+{-# Language ConstraintKinds     #-}+{-# Language DataKinds           #-}+{-# Language Safe                #-}+{-# Language ViewPatterns        #-}+{-# Language PatternSynonyms     #-}+{-# Language RankNTypes          #-}+{-# Language QuantifiedConstraints #-}  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-    Conn(..)-  , connl-  , connr-  , unit-  , counit-  , pcomparing-  , dual-  , first-  , second-  , left-  , right-  , strong+  , type Trip+  , pattern Conn+  , half+  , midpoint+  , round+  , round1+  , round2+  , truncate+  , truncate1+  , truncate2+  , maybeL+  , maybeR   , choice-  , (&&&)-  , (|||)-  , just-  , list-  , ordbin-  , binord-  -- * Triple-  , Trip(..)-  , tripl-  , tripr-  , unitl-  , unitr-  , counitl-  , counitr-  , bound-  , first'-  , second'-  , left'-  , right'-  , strong'-  , choice'-  , forked-  , joined-  , maybel-  , mayber+  , strong+  , fmapped+  -- * Connection+  , Conn()+  , Triple+  , Connection(..) ) where --import Control.Category (Category, (>>>))-import Data.Bifunctor (bimap)-import Data.Bool-import Data.Prd-import Data.Semigroup.Join-import Data.Semigroup.Meet-import Prelude hiding (Ord(..), Num(..), Fractional(..), RealFrac(..))--import qualified Control.Category as C+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 --- | A Galois connection between two monotone functions.------ Each side of the connection may be defined in terms of the other:+-- | Determine which half of the interval between 2 representations of /a/ a particular value lies. -- ---  \( connr(x) = \sup \{y \in E \mid connl(y) \leq x \} \)------  \( connl(x) = \inf \{y \in E \mid connr(y) \geq x \} \)------ Galois connections have the same properties as adjunctions defined over other categories:------  \( \forall x, y : connl \dashv connr \Rightarrow connl (x) \leq b \Leftrightarrow x \leq connr (y) \)------  \( \forall x, y : x \leq y \Rightarrow connl (x) \leq connl (y) \)+-- @ 'half' t x = 'pcompare' (x - 'counitR' t x) ('unitL' t x - x) @ -----  \( \forall x, y : x \leq y \Rightarrow connr (x) \leq connr (y) \)+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. -----  \( \forall x : connl \dashv connr \Rightarrow x \leq connr \circ connl (x) \)+-- >>> midpoint f32i08 4.3+-- 4.5+-- >>> midpoint f64i08 4.3+-- 4.5+-- >>> pi - midpoint f64f32 pi+-- 3.1786509424591713e-8 -----  \( \forall x : connl \dashv connr \Rightarrow connl \circ connr (x) \leq x \)+-- >>> maybe False (~~ EQ) $ half f64f32 (midpoint f64f32 pi)+-- True -----  \( \forall x : unit \circ unit (x) \sim unit (x) \)+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. -----  \( \forall x : counit \circ counit (x) \sim counit (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). -----  \( \forall x : counit \circ connl (x) \sim connl (x) \)+-- See <https://en.wikipedia.org/wiki/Rounding>. -----  \( \forall x : unit \circ connr (x) \sim connr (x) \)+-- Usable in conjunction with /RebindableSyntax/: ----- See also 'Data.Function.Connection.Property' and <https://en.wikipedia.org/wiki/Galois_connection>.+-- >>> fromRational = round+-- >>> fromRational @Float 1.3+-- 1.3+-- >>> fromRational @Float (1 :% 0)+-- Infinity+-- >>> fromRational @Float (0 :% 0)+-- NaN ---data Conn a b = Conn (a -> b) (b -> a)--instance Category Conn where-  id = Conn id id-  Conn f' g' . Conn f g = Conn (f' . f) (g . g')+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 --- | Extract the left side of a connection.----connl :: Prd a => Prd b => Conn a b -> a -> b-connl (Conn f _) = f+  where+    halfR = x - counitR (connR @a @b) x -- dist from lower bound --- | Extract the right side of a connection.----connr :: Prd a => Prd b => Conn a b -> b -> a-connr (Conn _ g) = g+    halfL = unitL (connL @a @b) x - x -- dist from upper bound --- | Round trip through a connection.+-- | Lift a unary function over a 'Trip'. ----- @x '<=' 'unit' x@+-- Results are rounded to the nearest value with ties away from 0. ---unit :: Prd a => Prd b => Conn a b -> a -> a-unit (Conn f g) = g . f+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 #-} --- | Reverse round trip through a connection.------ @'counit' x '<=' x@+-- | Lift a binary function over a 'Trip'. ---counit :: Prd a => Prd b => Conn a b -> b -> b-counit (Conn f g) = f . g---- | Partial version of 'Data.Ord.comparing'. +-- Results are rounded to the nearest value with ties away from 0. ---pcomparing :: Prd a => Prd b => Conn a b -> a -> a -> Maybe Ordering-pcomparing (Conn f _) x y = f x `pcompare` f y-------------------------------------------------------------------------- Instances-------------------------------------------------------------------------- | Reverse a connection using the dual partial order on each side.+-- >>> 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 ---dual :: Prd a => Prd b => Conn a b -> Conn (Down b) (Down a)-dual (Conn f g) = Conn (\(Down b) -> Down $ g b) (\(Down a) -> Down $ f a)+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 #-} --- | @'first' (ab '>>>' cd) = 'first' ab '>>>' 'first' cd@+-- | Truncate towards zero. ---first :: Prd a => Prd b => Prd c => Conn a b -> Conn (a, c) (b, c)-first = flip strong C.id---- | @'second' (ab '>>>' cd) = 'second' ab '>>>' 'second' cd@+-- > truncate @a @a = id ---second :: Prd a => Prd b => Prd c => Conn a b -> Conn (c, a) (c, b)-second = strong C.id+truncate :: (Num a, Triple a b) => a -> b+truncate x = if x >~ 0 then floor x else ceiling x --- | @'left' (ab '>>>' cd) = 'left' ab '>>>' 'left' cd@+-- | Lift a unary function over a 'Trip'. ---left :: Prd a => Prd b => Prd c => Conn a b -> Conn (Either a c) (Either b c)-left = flip choice C.id---- | @'right' (ab '>>>' cd) = 'right' ab '>>>' 'right' cd@+-- Results are truncated towards 0. ---right :: Prd a => Prd b => Prd c => Conn a b -> Conn (Either c a) (Either c b)-right = choice C.id --infixr 3 &&&-(&&&) :: Prd a => Prd b => JoinSemilattice c => MeetSemilattice c => Conn c a -> Conn c b -> Conn c (a, b)-f &&& g = tripr forked >>> f `strong` g--infixr 2 |||-(|||) :: Prd a => Prd b => Prd c => Conn a c -> Conn b c -> Conn (Either a b) c-f ||| g = f `choice` g >>> tripr joined--strong :: Prd a => Prd b => Prd c => Prd d => Conn a b -> Conn c d -> Conn (a, c) (b, d)-strong (Conn ab ba) (Conn cd dc) = Conn f g where-  f = bimap ab cd -  g = bimap ba dc--choice :: Prd a => Prd b => Prd c => Prd d => Conn a b -> Conn c d -> Conn (Either a c) (Either b d)-choice (Conn ab ba) (Conn cd dc) = Conn f g where-  f = either (Left . ab) (Right . cd)-  g = either (Left . ba) (Right . dc)--just :: Prd a => Prd b => Conn a b -> Conn (Maybe a) (Maybe b)-just (Conn f g) = Conn (fmap f) (fmap g)--list :: Prd a => Prd b => Conn a b -> Conn [a] [b]-list (Conn f g) = Conn (fmap f) (fmap g)--ordbin :: Conn Ordering Bool-ordbin = Conn f g where-  f GT = True-  f _  = False--  g True = GT-  g _    = EQ--binord :: Conn Bool Ordering-binord = Conn f g where-  f False = LT-  f _     = EQ--  g LT = False-  g _  = True-------------------------------------------------------------------------- Adjoint triples----------------------------------------------------------------------+truncate1 :: (Num a, Triple a b) => (a -> a) -> b -> b+truncate1 f x = truncate $ f (g x) where Conn _ g _ = connL+{-# INLINE truncate1 #-} --- | An adjoint triple.------ @'Trip' f g h@ satisfies:------ @--- f ⊣ g--- ⊥   ⊥--- g ⊣ h--- @+-- | Lift a binary function over a 'Trip'. ----- See <https://ncatlab.org/nlab/show/adjoint+triple>+-- Results are truncated towards 0. ---data Trip a b = Trip (a -> b) (b -> a) (a -> b)--instance Category Trip where-  id = Trip id id id-  Trip f' g' h' . Trip f g h = Trip (f' . f) (g . g') (h' . h)--tripl :: Prd a => Prd b => Trip a b -> Conn a b-tripl (Trip f g _) = Conn f g--tripr :: Prd a => Prd b => Trip a b -> Conn b a-tripr (Trip _ g h) = Conn g h--unitl :: Prd a => Prd b => Trip a b -> a -> a-unitl = unit . tripl--unitr :: Prd a => Prd b => Trip a b -> b -> b-unitr = unit . tripr--counitl :: Prd a => Prd b => Trip a b -> b -> b-counitl = counit . tripl--counitr :: Prd a => Prd b => Trip a b -> a -> a-counitr = counit . tripr--------------------------------------------------------------------------  Instances------------------------------------------------------------------------bound :: Prd a => Bound a => Trip () a-bound = Trip (const minimal) (const ()) (const maximal)--first' :: Prd a => Prd b => Prd c => Trip a b -> Trip (a, c) (b, c)-first' = flip strong' C.id--second' :: Prd a => Prd b => Prd c => Trip a b -> Trip (c, a) (c, b)-second' = strong' C.id--left' :: Prd a => Prd b => Prd c => Trip a b -> Trip (Either a c) (Either b c)-left' = flip choice' C.id--right' :: Prd a => Prd b => Prd c => Trip a b -> Trip (Either c a) (Either c b)-right' = choice' C.id--strong' :: Prd a => Prd b => Prd c => Prd d => Trip a b -> Trip c d -> Trip (a, c) (b, d)-strong' (Trip ab ba ab') (Trip cd dc cd') = Trip f g h where-  f = bimap ab cd -  g = bimap ba dc-  h = bimap ab' cd'--choice' :: Prd a => Prd b => Prd c => Prd d => Trip a b -> Trip c d -> Trip (Either a c) (Either b d)-choice' (Trip ab ba ab') (Trip cd dc cd') = Trip f g h where-  f = either (Left . ab) (Right . cd)-  g = either (Left . ba) (Right . dc)-  h = either (Left . ab') (Right . cd')--forked :: JoinSemilattice a => MeetSemilattice a => Trip (a, a) a-forked = Trip (uncurry (∨)) (\x -> (x,x)) (uncurry (∧))--joined :: Prd a => Trip a (Either a a)-joined = Trip Left (either id id) Right--maybel :: Prd a => Bound 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 :: Prd b => Bound 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+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 #-}

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

@@ -0,0 +1,377 @@+{-# Language TypeFamilies        #-}+{-# Language TypeApplications    #-}+{-# Language AllowAmbiguousTypes #-}+{-# Language ConstraintKinds     #-}+{-# Language Safe                #-}+{-# Language DeriveFunctor       #-}+{-# Language DeriveGeneric       #-}+{-# Language DataKinds           #-}+{-# Language ViewPatterns        #-}+{-# Language PatternSynonyms     #-}+{-# Language RankNTypes          #-}+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+) where++import safe Control.Arrow+import safe Control.Category (Category)+import safe Data.Bifunctor (bimap)+import safe Data.Order+import safe Prelude hiding (Ord(..), Bounded)+import safe qualified Control.Category as C++-- | 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'+--+-- * /R/-tagged types are 'downwards-directed'+--+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)++instance Category (Conn k) where+  id = Conn_ (id &&& id) id++  Conn_ f1 g1 . Conn_ f2 g2 = Conn_ ((fst.f1).(fst.f2) &&& (snd.f1).(snd.f2)) (g2 . g1)++-- | Obtain the center of a /Trip/, upper half of a /ConnL/, or the lower half of a /ConnR/.+--+embed :: Conn k a b -> b -> a+embed (Conn_ _ g) = g++-- Internal floor function. When \(f \dashv g \dashv h \) this is h.+_1 :: Conn k a b -> a -> b+_1 (Conn_ f _) = fst . f++-- Internal ceiling function. When \(f \dashv g \dashv h \) this is f.+_2 :: Conn k a b -> a -> b+_2 (Conn_ f _) = snd . f++---------------------------------------------------------------------+-- Trip+---------------------------------------------------------------------++-- | 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 \) +--+-- For detailed properties see 'Data.Connection.Property'.+--+type Trip a b = forall k. Conn k a b++-- | A view pattern for an arbitrary (left or right) 'Conn'.+--+-- /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 = Conn_ (h &&& f) g+{-# COMPLETE Conn #-}++-- | Obtain a /forall k. Conn k/ from an adjoint triple of monotone functions.+--+-- /Caution/: @Conn f g h@ must obey \(f \dashv g \dashv h\). This condition is not checked.+--+trip :: (a -> b) -> (b -> a) -> (a -> b) -> Trip a b+trip f g h = Conn_ (h &&& f) g++-- | Obtain the lower and upper functions from a 'Trip'.+--+-- > range c = upperR c &&& lowerL c+--+-- >>> range f64f32 pi+-- (3.1415925,3.1415927)+-- >>> range f64f32 (0/0)+-- (NaN,NaN)+--+range :: Trip a b -> a -> (b, b)+range c = upperR c &&& lowerL c ++---------------------------------------------------------------------+-- ConnL+---------------------------------------------------------------------++-- | A <https://ncatlab.org/nlab/show/Galois+connection Galois connection> between two monotone functions.+--+-- A Galois connection between /f/ and /g/, written \(f \dashv g \)+-- is an adjunction in the category of preorders.+--+-- 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 \} \)+--+-- 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+{-# COMPLETE ConnL #-}++-- | Witness to the symmetry between 'ConnL' and 'ConnR'.+--+-- > swapL . swapR = id+-- > swapR . swapL = id+--+swapL :: ConnR a b -> ConnL b a+swapL (ConnR f g) = ConnL f g++-- | Convert an arbitrary 'Conn' to an inverted 'ConnL'.+--+-- >>> unitL (downL $ conn @_ @() @Ordering) (Down LT)+-- Down LT+-- >>> unitL (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)++-- | Round trip through a connection.+--+-- > unitL c = upperL1 c id = embed c . lowerL c+-- > x <= unitL c x+-- +-- >>> compare pi $ unitL f64f32 pi+-- LT+--+unitL :: ConnL a b -> a -> a+unitL c = upperL1 c id++-- | Reverse round trip through a connection.+--+-- > x >= counitL c x+--+-- >>> counitL (conn @_ @() @Ordering) LT+-- LT+-- >>> counitL (conn @_ @() @Ordering) GT+-- LT+--+counitL :: ConnL a b -> b -> b+counitL c = lowerL1 c id++-- | Extract the lower half of a 'Trip' or 'ConnL'.+--+-- When /a/ and /b/ are lattices we have:+--+-- > lowerL c (x1 \/ a2) = lowerL c x1 \/ lowerL c x2+--+-- This is the adjoint functor theorem for preorders.+--+-- >>> upperR f64f32 pi+-- 3.1415925+-- >>> lowerL f64f32 pi+-- 3.1415927+--+lowerL :: ConnL a b -> a -> b+lowerL (ConnL f _) = f++-- | Map over a connection from the left.+--+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.+--+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.+--+upperL1 :: ConnL a b -> (b -> b) -> a -> a+upperL1 (ConnL f g) h a = g $ h (f a)++-- | Zip over a connection from the left.+--+upperL2 :: ConnL a b -> (b -> b -> b) -> a -> a -> a+upperL2 (ConnL f g) h a1 a2 = g $ h (f a1) (f a2)++---------------------------------------------------------------------+-- ConnR+---------------------------------------------------------------------++-- | A Galois connection between two monotone functions.+--+-- 'ConnR' is the mirror image of 'ConnL':+--+-- > swapR :: ConnL a b -> ConnR b a+--+-- If you only require one connection there is no particular reason to+-- use one version over the other.+--+-- However some use cases (e.g. rounding) require an adjoint triple+-- of connections (i.e. a 'Trip') 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+{-# COMPLETE ConnR #-}++-- | Convert an arbitrary 'Conn' to an inverted 'ConnR'.+--+-- >>> counitR (downR $ conn @_ @() @Ordering) (Down LT)+-- Down GT+-- >>> counitR (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)++-- | 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++-- | Round trip through a connection.+--+-- > unitR c = upperR1 c id = upperR c . embed c+-- > x <= unitR c x+--+-- >>> unitR (conn @_ @() @Ordering) LT+-- GT+-- >>> unitR (conn @_ @() @Ordering) GT+-- GT+--+unitR :: ConnR a b -> b -> b+unitR c = upperR1 c id++-- | Reverse round trip through a connection.+--+-- > x >= counitR c x+--+-- >>> compare pi $ counitR f64f32 pi+-- GT+--+counitR :: ConnR a b -> a -> a+counitR c = lowerR1 c id++-- | Extract the upper half of a connection.+--+-- When /a/ and /b/ are lattices we have:+--+-- > upperR c (x1 /\ x2) = upperR c x1 /\ upperR c x2+--+-- This is the adjoint functor theorem for preorders.+--+-- >>> upperR f64f32 pi+-- 3.1415925+-- >>> lowerL f64f32 pi+-- 3.1415927+--+upperR :: ConnR a b -> a -> b+upperR (ConnR _ g) = g++-- | Map over a connection from the left.+--+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.+--+upperR2 :: ConnR a b -> (a -> a -> a) -> b -> b -> b+upperR2 (ConnR f g) h b1 b2 = g $ h (f b1) (f b2)++-- | 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)++-- | 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)++---------------------------------------------------------------------+-- Connections+---------------------------------------------------------------------++-- | 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')++-- | 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)

@@ -0,0 +1,322 @@+{-# 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,173 +1,216 @@+{-# Language ConstraintKinds #-}+{-# Language Safe            #-} module Data.Connection.Float (-  -- * Float+  -- * Connections     f32i08   , f32i16-  , f32i32-  , i32f32-  -- * Double-  --, f64f32-  , f64i08-  , f64i16-  , f64i32-  , f64i64-  , i64f64+  --, f32i32+  , min32+  , max32+  , covers+  , ulp+  , shift+  , within+  , epsilon ) where -import Data.Connection-import Data.Float-import Data.Int-import Data.Prd-import Data.Prd.Nan-import Data.Semifield-import Data.Semilattice-import Data.Semilattice.Top-import Data.Semiring-import GHC.Real hiding ((^),(/))-import Prelude as P hiding (Ord(..), Num(..), Fractional(..), (^), Bounded)---- | All 'Int08' values are exactly representable in a 'Float'.-f32i08 :: Trip Float (Extended Int8)-f32i08 = Trip (liftNan f) (nan' g) (liftNan h) where-  f x | x > imax = Just Top-      | x =~ ninf = Nothing-      | x < imin = fin bottom-      | otherwise = fin $ P.ceiling x--  g = bounded ninf P.fromIntegral pinf--  h x | x =~ pinf = Just Top-      | x > imax = fin top-      | x < imin = Nothing-      | otherwise = fin $ P.floor x+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+import safe Data.Word+import safe GHC.Float as F+import safe Prelude hiding (Eq(..), Ord(..), until)+import safe qualified Prelude as P  -  imax = 127 +---------------------------------------------------------------------+-- Float+--------------------------------------------------------------------- -  imin = -128+-- | A /NaN/-handling min32 function.+--+-- > 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 --- | All 'Int16' values are exactly representable in a 'Float'.-f32i16 :: Trip Float (Extended Int16)-f32i16 = Trip (liftNan f) (nan' g) (liftNan h) where-  f x | x > imax = Just Top-      | x =~ ninf = Nothing-      | x < imin = fin bottom-      | otherwise = fin $ P.ceiling 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 -  g = bounded ninf P.fromIntegral pinf+-- | 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 -  h x | x =~ pinf = Just Top-      | x > imax = fin top-      | x < imin = Nothing-      | otherwise = fin $ P.floor x+-- | Compute the signed distance between two floats in units of least precision.+--+-- >>> ulp 1.0 (shift 1 1.0)+-- Just (LT,1)+-- >>> ulp (0.0/0.0) 1.0+-- Nothing+--+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') -  imax = 32767 +-- | Shift a float 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 :: Int32 -> Float -> Float+shift n x | x ~~ 0/0 = x+          | otherwise = int32Float . clamp32 . (+ n) . floatInt32 $ x -  imin = -32768+-- | 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 --- | Exact embedding up to the largest representable 'Int32'.-f32i32 :: Conn Float (Nan Int32)-f32i32 = Conn (liftNan f) (nan' g) where-  f x | abs x <= 2**24-1 = P.ceiling x-      | otherwise = if x >= 0 then 2^24 else minimal+-- | Difference between 1 and the smallest representable value greater than 1.+--+-- > epsilon = shift 1 1 - 1+--+-- >>> epsilon+-- 1.1920929e-7+--+epsilon :: Float+epsilon = shift 1 1.0 - 1.0 -  g i | abs' i <= 2^24-1 = fromIntegral i-      | otherwise = if i >= 0 then 1/0 else -2**24+{-+-- | Minimal32 positive value.+--+-- >>> minimal32+-- 1.0e-45+-- >>> shift (-1) minimal32+-- 0+--+minimal32 :: Float+minimal32 = shift 1 0.0 --- | Exact embedding up to the largest representable 'Int32'.-i32f32 :: Conn (Nan Int32) Float-i32f32 = Conn (nan' g) (liftNan f) where-  f x | abs x <= 2**24-1 = P.floor x-      | otherwise = if x >= 0 then maximal else -2^24+-- | Maximum finite value.+--+-- >>> maximal32+-- 3.4028235e38+-- >>> shift 1 maximal32+-- Infinity+-- >>> shift (-1) $ negate maximal32+-- -Infinity+--+maximal32 :: Float+maximal32 = shift (-1) (1/0)  -  g i | abs i <= 2^24-1 = fromIntegral i-      | otherwise = if i >= 0 then 2**24 else -1/0+-}  ------------------------------------------------------------------------ Double+-- Float --------------------------------------------------------------------- +-- | All 'Data.Int.Int08' values are exactly representable in a 'Float'.+f32i08 :: Conn k Float (Extended Int8)+f32i08 = signedTriple 127 --- | All 'Int8' values are exactly representable in a 'Double'.-f64i08 :: Trip Double (Extended Int8)-f64i08 = Trip (liftNan f) (nan' g) (liftNan h) where-  f x | x > imax = Just Top-      | x =~ ninf = Nothing-      | x < imin = fin bottom-      | otherwise = fin $ P.ceiling x+-- | All 'Data.Int.Int16' values are exactly representable in a 'Float'.+f32i16 :: Conn k Float (Extended Int16)+f32i16 = signedTriple 32767 -  g = bounded ninf P.fromIntegral pinf+{-+-- | Exact embedding up to the largest representable 'Int32'.+f32i32 :: ConnL Float (Maybe Int32)+f32i32 = Conn (nanf f) (nan g) where+  f x | abs x <~ 2**24-1 = P.ceiling x+      | otherwise = if x >~ 0 then 2^24 else minBound -  h x | x =~ pinf = Just Top-      | x > imax = fin top-      | x < imin = Nothing-      | otherwise = fin $ P.floor x+  g i | abs' i <~ 2^24-1 = fromIntegral i+      | otherwise = if i >~ 0 then 1/0 else -2**24 -  imax = 127  -  imin = -128---- | All 'Int16' values are exactly representable in a 'Double'.-f64i16 :: Trip Double (Extended Int16)-f64i16 = Trip (liftNan f) (nan' g) (liftNan h) where-  f x | x > imax = Just Top-      | x =~ ninf = Nothing-      | x < imin = fin bottom-      | otherwise = fin $ P.ceiling x--  g = bounded ninf P.fromIntegral pinf+-- | Exact embedding up to the largest representable 'Int32'.+i32f32 :: ConnL (Maybe Int32) Float+i32f32 = Conn (nan g) (nanf f) where+  f x | abs x <~ 2**24-1 = P.floor x+      | otherwise = if x >~ 0 then maxBound else -2^24 -  h x | x =~ pinf = Just Top-      | x > imax = fin top-      | x < imin = Nothing-      | otherwise = fin $ P.floor x+  g i | abs i <~ 2^24-1 = fromIntegral i+      | otherwise = if i >~ 0 then 2**24 else -1/0+-} -  imax = 32767 +---------------------------------------------------------------------+-- Internal+--------------------------------------------------------------------- -  imin = -32768+signedTriple :: (Bounded a, Integral a) => Float -> Conn k Float (Extended a)+signedTriple high = Conn f g h where --- | All 'Int32' values are exactly representable in a 'Double'.-f64i32 :: Trip Double (Extended Int32)-f64i32 = Trip (liftNan f) (nan' g) (liftNan h) where-  f x | x > imax = Just Top-      | x =~ ninf = Nothing-      | x < imin = fin bottom-      | otherwise = fin $ P.ceiling x+  f = liftExtended (~~ -1/0) (\x -> x ~~ 0/0 || x > high) $ \x -> if x < low then minBound else P.ceiling x -  g = bounded ninf P.fromIntegral pinf+  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 -  h x | x =~ pinf = Just Top-      | x > imax = fin top-      | x < imin = Nothing-      | otherwise = fin $ P.floor x+  low = -1 - high -  imax = 2147483647 +-- Non-monotonic function +signed32 :: Word32 -> Int32+signed32 x | x < 0x80000000 = fromIntegral x+           | otherwise      = fromIntegral (maxBound - (x - 0x80000000)) -  imin = -2147483648+-- Non-monotonic function converting from 2s-complement format.+unsigned32 :: Int32 -> Word32+unsigned32 x | x >= 0  = fromIntegral x+             | otherwise = 0x80000000 + (maxBound - (fromIntegral x)) --- | Exact embedding up to the largest representable 'Int64'.-f64i64 :: Conn Double (Nan Int64)-f64i64 = Conn (liftNan f) (nan' g) where-  f x | abs x <= 2**53-1 = P.ceiling x-      | otherwise = if x >= 0 then 2^53 else minimal+-- Clamp between the int representations of -1/0 and 1/0 +clamp32 :: Int32 -> Int32+clamp32 = P.max (-2139095041) . P.min 2139095040 -  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 (Nan Int64) Double-i64f64 = Conn (nan' g) (liftNan f) where-  f x | abs x <= 2**53-1 = P.floor x-      | otherwise = if x >= 0 then maximal else -2^53+int32Float :: Int32 -> Float+int32Float = word32Float . unsigned32 -  g i | abs i <= 2^53-1 = fromIntegral i-      | otherwise = if i >= 0 then 2**53 else -1/0+floatInt32 :: Float -> Int32+floatInt32 = signed32 . floatWord32  -abs' :: Ord a => Minimal a => Ring a => a -> a-abs' x = if x =~ minimal then abs (x+one) else abs x+-- Bit-for-bit conversion.+word32Float :: Word32 -> Float+word32Float = F.castWord32ToFloat -{- slightly broken-f32w08 :: Trip Float (Nan Word8)-f32w08 = Trip (liftNan f) (nan (0/0) g) (liftNan h) where-  h x = if x > 0 then 0 else connr w08w32 $ B.shift (floatWord32 x) (-23)-  g = word32Float . flip B.shift 23 . connl w08w32-  f x = 1 + min 254 (h x)--}+-- Bit-for-bit conversion.+floatWord32 :: Float -> Word32+floatWord32 = (+0) .  F.castFloatToWord32

@@ -1,161 +1,164 @@--- Note that in most cases the obvious implementation is not a valid--- Galois connection. For example:------ @--- i08i16  = Conn fromIntegral (fromIntegral . min 127 . max (-1208))--- @---+{-# Language ConstraintKinds #-}+{-# Language Safe            #-} module Data.Connection.Int (-    ConnInteger(..)-  , fromInteger   -- * Int8+    i08c08   , i08w08-  , i08w08'   , i08i16   , i08i32   , i08i64   , i08int   -- * Int16+  , i16c16   , i16w16-  , i16w16'   , i16i32   , i16i64   , i16int   -- * Int32+  , i32c32   , i32w32-  , i32w32'   , i32i64   , i32int   -- * Int64+  , i64c64   , i64w64-  , i64w64'   , i64int   -- * Int   , ixxwxx+  , ixxi64+  , ixxint   -- * Integer   , intnat   , natint   ) where -import Control.Category ((>>>))-import Data.Connection-import Data.Connection.Word-import Data.Int-import Data.Prd-import Data.Semilattice.Top-import Data.Word-import Numeric.Natural+import safe Control.Category ((>>>))+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 -import Prelude hiding (Num(..), (^), Bounded)-import qualified Prelude as P+i08c08 :: ConnL Int8 CChar+i08c08 = ConnL CChar $ \(CChar x) -> x -class Prd a => ConnInteger a where-  intxxx :: Conn (Bounded Integer) a+i08w08 :: Conn k Int8 Word8+i08w08 = unsigned -instance ConnInteger Int8 where-  intxxx = tripr i08int+i08int :: ConnL Int8 (Maybe Integer)+i08int = signed -instance ConnInteger Int16 where-  intxxx = tripr i16int+i16c16 :: ConnL Int16 CShort+i16c16 = ConnL CShort $ \(CShort x) -> x -instance ConnInteger Int32 where-  intxxx = tripr i32int+i16w16 :: Conn k Int16 Word16+i16w16 = unsigned -instance ConnInteger Int64 where-  intxxx = tripr i64int+i16int :: ConnL Int16 (Maybe Integer)+i16int = signed -instance ConnInteger Word8 where-  intxxx = tripr i08int >>> i08w08+i32c32 :: ConnL Int32 CInt+i32c32 = ConnL CInt $ \(CInt x) -> x -instance ConnInteger Word16 where-  intxxx = tripr i16int >>> i16w16+i32w32 :: Conn k Int32 Word32+i32w32 = unsigned -instance ConnInteger Word32 where-  intxxx = tripr i32int >>> i32w32+i32int :: ConnL Int32 (Maybe Integer)+i32int = signed -instance ConnInteger Word64 where-  intxxx = tripr i64int >>> i64w64+i64c64 :: ConnL Int64 CLong+i64c64 = ConnL CLong $ \(CLong x) -> x --- | Lawful replacement for the version in base.----fromInteger :: ConnInteger a => Integer -> a-fromInteger = connl intxxx . Just . Fin+i64w64 :: Conn k Int64 Word64+i64w64 = unsigned -unsigned :: (Bound a, Integral a, Integral b) => Conn a b-unsigned = Conn (\y -> fromIntegral (y P.+ maximal P.+ 1))-                (\x -> fromIntegral x P.- minimal) +-- | /Caution/: This assumes that 'Int' on your system is 64 bits.+ixxi64 :: Conn k Int Int64+ixxi64 = Conn fromIntegral fromIntegral fromIntegral -i08w08' :: Conn Int8 Word8-i08w08' = unsigned+i64int :: ConnL Int64 (Maybe Integer)+i64int = signed -i08w08 :: Conn Int8 Word8-i08w08 = Conn (fromIntegral . max 0) (fromIntegral . min 127)+ixxwxx :: Conn k Int Word+ixxwxx = unsigned -i08i16 :: Conn Int8 Int16-i08i16 = i08w08' >>> w08w16 >>> w16i16+-- | /Caution/: This assumes that 'Int' on your system is 64 bits.+ixxint :: ConnL Int (Maybe Integer)+ixxint = signed -i08i32 :: Conn Int8 Int32-i08i32 = i08w08' >>> w08w32 >>> w32i32+intnat :: ConnL Integer Natural+intnat = ConnL (fromIntegral . max 0) fromIntegral -i08i64 :: Conn Int8 Int64-i08i64 = i08w08' >>> w08w64 >>> w64i64+natint :: ConnL Natural (Maybe Integer)+natint = ConnL (fmap fromIntegral . fromPred (==0)) (maybe 0 $ P.fromInteger . max 0) -i08int :: Trip Int8 (Bounded Integer)-i08int = Trip (liftBottom' fromIntegral)-              (bounded' $ P.fromInteger . min 127 . max (-128))-              (liftTop' fromIntegral)+i08i16 :: ConnL Int8 Int16+i08i16 = i08w08 >>> w08w16 >>> w16i16 -i16w16' :: Conn Int16 Word16-i16w16' = unsigned+i08i32 :: ConnL Int8 Int32+i08i32 = i08w08 >>> w08w32 >>> w32i32 -i16w16 :: Conn Int16 Word16-i16w16 = Conn (fromIntegral . max 0) (fromIntegral . min 32767) +i08i64 :: ConnL Int8 Int64+i08i64 = i08w08 >>> w08w64 >>> w64i64 -i16i32 :: Conn Int16 Int32-i16i32 = i16w16' >>> w16w32 >>> w32i32+i16i32 :: ConnL Int16 Int32+i16i32 = i16w16 >>> w16w32 >>> w32i32 -i16i64 :: Conn Int16 Int64-i16i64 = i16w16' >>> w16w64 >>> w64i64+i16i64 :: ConnL Int16 Int64+i16i64 = i16w16 >>> w16w64 >>> w64i64 -i16int :: Trip Int16 (Bounded Integer)-i16int = Trip (liftBottom' fromIntegral)-              (bounded' $ P.fromInteger . min 32767 . max (-32768))-              (liftTop' fromIntegral)+i32i64 :: ConnL Int32 Int64+i32i64 = i32w32 >>> w32w64 >>> w64i64 -i32w32' :: Conn Int32 Word32-i32w32' = unsigned+---------------------------------------------------------------------+-- Internal+--------------------------------------------------------------------- -i32w32 :: Conn Int32 Word32-i32w32 = Conn (fromIntegral . max 0) (fromIntegral . min 2147483647) -i32i64 :: Conn Int32 Int64-i32i64 = i32w32' >>> w32w64 >>> w64i64+fromPred :: Alternative f => (t -> Bool) -> t -> f t+fromPred p a = a <$ guard (p a) -i32int :: Trip Int32 (Bounded Integer)-i32int = Trip (liftBottom' fromIntegral)-              (bounded' $ P.fromInteger . min 2147483647 . max (-2147483648))-              (liftTop' fromIntegral)+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 -i64w64' :: Conn Int64 Word64-i64w64' = unsigned+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) -i64w64 :: Conn Int64 Word64-i64w64 = Conn (fromIntegral . max 0) (fromIntegral . min 9223372036854775807)+{- -i64int :: Trip Int64 (Bounded Integer)-i64int = Trip (liftBottom' fromIntegral)-              (bounded' $ P.fromInteger . min 9223372036854775807 . max (-9223372036854775808))-              (liftTop' fromIntegral) -ixxwxx :: Conn Int Word-ixxwxx = unsigned+clip08 :: Integer -> Integer+clip08 = min 127 . max (-128) -intnat :: Conn Integer Natural-intnat = Conn (fromIntegral . max 0) fromIntegral+clip16 :: Integer -> Integer+clip16 = min 32767 . max (-32768) -natint :: Conn Natural (Maybe Integer)-natint = Conn f (maybe minimal g) where-  f i | i == 0 = Nothing-      | otherwise = Just $ fromIntegral i+clip32 :: Integer -> Integer+clip32 = min 2147483647 . max (-2147483648) -  g = P.fromInteger . max 0+clip64 :: Integer -> Integer+clip64 = min 9223372036854775807 . max (-9223372036854775808)++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)++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+-}++

@@ -1,88 +1,143 @@+{-# Language DataKinds #-} {-# Language TypeFamilies #-} {-# Language TypeApplications #-}+{-# Language ConstraintKinds #-}+{-# Language RankNTypes #-}++-- | Galois connections have the same properties as adjunctions defined over other categories:+--+--  \( \forall x, y : f \dashv g \Rightarrow f (x) \leq b \Leftrightarrow x \leq g (y) \)+--+--  \( \forall x, y : x \leq y \Rightarrow f (x) \leq f (y) \)+--+--  \( \forall x, y : x \leq y \Rightarrow g (x) \leq g (y) \)+--+--  \( \forall x : f \dashv g \Rightarrow x \leq g \circ f (x) \)+--+--  \( \forall x : f \dashv g \Rightarrow f \circ g (x) \leq x \)+--+--  \( \forall x : unit \circ unit (x) \sim unit (x) \)+--+--  \( \forall x : counit \circ counit (x) \sim counit (x) \)+--+--  \( \forall x : counit \circ f (x) \sim f (x) \)+--+--  \( \forall x : unit \circ g (x) \sim g (x) \)+-- module Data.Connection.Property where -import Data.Prd+import Data.Order+import Data.Order.Property import Data.Connection-import Prelude hiding (Num(..),Ord(..))--import qualified Test.Function.Idempotent as Prop-import qualified Test.Function.Invertible as Prop-import qualified Test.Function.Monotone   as Prop+import Data.Connection.Conn+import Prelude hiding (Num(..),Ord(..), floor, ceiling)  -- | \( \forall x, y : f \dashv g \Rightarrow f (x) \leq y \Leftrightarrow x \leq g (y) \) ----- A Galois connection. This is a required property.+-- A Galois connection is an adjunction of preorders. This is a required property. ---connection :: Prd a => Prd b => Conn a b -> a -> b -> Bool-connection (Conn f g) = Prop.adjoint_on (<=) (<=) f g+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 --- | \( \forall x : f \dashv g \Rightarrow x \leq g \circ f (x) \)------ This is a required property.----closed :: Prd a => Prd b => Conn a b -> a -> Bool-closed (Conn f g) = Prop.invertible_on (>=) f g+adjointL :: (Preorder a, Preorder b) => ConnL a b -> a -> b -> Bool+adjointL (ConnL f g) = adjunction (<~) (<~) f g +adjointR :: (Preorder a, Preorder b) => ConnR a b -> a -> b -> Bool+adjointR (ConnR f g) = adjunction (>~) (>~) g f+ -- | \( \forall x : f \dashv g \Rightarrow x \leq g \circ f (x) \) -- -- This is a required property. ---closed' :: Prd a => Prd b => Trip a b -> a -> Bool-closed' t x = closed (tripl t) x && kernel (tripr t) x+closed :: (Preorder a, Preorder b) => Trip a b -> a -> Bool+closed t a = closedL t a && closedR t a --- | \( \forall x : f \dashv g \Rightarrow f \circ g (x) \leq x \)------ This is a required property.----kernel :: Prd a => Prd b => Conn a b -> b -> Bool-kernel (Conn f g) = Prop.invertible_on (<=) g f+closedL :: (Preorder a, Preorder b) => ConnL a b -> a -> Bool+closedL (ConnL f g) = invertible (>~) f g +closedR :: (Preorder a, Preorder b) => ConnR a b -> a -> Bool+closedR (ConnR f g) = invertible (<~) g f+ -- | \( \forall x : f \dashv g \Rightarrow x \leq g \circ f (x) \) -- -- This is a required property. ---kernel' :: Prd a => Prd b => Trip a b -> b -> Bool-kernel' t x = closed (tripr t) x && kernel (tripl t) x+kernel :: (Preorder a, Preorder b) => Trip a b -> b -> Bool+kernel t b = kernelL t b && kernelR t b --- | \( \forall x, y : x \leq y \Rightarrow g (x) \leq g (y) \)------ This is a required property.----monotoner :: Prd a => Prd b => Conn a b -> b -> b -> Bool-monotoner (Conn _ g) = Prop.monotone_on (<=) (<=) g+kernelL :: (Preorder a, Preorder b) => ConnL a b -> b -> Bool+kernelL (ConnL f g) = invertible (<~) g f +kernelR :: (Preorder a, Preorder b) => ConnR a b -> b -> Bool+kernelR (ConnR f g) = invertible (>~) f g+ -- | \( \forall x, y : x \leq y \Rightarrow f (x) \leq f (y) \) -- -- This is a required property. ---monotonel :: Prd a => Prd b => Conn a b -> a -> a -> Bool-monotonel (Conn f _) = Prop.monotone_on (<=) (<=) f+monotonic :: (Preorder a, Preorder b) => Trip a b -> a -> a -> b -> b -> Bool+monotonic t a1 a2 b1 b2 = monotonicL t a1 a2 b1 b2 && monotonicR t a1 a2 b1 b2 --- | \( \forall x : f \dashv g \Rightarrow unit \circ unit (x) \sim unit (x) \)+monotonicR :: (Preorder a, Preorder b) => ConnR a b -> a -> a -> b -> b -> Bool+monotonicR (ConnR f g) a1 a2 b1 b2 = monotone (<~) (<~) g a1 a2 && monotone (<~) (<~) f b1 b2++monotonicL :: (Preorder a, Preorder b) => ConnL a b -> a -> a -> b -> b -> Bool+monotonicL (ConnL f g) a1 a2 b1 b2 = monotone (<~) (<~) f a1 a2 && monotone (<~) (<~) g b1 b2++-- | \( \forall x: f \dashv g \Rightarrow counit \circ f (x) \sim f (x) \wedge unit \circ g (x) \sim g (x) \) ----- This is a required property.+-- See <https://ncatlab.org/nlab/show/idempotent+adjunction> ---idempotent_unit :: Prd a => Prd b => Conn a b -> a -> Bool-idempotent_unit conn = Prop.idempotent_on (=~) $ unit conn+idempotent :: (Preorder a, Preorder b) => Trip a b -> a -> b -> Bool+idempotent t a b = idempotentL t a b && idempotentR t a b --- | \( \forall x : f \dashv g \Rightarrow counit \circ counit (x) \sim counit (x) \)+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++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++---------------------------------------------------------------------+-- Properties of general relations+---------------------------------------------------------------------++-- | \( \forall a, b: a \leq b \Rightarrow f(a) \leq f(b) \) ----- This is a required property.+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) \) ---idempotent_counit :: Prd a => Prd b => Conn a b -> b -> Bool-idempotent_counit conn = Prop.idempotent_on (=~) $ counit conn+antitone :: Rel r Bool -> Rel s Bool -> (r -> s) -> r -> r -> Bool+antitone (#) (%) f a b = a # b ==> f b % f a --- | \( \forall x: f \dashv g \Rightarrow counit \circ f (x) \sim f (x) \)+-- | \( \forall a: f a \leq b \Leftrightarrow a \leq g b \) ----- See <https://ncatlab.org/nlab/show/idempotent+adjunction>+-- For example, a monotone Galois connection is defined by @adjunction (<~) (<~)@,+-- and an antitone Galois connection is defined by @adjunction (>~) (<~)@. ---projectivel :: Prd a => Prd b => Conn a b -> a -> Bool-projectivel conn@(Conn f _) = Prop.projective_on (=~) f $ counit conn+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 --- | \( \forall x: f \dashv g \Rightarrow unit \circ g (x) \sim g (x) \)+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 \) ----- See <https://ncatlab.org/nlab/show/idempotent+adjunction>+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) \) ---projectiver :: Prd a => Prd b => Conn a b -> b -> Bool-projectiver conn@(Conn _ g) = Prop.projective_on (=~) g $ unit conn+-- > 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,292 +1,222 @@ {-# Language AllowAmbiguousTypes #-}-{-# Language FunctionalDependencies #-}+{-# Language ConstraintKinds     #-}+{-# Language Safe                #-}+module Data.Connection.Ratio (+    Ratio(..) +  , reduce+  , shiftd+  -- * Rational+  , ratf32+  , ratf64+  , rati08+  , rati16+  , rati32+  , rati64+  , ratixx+  , ratint+  -- * Positive+  , posw08+  , posw16+  , posw32+  , posw64+  , poswxx+  , posnat+) where -module Data.Connection.Ratio where+import safe Data.Connection.Conn+import safe Data.Int+import safe Data.Order+import safe Data.Order.Extended+import safe Data.Ratio+import safe Data.Word+import safe GHC.Real (Ratio(..), Rational)+import safe Numeric.Natural+import safe Prelude hiding (Ord(..), until)+import safe qualified Prelude as P+import safe qualified Data.Connection.Float as F32+import safe qualified Data.Connection.Double as F64 -import Data.Connection-import Data.Float-import Data.Int-import Data.Prd-import Data.Prd.Nan-import Data.Ratio-import Data.Semifield-import Data.Semilattice-import Data.Semilattice.Top-import Data.Semiring-import Data.Word-import GHC.Real hiding ((/), (^))-import Numeric.Natural-import Prelude hiding (until, Ord(..), Num(..), Fractional(..), (^), Bounded)-import qualified Control.Category as C-import qualified Prelude as P+-- | 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 -reduce :: Integral a => a -> 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.+--+shiftd :: Num a => a -> Ratio a -> Ratio a+shiftd n (x :% y) = (n + x) :% y --- x % y = reduce (x * signum y) (abs y)-cancel :: Prd a => (Additive-Group) a => Ratio a -> Ratio a-cancel (x :% y) = if x < zero && y < zero then (pabs x) :% (pabs y) else x :% y+---------------------------------------------------------------------+-- Rational+--------------------------------------------------------------------- --- TODO replace w/ Yoneda / Index / Graded--- shift by n 'units of least precision' where the ULP is--- determined by the denominator-shiftd :: (Additive-Semigroup) a => a -> Ratio a -> Ratio a-shiftd n (x :% y) = (n + x) :% y+rati08 :: Conn k Rational (Extended Int8)+rati08 = signedTriple 127 -class (Prd (Ratio a), Prd b) => TripRatio a b | b -> a where-  ratxxx :: Trip (Ratio a) b+rati16 :: Conn k Rational (Extended Int16)+rati16 = signedTriple 32767 --- | Lawful replacement for the version in base.------ >>> fromRational @Float 1.3--- 1.3000001--- >>> fromRational @Float (1/0)--- Infinity--- >>> fromRational @Float (0/0)--- NaN------ >>> fromRational @(Extended Int8) 4.9--- Def (fin 5)--- >>> fromRational @(Extended Int8) (-1.2)--- Def (fin (-1))--- >>> fromRational @(Extended Int8) (1/0)--- Def Just Top--- >>> fromRational @(Extended Int8) (0/0)--- Nan--- >>> fromRational @(Extended Int8) (-1/0)--- Def Nothing----fromRational :: TripRatio a b => Ratio a -> b-fromRational = connl . tripl $ ratxxx+rati32 :: Conn k Rational (Extended Int32)+rati32 = signedTriple 2147483647 -ratf32 :: Trip (Ratio Integer) Float-ratf32 = Trip (extend' f) (extend' g) (extend' h) where+rati64 :: Conn k Rational (Extended Int64)+rati64 = signedTriple 9223372036854775807++ratixx :: Conn k Rational (Extended Int)+ratixx = signedTriple 9223372036854775807++ratint :: Conn k Rational (Extended Integer)+ratint = Conn f g h where+  +  f = liftExtended (~~ ninf) (\x -> x ~~ nan || x ~~ pinf) P.ceiling++  g = extended ninf pinf P.fromIntegral++  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 extend' g est >= x+          if fromFloating g est >~ x           then est-          else ascendf est (extend' g) x+          else ascendf est (fromFloating g) x        g = flip approxRational 0     h x = let est = P.fromRational x in-          if extend' g est <= x+          if fromFloating g est <~ x           then est-          else descendf est (extend' g) x+          else descendf est (fromFloating g) x -  ascendf z g1 y = until (\x -> g1 x >= y) (<=) (shiftf 1) z+  ascendf z g1 y = F64.until (\x -> g1 x >~ y) (<~) (F32.shift 1) z -  descendf z f1 x = until (\y -> f1 y <= x) (>=) (shiftf (-1)) z+  descendf z f1 x = F64.until (\y -> f1 y <~ x) (>~) (F32.shift (-1)) z -ratf64 :: Trip (Ratio Integer) Double-ratf64 = Trip (extend' f) (extend' g) (extend' h) where+ratf64 :: Conn k Rational Double+ratf64 = Conn (toFloating f) (fromFloating g) (toFloating h) where   f x = let est = P.fromRational x in-          if extend' g est >= x+          if fromFloating g est >~ x           then est-          else ascendf est (extend' g) x+          else ascendf est (fromFloating g) x        g = flip approxRational 0     h x = let est = P.fromRational x in-          if extend' g est <= x+          if fromFloating g est <~ x           then est-          else descendf est (extend' g) x+          else descendf est (fromFloating g) x -  ascendf z g1 y = until (\x -> g1 x >= y) (<=) (shift 1) z+  ascendf z g1 y = F64.until (\x -> g1 x >~ y) (<~) (F64.shift 1) z -  descendf z f1 x = until (\y -> f1 y <= x) (>=) (shift (-1)) z+  descendf z f1 x = F64.until (\y -> f1 y <~ x) (>~) (F64.shift (-1)) z -rati08 :: Trip (Ratio Integer) (Extended Int8) -rati08 = Trip (liftNan f) (nan' g) (liftNan h) where-  f x | x > imax = Just Top-      | x =~ ninf = Nothing-      | x < imin = fin bottom-      | otherwise = fin $ P.ceiling $ cancel x+---------------------------------------------------------------------+-- Ratio Natural+--------------------------------------------------------------------- -  g = bounded ninf P.fromIntegral pinf+posw08 :: Conn k Positive (Lowered Word8) +posw08 = unsignedTriple 255 -  h x | x =~ pinf = Just Top-      | x > imax = fin top-      | x < imin = Nothing-      | otherwise = fin $ P.floor $ cancel x+posw16 :: Conn k Positive (Lowered Word16) +posw16 = unsignedTriple 65535 -  imax = 127+posw32 :: Conn k Positive (Lowered Word32) +posw32 = unsignedTriple 4294967295 -  imin = -128+posw64 :: Conn k Positive (Lowered Word64) +posw64 = unsignedTriple 18446744073709551615 -rati16 :: Trip (Ratio Integer) (Extended Int16) -rati16 = Trip (liftNan f) (nan' g) (liftNan h) where-  f x | x > imax = Just Top-      | x =~ ninf = Nothing-      | x < imin = fin bottom-      | otherwise = fin $ P.ceiling $ cancel x+poswxx :: Conn k Positive (Lowered Word) +poswxx = unsignedTriple 18446744073709551615 -  g = bounded ninf P.fromIntegral pinf+posnat :: Conn k Positive (Lowered Natural)+posnat = Conn f g h where+  +  f = liftEitherR (\x -> x ~~ nan || x ~~ pinf) P.ceiling -  h x | x =~ pinf = Just Top-      | x > imax = fin top-      | x < imin = Nothing-      | otherwise = fin $ P.floor $ cancel x+  g = either P.fromIntegral (const pinf) -  imax = 32767+  h = liftEitherR (~~ pinf) $ \x -> if x ~~ nan then 0 else P.floor x -  imin = -32768+---------------------------------------------------------------------+-- Internal+--------------------------------------------------------------------- -rati32 :: Trip (Ratio Integer) (Extended Int32) -rati32 = Trip (liftNan f) (nan' g) (liftNan h) where-  f x | x > imax = Just Top-      | x =~ ninf = Nothing-      | x < imin = fin bottom-      | otherwise = fin $ P.ceiling $ cancel x+{-+pabs :: (Lattice a, Eq a, Num a) => a -> a+pabs x = if 0 <~ x then x else negate x -  g = bounded ninf P.fromIntegral pinf+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 -  h x | x =~ pinf = Just Top-      | x > imax = fin top-      | x < imin = Nothing-      | otherwise = fin $ P.floor $ cancel x+-- | An exception-safe version of 'nanf' for rationals.+--+nanr :: Integral b => (a -> Ratio b) -> Maybe a -> Ratio b+nanr f = maybe (0 :% 0) f+-} -  imax = 2147483647 +pinf :: Num a => Ratio a+pinf = 1 :% 0 -  imin = -2147483648+ninf :: Num a => Ratio a+ninf = (-1) :% 0 -rati64 :: Trip (Ratio Integer) (Extended Int64) -rati64 = Trip (liftNan f) (nan' g) (liftNan h) where-  f x | x > imax = Just Top-      | x =~ ninf = Nothing-      | x < imin = fin bottom-      | otherwise = fin $ P.ceiling $ cancel x+nan :: Num a => Ratio a+nan = 0 :% 0 -  g = bounded ninf P.fromIntegral pinf+{-+intnat :: Conn Integer Natural+intnat = Conn (fromIntegral . max 0) fromIntegral -  h x | x =~ pinf = Just Top-      | x > imax = fin top-      | x < imin = Nothing-      | otherwise = fin $ P.floor $ cancel x- -  imax = 9223372036854775807+natint :: Conn Natural (Lifted Integer)+natint = Conn (lifts P.fromIntegral) (lifted $ P.fromInteger . max 0) -  imin = -9223372036854775808+ratpos :: Conn k Rational Positive+ratpos = Conn k f g h where+  +  f = liftExtended (~~ ninf) (\x -> x ~~ nan || x ~~ pinf) P.ceiling -ratint :: Trip (Ratio Integer) (Extended Integer)-ratint = Trip (liftNan f) (nan' g) (liftNan h) where-  f x | x =~ pinf = Just Top-      | x =~ ninf = Nothing-      | otherwise = fin $ P.ceiling $ cancel x+  g = extended minBound maxBound P.fromIntegral -  g = bounded ninf P.fromIntegral pinf+  h = liftExtended (\x -> x ~~ nan || x ~~ ninf) (~~ pinf) P.floor+-} -  h x | x =~ pinf = Just Top-      | x =~ ninf = Nothing-      | otherwise = fin $ P.floor $ cancel 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 -ratw08 :: Trip (Ratio Natural) (Lifted Word8) -ratw08 = Trip (liftNan f) (nan' g) (liftNan h) where-  f x | x > imax = Top-      | otherwise = Fin $ P.ceiling x+  g = either P.fromIntegral (const pinf) -  g = topped P.fromIntegral pinf+  h x | x ~~ nan = Left minBound+      | x ~~ pinf = Right maxBound+      | x > high = Left maxBound+      | otherwise = Left $ P.floor x -  h x | x =~ pinf = Top-      | x > imax = Fin top-      | otherwise = Fin $ P.floor x+signedTriple :: (Bounded a, Integral a) => Rational -> Conn k Rational (Extended a)+signedTriple high = Conn f g h where -  imax = 255+  f = liftExtended (~~ ninf) (\x -> x ~~ nan || x > high) $ \x -> if x < low then minBound else P.ceiling x -ratw16 :: Trip (Ratio Natural) (Lifted Word16) -ratw16 = Trip (liftNan f) (nan' g) (liftNan h) where-  f x | x > imax = Top-      | otherwise = Fin $ P.ceiling 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 -  g = topped P.fromIntegral pinf+  low = -1 - high -  h x | x =~ pinf = Top-      | x > imax = Fin top-      | otherwise = Fin $ P.floor x -  imax = 65535--ratw32 :: Trip (Ratio Natural) (Lifted Word32) -ratw32 = Trip (liftNan f) (nan' g) (liftNan h) where-  f x | x > imax = Top-      | otherwise = Fin $ P.ceiling x--  g = topped P.fromIntegral pinf--  h x | x =~ pinf = Top-      | x > imax = Fin top-      | otherwise = Fin $ P.floor x--  imax = 4294967295--ratw64 :: Trip (Ratio Natural) (Lifted Word64) -ratw64 = Trip (liftNan f) (nan' g) (liftNan h) where-  f x | x > imax = Top-      | otherwise = Fin $ P.ceiling x--  g = topped P.fromIntegral pinf--  h x | x =~ pinf = Top-      | x > imax = Fin top-      | otherwise = Fin $ P.floor x--  imax = 18446744073709551615--ratnat :: Trip (Ratio Natural) (Lifted Natural)-ratnat = Trip (liftNan f) (nan' g) (liftNan h) where-  f x | x =~ pinf = Top-      | otherwise = Fin $ P.ceiling x--  g = topped P.fromIntegral pinf--  h x | x =~ pinf = Top-      | otherwise = Fin $ P.floor x-------------------------------------------------------------------------- Instances------------------------------------------------------------------------instance TripRatio Integer Float where-  ratxxx = ratf32--instance TripRatio Integer Double where-  ratxxx = ratf64--instance TripRatio Integer (Ratio Integer) where-  ratxxx = C.id--instance TripRatio Integer (Nan Ordering) where-  ratxxx = fldord--instance TripRatio Integer (Extended Int8) where-  ratxxx = rati08--instance TripRatio Integer (Extended Int16) where-  ratxxx = rati16--instance TripRatio Integer (Extended Int32) where-  ratxxx = rati32--instance TripRatio Integer (Extended Int64) where-  ratxxx = rati64--instance TripRatio Integer (Extended Integer) where-  ratxxx = ratint--instance TripRatio Natural (Ratio Natural) where-  ratxxx = C.id--instance TripRatio Natural (Lifted Word8) where-  ratxxx = ratw08--instance TripRatio Natural (Lifted Word16) where-  ratxxx = ratw16--instance TripRatio Natural (Lifted Word32) where-  ratxxx = ratw32--instance TripRatio Natural (Lifted Word64) where-  ratxxx = ratw64+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 -instance TripRatio Natural (Lifted Natural) where-  ratxxx = ratnat+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

@@ -1,249 +0,0 @@-{-# Language AllowAmbiguousTypes #-}--module Data.Connection.Round (-  -- * Rounding Classes-    TripInt16(..) -  , ceil16-  , floor16-  , trunc16-  , round16-  , TripInt32(..)-  , ceil32-  , floor32-  , trunc32-  , round32-  -- * Rounding Utils-  , Mode(..)-  , half-  , tied-  , above-  , below-  , addWith-  , negWith-  , subWith-  , mulWith-  , fmaWith-  , remWith-  , divWith-  , divWith'-) where--import Data.Bool-import Data.Connection-import Data.Connection.Float-import Data.Connection.Ratio-import Data.Float-import Data.Int-import Data.Prd-import Data.Ratio-import Data.Semifield-import Data.Semilattice-import Data.Semilattice.Top-import Data.Semiring-import Prelude hiding (until, Ord(..), Num(..), Fractional(..), (^), Bounded)-import Test.Logic (xor)--class Prd a => TripInt16 a where-  xxxi16 :: Trip a (Extended Int16)--ceil16 :: TripInt16 a => a -> a-ceil16 = unitl xxxi16--floor16 :: TripInt16 a => a -> a-floor16 = counitr xxxi16--trunc16 :: (Additive-Monoid) a => TripInt16 a => a -> a-trunc16 x = bool (ceil16 x) (floor16 x) $ x >= zero--round16 :: (Additive-Group) a => TripInt16 a => a -> a-round16 x | above xxxi16 x = ceil16 x -- upper half interval-          | below xxxi16 x = floor16 x -- lower half interval-          | otherwise = trunc16 x--class Prd a => TripInt32 a where-  xxxi32 :: Trip a (Extended Int32)--ceil32 :: TripInt32 a => a -> a-ceil32 = unitl xxxi32--floor32 :: TripInt32 a => a -> a-floor32 = counitr xxxi32--trunc32 :: (Additive-Monoid) a => TripInt32 a => a -> a-trunc32 x = bool (ceil32 x) (floor32 x) $ x >= zero --round32 :: (Additive-Group) a => TripInt32 a => a -> a-round32 x | above xxxi32 x = ceil32 x -- upper half interval-          | below xxxi32 x = floor32 x -- lower half interval-          | otherwise = trunc32 x-------------------------------------------------------------------------- Rounding-------------------------------------------------------------------------- | The four primary IEEE rounding modes.------ See <https://en.wikipedia.org/wiki/Rounding>.----data Mode = -    RNZ -- ^ round to nearest with ties towards zero-  | RTP -- ^ round towards pos infinity-  | RTN -- ^ round towards neg infinity-  | RTZ -- ^ round towards zero-  deriving (Eq, Show)---- | Determine which half of the interval between two representations of /a/ a particular value lies.--- -half :: Prd a => Prd b => (Additive-Group) a => Trip a b -> a -> Maybe Ordering-half t x = pcompare (x - unitl t x) (counitr t x - x) ---- | Determine whether /x/ lies above the halfway point between two representations.--- --- @ 'above' t x '==' (x '-' 'unitl' t x) '`gt`' ('counitr' t x '-' x) @----above :: Prd a => Prd b => (Additive-Group) a => Trip a b -> a -> Bool-above t = maybe False (== GT) . half t---- | Determine whether /x/ lies below the halfway point between two representations.--- --- @ 'below' t x '==' (x '-' 'unitl' t x) '`lt`' ('counitr' t x '-' x) @----below :: Prd a => Prd b => (Additive-Group) a => Trip a b -> a -> Bool-below t = maybe False (== LT) . half t---- | Determine whether /x/ lies exactly halfway between two representations.--- --- @ 'tied' t x '==' (x '-' 'unitl' t x) '=~' ('counitr' t x '-' x) @----tied :: Prd a => Prd b => (Additive-Group) a => Trip a b -> a -> Bool-tied t = maybe False (== EQ) . half t---- >>> addWith ratf32 RTN 1 2--- 3.0--- minSubf-addWith :: (Prd a, Prd b, (Additive-Group) a) => Trip a b -> Mode -> b -> b -> b -addWith t@(Trip _ f _) rm x y = rnd t rm (addSgn t rm x y) (f x + f y)--negWith :: (Prd a, Prd b, (Additive-Group) a) => Trip a b -> Mode -> b -> b -negWith t@(Trip _ f _) rm x = rnd t rm (neg' t rm x) (zero - f x)--subWith :: (Prd a, Prd b, (Additive-Group) a) => Trip a b -> Mode -> b -> b -> b -subWith t@(Trip _ f _) rm x y = rnd t rm (subSgn t rm x y) (f x - f y)--mulWith :: (Prd a, Prd b, Ring a) => Trip a b -> Mode -> b -> b -> b -mulWith t@(Trip _ f _) rm x y = rnd t rm (xorSgn t rm x y) (f x * f y)--{--big = shiftf (-1) maximal-λ> fmaWith ratf32 RTN big 2 (-big)-3.4028235e38-λ> big * 2 - big-Infinity--}-fmaWith :: (Prd a, Prd b, Ring a) => Trip a b -> Mode -> b -> b -> b -> b-fmaWith t@(Trip _ f _) rm x y z = rnd t rm (fmaSgn t rm x y z) $ f x * f y + f z--{--λ> remWith @Int RTP 17 5--3-λ> remWith @Int RNZ 17 5-2--}-remWith :: (Prd a, Prd b, Field a) => Trip a b -> Mode -> b -> b -> b-remWith t rm x y = fmaWith t rm (negWith t rm $ divWith t rm x y) y x--{--λ> divWith @Int RNZ 17 5-3-λ> divWith @Int RTP 17 5-4--}--- when pos numbers are divided by −0 we return minus infinity rather than pos:--- >>> divWith C.id RNZ 1 (shiftf (-1) 0)--- -Infinity-divWith :: (Prd a, Prd b, Field a) => Trip a b -> Mode -> b -> b -> b -divWith t@(Trip _ f _) rm x y = rnd t rm (xorSgn t rm x y) (f x / f y)---- requires that sign be flipped back in /a/.-divWith' :: (Prd a, Prd b, Field a) => Trip a b -> Mode -> b -> b -> b -divWith' t@(Trip _ f _) rm x y | xorSgn t rm x y = rnd t rm True (negate $ f x / f y)-                               | otherwise  = rnd t rm False (f x / f y)-------------------------------------------------------------------------- Internal-------------------------------------------------------------------------- @ truncateWith C.id == id @-truncateWith :: (Prd a, Prd b, (Additive-Monoid) a) => Trip a b -> a -> b-truncateWith t x = bool (ceilingWith t x) (floorWith t x) $ x >= zero---- @ ceilingWith C.id == id @-ceilingWith :: Prd a => Prd b => Trip a b -> a -> b-ceilingWith = connl . tripl---- @ floorWith C.id == id @-floorWith :: Prd a => Prd b => Trip a b -> a -> b-floorWith = connr . tripr---- @ roundWith C.id == id @-roundWith :: (Prd a, Prd b, (Additive-Group) a) => Trip a b -> a -> b-roundWith t x | above t x = ceilingWith t x -- upper half interval-              | below t x = floorWith t x -- lower half interval-              | otherwise = truncateWith t x--{---rndWith :: (Prd a, Prd b, (Additive-Group) a) => Trip a b -> Mode -> b -> b -rndWith t@(Trip f g h) rm x = rnd t rm (neg' t rm x) (g x)---}---- Determine the sign of 0 when /a/ contains signed 0s-rsz :: (Prd a, Prd b) => Trip a b -> Bool -> a -> b-rsz t = bool (floorWith t) (ceilingWith t)--rnd :: (Prd a, Prd b, (Additive-Group) a) => Trip a b -> Mode -> Bool -> a -> b-rnd t RNZ s x = bool (roundWith t x) (rsz t s x) $ x =~ zero-rnd t RTP s x = bool (ceilingWith t x) (rsz t s x) $ x =~ zero-rnd t RTN s x = bool (floorWith t x) (rsz t s x) $ x =~ zero-rnd t RTZ s x = bool (truncateWith t x) (rsz t s x) $ x =~ zero--neg' :: (Prd a, Prd b, (Additive-Group) a) => Trip a b -> Mode -> b -> Bool-neg' t rm x = x < rnd t rm False zero----pos'  :: (Prd a, Prd b, (Additive-Group) a) => Trip a b -> Mode -> b -> Bool ---pos' t rm x = x > rnd t rm False zero---- | Determine signed-0 behavior under addition.-addSgn :: (Prd a, Prd b, (Additive-Group) a) => Trip a b -> Mode -> b -> b -> Bool-addSgn t rm x y | rm == RTN = neg' t rm x || neg' t rm y-                | otherwise = neg' t rm x && neg' t rm y--subSgn :: (Prd a, Prd b, (Additive-Group) a) => Trip a b -> Mode -> b -> b -> Bool-subSgn t rm x y = not (addSgn t rm x y)---- | Determine signed-0 behavior under multiplication and division.-xorSgn :: (Prd a, Prd b, (Additive-Group) a) => Trip a b -> Mode -> b -> b -> Bool-xorSgn t rm x y = neg' t rm x `xor` neg' t rm y--fmaSgn :: (Prd a, Prd b, Ring a) => Trip a b -> Mode -> b -> b -> b -> Bool-fmaSgn t rm x y z = addSgn t rm (mulWith t rm x y) z-------------------------------------------------------------------------- Instances------------------------------------------------------------------------instance TripInt16 Float where-  xxxi16 = f32i16--instance TripInt16 Double where-  xxxi16 = f64i16--instance TripInt16 (Ratio Integer) where-  xxxi16 = rati16 --instance TripInt32 Double where-  xxxi32 = f64i32--instance TripInt32 (Ratio Integer) where-  xxxi32 = rati32

@@ -1,74 +1,145 @@+{-# Language Safe                #-} module Data.Connection.Word (+  -- * Bool+    c08bin+  , binc08   -- * Word8-    w08i08+  , 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 ) where -import Data.Connection-import Data.Int-import Data.Word-import Numeric.Natural+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(..)) -signed :: (Bounded b, Integral a, Integral b) => Conn a b-signed = Conn (\x -> fromIntegral x - minBound)-              (\y -> fromIntegral (y + maxBound + 1))+c08bin :: ConnL CBool Bool+c08bin = ConnL f g where+  f (CBool i) | i == 255 = True+              | otherwise = False+  +  g True = CBool 255+  g _ = CBool 254 -w08i08 :: Conn Word8 Int8+binc08 :: ConnL Bool CBool+binc08 = ConnL f g where+  f False = CBool 0+  f _ = CBool 1++  g (CBool i) | i == 0 = False+              | otherwise = True++w08c08 :: ConnL Word8 CUChar+w08c08 = ConnL CUChar $ \(CUChar x) -> x++w08i08 :: ConnL Word8 Int8 w08i08 = signed -w08w16 :: Conn Word8 Word16-w08w16 = Conn fromIntegral (fromIntegral . min 255)+w08nat :: ConnL Word8 Natural+w08nat = unsigned +w08w16 :: ConnL Word8 Word16+w08w16 = unsigned+ -- w08w32 = w08w16 >>> w16w32-w08w32 :: Conn Word8 Word32-w08w32 = Conn fromIntegral (fromIntegral . min 255)+w08w32 :: ConnL Word8 Word32+w08w32 = unsigned  -- w08w64 = w08w32 >>> w32w64 = w08w16 >>> w16w64-w08w64 :: Conn Word8 Word64-w08w64 = Conn fromIntegral (fromIntegral . min 255)+w08w64 :: ConnL Word8 Word64+w08w64 = unsigned -w08nat :: Conn Word8 Natural-w08nat = Conn fromIntegral (fromIntegral . min 255)+w08wxx :: ConnL Word8 Word+w08wxx = unsigned -w16i16 :: Conn Word16 Int16+w16c16 :: ConnL Word16 CUShort+w16c16 = ConnL CUShort $ \(CUShort x) -> x++w16i16 :: ConnL Word16 Int16 w16i16 = signed -w16w32 :: Conn Word16 Word32-w16w32 = Conn fromIntegral (fromIntegral . min 65535)+w16w32 :: ConnL Word16 Word32+w16w32 = unsigned  -- w16w64 = w16w32 >>> w32w64-w16w64 :: Conn Word16 Word64-w16w64 = Conn fromIntegral (fromIntegral . min 65535)+w16w64 :: ConnL Word16 Word64+w16w64 = unsigned -w16nat :: Conn Word16 Natural-w16nat = Conn fromIntegral (fromIntegral . min 65535)+w16wxx :: ConnL Word16 Word+w16wxx = unsigned -w32i32 :: Conn Word32 Int32+w16nat :: ConnL Word16 Natural+w16nat = unsigned++w32c32 :: ConnL Word32 CUInt+w32c32 = ConnL CUInt $ \(CUInt x) -> x++w32i32 :: ConnL Word32 Int32 w32i32 = signed -w32w64 :: Conn Word32 Word64-w32w64 = Conn fromIntegral (fromIntegral . min 4294967295)+w32w64 :: ConnL Word32 Word64+w32w64 = unsigned -w32nat :: Conn Word32 Natural-w32nat = Conn fromIntegral (fromIntegral . min 4294967295)+w32wxx :: ConnL Word32 Word+w32wxx = unsigned -w64i64 :: Conn Word64 Int64+w32nat :: ConnL Word32 Natural+w32nat = unsigned++w64c64 :: ConnL Word64 CULong+w64c64 = ConnL CULong $ \(CULong x) -> x++w64i64 :: ConnL Word64 Int64 w64i64 = signed -w64nat :: Conn Word64 Natural-w64nat = Conn fromIntegral (fromIntegral . min 18446744073709551615)+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)++---------------------------------------------------------------------+-- 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)

@@ -1,875 +0,0 @@-{-# LANGUAGE CPP, ForeignFunctionInterface #-}-{-# LANGUAGE FlexibleContexts #-}-module Data.Float (-    Float-  , Double-  , module Data.Float-) where--import Data.Bits ((.&.))-import Data.Connection -import Data.Function (on)-import Data.Int-import Data.Prd-import Data.Semifield-import Data.Semigroup.Join-import Data.Semigroup.Meet-import Data.Semiring-import Data.Word-import Foreign hiding (shift)-import Foreign.C-import GHC.Float as F-import Prelude (Double,realToFrac,fromIntegral,($),return,IO)-import Prelude hiding (Ord(..), Num(..), Fractional(..), Floating(..),  (^^), (^), RealFloat(..), Real(..), Enum(..))-import System.IO.Unsafe (unsafePerformIO)-import qualified Prelude as P---{-# LINE 28 "Foreign/C/Math/Double.hsc" #-}----- | The acos function computes the principal value of the arc cosine of x--- in the range [0, pi]----acos :: Double -> Double-acos x = realToFrac (c_acos (realToFrac x))-{-# INLINE acos #-}--foreign import ccall unsafe "math.h acos"-     c_acos     :: CDouble -> CDouble---- | The asin function computes the principal value of the arc sine of x in--- the range [-pi/2, +pi/2].----asin :: Double -> Double-asin x = realToFrac (c_asin (realToFrac x))-{-# INLINE asin #-}--foreign import ccall unsafe "math.h asin"-     c_asin     :: CDouble -> CDouble---- | The atan function computes the principal value of the arc tangent of x--- in the range [-pi/2, +pi/2].----atan :: Double -> Double-atan x = realToFrac (c_atan (realToFrac x))-{-# INLINE atan #-}--foreign import ccall unsafe "math.h atan"-     c_atan     :: CDouble -> CDouble---- | The atan2 function computes the principal value of the arc tangent of--- y/x, using the signs of both arguments to determine the quadrant of the--- return value.----atan2 :: Double -> Double -> Double-atan2 x y = realToFrac (c_atan2 (realToFrac x) (realToFrac y))-{-# INLINE atan2 #-}--foreign import ccall unsafe "math.h atan2"-     c_atan2    :: CDouble -> CDouble -> CDouble---- | The cos function computes the cosine of x (measured in radians).--- A large magnitude argument may yield a result with little or no significance.  For a--- discussion of error due to roundoff, see math(3).----cos :: Double -> Double-cos x = realToFrac (c_cos (realToFrac x))-{-# INLINE cos #-}--foreign import ccall unsafe "math.h cos"-     c_cos      :: CDouble -> CDouble---- | The sin function computes the sine of x (measured in radians). --- A large magnitude argument may yield a result with little or no--- significance.  For a discussion of error due to roundoff, see math(3).----sin :: Double -> Double-sin x = realToFrac (c_sin (realToFrac x))-{-# INLINE sin #-}--foreign import ccall unsafe "math.h sin"-     c_sin      :: CDouble -> CDouble---- | The tan function computes the tangent of x (measured in radians). --- A large magnitude argument may yield a result with little or no--- significance.  For a discussion of error due to roundoff, see math(3).----tan :: Double -> Double-tan x = realToFrac (c_tan (realToFrac x))-{-# INLINE tan #-}--foreign import ccall unsafe "math.h tan"-     c_tan      :: CDouble -> CDouble---- | The cosh function computes the hyperbolic cosine of x.----cosh :: Double -> Double-cosh x = realToFrac (c_cosh (realToFrac x))-{-# INLINE cosh #-}--foreign import ccall unsafe "math.h cosh"-     c_cosh     :: CDouble -> CDouble---- | The sinh function computes the hyperbolic sine of x.----sinh :: Double -> Double-sinh x = realToFrac (c_sinh (realToFrac x))-{-# INLINE sinh #-}--foreign import ccall unsafe "math.h sinh"-     c_sinh     :: CDouble -> CDouble---- | The tanh function computes the hyperbolic tangent of x.----tanh :: Double -> Double-tanh x = realToFrac (c_tanh (realToFrac x))-{-# INLINE tanh #-}--foreign import ccall unsafe "math.h tanh"-     c_tanh     :: CDouble -> CDouble------------------------------------------------------------------------------ | The exp() function computes the exponential value of the given argument x. ----exp :: Double -> Double-exp x = realToFrac (c_exp (realToFrac x))-{-# INLINE exp  #-}--foreign import ccall unsafe "math.h exp"-     c_exp      :: CDouble -> CDouble---- | frexp convert floating-point number to fractional and integral components--- frexp is not defined in the Haskell 98 report.----frexp :: Double -> (Double,Int)-frexp x = unsafePerformIO $-    alloca $ \p -> do-        d <- c_frexp (realToFrac x) p-        i <- peek p-        return (realToFrac d, fromIntegral i)--foreign import ccall unsafe "math.h frexp"-     c_frexp    :: CDouble -> Ptr CInt -> IO Double---- | The ldexp function multiplies a floating-point number by an integral power of 2.--- ldexp is not defined in the Haskell 98 report.----ldexp :: Double -> Int -> Double-ldexp x i = realToFrac (c_ldexp (realToFrac x) (fromIntegral i))-{-# INLINE ldexp #-}--foreign import ccall unsafe "math.h ldexp"-     c_ldexp    :: CDouble -> CInt -> Double---- | The log() function computes the value of the natural logarithm of argument x.----log :: Double -> Double-log x = realToFrac (c_log (realToFrac x))-{-# INLINE log  #-}--foreign import ccall unsafe "math.h log"-     c_log      :: CDouble -> CDouble---- | The log10 function computes the value of the logarithm of argument x to base 10.--- log10 is not defined in the Haskell 98 report.-log10 :: Double -> Double-log10 x = realToFrac (c_log10 (realToFrac x))-{-# INLINE log10 #-}--foreign import ccall unsafe "math.h log10"-     c_log10    :: CDouble -> CDouble---- | The modf function breaks the argument value into integral and fractional--- parts, each of which has the same sign as the argument.--- modf is not defined in the Haskell 98 report.----modf :: Double -> (Double,Double)-modf x = unsafePerformIO $-    alloca $ \p -> do-        d <- c_modf (realToFrac x) p-        i <- peek p-        return (realToFrac d, realToFrac i)--foreign import ccall unsafe "math.h modf"-     c_modf     :: CDouble -> Ptr CDouble -> IO CDouble---- | The pow function computes the value of x to the exponent y.----pow :: Double -> Double -> Double-pow x y = realToFrac (c_pow (realToFrac x) (realToFrac y))-{-# INLINE pow #-}--foreign import ccall unsafe "math.h pow"-     c_pow      :: CDouble -> CDouble -> CDouble---- | The sqrt function computes the non-negative square root of x.----sqrt :: Double -> Double-sqrt x = realToFrac (c_sqrt (realToFrac x))-{-# INLINE sqrt #-}--foreign import ccall unsafe "math.h sqrt"-     c_sqrt     :: CDouble -> CDouble---- | The ceil function returns the smallest integral value greater than or equal to x.----ceil :: Double -> Double-ceil x = realToFrac (c_ceil (realToFrac x))-{-# INLINE ceil #-}--foreign import ccall unsafe "math.h ceil"-     c_ceil     :: CDouble -> CDouble---- | The fabs function computes the absolute value of a floating-point number x.----fabs :: Double -> Double-fabs x = realToFrac (c_fabs (realToFrac x))-{-# INLINE fabs #-}--foreign import ccall unsafe "math.h fabs"-     c_fabs     :: CDouble -> CDouble---- | The floor function returns the largest integral value less than or equal to x.----floor :: Double -> Double-floor x = realToFrac (c_floor (realToFrac x))-{-# INLINE floor #-}--foreign import ccall unsafe "math.h floor"-     c_floor    :: CDouble -> CDouble---- | The fmod function computes the floating-point remainder of x \/ y.----fmod :: Double -> Double -> Double-fmod x y = realToFrac (c_fmod (realToFrac x) (realToFrac y))-{-# INLINE fmod #-}--foreign import ccall unsafe "math.h fmod"-     c_fmod     :: CDouble -> CDouble -> CDouble---- | The round function returns the nearest integral value to x; if x lies--- halfway between two integral values, then these functions return the integral--- value with the larger absolute value (i.e., it rounds away from zero).--- -round :: Double -> Double-round x = realToFrac (c_round (realToFrac x))-{-# INLINE round #-}--foreign import ccall unsafe "math.h round"-     c_round    :: CDouble -> CDouble---- | The fmod function computes the floating-point remainder of x \/ y.----trunc :: Double -> Double-trunc x = realToFrac (c_trunc (realToFrac x))-{-# INLINE trunc #-}--foreign import ccall unsafe "math.h trunc"-     c_trunc    :: CDouble -> CDouble---- | The erf calculates the error function of x. The error function is defined as:------ > erf(x) = 2/sqrt(pi)*integral from 0 to x of exp(-t*t) dt.----erf :: Double -> Double-erf x = realToFrac (c_erf (realToFrac x))-{-# INLINE erf #-}--foreign import ccall unsafe "math.h erf"-     c_erf      :: CDouble -> CDouble---- | The erfc function calculates the complementary error function of x;--- that is erfc() subtracts the result of the error function erf(x) from--- 1.0.  This is useful, since for large x places disappear.----erfc :: Double -> Double-erfc x = realToFrac (c_erfc (realToFrac x))-{-# INLINE erfc #-}--foreign import ccall unsafe "math.h erfc"-     c_erfc     :: CDouble -> CDouble---- | The gamma function.----gamma :: Double -> Double-gamma x = realToFrac (c_gamma (realToFrac x))-{-# INLINE gamma #-}--foreign import ccall unsafe "math.h gamma"-     c_gamma    :: CDouble -> CDouble---- | The hypot function function computes the sqrt(x*x+y*y) in such a way that--- underflow will not happen, and overflow occurs only if the final result--- deserves it.  --- --- > hypot(Infinity, v) = hypot(v, Infinity) = +Infinity for all v, including NaN.----hypot :: Double -> Double -> Double-hypot x y = realToFrac (c_hypot (realToFrac x) (realToFrac y))-{-# INLINE hypot #-}--foreign import ccall unsafe "math.h hypot"-     c_hypot    :: CDouble -> CDouble -> CDouble---- | The isinf function returns 1 if the number n is Infinity, otherwise 0.----isinf :: Double -> Int-isinf x = fromIntegral (c_isinf (realToFrac x))-{-# INLINE isinf #-}--foreign import ccall unsafe "math.h isinf"-     c_isinf    :: CDouble -> CInt---- | The isnan function returns 1 if the number n is ``not-a-number'',--- otherwise 0.----isnan :: Double -> Int-isnan x = fromIntegral (c_isnan (realToFrac x))-{-# INLINE isnan #-}--foreign import ccall unsafe "math.h isnan"-     c_isnan    :: CDouble -> CInt---- | finite returns the value 1 just when -Infinity < x < +Infinity; otherwise--- a zero is returned (when |x| = Infinity or x is NaN.----finite :: Double -> Int-finite x = fromIntegral (c_finite (realToFrac x))-{-# INLINE finite #-}--foreign import ccall unsafe "math.h finite"-     c_finite    :: CDouble -> CInt---- | The functions j0() and j1() compute the Bessel function of the--- first kind of the order 0 and the order 1, respectively, for the real--- value x----j0 :: Double -> Double-j0 x = realToFrac (c_j0 (realToFrac x))-{-# INLINE j0 #-}--foreign import ccall unsafe "math.h j0"-     c_j0    :: CDouble -> CDouble---- | The functions j0() and j1() compute the Bessel function of the--- first kind of the order 0 and the order 1, respectively, for the real--- value x----j1 :: Double -> Double-j1 x = realToFrac (c_j1 (realToFrac x))-{-# INLINE j1 #-}--foreign import ccall unsafe "math.h j1"-     c_j1    :: CDouble -> CDouble---- | The functions y0() and y1() compute the linearly independent Bessel--- function of the second kind of the order 0 and the order 1,--- respectively, for the positive integer value x (expressed as a double)----y0 :: Double -> Double-y0 x = realToFrac (c_y0 (realToFrac x))-{-# INLINE y0 #-}--foreign import ccall unsafe "math.h y0"-     c_y0    :: CDouble -> CDouble---- | The functions y0() and y1() compute the linearly independent Bessel--- function of the second kind of the order 0 and the order 1,--- respectively, for the positive integer value x (expressed as a double)----y1 :: Double -> Double-y1 x = realToFrac (c_y1 (realToFrac x))-{-# INLINE y1 #-}--foreign import ccall unsafe "math.h y1"-     c_y1    :: CDouble -> CDouble---- | yn() computes the Bessel function of the second kind for the--- integer Bessel0 n for the positive integer value x (expressed as a--- double).----yn :: Int -> Double -> Double-yn x y = realToFrac (c_yn (fromIntegral x) (realToFrac y))-{-# INLINE yn #-}--foreign import ccall unsafe "math.h yn"-     c_yn    :: CInt -> CDouble -> CDouble---- | lgamma(x) returns ln|| (x)|.----lgamma :: Double -> Double-lgamma x = realToFrac (c_lgamma (realToFrac x))-{-# INLINE lgamma #-}--foreign import ccall unsafe "math.h lgamma"-     c_lgamma    :: CDouble -> CDouble----- | The acosh function computes the inverse hyperbolic cosine of the real argument x. ----acosh :: Double -> Double-acosh x = realToFrac (c_acosh (realToFrac x))-{-# INLINE acosh #-}--foreign import ccall unsafe "math.h acosh"-     c_acosh    :: CDouble -> CDouble---- | The asinh function computes the inverse hyperbolic sine of the real argument. ----asinh :: Double -> Double-asinh x = realToFrac (c_asinh (realToFrac x))-{-# INLINE asinh #-}--foreign import ccall unsafe "math.h asinh"-     c_asinh    :: CDouble -> CDouble---- | The atanh function computes the inverse hyperbolic tangent of the real argument x.----atanh :: Double -> Double-atanh x = realToFrac (c_atanh (realToFrac x))-{-# INLINE atanh #-}--foreign import ccall unsafe "math.h atanh"-     c_atanh    :: CDouble -> CDouble---- | The cbrt function computes the cube root of x.----cbrt :: Double -> Double-cbrt x = realToFrac (c_cbrt (realToFrac x))-{-# INLINE cbrt #-}--foreign import ccall unsafe "math.h cbrt"-     c_cbrt    :: CDouble -> CDouble---- | logb x returns x's exponent n, a signed integer converted to--- double-precision floating-point.  --- --- > logb(+-Infinity) = +Infinity;--- > logb(0) = -Infinity with a division by zero exception.----logb :: Double -> Double-logb x = realToFrac (c_logb (realToFrac x))-{-# INLINE logb #-}--foreign import ccall unsafe "math.h logb"-     c_logb    :: CDouble -> CDouble----- | nextafter returns the next machine representable number from x in direction y.----nextafter :: Double -> Double -> Double-nextafter x y = realToFrac (c_nextafter (realToFrac x) (realToFrac y))-{-# INLINE nextafter #-}--foreign import ccall unsafe "math.h nextafter"-     c_nextafter    :: CDouble -> CDouble -> CDouble---- | remainder returns the remainder r := x - n*y where n is the integer--- nearest the exact value of x/y; moreover if |n - x/y| = 1/2 then n is even.--- Consequently, the remainder is computed exactly and |r| <= |y|/2.  But--- remainder(x, 0) and remainder(Infinity, 0) are invalid operations that produce--- a NaN.  ---remainder :: Double -> Double -> Double-remainder x y = realToFrac (c_remainder (realToFrac x) (realToFrac y))-{-# INLINE remainder #-}--foreign import ccall unsafe "math.h remainder"-     c_remainder    :: CDouble -> CDouble -> CDouble---- | scalb(x, n) returns x*(2**n) computed by exponent manipulation.-scalb :: Double -> Double -> Double-scalb x y = realToFrac (c_scalb (realToFrac x) (realToFrac y))-{-# INLINE scalb #-}--foreign import ccall unsafe "math.h scalb"-     c_scalb    :: CDouble -> CDouble -> CDouble---- | significand(x) returns sig, where x := sig * 2**n with 1 <= sig < 2.--- significand(x) is not defined when x is 0, +-Infinity, or NaN.----significand :: Double -> Double-significand x = realToFrac (c_significand (realToFrac x))-{-# INLINE significand #-}--foreign import ccall unsafe "math.h significand"-     c_significand    :: CDouble -> CDouble----- |  copysign x y returns x with its sign changed to y's.-copysign :: Double -> Double -> Double-copysign x y = realToFrac (c_copysign (realToFrac x) (realToFrac y))-{-# INLINE copysign #-}--foreign import ccall unsafe "math.h copysign"-     c_copysign    :: CDouble -> CDouble -> CDouble---- | ilogb() returns x's exponent n, in integer format.---    ilogb(+-Infinity) re- turns INT_MAX and ilogb(0) returns INT_MIN.----ilogb :: Double -> Int-ilogb x = fromIntegral (c_ilogb (realToFrac x))-{-# INLINE ilogb #-}--foreign import ccall unsafe "math.h ilogb"-     c_ilogb    :: CDouble -> CInt---- | The rint() function returns the integral value (represented as a--- double precision number) nearest to x according to the prevailing--- rounding mode.----rint :: Double -> Double-rint x = realToFrac (c_rint (realToFrac x))-{-# INLINE rint #-}--foreign import ccall unsafe "math.h rint"-     c_rint    :: CDouble -> CDouble----- | Determine bitwise equality.----eq :: Double -> Double -> Bool-eq = (==) `on` doubleWord64--eqf :: Float -> Float -> Bool-eqf = (==) `on` floatWord32---- | Maximum finite value.------ >>> shift 1 maxNorm--- Infinity--- -maxNorm :: Double-maxNorm = shift (-1) maximal --maxNormf :: Float-maxNormf = shiftf (-1) maximal ---- | Minimum normalized value.------ >>> shift (-1) minNorm--- 0--- -minNorm :: Double-minNorm = word64Double 0x0080000000000000--minNormf :: Float-minNormf = word32Float 0x00800000---- | Maximum representable odd integer. ------ @ maxOdd = 2**53 - 1@----maxOdd :: Double-maxOdd = 9.007199254740991e15---- | Maximum representable odd integer. ------ @ maxOddf = 2**24 - 1@----maxOddf :: Float-maxOddf = 1.6777215e7---- | Minimum (pos) value.------ >>> shift (-1) minSub--- 0.0--- -minSub :: Double-minSub = shift 1 0--minSubf :: Float-minSubf = shiftf 1 0---- | Difference between 1 and the smallest representable value greater than 1.-epsilon :: Double-epsilon = shift 1 1 - 1--epsilonf :: Float-epsilonf = shiftf 1 1 - 1---- | Split a 'Double' symmetrically along the sign bit.------ >>> split 0--- Right 0.0--- >>> split (shift (-1) 0)--- Left (-0.0)--- -split :: Double -> Either Double Double-split x = case signBit x of-  True -> Left x-  _    -> Right x--splitf :: Float -> Either Float Float-splitf x = case signBitf x of-  True -> Left x-  _    -> Right x----- TODO replace w/ Yoneda / Index / Graded--- | Shift by /Int64/ units of least precision.----shift :: Int64 -> Double -> Double-shift n = int64Double . (+ n) . doubleInt64--shiftf :: Int32 -> Float -> Float-shiftf n = int32Float . (+ n) . floatInt32---- | Compute signed distance in units of least precision.------ @ 'ulps' x ('shift' ('abs' n) x) '==' ('True', 'abs' n) @----ulps :: Double -> Double -> (Bool, Word64)-ulps x y = o-  where  x' = doubleInt64 x-         y' = doubleInt64 y-         o  | x' >= y' = (False, fromIntegral . abs $ x' - y')-            | otherwise = (True, fromIntegral . abs $ y' - x')--ulpsf :: Float -> Float -> (Bool, Word32)-ulpsf x y = o-  where  x' = floatInt32 x-         y' = floatInt32 y-         o  | x' >= y' = (False, fromIntegral . abs $ x' - y')-            | otherwise = (True, fromIntegral . abs $ y' - x')---- | Compute distance in units of least precision.------ @ 'ulps'' x ('shift' n x) '==' 'abs' n @----ulps' :: Double -> Double -> Word64-ulps' x y = snd $ ulps x y--ulpsf' :: Float -> Float -> Word32-ulpsf' x y = snd $ ulpsf x y---- | Compare two values 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 a b = ulps' a b <= tol--withinf :: Word32 -> Float -> Float -> Bool-withinf tol a b = ulpsf' a b <= tol----{--ulpDelta :: Float -> Float -> Int-ulpDelta x y = if lesser then d' else (-1) * d'-  where (lesser, d) = ulps x y-        d' = fromIntegral d--ulpDelta' :: Float -> Float -> Int32-ulpDelta' x y = if lesser then d' else (-1) * d'-  where (lesser, d) = ulps x y-        d' = fromIntegral d--}--------------------------------------------------------------------- Ulp32--------------------------------------------------------------------- | 32 bit unit of least precision type.----newtype Ulp32 = Ulp32 { unUlp32 :: Int32 } deriving Show--ulp32Nan :: Ulp32 -> Bool-ulp32Nan (Ulp32 x) = x /= (min 2139095040 . max (- 2139095041)) x--instance Eq Ulp32 where-    x == y | ulp32Nan x && ulp32Nan y = True-           | ulp32Nan x || ulp32Nan y = False-           | otherwise                = on (==) unUlp32 x y--instance Prd Ulp32 where-    x <= y | ulp32Nan x && ulp32Nan y = True-           | ulp32Nan x || ulp32Nan y = False-           | otherwise                = on (<=) unUlp32 x y--instance Minimal Ulp32 where-    minimal = Ulp32 $ -2139095041--instance Maximal Ulp32 where-    maximal = Ulp32 $ 2139095040--instance Semigroup (Additive Ulp32) where-    Additive (Ulp32 x) <> Additive (Ulp32 y) = Additive . Ulp32 $ x + y--instance Monoid (Additive Ulp32) where-    mempty = Additive $ Ulp32 0--instance Semigroup (Multiplicative Ulp32) where-    Multiplicative (Ulp32 x) <> Multiplicative (Ulp32 y) = Multiplicative . Ulp32 $ x * y--instance Monoid (Multiplicative Ulp32) where-    mempty = Multiplicative $ Ulp32 1--instance Presemiring Ulp32-instance Semiring Ulp32--instance Semigroup (Join Ulp32) where-    Join (Ulp32 x) <> Join (Ulp32 y) = Join . Ulp32 $ P.max x y--instance Semigroup (Meet Ulp32) where-    Meet (Ulp32 x) <> Meet (Ulp32 y) = Meet . Ulp32 $ P.min x y--f32u32 :: Conn Float Ulp32-f32u32 = Conn (Ulp32 . floatInt32) (int32Float . unUlp32)--u32f32 :: Conn Ulp32 Float-u32f32 = Conn (int32Float . unUlp32) (Ulp32 . floatInt32)---- fromIntegral (maxBound :: Ulp32) + 1 , image of aNan-----newtype Ulp a = Ulp { unUlp :: a }--- instance -{- correct but should replace w/ Graded / Yoneda / Indexed etc-u32w64 :: Conn Ulp32 (Nan Word64)-u32w64 = Conn f g where-  conn = i32w32 >>> w32w64--  offset  = 2139095041 :: Word64-  offset' = 2139095041 :: Int32--  f x@(Ulp32 y) | ulp32Nan x = Nan-                | neg y = Def $ fromIntegral (y + offset')-                | otherwise = Def $ (fromIntegral y) + offset-               where fromIntegral = connl conn--  g x = case x of-          Nan -> Ulp32 offset'-          Def y | y < offset -> Ulp32 $ (fromIntegral y) P.- offset'-                | otherwise  -> Ulp32 $ fromIntegral ((min 4278190081 y) P.- offset)-               where fromIntegral = connr conn--}----- internal-------TODO handle neg case, get # of nans/denormals, collect constants         ----abs' :: Eq a => Ord a => Bound a => Ring a => a -> a---abs' x = if x == minimal then abs (x+one) else abs x--signBit :: Double -> Bool-signBit x = if x =~ anan then False else msbMask x /= 0--evenBit :: Double -> Bool-evenBit x = lsbMask x == 0--lsbMask :: Double -> Word64-lsbMask x = 0x0000000000000001 .&. doubleWord64 x--msbMask :: Double -> Word64-msbMask x = 0x8000000000000000 .&. doubleWord64 x---- loatWord64 maximal == exponent maximal---expMask :: Double -> Word64---expMask x = 0x7F80000000000000 .&. doubleWord64 x---- chk  =  >= 0 ==>  == word64Double $ exponent  + signiicand -sigMask :: Double -> Word64-sigMask x = 0x007FFFFFFFFFFFFF .&. doubleWord64 x----signBitf :: Float -> Bool-signBitf x = if x =~ anan then False else msbMaskf x /= 0--evenBitf :: Float -> Bool-evenBitf x = lsbMaskf x == 0--lsbMaskf :: Float -> Word32-lsbMaskf x = 0x00000001 .&. floatWord32 x--msbMaskf :: Float -> Word32-msbMaskf x = 0x80000000 .&. floatWord32 x---- floatWord32 maximal == exponent maximal-expMaskf :: Float -> Word32-expMaskf x = 0x7f800000 .&. floatWord32 x---- chk f = f >= 0 ==> f == word32Float $ exponent f + significand f-sigMaskf :: Float -> Word32-sigMaskf x = 0x007FFFFF .&. floatWord32 x----{---- | first /NaN/ value. ---naN :: Float---naN = 0/0 -- inc pInf ---- | Positive infinity------ @nInf = 1/0@----pInf :: Float-pInf = word32Float 0x7f800000---- | Negative infinity------ @nInf = -1/0@----nInf :: Float-nInf = word32Float 0xff800000 --}----- Non-monotonic function -signed64 :: Word64 -> Int64-signed64 x | x < 0x8000000000000000 = fromIntegral x-           | otherwise      = fromIntegral (maximal P.- (x P.- 0x8000000000000000))---- Non-monotonic function converting from 2s-complement format.-unsigned64 :: Int64 -> Word64-unsigned64 x | x >= 0  = fromIntegral x-             | otherwise = 0x8000000000000000 + (maximal P.- (fromIntegral x))--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---- Non-monotonic function -signed32 :: Word32 -> Int32-signed32 x | x < 0x80000000 = fromIntegral x-           | otherwise      = fromIntegral (maximal P.- (x P.- 0x80000000))---- Non-monotonic function converting from 2s-complement format.-unsigned32 :: Int32 -> Word32-unsigned32 x | x >= 0  = fromIntegral x-             | otherwise = 0x80000000 + (maximal P.- (fromIntegral x))--int32Float :: Int32 -> Float-int32Float = word32Float . unsigned32--floatInt32 :: Float -> Int32-floatInt32 = signed32 . floatWord32 ---- Bit-for-bit conversion.-word32Float :: Word32 -> Float-word32Float = F.castWord32ToFloat---- TODO force to pos representation?--- Bit-for-bit conversion.-floatWord32 :: Float -> Word32-floatWord32 = (+0) .  F.castFloatToWord32-

@@ -0,0 +1,696 @@+{-# LANGUAGE Safe                       #-}+{-# LANGUAGE PolyKinds                  #-}+{-# LANGUAGE DataKinds                  #-}+{-# LANGUAGE ConstraintKinds            #-}+{-# LANGUAGE DefaultSignatures          #-}+{-# LANGUAGE DeriveFunctor              #-}+{-# LANGUAGE DeriveGeneric              #-}+{-# LANGUAGE DerivingVia                #-}+{-# LANGUAGE FlexibleContexts           #-}+{-# LANGUAGE FlexibleInstances          #-}+{-# LANGUAGE StandaloneDeriving         #-}+{-# LANGUAGE TypeOperators              #-}+-- | 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(..)+) 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.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 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++-------------------------------------------------------------------------------+-- Lattices+-------------------------------------------------------------------------------++-- | Bounded < https://ncatlab.org/nlab/show/lattice lattices >.+--+-- /Neutrality/:+--+-- The least and greatest elements of a complete /a/ are given by the unique+-- upper and lower adjoints to the function /a -> ()/.+--+-- @+-- x '\/' 'false' = x+-- x '/\' 'true' = x+-- 'glb' 'false' x 'true' = x+-- 'lub' 'false' x 'true' = x+-- @+--+type Lattice a = (Eq a, Semilattice 'L a, Extremal 'L a, Semilattice 'R a, Extremal 'R a)++-- | The unique top element of a bounded lattice+--+-- > x /\ true = x+-- > x \/ true = true+--+true :: Lattice a => a+true = maximal++-- | The unique bottom element of a bounded lattice+--+-- > x /\ false = false+-- > x \/ false = x+--+false :: Lattice a => a+false = minimal++-------------------------------------------------------------------------------+-- Heyting algebras+-------------------------------------------------------------------------------++-- | A < https://ncatlab.org/nlab/show/co-Heyting+algebra bi-Heyting algebra >.+--+-- /Laws/:+--+-- > 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++-- | Heyting algebras+--+-- A Heyting algebra is a bounded, distributive complete 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 dual complete of open subsets of a trueological space is likewise+-- the primordial example of a /HeytingR/ algebra.+--+-- /Heyting 'L/:+-- +-- Co-implication to /a/ is the lower adjoint of disjunction with /a/:+--+-- > x \\ a <= y <=> x <= y \/ a+--+-- Note that co-Heyting algebras needn't obey the law of non-contradiction:+--+-- > EQ /\ non EQ = EQ /\ GT \\ EQ = EQ /\ GT = EQ /= LT+--+-- See < https://ncatlab.org/nlab/show/co-Heyting+algebra >+--+-- /Heyting 'R/:+--+-- 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:+--+-- > 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+    +    -- | 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++-------------------------------------------------------------------------------+-- HeytingL+-------------------------------------------------------------------------------++infixl 8 \\++-- | Logical co-implication:+--+-- \( 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 /\ z) >= x \\ y+-- > z \\ (x \/ y) = z \\ x \\ y+-- > (y \/ z) \\ x = y \\ x \/ z \\ x+-- > x \/ y \\ x = x \/ y+--+-- >>> False \\ False+-- False+-- >>> False \\ True+-- False+-- >>> True \\ False+-- True+-- >>> True \\ True+-- False+--+-- For many collections (e.g. 'Data.Set.Set') '\\' coincides with the native 'Data.Set.\\' operator.+--+-- >>> :set -XOverloadedLists+-- >>> [GT,EQ] Set.\\ [LT]+-- fromList [EQ,GT]+-- >>> [GT,EQ] \\ [LT]+-- fromList [EQ,GT]+-- +(\\) :: Heyting 'L a => a -> a -> a+(\\) = flip $ lowerL . heyting++-- | Logical < https://ncatlab.org/nlab/show/co-Heyting+negation co-negation >.+--+-- @ 'non' x = 'true' '\\' x @+--+-- /Laws/:+-- +-- > non false = true+-- > non true = false+-- > 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+-- > 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)++-- | 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 x = x /\ non x++-- | 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 =+  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`)++-------------------------------------------------------------------------------+-- Symmetric+-------------------------------------------------------------------------------++-- | 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.+--+-- /Laws/:+--+-- > x <= y => not y <= not x -- antitone+-- > not . not = id           -- idempotence+-- > x \\ y = not (not y // not x)+-- > x // y = not (not y \\ not x)+--+-- and:+--+-- > converseR x <= converseL x+--+-- with equality occurring iff /a/ is a 'Boolean' algebra.+--+class Biheyting a => Symmetric a where++    -- | Symmetric negation.+    --+    -- > not . not = id+    -- > neg . neg = converseR . converseL+    -- > non . non = converseL . converseR+    -- > neg . non = converseR . converseR+    -- > non . neg = converseL . converseL+    --+    -- > neg = converseR . not = not . converseL+    -- > 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`++    -- | 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++-- | Default constructor for a co-Heyting algebra.+--+symmetricL :: Symmetric a => a -> ConnL a a+symmetricL = heytingL $ \x y -> not (not y // not x)++-- | Default constructor for a Heyting algebra.+--+symmetricR :: Symmetric a => a -> ConnR a a+symmetricR = heytingR $ \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+-- and the law of law of non-contradiction:+--+-- > x \/ neg x = true+-- > x /\ non x = false+--+-- 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 (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 Symmetric () where not _ = ()+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+-------------------------------------------------------------------------------++++-- |+-- Subdirectly irreducible Heyting algebra.+instance Heyting 'R a => Heyting 'R (Lowered a) where+  heyting = heytingR f where++    (Left a)  `f` (Left b) | a <= b    = true+                           | otherwise = Left (a // b)+    (Right _) `f` a                    = a+    _         `f` (Right _)            = true++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 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 Complete k a => Complete k (Extended a)+instance Heyting 'R a => Heyting 'R (Extended a) where+  heyting = heytingR 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++--instance Symmetric a => Symmetric (Extended a) where++-------------------------------------------------------------------------------+-- Instances: product types+-------------------------------------------------------------------------------++instance (Heyting k a, Heyting k b) => Heyting k (a, b) where+  heyting (a,b) = heyting a `strong` heyting b++instance (Symmetric a, Symmetric b) => Symmetric (a, b) where+  not = bimap not not++instance (Boolean a, Boolean b) => Boolean (a, b) where++-------------------------------------------------------------------------------+-- Instances: function types+-------------------------------------------------------------------------------+++instance (U.Finite a, Biheyting b) => Heyting 'L (a -> b) where+  heyting = heytingL $ liftA2 (\\)++instance (U.Finite a, Biheyting b) => Heyting 'R (a -> b) where+  heyting = heytingR $ liftA2 (//)++instance (U.Finite a, Symmetric b) => Symmetric (a -> b) where not = fmap not++instance (U.Finite a, Boolean b) => Boolean (a -> b)++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)++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)++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)++-------------------------------------------------------------------------------+-- Instances: collections+-------------------------------------------------------------------------------+++instance (Total a, U.Finite a) => Heyting 'L (Set.Set a) where+  heyting = heytingL (Set.\\)++instance (Total a, U.Finite a) => Heyting 'R (Set.Set a) where+  heyting = symmetricR++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 Heyting 'L IntSet.IntSet where+  heyting = heytingL (IntSet.\\)++instance Heyting 'R IntSet.IntSet where+  --heyting = heytingR $ \x y -> non x \/ y+  heyting = symmetricR++instance Symmetric IntSet.IntSet where+  not = non --(U.universe IntSet.\\)++instance Boolean IntSet.IntSet where++{- 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++  heyting = heytingR $ \a b ->+    let+      x = Map.merge+            Map.dropMissing                    -- drop if an element is missing in @b@+            (Map.mapMissing (\_ _ -> true))     -- put @true@ if an element is missing in @a@+            (Map.zipWithMatched (\_ -> (//) )) -- merge  matching elements with @`implies`@+            a b++      y = Map.fromList [(k, true) | k <- U.universeF, not (Map.member k a), not (Map.member k b) ]+        -- for elements which are not in a, nor in b add+        -- 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+  f (x1,x2) (y1,y2) = (x1 // y1 /\ x2 // y2, x2 // y2)++  --TODO: would this work for interval orders?+  f (x1,x2) (y1,y2) = (x1 // y1 /\ x2 // y2, x1 // y1 \/ x2 // y2)++coimplies i1 i2 = not (not i1 `implies` not i2)++-- The symmetry+-- neg x = true \\ not x+-- non x = not x // false+-- λ> 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++-- λ> neg' (False ... True)+-- Interval False False+-- λ> (False ... True) `implies` (singleton False)+-- Interval False False+-- +neg' x = (false ... true) `coimplies` (not x)++-- λ> non' (False ... True)+-- Interval False False+-- λ> (singleton True) `coimplies` (False ... True)+-- Interval False False+-- +non' x = not x `implies` (singleton false)++-}++

@@ -0,0 +1,356 @@+{-# LANGUAGE DataKinds                  #-}+module Data.Lattice.Property where++import Data.Connection.Conn+import Data.Connection.Property+import Data.Order+import Data.Order.Property+import Data.Order.Syntax+import Data.Lattice+import Prelude hiding (Eq(..), Ord(..), Bounded, 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)+-- +--+++-- 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)+++heytingL0 :: Heyting 'L a => a -> a -> a -> Bool+heytingL0 x y z = x \\ y <= z <=> x <= y \/ z++heytingL1 :: Heyting 'L a => a -> a -> a -> Bool+heytingL1 x y z = x \\ y >= (x /\ z) \\ y++heytingL2 :: Heyting 'L a => a -> a -> a -> Bool+heytingL2 x y z = x \\ (y /\ z) >= x \\ y++heytingL3 :: Heyting 'L a => a -> a -> a -> Bool+heytingL3 x y z = x >= y ==> x \\ z >= y \\ z++heytingL4 :: Heyting 'L a => a -> a -> a -> Bool+heytingL4 x y z = z \\ (x \/ y) == z \\ x \\ y++heytingL5 :: Heyting 'L a => a -> a -> a -> Bool+heytingL5 x y z = (y \/ z) \\ x == y \\ x \/ z \\ x++heytingL6 :: Heyting 'L a => a -> a -> Bool+heytingL6 x y = x >= x \\ y++heytingL7 :: Heyting 'L a => a -> a -> Bool+heytingL7 x y = x \/ y \\ x == x \/ y++heytingL8 :: forall a. Heyting 'L a => a -> Bool+heytingL8 _ = non false == true @a && non true == false @a++-- Double co-negation is a co-monad.+heytingL9 :: Heyting 'L a => a -> a -> Bool+heytingL9 x y = x /\ non y >= x \\ y++heytingL10 :: Heyting 'L a => a -> a -> Bool+heytingL10 x y = x >= y <=> y \\ x == false++heytingL11 :: Heyting 'L a => a -> a -> Bool+heytingL11 x y = non (x /\ y) >= non x++heytingL12 :: Heyting 'L a => a -> a -> Bool+heytingL12 x y = non (y \\ x) == non (non x) \/ non y++heytingL13 :: Heyting 'L a => a -> a -> Bool+heytingL13 x y = non (x /\ y) == non x \/ non y++heytingL14 :: Heyting 'L a => a -> Bool+heytingL14 x = x \/ non x == true++heytingL15 :: Heyting 'L a => a -> Bool+heytingL15 x = non (non (non x)) == non x++heytingL16 :: Heyting 'L a => a -> Bool+heytingL16 x = non (non (x /\ non x)) == false++heytingL17 :: Heyting 'L a => a -> Bool+heytingL17 x = x >= non (non x)++heytingL18 :: Heyting 'L c => c -> Bool+heytingL18 x = x == boundary x \/ (non . non) x++heytingL19 :: Heyting 'L a => a -> a -> Bool+heytingL19 x y = boundary (x /\ y) == (boundary x /\ y) \/ (x /\ boundary y)  -- (Leibniz rule)++heytingL20 :: Heyting 'L a => a -> a -> Bool+heytingL20 x y = boundary (x \/ y) \/ boundary (x /\ y) == boundary x \/ boundary y+++heytingR0 :: Heyting 'R a => a -> a -> a -> Bool+heytingR0 x y z = x /\ y <= z <=> x <= y // z++heytingR1 :: Heyting 'R a => a -> a -> a -> Bool+heytingR1 x y z = x // y <= x // (y \/ z)++heytingR2 :: Heyting 'R a => a -> a -> a -> Bool+heytingR2 x y z = (x \/ z) // y <= x // y++heytingR3 :: Heyting 'R a => a -> a -> a -> Bool+heytingR3 x y z = x <= y ==> z // x <= z // y++heytingR4 :: Heyting 'R a => a -> a -> a -> Bool+heytingR4 x y z = (x /\ y) // z == x // y // z++heytingR5 :: Heyting 'R a => a -> a -> a -> Bool+heytingR5 x y z = x // (y /\ z) == x // y /\ x // z++heytingR6 :: Heyting 'R a => a -> a -> Bool+heytingR6 x y = y <= x // (x /\ y)++heytingR7 :: Heyting 'R a => a -> a -> Bool+heytingR7 x y = x /\ x // y == x /\ y++heytingR8 :: forall a. Heyting 'R a => a -> Bool+heytingR8 _ = neg false == true @a && neg true == false @a++-- Double negation is a monad.+heytingR9 :: Heyting 'R a => a -> a -> Bool+heytingR9 x y = neg x \/ y <= x // y++heytingR10 :: Heyting 'R a => a -> a -> Bool+heytingR10 x y = x <= y <=> x // y == true++heytingR11 :: Heyting 'R a => a -> a -> Bool+heytingR11 x y = neg (x \/ y) <= neg x++heytingR12 :: Heyting 'R a => a -> a -> Bool+heytingR12 x y = neg (x // y) == neg (neg x) /\ neg y++heytingR13 :: Heyting 'R a => a -> a -> Bool+heytingR13 x y = neg (x \/ y) == neg x /\ neg y++heytingR14 :: Heyting 'R a => a -> Bool+heytingR14 x = x /\ neg x == false++heytingR15 :: Heyting 'R a => a -> Bool+heytingR15 x = neg (neg (neg x)) == neg x++heytingR16 :: Heyting 'R a => a -> Bool+heytingR16 x = neg (neg (x \/ neg x)) == true++heytingR17 :: Heyting 'R a => a -> Bool+heytingR17 x = x <= neg (neg x)++{-+infix 4 `joinLe`+-- | The partial ordering induced by the join-semilattice structure.+--+--+-- Normally when /a/ implements 'Ord' we should have:+-- @ 'joinLe' x y = x '<=' y @+--+joinLe :: Lattice a => a -> a -> Bool+joinLe x y = y == x \/ y++infix 4 `joinGe`+-- | The partial ordering induced by the join-semilattice structure.+--+-- Normally when /a/ implements 'Ord' we should have:+-- @ 'joinGe' x y = x '>=' y @+--+joinGe :: Lattice a => a -> a -> Bool+joinGe x y = x == x \/ y++-- | Partial version of 'Data.Ord.compare'.+--+-- Normally when /a/ implements 'Preorder' we should have:+-- @ 'pcompareJoin' x y = 'pcompare' x y @+--+pcompareJoin :: Lattice a => a -> a -> Maybe Ordering+pcompareJoin x y+  | x == y = Just EQ+  | joinLe x y && x /= y = Just LT+  | joinGe x y && x /= y = Just GT+  | otherwise = Nothing++infix 4 `meetLe`+-- | The partial ordering induced by the meet-semilattice structure.+--+-- Normally when /a/ implements 'Preorder' we should have:+-- @ 'meetLe' x y = x '<~' y @+--+meetLe :: Lattice a => a -> a -> Bool+meetLe x y = x == x /\ y++infix 4 `meetGe`+-- | The partial ordering induced by the meet-semilattice structure.+--+-- Normally when /a/ implements 'Preorder' we should have:+-- @ 'meetGe' x y = x '>~' y @+--+meetGe :: Lattice a => a -> a -> Bool+meetGe x y = y == x /\ y++-- | Partial version of 'Data.Ord.compare'.+--+-- Normally when /a/ implements 'Preorder' we should have:+-- @ 'pcompareJoin' x y = 'pcompare' x y @+--+pcompareMeet :: Lattice a => a -> a -> Maybe Ordering+pcompareMeet x y+  | x == y = Just EQ+  | meetLe x y && x /= y = Just LT+  | meetGe x y && x /= y = Just GT+  | otherwise = Nothing++-- | \( \forall a \in R: a \/ a = a \)+--+-- @ 'idempotent_join' = 'absorbative' 'true' @+-- +-- See < https:\\en.wikipedia.org/wiki/Band_(mathematics) >.+--+-- This is a required property.+--+idempotent_join :: Lattice r => r -> Bool+idempotent_join = idempotent_join_on (~~)++idempotent_join_on :: Semilattice 'L r => Rel r b -> r -> b+idempotent_join_on (~~) r = (\/) r r ~~ r++-- | \( \forall a, b, c \in R: (a \/ b) \/ c = a \/ (b \/ c) \)+--+-- This is a required property.+--+associative_join :: Lattice r => r -> r -> r -> Bool+associative_join = associative_on (~~) (\/) ++associative_join_on :: Semilattice 'L r => Rel r b -> r -> r -> r -> b+associative_join_on (=~) = associative_on (=~) (\/) ++-- | \( \forall a, b, c: (a \# b) \# c \doteq a \# (b \# c) \)+--+associative_on :: Rel r b -> (r -> r -> r) -> (r -> r -> r -> b)+associative_on (~~) (#) a b c = ((a # b) # c) ~~ (a # (b # c))++-- | \( \forall a, b \in R: a \/ b = b \/ a \)+--+-- This is a required property.+--+commutative_join :: Lattice r => r -> r -> Bool+commutative_join = commutative_join_on (~~)++commutative_join_on :: Semilattice 'L r => Rel r b -> r -> r -> b+commutative_join_on (=~) = commutative_on (=~) (\/) +++-- | \( \forall a, b: a \# b \doteq b \# a \)+--+commutative_on :: Rel r b -> (r -> r -> r) -> r -> r -> b+commutative_on (=~) (#) a b = (a # b) =~ (b # a)++-- | \( \forall a, b \in R: a /\ b \/ b = b \)+--+-- Absorbativity is a generalized form of idempotency:+--+-- @+-- 'absorbative' 'true' a = a \/ a = a+-- @+--+-- This is a required property.+--+absorbative_on :: Lattice r => Rel r Bool -> r -> r -> Bool+absorbative_on (=~) x y = (x /\ y \/ y) =~ y++-- | \( \forall a, b \in R: a \/ b /\ b = b \)+--+-- Absorbativity is a generalized form of idempotency:+--+-- @+-- 'absorbative'' 'false' a = a \/ a = a+-- @+--+-- This is a required property.+--+absorbative_on' :: Lattice r => Rel r Bool -> r -> r -> Bool+absorbative_on' (=~) x y = ((x \/ y) /\ y) =~ y++distributive :: Lattice r => r -> r -> r -> Bool+distributive = distributive_on (~~) (/\) (\/)++codistributive :: Lattice r => r -> r -> r -> Bool+codistributive = distributive_on (~~) (\/) (/\)++distributive_on :: Rel r b -> (r -> r -> r) -> (r -> r -> r) -> (r -> r -> r -> b)+distributive_on (=~) (#) (%) a b c = ((a # b) % c) =~ ((a % c) # (b % c))++distributive_on' :: Rel r b -> (r -> r -> r) -> (r -> r -> r) -> (r -> r -> r -> b)+distributive_on' (=~) (#) (%) a b c = (c % (a # b)) =~ ((c % a) # (c % b))++-- | @ 'glb' x x y = x @+--+-- See < https:\\en.wikipedia.org/wiki/Median_algebra >.+majority_glb :: Lattice r => r -> r -> Bool+majority_glb x y = glb x y y ~~ y++-- | @ 'glb' x y z = 'glb' z x y @+--+commutative_glb :: Lattice r => r -> r -> r -> Bool+commutative_glb x y z = glb x y z ~~ glb z x y++-- | @ 'glb' x y z = 'glb' x z y @+--+commutative_glb' :: Lattice r => r -> r -> r -> Bool+commutative_glb' x y z = glb x y z ~~ glb x z y++-- | @ 'glb' ('glb' x w y) w z = 'glb' x w ('glb' y w z) @+--+associative_glb :: Lattice r => r -> r -> r -> r -> Bool+associative_glb x y z w = glb (glb x w y) w z ~~ glb x w (glb y w z)++distributive_glb :: (Bounded r, Lattice r) => r -> r -> r -> Bool+distributive_glb x y z = glb x y z ~~ lub x y z++interval_glb :: Lattice r => r -> r -> r -> Bool+interval_glb x y z = glb x y z ~~ y ==> (x <~ y && y <~ z) || (z <~ y && y <~ x)++-- |  \( \forall a, b, c: a \leq b \Rightarrow a \/ (c /\ b) \eq (a \/ c) /\ b \)+--+-- 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 +++-}

@@ -0,0 +1,563 @@+{-# 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               #-}++module Data.Order (+  -- * 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 Data.Functor.Identity+import safe Data.Functor.Contravariant+import safe Data.Int+import safe Data.List.NonEmpty+import safe Data.Maybe+import safe Data.Ord (Down(..))+import safe Data.Semigroup+import safe Data.Universe.Class (Finite(..))+import safe Data.Word+import safe Data.Void+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+++-- | An < https://en.wikipedia.org/wiki/Order_theory#Partially_ordered_sets order > on /a/.+--+-- Note: ideally this would be a subclass of /Preorder/.+--+-- 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+-- 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)++-------------------------------------------------------------------------------+-- Preorders+-------------------------------------------------------------------------------++-- | A < https://en.wikipedia.org/wiki/Preorder preorder > on /a/.+--+-- 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+-- /a ~~ b/ if and only if /a <~ b/ and /b <~ a/.+--+-- If no partion induced by '~~' contains more than a single element, then /a/+-- is a partial order and we may define an 'Eq' instance such that the+-- following holds:+--+-- @+-- x '==' y = x '~~' y+-- x '<=' y = x '<' y '||' x '~~' y+-- @+--+-- Minimal complete definition: either 'pcompare' or '<~'. Using 'pcompare' can+-- be more efficient for complex types.+--+class Preorder a where+    {-# MINIMAL (<~) | pcompare #-} ++    infix 4 <~, >~, <, >, ?~, ~~, /~, `pcompare`, `pmax`, `pmin`++    -- | 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)++    -- | A converse non-strict preorder relation on /a/.+    --+    -- 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?+    --+    -- 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+    -- > x ~~ y = maybe False (~~ EQ) (pcompare x y)+    --+    -- 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/. +    --+    -- Are /x/ and /y/ either equivalent or incomparable?+    --+    -- 'similar' is reflexive and symmetric, but not necessarily transitive.+    --+    -- Note this is only equivalent to '==' in a total order:+    --+    -- > 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.compare'.+    --+    -- > x <  y = maybe False (<  EQ) $ pcompare x y+    -- > x >  y = maybe False (>  EQ) $ pcompare x y+    -- > x <~ y = maybe False (<~ EQ) $ pcompare x y+    -- > x >~ y = maybe False (>~ EQ) $ pcompare x y+    -- > 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@.+    --+    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++-- | 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 +-- any total function /f/.+--+pcomparing :: Preorder a => (b -> a) -> b -> b -> Maybe Ordering+pcomparing p x y = pcompare (p x) (p y)++---------------------------------------------------------------------+-- DerivingVia+---------------------------------------------------------------------++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++--instance Preorder Void where  _ <~ _ = True+deriving via (Base Void) instance Preorder Void+deriving via (Base ()) instance Preorder ()+deriving via (Base Bool) instance Preorder Bool+deriving via (Base Ordering) instance Preorder Ordering+deriving via (Base Char) instance Preorder Char+deriving via (Base Word) instance Preorder Word+deriving via (Base Word8) instance Preorder Word8+deriving via (Base Word16) instance Preorder Word16+deriving via (Base Word32) instance Preorder Word32+deriving via (Base Word64) instance Preorder Word64+deriving via (Base Natural) instance Preorder Natural+deriving via (Base Int) instance Preorder Int+deriving via (Base Int8) instance Preorder Int8+deriving via (Base Int16) instance Preorder Int16+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++instance (Ord.Ord a, Fractional a) => Preorder (N5 a) where+  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++deriving via (N5 Float) instance Preorder Float+deriving via (N5 Double) instance Preorder Double+++---------------------------------------------------------------------+-- Instances+---------------------------------------------------------------------++++-- N5 lattice ordering: NInf <= NaN <= PInf+{-+pinf = 1 :% 0+ninf = (-1) :% 0+anan = 0 :% 0++λ> pcompareRat anan pinf+Just LT+λ> pcompareRat pinf anan+Just GT+λ> pcompareRat anan anan+Just EQ+λ> pcompareRat anan (3 :% 5)+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 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)++instance Preorder Rational where+  pcompare = pcompareRat++instance Preorder Positive where+  pcompare = pcomparePos++instance (Preorder a, Num a) => Preorder (Complex a) where+  pcompare = pcomparing $ \(x :+ y) -> x^2 + y^2++instance Preorder a => Preorder (Down a) where+  (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++instance Preorder a => Preorder (Max a) where+  Max a <~ Max b = a <~ b++instance Preorder a => Preorder (Min a) where+  Min a <~ Min b = a <~ b++instance Preorder Any where+  Any x <~ Any y = x <~ y++instance Preorder All where+  All x <~ All y = y <~ x++instance Preorder a => Preorder (Identity a) where+  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++instance Preorder a => Preorder [a] where+  {-# SPECIALISE instance Preorder [Char] #-}+  --[] <~ _     = 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++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++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 (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 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 (Foldable1 f, Representable f, Preorder a) => Preorder (Co f a) where+--  Co f <~ Co g = and $ liftR2 (<~) f g++instance (Ord.Ord k, Preorder a) => Preorder (Map.Map k a) where+  (<~) = Map.isSubmapOfBy (<~)++instance Ord.Ord a => Preorder (Set.Set a) where+  (<~) = Set.isSubsetOf++instance Preorder a => Preorder (IntMap.IntMap a) where+  (<~) = 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)