packages feed

connections (empty) → 0.0.1

raw patch · 24 files changed

+3968/−0 lines, 24 filesdep +basedep +containersdep +hedgehogsetup-changed

Dependencies added: base, containers, hedgehog, orders, property, rings, semigroupoids

Files

+ ChangeLog.md view
@@ -0,0 +1,5 @@+# Revision history for orders++## 0.0.1  -- YYYY-mm-dd++* First version. Released on an unsuspecting world.
+ LICENSE view
@@ -0,0 +1,14 @@+BSD 3-Clause License++Copyconnr Christopher McKinlay (c) 2019++Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:++1. Redistributions of source code must retain the above copyconnr notice, this list of conditions and the following disclaimer.++2. Redistributions in binary form must reproduce the above copyconnr notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.++3. Neither the name of the copyconnr holder nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.+
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ connections.cabal view
@@ -0,0 +1,67 @@+name:                connections+version:             0.0.1+description:         partial orders+synopsis:            Partial orders, Galois connections, ordered semirings, & residuated lattices.+homepage:            https://github.com/cmk/connections+license:             BSD3+license-file:        LICENSE+author:              Chris McKinlay+maintainer:          chris.mckinlay@gmail.com+category:            Math+build-type:          Simple+extra-source-files:  ChangeLog.md+cabal-version:       >=1.10++library+  exposed-modules:+      Data.Prd+    , Data.Prd.Property+    , Data.Prd.Lattice+    , Data.Prd.Nan+    , Data.Dioid.Property+    , Data.Dioid.Interval+    , Data.Dioid.Signed+    , Data.Semigroup.Quantale+    , Data.Connection+    , Data.Connection.Property+    , Data.Connection.Word+    , Data.Connection.Int+    , Data.Connection.Float+    , Data.Connection.Yoneda+    , Data.Float++  build-depends:       +      base           >= 4.8   && < 5.0+    , containers     >= 0.4.0 && < 0.7+    , rings          >= 0.0.1 && < 1.0+    , semigroupoids  == 5.*+    , property       >= 0.0.1 && < 1.0++  default-extensions:+      ScopedTypeVariables+    , TypeApplications+    , MultiParamTypeClasses+    , UndecidableInstances+    , FlexibleInstances+  hs-source-dirs: src+  default-language: Haskell2010++test-suite test+  type: exitcode-stdio-1.0+  other-modules:+      Test.Data.Float+    , Test.Data.Dioid.Signed+    , Test.Data.Connection.Int+    , Test.Data.Connection.Word+  build-depends:       +      base == 4.*+    , orders -any +    , hedgehog+    , property+  default-extensions:+      ScopedTypeVariables,+      TypeApplications+  main-is: test.hs+  hs-source-dirs: test+  default-language: Haskell2010+  ghc-options: -threaded -rtsopts -with-rtsopts=-N -Wall
+ src/Data/Connection.hs view
@@ -0,0 +1,288 @@+{-# Language TypeFamilies #-}+{-# Language TypeApplications #-}+{-# Language AllowAmbiguousTypes #-}++module Data.Connection (++  -- * Connection+    Conn(..)+  , connl+  , connr+  , unit+  , counit+  , pcomparing+  , dual+  , (***)+  , (+++)+  , (&&&)+  , (|||)+  , _1+  , _2+  , _L+  , _R+  , just+  , list+  , binord+  , ordbin++  -- * Triple+  , Trip(..)+  , tripl+  , tripr+  , unitl+  , unitr+  , counitl+  , counitr+  , ceiling'+  , floor'+  , (****)+  , (++++)+  , (&&&&)+  , (||||)+  , _1'+  , _2'+  , _L'+  , _R'+  , diag+  , codiag+  , bound+  , maybel+  , mayber+) where++import Control.Category (Category, (>>>))+import Data.Bifunctor (bimap)+import Data.Word+import Data.Int+import Data.Prd+import Data.Prd.Lattice+import Data.Ord (Down(..))+import Prelude ++import qualified Data.Ord as O+import qualified Control.Category as C+++infixr 3 ***, ****, &&&, &&&&+infixr 2 +++, ++++, |||, ||||++-- | A Galois connection between two monotone functions: \(connl \dashv connr \)+--+-- Each side of the adjunction may be defined in terms of the other:+-- +--  \( 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) \)+--+--  \( \forall x, y : x \leq y \Rightarrow connr (x) \leq connr (y) \)+--+--  \( \forall x : connl \dashv connr \Rightarrow x \leq connr \circ connl (x) \)+--+--  \( \forall x : connl \dashv connr \Rightarrow connl \circ connr (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 connl (x) \sim connl (x) \)+--+--  \( \forall x : unit \circ connr (x) \sim connr (x) \)+--+-- See also 'Data.Function.Connection.Property' and <https://en.wikipedia.org/wiki/Galois_connection>.+--+data Conn a b = Conn (a -> b) (b -> a)++connl :: Prd a => Prd b => Conn a b -> a -> b+connl (Conn f _) = f++connr :: Prd a => Prd b => Conn a b -> b -> a+connr (Conn _ g) = g++-- @x <~ unit x@+unit :: Prd a => Prd b => Conn a b -> a -> a+unit (Conn f g) = g . f++-- @counit x <~ x@+counit :: Prd a => Prd b => Conn a b -> b -> b+counit (Conn f g) = f . g++-- | Partial version of 'Data.Ord.comparing'. +--+-- Helpful in conjunction with the @xxxBy@ functions from 'Data.List'.+--+pcomparing :: Eq b => Prd a => Prd b => Conn a b -> a -> a -> Maybe Ordering+pcomparing (Conn f _) x y = f x `pcompare` f y++instance Category Conn where+  id = Conn id id+  Conn f' g' . Conn f g = Conn (f' . f) (g . g')++---------------------------------------------------------------------+--  Instances+---------------------------------------------------------------------++dual :: Prd a => Prd b => Conn a b -> Conn (Down b) (Down a)+dual (Conn f g) = Conn (fmap g) (fmap f)++(***) :: Prd a => Prd b => Prd c => Prd d => Conn a b -> Conn c d -> Conn (a, c) (b, d)+(***) (Conn ab ba) (Conn cd dc) = Conn f g where+  f = bimap ab cd +  g = bimap ba dc++(+++) :: Prd a => Prd b => Prd c => Prd d => Conn a b -> Conn c d -> Conn (Either a c) (Either b d)+(+++) (Conn ab ba) (Conn cd dc) = Conn f g where+  f = either (Left . ab) (Right . cd)+  g = either (Left . ba) (Right . dc)++(&&&) :: Prd a => Prd b => Lattice c => Conn c a -> Conn c b -> Conn c (a, b)+f &&& g = tripr diag >>> f *** g++(|||) :: Prd a => Prd b => Prd c => Conn a c -> Conn b c -> Conn (Either a b) c+f ||| g = f +++ g >>> tripr codiag++-- | Lens into first part of a product.+--+-- @'_1' (ab >>> cd) = '_1' ab >>> '_1' cd@+--+_1 :: Prd a => Prd b => Prd c => Conn a b -> Conn (a, c) (b, c)+_1 = (*** C.id)++_2 :: Prd a => Prd b => Prd c => Conn a b -> Conn (c, a) (c, b)+_2 = (C.id ***)++-- | Prism into left part of a sum.+--+-- @'_L' (ab >>> cd) = '_L' ab >>> '_L' cd@+--+_L :: Prd a => Prd b => Prd c => Conn a b -> Conn (Either a c) (Either b c)+_L = (+++ C.id)++_R :: Prd a => Prd b => Prd c => Conn a b -> Conn (Either c a) (Either c b)+_R = (C.id +++)++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++---------------------------------------------------------------------+--  'Trip'+---------------------------------------------------------------------++-- | An adjoint triple.+--+-- @'Trip' f g h@ satisfies:+--+-- f ⊣ g+-- ⊥   ⊥+-- g ⊣ h+--+-- See <https://ncatlab.org/nlab/show/adjoint+triple>+--+data Trip a b = Trip (a -> b) (b -> a) (a -> b)++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++ceiling' :: Prd a => Prd b => Trip a b -> a -> b+ceiling' = connl . tripl++floor' :: Prd a => Prd b => Trip a b -> a -> b+floor' = connr . tripr++instance Category Trip where+  id = Trip id id id+  Trip f' g' h' . Trip f g h = Trip (f' . f) (g . g') (h' . h)++---------------------------------------------------------------------+--  Instances+---------------------------------------------------------------------++(****) :: Prd a => Prd b => Prd c => Prd d => Trip a b -> Trip c d -> Trip (a, c) (b, d)+(****) (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'++(++++) :: Prd a => Prd b => Prd c => Prd d => Trip a b -> Trip c d -> Trip (Either a c) (Either b d)+(++++) (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')++(&&&&) :: Prd a => Prd b => Lattice c => Trip a c -> Trip b c -> Trip (a, b) c+f &&&& g = f **** g >>> diag++(||||) :: Prd a => Prd b => Prd c => Trip c a -> Trip c b -> Trip c (Either a b)+(||||) f g = codiag >>> f ++++ g++_1' :: Prd a => Prd b => Prd c => Trip a b -> Trip (a, c) (b, c)+_1' = (**** C.id)++_2' :: Prd a => Prd b => Prd c => Trip a b -> Trip (c, a) (c, b)+_2' = (C.id ****)++_L' :: Prd a => Prd b => Prd c => Trip a b -> Trip (Either a c) (Either b c)+_L' = (++++ C.id)++_R' :: Prd a => Prd b => Prd c => Trip a b -> Trip (Either c a) (Either c b)+_R' = (C.id ++++)++diag :: Lattice a => Trip (a, a) a+diag = Trip (uncurry (\/)) (\x -> (x,x)) (uncurry (/\))++codiag :: Prd a => Trip a (Either a a)+codiag = Trip Left (either id id) Right++bound :: Prd a => Bound a => Trip () a+bound = Trip (const minimal) (const ()) (const maximal)++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
+ src/Data/Connection/Float.hs view
@@ -0,0 +1,142 @@+module Data.Connection.Float where++import Control.Category ((>>>))+import Data.Bits ((.&.))+import Data.Int+import Data.Prd.Nan+import Data.Word+import Data.Prd+import Data.Function (on)+import Data.Connection+import Data.Connection.Int+import Data.Connection.Word+import GHC.Num (subtract)+import qualified Data.Bits as B+import qualified GHC.Float as F++import Prelude++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 Min Ulp32 where+    minimal = Ulp32 $ -2139095041++instance Max Ulp32 where+    maximal = Ulp32 $ 2139095040++instance Bounded Ulp32 where+    minBound = minimal  +    maxBound = maximal++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++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+                | negative 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) - offset'+                | otherwise  -> Ulp32 $ fromIntegral ((min 4278190081 y) - offset)+               where fromIntegral = connr conn+++--+--TODO handle neg case, get # of nans/denormals, collect constants         ++abs' :: (Eq a, Bound a, Num a) => a -> a+abs' x = if x == minimal then abs (x+1) else abs x++f32i64 :: Conn Float (Nan Int64)+f32i64 = Conn (liftNan f) (nan (0/0) g) where+  f x | abs x <~ 2**24-1 = ceiling x+      | otherwise = if x >~ 0 then 2^24 else minimal++  g i | abs' i <~ 2^24-1 = fromIntegral i+      | otherwise = if i >~ 0 then 1/0 else -2**24+  +i64f32 :: Conn (Nan Int64) Float+i64f32 = Conn (nan (0/0) f) (liftNan g) where+  f i | abs i <~ 2^24-1 = fromIntegral i+      | otherwise = if i >~ 0 then 2**24 else -1/0++  g x | abs x <~ 2**24-1 = floor x+      | otherwise = if x >~ 0 then maximal else -2^24++f64i64 :: Conn Double (Nan Int64)+f64i64 = Conn (liftNan f) (nan (0/0) g) where+  f x | abs x <~ 2**53-1 = ceiling x+      | otherwise = if x >~ 0 then 2^53 else minimal++  g i | abs' i <~ 2^53-1 = fromIntegral i+      | otherwise = if i >~ 0 then 1/0 else -2**53+  +i64f64 :: Conn (Nan Int64) Double+i64f64 = Conn (nan (0/0) f) (liftNan g) where+  f i | abs i <~ 2^53-1 = fromIntegral i+      | otherwise = if i >~ 0 then 2**53 else -1/0++  g x | abs x <~ 2**53-1 = floor x+      | otherwise = if x >~ 0 then maximal else -2^53++float_word8 :: Trip Float (Nan Word8)+float_word8 = 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)++-- | Shift by /Int32/ units of least precision.+shift :: Int32 -> Float -> Float+shift n = int32Float . (+ n) . floatInt32++-- internal++-- Non-monotonic function +signed32 :: Word32 -> Int32+signed32 x | x < 0x80000000 = fromIntegral x+           | otherwise      = fromIntegral (maximal - (x - 0x80000000))++-- Non-monotonic function converting from 2s-complement format.+unsigned32 :: Int32 -> Word32+unsigned32 x | x >= 0  = fromIntegral x+             | otherwise = 0x80000000 + (maximal - (fromIntegral x))++int32Float :: Int32 -> Float+int32Float = word32Float . unsigned32++floatInt32 :: Float -> Int32+floatInt32 = signed32 . floatWord32 ++word32Float :: Word32 -> Float+word32Float = F.castWord32ToFloat++-- force to positive representation?+floatWord32 :: Float -> Word32+floatWord32 = (+0) .  F.castFloatToWord32
+ src/Data/Connection/Int.hs view
@@ -0,0 +1,87 @@+-- Note that in most cases the obvious implementation is not a valid+-- Galois connection. For example:+--+-- @+-- i08i16  = Conn fromIntegral (fromIntegral . min 127 . max (-1208))+-- @+--+module Data.Connection.Int (+  -- * Int8+    i08w08+  , i08w08'+  , i08i16+  , i08i32+  , i08i64+  -- * Int16+  , i16w16+  , i16w16'+  , i16i32+  , i16i64+  -- * Int32+  , i32w32+  , i32w32'+  , i32i64+  -- * Int64+  , i64w64+  , i64w64'+  -- * Integer+  , intnat+  ) where++import Control.Category ((>>>))+import Data.Connection+import Data.Connection.Word+import Data.Int+import Data.Prd+import Data.Word++import Numeric.Natural++unsigned :: (Bounded a, Integral a, Integral b) => Conn a b+unsigned = +  Conn (\y -> fromIntegral (y + maxBound + 1)) (\x -> fromIntegral x - minBound) ++i08w08 :: Conn Int8 Word8+i08w08 = unsigned++i08w08' :: Conn Int8 Word8+i08w08' = Conn (fromIntegral . max 0) (fromIntegral . min 127)++i08i16 :: Conn Int8 Int16+i08i16 = i08w08 >>> w08w16 >>> w16i16++i08i32 :: Conn Int8 Int32+i08i32 = i08w08 >>> w08w32 >>> w32i32++i08i64 :: Conn Int8 Int64+i08i64 = i08w08 >>> w08w64 >>> w64i64++i16w16 :: Conn Int16 Word16+i16w16 = unsigned++i16w16' :: Conn Int16 Word16+i16w16' = Conn (fromIntegral . max 0) (fromIntegral . min 32767) ++i16i32 :: Conn Int16 Int32+i16i32 = i16w16 >>> w16w32 >>> w32i32++i16i64 :: Conn Int16 Int64+i16i64 = i16w16 >>> w16w64 >>> w64i64++i32w32 :: Conn Int32 Word32+i32w32 = unsigned++i32w32' :: Conn Int32 Word32+i32w32' = Conn (fromIntegral . max 0) (fromIntegral . min 2147483647)++i32i64 :: Conn Int32 Int64+i32i64 = i32w32 >>> w32w64 >>> w64i64++i64w64 :: Conn Int64 Word64+i64w64 = unsigned++i64w64' :: Conn Int64 Word64+i64w64' = Conn (fromIntegral . max 0) (fromIntegral . min 9223372036854775807)++intnat :: Conn Integer Natural+intnat = Conn (fromIntegral . max 0) fromIntegral
+ src/Data/Connection/Property.hs view
@@ -0,0 +1,89 @@+{-# Language TypeFamilies #-}+{-# Language TypeApplications #-}+module Data.Connection.Property where++import Data.Proxy+import Data.Prd+import Data.Connection++import qualified Test.Property.Function.Idempotent as Prop+import qualified Test.Property.Function.Invertible as Prop+import qualified Test.Property.Function.Monotone   as Prop++import Test.Property.Util+import Prelude hiding (Ord(..))+++-- | \( \forall x, y : f \dashv g \Rightarrow f (x) \leq y \Leftrightarrow x \leq g (y) \)+--+-- A monotone Galois connection.+--+connection :: Prd a => Prd b => Conn a b -> a -> b -> Bool+connection (Conn f g) = Prop.adjoint_on (<~) (<~) f g++-- | \( \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++-- | \( \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++-- | \( \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++-- | \( \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++-- | \( \forall x, y : x \leq y \Rightarrow g (x) \leq g (y) \)+--+-- This is a required property.+--+monotone :: Prd a => Prd b => Conn a b -> b -> b -> Bool+monotone (Conn _ g) = Prop.monotone_on (<~) (<~) g++-- | \( \forall x, y : x \leq y \Rightarrow f (x) \leq f (y) \)+--+-- This is a required property.+--+monotone' :: Prd a => Prd b => Conn a b -> a -> a -> Bool+monotone' (Conn f _) = Prop.monotone_on (<~) (<~) f++-- | \( \forall x : f \dashv g \Rightarrow unit \circ unit (x) \sim unit (x) \)+--+idempotent_unit :: Prd a => Prd b => Conn a b -> a -> Bool+idempotent_unit conn = Prop.idempotent_on (=~) $ unit conn++-- | \( \forall x : f \dashv g \Rightarrow counit \circ counit (x) \sim counit (x) \)+--+idempotent_counit :: Prd a => Prd b => Conn a b -> b -> Bool+idempotent_counit conn = Prop.idempotent_on (=~) $ counit conn++-- | \( \forall x: f \dashv g \Rightarrow counit \circ f (x) \sim f (x) \)+--+-- See <https://ncatlab.org/nlab/show/idempotent+adjunction>+--+projective_l :: Prd a => Prd b => Conn a b -> a -> Bool+projective_l conn@(Conn f _) = Prop.projective_on (=~) f $ counit conn++-- | \( \forall x: f \dashv g \Rightarrow unit \circ g (x) \sim g (x) \)+--+-- See <https://ncatlab.org/nlab/show/idempotent+adjunction>+--+projective_r :: Prd a => Prd b => Conn a b -> b -> Bool+projective_r conn@(Conn _ g) = Prop.projective_on (=~) g $ unit conn+
+ src/Data/Connection/Word.hs view
@@ -0,0 +1,77 @@+module Data.Connection.Word (+  -- * Word8+    w08i08+  , w08w16+  , w08w32+  , w08w64+  , w08nat+  -- * Word16+  , w16i16+  , w16w32+  , w16w64+  , w16nat+  -- * Word32+  , w32i32+  , w32w64+  , w32nat+  -- * Word64+  , w64i64+  , w64nat+) where++import Control.Category ((>>>))+import Data.Connection+import Data.Int+import Data.Prd+import Data.Word++import Numeric.Natural++signed :: (Bounded b, Integral a, Integral b) => Conn a b+signed = +  Conn (\x -> fromIntegral x - minBound) (\y -> fromIntegral (y + maxBound + 1))++w08i08 :: Conn Word8 Int8+w08i08 = signed++w08w16 :: Conn Word8 Word16+w08w16 = Conn fromIntegral (fromIntegral . min 255)++-- w08w32 = w08w16 >>> w16w32+w08w32 :: Conn Word8 Word32+w08w32 = Conn fromIntegral (fromIntegral . min 255)++-- w08w64 = w08w32 >>> w32w64 = w08w16 >>> w16w64+w08w64 :: Conn Word8 Word64+w08w64 = Conn fromIntegral (fromIntegral . min 255)++w08nat :: Conn Word8 Natural+w08nat = Conn fromIntegral (fromIntegral . min 255)++w16i16 :: Conn Word16 Int16+w16i16 = signed++w16w32 :: Conn Word16 Word32+w16w32 = Conn fromIntegral (fromIntegral . min 65535)++-- w16w64 = w16w32 >>> w32w64+w16w64 :: Conn Word16 Word64+w16w64 = Conn fromIntegral (fromIntegral . min 65535)++w16nat :: Conn Word16 Natural+w16nat = Conn fromIntegral (fromIntegral . min 65535)++w32i32 :: Conn Word32 Int32+w32i32 = signed++w32w64 :: Conn Word32 Word64+w32w64 = Conn fromIntegral (fromIntegral . min 4294967295)++w32nat :: Conn Word32 Natural+w32nat = Conn fromIntegral (fromIntegral . min 4294967295)++w64i64 :: Conn Word64 Int64+w64i64 = signed++w64nat :: Conn Word64 Natural+w64nat = Conn fromIntegral (fromIntegral . min 18446744073709551615)
+ src/Data/Connection/Yoneda.hs view
@@ -0,0 +1,88 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE Rank2Types #-}++module Data.Connection.Yoneda where++import Data.Int+import Data.Word+import Data.Prd+import Data.Prd.Nan+import Data.Prd.Lattice+import Data.Bifunctor+import Data.Dioid.Interval+import Data.Function+import Data.Functor.Identity+import Data.Functor.Product+import Data.Functor.Sum+import Data.Connection+import Data.Connection.Int+import Data.Connection.Word+import Data.Connection.Float+import Data.Foldable+import Data.List (unfoldr)+import GHC.Num (subtract)+import Numeric.Natural+import Data.Bool+import Prelude hiding (Enum(..), Ord(..), until)++import qualified Control.Category as C+++type family Rep a :: *+++-- | Yoneda representation for lattice ideals & filters.+--+-- A subset /I/ 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 /I/, the element /x \vee y/ is also in /I/.+--+-- /upper/ and /lower/ commute with /Down/:+--+-- * @lower x y == upper (Down x) (Down y)@+--+-- * @lower (Down x) (Down y) == upper x y@+--+-- /Rep a/ is upward-closed:+--+-- * @upper x s && x <~ y ==> upper y s@+--+-- * @upper x s && upper y s ==> connl filter x /\ connl filter y >~ s@+--+-- /Rep a/ is downward-closed:+--+-- * @lower x s && x >~ y ==> lower y s@+--+-- * @lower x s && lower y s ==> connl ideal x \/ connl ideal y ~< s@+--+-- Finally /filter >>> ideal/ and /ideal >>> filter/ are both connections+-- on /a/ and /Rep a/ respectively.+--+-- See also:+--+-- * <https://en.wikipedia.org/wiki/Filter_(mathematics)>+-- * <https://en.wikipedia.org/wiki/Ideal_(order_theory)>+--+class (Prd a, Lattice (Rep a)) => Yoneda a where++    -- Principal ideal generated by an element of /a/.+    ideal :: Conn (Rep a) a++    lower :: Rep a -> a -> Bool++    -- Principal filter generated by an element of /a/.+    filter :: Conn a (Rep a)++    upper :: Rep a -> a -> Bool++type instance Rep (Down a) = Down (Rep a)+type instance Rep Bool = Bool++instance Yoneda Bool where+    ideal = C.id+    lower = (>~)+    filter = C.id+    upper = (<~)
+ src/Data/Dioid/Interval.hs view
@@ -0,0 +1,116 @@+-- | <https://en.wikipedia.org/wiki/Partially_ordered_set#Intervals>+module Data.Dioid.Interval (+    Interval()+  , (...)+  , endpts+  , singleton+  , upset+  , dnset+  , empty+) where++import Data.Prd+import Data.Prd.Lattice+import Data.Connection++import Prelude++{-++ivllat :: (Lattice a, Bound a) => Trip (Interval a) a+ivllat = Trip f g h where+  f = maybe minimal (uncurry (\/)) . endpts+  g = singleton+  h = maybe maximal (uncurry (/\)) . endpts ++indexed :: Index a => Conn (Interval a) (Maybe (Down a, a))++https://en.wikipedia.org/wiki/Locally_finite_poset+https://en.wikipedia.org/wiki/Incidence_algebra++An interval in a poset P is a subset I of P with the property that, for any x and y in I and any z in P, if x ≤ z ≤ y, then z is also in I. ++-}++data Interval a = I !a !a | Empty deriving (Eq, Show)++-- Interval order+-- https://en.wikipedia.org/wiki/Interval_order+instance Ord a => Prd (Interval a) where+  Empty <~ Empty = True+  Empty <~ _ = False++  i@(I _ x) <~ j@(I y _) = x < y || i == j++{-+-- Containment order+-- https://en.wikipedia.org/wiki/Containment_order+instance Prd a => Prd (Interval a) where+  Empty <~ _ = True+  I x y <~ I x' y' = x' <~ x && y <~ y'+-}+++infix 3 ...++-- | Construct an interval from a pair of points.+--+-- If @a <~ b@ then @a ... b = Empty@.+--+(...) :: Prd a => a -> a -> Interval a+a ... b+  | a <~ b = I a b+  | otherwise = Empty+{-# INLINE (...) #-}++-- | Obtain the endpoints of an interval.+--+endpts :: Interval a -> Maybe (a, a)+endpts Empty = Nothing+endpts (I x y) = Just (x, y)+{-# INLINE endpts #-}++-- | Construct an interval containing a single point.+--+-- >>> singleton 1+-- 1 ... 1+--+singleton :: a -> Interval a+singleton a = I a a+{-# INLINE singleton #-}++{-+properties: ++Yoneda lemma for preorders:+x <~ y <==> upset x <~ upset y --containment order++-}++-- | \( X_\geq(x) = \{ y \in X | y \geq x \} \)+--+-- Construct the upper set of an element /x/.+--+-- This function is monotone wrt the containment order.+--+upset :: Max a => a -> Interval a+upset x = x ... maximal+{-# INLINE upset #-}++-- | \( X_\leq(x) = \{ y \in X | y \leq x \} \)+--+-- Construct the lower set of an element /x/.+--+-- This function is antitone wrt the containment order.+--+dnset :: Min a => a -> Interval a+dnset x = minimal ... x+{-# INLINE dnset #-}++-- | The empty interval.+--+-- >>> empty+-- Empty+empty :: Interval a+empty = Empty+{-# INLINE empty #-}
+ src/Data/Dioid/Property.hs view
@@ -0,0 +1,408 @@+{-# Language AllowAmbiguousTypes #-}++module Data.Dioid.Property (+  -- * Properties of pre-semirings & semirings+    neutral_addition+  , neutral_addition'+  , neutral_multiplication+  , neutral_multiplication'+  , associative_addition +  , associative_multiplication +  , distributive +  -- * Properties of non-unital (near-)semirings+  , nonunital+  -- * Properties of unital semirings+  , annihilative_multiplication +  , Prop.homomorphism_boolean+  -- * Properties of cancellative semirings +  , cancellative_addition +  , cancellative_multiplication +  -- * Properties of commutative semirings +  , commutative_addition +  , commutative_multiplication+  -- * Properties of absorbative semirings +  , absorbative_addition+  , absorbative_addition'+  , idempotent_addition+  , absorbative_multiplication+  , absorbative_multiplication' +  -- * Properties of annihilative semirings +  , annihilative_addition +  , annihilative_addition' +  , codistributive+  -- * Properties of ordered semirings +  , ordered_preordered+  , ordered_monotone_zero+  , ordered_monotone_addition+  , ordered_positive_addition+  , ordered_monotone_multiplication+  , ordered_annihilative_unit +  , ordered_idempotent_addition+  , ordered_positive_multiplication+) where++import Data.Prd+import Data.List (unfoldr)+import Data.List.NonEmpty (NonEmpty(..))+import Data.Semiring+import Data.Semigroup.Orphan ()+import Test.Property.Util ((<==>),(==>))+import qualified Test.Property as Prop hiding (distributive_on)+import qualified Data.Semiring.Property as Prop++++------------------------------------------------------------------------------------+-- Properties of pre-semirings & semirings++-- | \( \forall a \in R: (z + a) = a \)+--+-- A (pre-)semiring with a right-neutral additive unit must satisfy:+--+-- @+-- 'neutral_addition' 'mempty' ~~ const True+-- @+-- +-- Or, equivalently:+--+-- @+-- 'mempty' '<>' r ~~ r+-- @+--+-- This is a required property.+--+neutral_addition :: (Eq r, Prd r, Semigroup r) => r -> r -> Bool+neutral_addition = Prop.neutral_addition_on (~~)++neutral_addition' :: (Eq r, Prd r, Monoid r, Semigroup r) => r -> Bool+neutral_addition' = Prop.neutral_addition_on' (~~)++-- | \( \forall a \in R: (o * a) = a \)+--+-- A (pre-)semiring with a right-neutral multiplicative unit must satisfy:+--+-- @+-- 'neutral_multiplication' 'unit' ~~ const True+-- @+-- +-- Or, equivalently:+--+-- @+-- 'unit' '><' r ~~ r+-- @+--+-- This is a required property.+--+neutral_multiplication :: (Eq r, Prd r, Semiring r) => r -> r -> Bool+neutral_multiplication = Prop.neutral_multiplication_on (~~)++neutral_multiplication' :: (Eq r, Prd r, Monoid r, Semiring r) => r -> Bool+neutral_multiplication' = Prop.neutral_multiplication_on' (~~)++-- | \( \forall a, b, c \in R: (a + b) + c = a + (b + c) \)+--+-- /R/ must right-associate addition.+--+-- This should be verified by the underlying 'Semigroup' instance,+-- but is included here for completeness.+--+-- This is a required property.+--+associative_addition :: (Eq r, Prd r, Semigroup r) => r -> r -> r -> Bool+associative_addition = Prop.associative_addition_on (~~)++-- | \( \forall a, b, c \in R: (a * b) * c = a * (b * c) \)+--+-- /R/ must right-associate multiplication.+--+-- This is a required property.+--+associative_multiplication :: (Eq r, Prd r, Semiring r) => r -> r -> r -> Bool+associative_multiplication = Prop.associative_multiplication_on (~~)++-- | \( \forall a, b, c \in R: (a + b) * c = (a * c) + (b * c) \)+--+-- /R/ must right-distribute multiplication.+--+-- When /R/ is a functor and the semiring structure is derived from 'Alternative', +-- this translates to: +--+-- @+-- (a '<|>' b) '*>' c = (a '*>' c) '<|>' (b '*>' c)+-- @  +--+-- See < https://en.wikibooks.org/wiki/Haskell/Alternative_and_MonadPlus >.+--+-- This is a required property.+--+distributive :: (Eq r, Prd r, Semiring r) => r -> r -> r -> Bool+distributive = Prop.distributive_on (~~)++------------------------------------------------------------------------------------+-- Properties of non-unital semirings (aka near-semirings)++-- | \( \forall a, b \in R: a * b = a * b + b \)+--+-- If /R/ is non-unital (i.e. /unit/ equals /mempty/) then it will instead satisfy +-- a right-absorbtion property. +--+-- This follows from right-neutrality and right-distributivity.+--+-- Compare 'codistributive' and 'closed_stable'.+--+-- When /R/ is also left-distributive we get: \( \forall a, b \in R: a * b = a + a * b + b \)+--+-- See also 'Data.Warning' and < https://blogs.ncl.ac.uk/andreymokhov/united-monoids/#whatif >.+--+nonunital :: forall r. (Eq r, Prd r, Monoid r, Semiring r) => r -> r -> Bool+nonunital = Prop.nonunital_on (~~)++------------------------------------------------------------------------------------+-- Properties of unital semirings++-- | \( \forall a \in R: (z * a) = u \)+--+-- A /R/ is unital then its addititive unit must be right-annihilative, i.e.:+--+-- @+-- 'mempty' '><' a ~~ 'mempty'+-- @+--+-- For 'Alternative' instances this property translates to:+--+-- @+-- 'empty' '*>' a ~~ 'empty'+-- @+--+-- All right semirings must have a right-absorbative addititive unit,+-- however note that depending on the 'Prd' instance this does not preclude +-- IEEE754-mandated behavior such as: +--+-- @+-- 'mempty' '><' NaN ~~ NaN+-- @+--+-- This is a required property.+--+annihilative_multiplication :: (Eq r, Prd r, Monoid r, Semiring r) => r -> Bool+annihilative_multiplication = Prop.annihilative_multiplication_on (~~)++------------------------------------------------------------------------------------+-- Properties of cancellative & commutative semirings+++-- | \( \forall a, b, c \in R: b + a = c + a \Rightarrow b = c \)+--+-- If /R/ is right-cancellative wrt addition then for all /a/+-- the section /(a <>)/ is injective.+--+cancellative_addition :: (Eq r, Prd r, Semigroup r) => r -> r -> r -> Bool+cancellative_addition = Prop.cancellative_addition_on (~~)+++-- | \( \forall a, b, c \in R: b * a = c * a \Rightarrow b = c \)+--+-- If /R/ is right-cancellative wrt multiplication then for all /a/+-- the section /(a ><)/ is injective.+--+cancellative_multiplication :: (Eq r, Prd r, Semiring r) => r -> r -> r -> Bool+cancellative_multiplication = Prop.cancellative_multiplication_on (~~)++-- | \( \forall a, b \in R: a + b = b + a \)+--+commutative_addition :: (Eq r, Prd r, Semigroup r) => r -> r -> Bool+commutative_addition = Prop.commutative_addition_on (=~)+++-- | \( \forall a, b \in R: a * b = b * a \)+--+commutative_multiplication :: (Eq r, Prd r, Semiring r) => r -> r -> Bool+commutative_multiplication = Prop.commutative_multiplication_on (=~)+++------------------------------------------------------------------------------------+-- Properties of idempotent & absorbative semirings++-- | \( \forall a, b \in R: a * b + b = b \)+--+-- Right-additive absorbativity is a generalized form of idempotency:+--+-- @+-- 'absorbative_addition' 'unit' a ~~ a <> a ~~ a+-- @+--+absorbative_addition :: (Eq r, Prd r, Semiring r) => r -> r -> Bool+absorbative_addition a b = a >< b <> b ~~ b++idempotent_addition :: (Eq r, Prd r, Monoid r, Semiring r) => r -> Bool+idempotent_addition = absorbative_addition unit+ +-- | \( \forall a, b \in R: b + b * a = b \)+--+-- Left-additive absorbativity is a generalized form of idempotency:+--+-- @+-- 'absorbative_addition' 'unit' a ~~ a <> a ~~ a+-- @+--+absorbative_addition' :: (Eq r, Prd r, Semiring r) => r -> r -> Bool+absorbative_addition' a b = b <> b >< a ~~ b++-- | \( \forall a, b \in R: (a + b) * b = b \)+--+-- Right-mulitplicative absorbativity is a generalized form of idempotency:+--+-- @+-- 'absorbative_multiplication' 'mempty' a ~~ a '><' a ~~ a+-- @+--+-- See < https://en.wikipedia.org/wiki/Absorption_law >.+--+absorbative_multiplication :: (Eq r, Prd r, Semiring r) => r -> r -> Bool+absorbative_multiplication a b = (a <> b) >< b ~~ b++--absorbative_multiplication a b c = (a <> b) >< c ~~ c+--closed a = +--  absorbative_multiplication (star a) unit a && absorbative_multiplication unit (star a) a ++-- | \( \forall a, b \in R: b * (b + a) = b \)+--+-- Left-mulitplicative absorbativity is a generalized form of idempotency:+--+-- @+-- 'absorbative_multiplication'' 'mempty' a ~~ a '><' a ~~ a+-- @+--+-- See < https://en.wikipedia.org/wiki/Absorption_law >.+--+absorbative_multiplication' :: (Eq r, Prd r, Semiring r) => r -> r -> Bool+absorbative_multiplication' a b = b >< (b <> a) ~~ b++-- | \( \forall a \in R: o + a = o \)+--+-- A unital semiring with a right-annihilative muliplicative unit must satisfy:+--+-- @+-- 'unit' <> a ~~ 'unit'+-- @+--+-- For a dioid this is equivalent to:+-- +-- @+-- ('unit' '<~') ~~ ('unit' '~~')+-- @+--+-- For 'Alternative' instances this is known as the left-catch law:+--+-- @+-- 'pure' a '<|>' _ ~~ 'pure' a+-- @+--+annihilative_addition :: (Eq r, Prd r, Monoid r, Semiring r) => r -> Bool+annihilative_addition r = Prop.annihilative_on (~~) (<>) unit r+++-- | \( \forall a \in R: a + o = o \)+--+-- A unital semiring with a left-annihilative muliplicative unit must satisfy:+--+-- @+-- a '<>' 'unit' ~~ 'unit'+-- @+--+-- Note that the left-annihilative property is too strong for many instances. +-- This is because it requires that any effects that /r/ generates be undunit.+--+-- See < https://winterkoninkje.dreamwidth.org/90905.html >.+--+annihilative_addition' :: (Eq r, Prd r, Monoid r, Semiring r) => r -> Bool+annihilative_addition' r = Prop.annihilative_on' (~~) (<>) unit r++-- | \( \forall a, b, c \in R: c + (a * b) \equiv (c + a) * (c + b) \)+--+-- A right-codistributive semiring has a right-annihilative muliplicative unit:+--+-- @ 'codistributive' 'unit' a 'mempty' ~~ 'unit' ~~ 'unit' '<>' a @+--+-- idempotent mulitiplication:+--+-- @ 'codistributive' 'mempty' 'mempty' a ~~ a ~~ a '><' a @+--+-- and idempotent addition:+--+-- @ 'codistributive' a 'mempty' a ~~ a ~~ a '<>' a @+--+-- Furthermore if /R/ is commutative then it is a right-distributive lattice.+--+codistributive :: (Eq r, Prd r, Semiring r) => r -> r -> r -> Bool+codistributive = Prop.distributive_on' (~~) (><) (<>)++------------------------------------------------------------------------------------+-- Properties of ordered semirings (aka dioids).++-- | '<~' is a preordered relation relative to '<>'.+--+-- This is a required property.+--+ordered_preordered :: (Prd r, Semiring r) => r -> r -> Bool+ordered_preordered a b = a <~ (a <> b)++-- | 'mempty' is a minimal or least element of @r@.+--+-- This is a required property.+--+ordered_monotone_zero :: (Prd r, Monoid r) => r -> Bool+ordered_monotone_zero a = mempty ?~ a ==> mempty <~ a ++-- | \( \forall a, b, c: b \leq c \Rightarrow b + a \leq c + a+--+-- In an ordered semiring this follows directly from the definition of '<~'.+--+-- Compare 'cancellative_addition'.+-- +-- This is a required property.+--+ordered_monotone_addition :: (Prd r, Semiring r) => r -> r -> r -> Bool+ordered_monotone_addition a = Prop.monotone_on (<~) (<~) (<> a)++-- |  \( \forall a, b: a + b = 0 \Rightarrow a = 0 \wedge b = 0 \)+--+-- This is a required property.+--+ordered_positive_addition :: (Prd r, Monoid r) => r -> r -> Bool+ordered_positive_addition a b = a <> b =~ mempty ==> a =~ mempty && b =~ mempty++-- | \( \forall a, b, c: b \leq c \Rightarrow b * a \leq c * a+--+-- In an ordered semiring this follows directly from 'distributive' and the definition of '<~'.+--+-- Compare 'cancellative_multiplication'.+--+-- This is a required property.+--+ordered_monotone_multiplication :: (Prd r, Semiring r) => r -> r -> r -> Bool+ordered_monotone_multiplication a = Prop.monotone_on (<~) (<~) (>< a)++------------------------------------------------------------------------------------+-- Properties of idempotent and annihilative dioids.++-- | '<~' is consistent with annihilativity.+--+-- This means that a dioid with an annihilative multiplicative unit must satisfy:+--+-- @+-- ('one' <~) ≡ ('one' ==)+-- @+--+ordered_annihilative_unit :: (Prd r, Monoid r, Semiring r) => r -> Bool+ordered_annihilative_unit a = unit <~ a <==> unit =~ a++-- | \( \forall a, b: a \leq b \Rightarrow a + b = b+--+ordered_idempotent_addition :: (Prd r, Monoid r) => r -> r -> Bool+ordered_idempotent_addition a b = (a <~ b) <==> (a <> b =~ b)++-- |  \( \forall a, b: a * b = 0 \Rightarrow a = 0 \vee b = 0 \)+--+ordered_positive_multiplication :: (Prd r, Monoid r, Semiring r) => r -> r -> Bool+ordered_positive_multiplication a b = a >< b =~ mempty ==> a =~ mempty || b =~ mempty
+ src/Data/Dioid/Signed.hs view
@@ -0,0 +1,195 @@+{-# Language ConstraintKinds #-}+{-# Language Rank2Types #-}++module Data.Dioid.Signed where++import Data.Bifunctor (first)+import Data.Connection+import Data.Connection.Float+import Data.Float+import Data.Ord (Down(..))+import Data.Prd+import Data.Prd.Lattice+import Data.Semigroup.Quantale+import Data.Semiring+import Prelude++-- | 'Sign' is isomorphic to 'Maybe Ordering' and (Bool,Bool), but has a distinct poset ordering:+--+-- @ 'Indeterminate' >= 'Positive' >= 'Zero'@ and+-- @ 'Indeterminate' >= 'Negative' >= 'Zero'@ +--+-- Note that 'Positive' and 'Negative' are not comparable. +--+--   * 'Positive' can be regarded as representing (0, +∞], +--   * 'Negative' as representing [−∞, 0), +--   * 'Indeterminate' as representing [−∞, +∞] v NaN, and +--   * 'Zero' as representing the set {0}.+--+data Sign = Zero | Negative | Positive | Indeterminate deriving (Show, Eq)++signOf :: (Eq a, Num a, Prd a) => a -> Sign+signOf x = case sign x of+    Nothing -> Indeterminate+    Just EQ -> Zero+    Just LT -> Negative+    Just GT -> Positive++instance Semigroup Sign where+    Positive <> Positive            = Positive+    Positive <> Negative            = Indeterminate+    Positive <> Zero                = Positive+    Positive <> Indeterminate       = Indeterminate++    Negative <> Positive            = Indeterminate+    Negative <> Negative            = Negative+    Negative <> Zero                = Negative+    Negative <> Indeterminate       = Indeterminate++    Zero <> a                       = a++    Indeterminate <> _              = Indeterminate++instance Monoid Sign where+    mempty = Zero++instance Semiring Sign where+    Positive >< a = a++    Negative >< Positive            = Negative+    Negative >< Negative            = Positive+    Negative >< Zero                = Zero+    Negative >< Indeterminate       = Indeterminate++    Zero >< _                       = Zero++    --NB: measure theoretic zero+    Indeterminate >< Zero           = Zero+    Indeterminate >< _              = Indeterminate++    fromBoolean = fromBooleanDef Positive++-- TODO if we dont use canonical ordering then we can define a+-- monotone map to floats+instance Prd Sign where+    Positive <~ Positive         = True+    Positive <~ Negative         = False+    Positive <~ Zero             = False+    Positive <~ Indeterminate    = True ++    Negative <~ Positive         = False+    Negative <~ Negative         = True+    Negative <~ Zero             = False+    Negative <~ Indeterminate    = True+    +    --Zero <~ Indeterminate        = False+    Zero <~ _                    = True++    Indeterminate <~ Indeterminate  = True+    Indeterminate <~ _              = False++instance Min Sign where+    minimal = Zero++instance Max Sign where+    maximal = Indeterminate++instance Bounded Sign where+    minBound = minimal+    maxBound = maximal++-- Signed++newtype Signed = Signed { unSigned :: Float }++instance Show Signed where+    show (Signed x) = show x++instance Eq Signed where+    (Signed x) == (Signed y) | isNan x && isNan y = True +                             | isNan x || isNan y = False+                             | otherwise = split x == split y -- 0 /= -0++instance Prd Signed where+    Signed x <~ Signed y | isNan x && isNan y = True+                         | isNan x || isNan y = False+                         | otherwise = (first Down $ split x) <~ (first Down $ split y)++    pcompare (Signed x) (Signed y) | isNan x && isNan y = Just EQ +                                   | isNan x || isNan y = Nothing +                                   | otherwise = pcompare (first Down $ split x) (first Down $ split y)++f32sgn :: Conn Float Signed+f32sgn = Conn f g where+  f x | x == nInf = Signed $ -0+      | otherwise = Signed $ either (const 0) id $ split x++  g (Signed x) = either (const nInf) id $ split x++ugnsgn :: Conn Unsigned Signed+ugnsgn = Conn f g where+  f (Unsigned x) = Signed $ abs x+  g (Signed x) = Unsigned $ either (const 0) id $ split x++{-+ugnf32 :: Conn Unsigned (Down Float)+ugnf32 = Conn f g where+  g (Down x) = Unsigned . max 0 $ x+  f (Unsigned x) = Down x+-}++--TODO +--dont export constructor, qquoters and/or rebindable syntax++newtype Unsigned = Unsigned Float++unsigned :: Signed -> Unsigned+unsigned (Signed x) = Unsigned (abs x)++instance Show Unsigned where+    show (Unsigned x) = show $ abs x++instance Eq Unsigned where+    (Unsigned x) == (Unsigned y) | finite x && finite y = (abs x) == (abs y) +                                 | not (finite x) && not (finite y) = True+                                 | otherwise = False++-- Unsigned has a 2-Ulp interval semiorder containing all joins and meets.+instance Prd Unsigned where+    u <~ v = u `ltugn` v || u == v ++ltugn :: Unsigned -> Unsigned -> Bool+ltugn (Unsigned x) (Unsigned y) | finite x && finite y = (abs x) < shift (-2) (abs y) +                                | finite x && not (finite y) = True+                                | otherwise = False++instance Min Unsigned where+    minimal = Unsigned 0++instance Max Unsigned where+    maximal = Unsigned pInf++instance Lattice Unsigned where+  (Unsigned x) \/ (Unsigned y) | finite x && finite y = Unsigned $ max (abs x) (abs y)+                               | otherwise = Unsigned x++  (Unsigned x) /\ (Unsigned y) | finite x && finite y = Unsigned $ min (abs x) (abs y)+                               | not (finite x)  && finite y = Unsigned y+                               | otherwise = Unsigned x++instance Semigroup Unsigned where+    Unsigned x <> Unsigned y = Unsigned $ abs x + abs y++instance Monoid Unsigned where+    mempty = Unsigned 0++instance Semiring Unsigned where+    Unsigned x >< Unsigned y | zero x || zero y = Unsigned 0+                             | otherwise = Unsigned $ abs x * abs y++    fromBoolean = fromBooleanDef (Unsigned 1)++instance Quantale Unsigned where+    x \\ y = y // x++    Unsigned y // Unsigned x = Unsigned . max 0 $ y // x
+ src/Data/Float.hs view
@@ -0,0 +1,424 @@+{-# LANGUAGE CPP, ForeignFunctionInterface #-}+{-# LANGUAGE FlexibleContexts #-}+module Data.Float (+    Float+  , module Data.Float+  , module Data.Connection.Float+) where++import Prelude hiding (Floating(..), RealFloat(..), Real(..), Enum(..))++import Foreign.C+import Data.Word+import Data.Prd.Nan+import Data.Connection.Float+import Data.Int (Int32)+import Data.Prd+import Data.Function (on)+import Data.Connection ++--import Data.Numbers.CrackNum (floatToFP)+import Data.Bits ((.&.))++import qualified Prelude as P+import qualified Data.Bits as B+import qualified GHC.Float as F++--disp x = floatToFP x+++split :: Float -> Either Float Float+split x = case signBit x of+  True -> Left x+  _    -> Right x++lsbMask :: Float -> Word32+lsbMask x = 0x00000001 .&. floatWord32 x++msbMask :: Float -> Word32+msbMask x = 0x80000000 .&. floatWord32 x++-- floatWord32 maximal == exponent maximal+expMask :: Float -> Word32+expMask x = 0x7f800000 .&. floatWord32 x++-- chk f = f >= 0 ==> f == word32Float $ exponent f + significand f+sigMask :: Float -> Word32+sigMask x = 0x007FFFFF .&. floatWord32 x++signBit :: Float -> Bool+signBit x = if isNan x then False else msbMask x /= 0++evenBit :: Float -> Bool+evenBit x = lsbMask x == 0++-- | maximal (positive) finite value.+maxNorm :: Float+maxNorm = shift (-1) pInf++-- | minimal (positive) normalized value.+minNorm :: Float+minNorm = word32Float 0x00800000++-- | maximal representable odd integer. +--+-- @ maxOdd = 2**24 - 1@+--+maxOdd :: Float+maxOdd = 16777215++-- | minimal (positive) value.+minSub :: Float+minSub = shift 0 1++-- | difference between 1 and the smallest representable value greater than 1.+epsilon :: Float+epsilon = shift 1 1 - 1++-- | first /NaN/ value. +aNan :: Float+aNan = 0/0 -- inc pInf ++-- | Positive infinity+--+-- @nInf = 1/0@+--+pInf :: Float+pInf = word32Float 0x7f800000++-- | Negative infinity+--+-- @nInf = -1/0@+--+nInf :: Float+nInf = word32Float 0xff800000 ++-- Bitwise equality+eq' :: Float -> Float -> Bool+eq' = (==) `on` floatWord32++{-+instance Num Float where+  Float x + Float y = Float $ F.plusFloat x y+  Float x * Float y = Float $ F.timesFloat x y+  Float x - Float y = Float $ F.minusFloat x y+  negate x  = Float $ F.negateFloat x+  abs x = Float $ F.fabsFloat x+  signum x  = Float $ signum x+  fromInteger = Float . fromInteger -- TODO dont use fromInteger++f32i64 :: Conn Float Int+f32i64 = Conn (liftFloat' F.float2Int) (Float . F.int2Float)++λ> unit f32i64 nan+Float (-9.223372e18)+λ> F.float2Int (3.0252336e+35)+-9223372036854775808+λ> F.float2Int (3.0252336e+25)+-9223372036854775808++TODO:+different Conns for embedding a Float in the lower portion of a Double,+versus middle / higher++-}++-- | +--+-- @nan x == indeterminate x@+--+isNan :: Float -> Bool+isNan x = F.isFloatNaN x == 1++pinf :: Float -> Bool+pinf x = infinite x && positive x ++ninf :: Float -> Bool+ninf x = infinite x && negative x++infinite :: Float -> Bool+infinite x = F.isFloatInfinite x == 1++denormalized :: Float -> Bool+denormalized x = F.isFloatDenormalized x == 1++finite :: Float -> Bool+finite x = F.isFloatFinite x == 1++nzero :: Float -> Bool+nzero x = F.isFloatNegativeZero x == 1+++----------------------------------------------------------------+-- Ulps-based comparison+----------------------------------------------------------------++{-++-- |+-- Calculate relative error of two numbers:+--+-- \[ \frac{|a - b|}{\max(|a|,|b|)} \]+--+-- It lies in [0,1) interval for numbers with same sign and (1,2] for+-- numbers with different sign. If both arguments are zero or negative+-- zero function returns 0. If at least one argument is transfinite it+-- returns NaN+relativeError :: Float -> Float -> Float+relativeError a b+  | a == 0 && b == 0 = 0+  | otherwise        = abs (a - b) / fmax (abs a) (abs b) -- TODO need /++-- | Check that relative error between two numbers @a@ and @b@. If+-- 'relativeError' returns NaN it returns @False@.+eqRelErr :: Float -- ^ /eps/ relative error should be in [0,1) range+         -> Float -- ^ /a/+         -> Float -- ^ /b/+         -> Bool+eqRelErr eps a b = relativeError a b < eps++-}++----------------------------------------------------------------+-- Ulps-based comparison+----------------------------------------------------------------++++ulps :: Float -> Float -> (Bool, Word32)+ulps x y = o+  where  x' = floatInt32 x+         y' = floatInt32 y+         o  | x' >~ y' = (False, fromIntegral . abs $ x' - y')+            | otherwise = (True, fromIntegral . abs $ y' - x')++ulpDistance :: Float -> Float -> Word32+ulpDistance x y = snd $ ulps x y++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++-- | Compare two 'Float' values for approximate equality, using+-- Dawson's method.+--+-- required accuracy is specified in ULPs (units of least+-- precision).  If the two numbers differ by the given number of ULPs+-- or less, this function returns @True@.+within :: Word32 -> Float -> Float -> Bool+within tol a b = ulpDistance a b <~ tol++{-++foreign import ccall unsafe "fdimf" fdim :: Float -> Float -> Float++foreign import ccall unsafe "fmaxf" fmax :: Float -> Float -> Float++foreign import ccall unsafe "fminf" fmin :: Float -> Float -> Float+++-- Arithmetic functions++mul :: Float -> Float -> Float+mul = liftFloat2 F.timesFloat ++-- | 'pow' returns the value of x to the exponent y.+--+pow :: Float -> Float -> Float+pow = liftFloat2 F.powerFloat++add :: Float -> Float -> Float+add = liftFloat2 F.plusFloat++sub :: Float -> Float -> Float+sub = liftFloat2 F.minusFloat++neg :: Float -> Float+neg = liftFloat F.negateFloat++div :: Float -> Float -> Float+div = liftFloat2 F.divideFloat++-- | 'sqrt' returns the non-negative square root of x.+--+sqrt :: Float -> Float+sqrt = liftFloat F.sqrtFloat++-- | 'fabs' returns the absolute value of a floating-point number x.+--+fabs :: Float -> Float+fabs = liftFloat F.fabsFloat++-- | 'fma a x b' returns /a*x + b/+foreign import ccall unsafe "fmaf" fma :: Float -> Float -> Float -> Float++-- | 'cbrt' returns the cube root of x.+--+foreign import ccall unsafe "cbrtf" cbrt :: Float -> Float+++-- Exponential and logarithmic functions++-- | 'exp' returns /e/ raised to the value of the given argument /x/. +--+exp :: Float -> Float+exp = liftFloat F.expFloat++-- | 'exp2' returns 2 raised to the value of the given argument /x/. +--+foreign import ccall unsafe "exp2f" exp2 :: Float -> Float++-- | 'exmp1' returns the exponential of /x-1/.+--+expm1 :: Float -> Float+expm1 = liftFloat F.expm1Float++-- | 'log' returns the value of the natural logarithm of argument x.+--+log :: Float -> Float+log = liftFloat F.logFloat++-- | 'log1pf' returns the log of 1+x.+--+log1p :: Float -> Float+log1p = liftFloat F.log1pFloat++-- | 'ilogb' returns x's exponent n, in integer format.+--    ilogb(+-Infinity) re- turns INT_MAX and ilogb(0) returns INT_MIN.+--+foreign import ccall unsafe "ilogbf" ilogb :: Float -> CInt++-- | ldexp function multiplies a floating-point number by an integral power of 2.+-- ldexp is not defined in the Haskell 98 report.+--+foreign import ccall unsafe "ldexpf" ldexp :: Float -> CInt -> Float++-- | 'log10' returns the value of the logarithm of argument x to base 10.+-- log10 is not defined in the Haskell 98 report.+--+foreign import ccall unsafe "log10f" log10 :: Float -> Float++-- | 'log1pf' returns the log of 1+x.+--+--foreign import ccall unsafe "log1pf" log1p :: Float -> Float++foreign import ccall unsafe "log2f" log2 :: Float -> Float++-- | 'logb' returns x's exponent n, a signed integer converted to floating-point.  +-- +-- > logb(+-Infinity) = +Infinity;+-- > logb(0) = -Infinity with a division by zero exception.+--+foreign import ccall unsafe "logbf" logb :: Float -> Float++-- | scalbn(x, n) returns x*(2**n) computed by exponent manipulation.+foreign import ccall unsafe "scalbnf" scalbn :: Float -> CInt -> Float++-- | scalbln(x, n) returns x*(2**n) computed by exponent manipulation.+foreign import ccall unsafe "scalblnf" scalbln :: Float -> CLong -> Float++++-- Trigonometric functions++-- | 'hypot' returns 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.+--+foreign import ccall unsafe "hypotf" hypot :: Float -> Float -> Float++-- | 'tan' returns the tangent of x (measured in radians). +-- A large magnitude argument may yield a result with little or no+-- significance.+--+tan :: Float -> Float+tan = liftFloat F.tanFloat++-- | 'sin' returns the sine of x (measured in radians). +-- A large magnitude argument may yield a result with little or no+-- significance.+--+sin :: Float -> Float+sin = liftFloat F.sinFloat++-- | 'cos' returns the cosine of x (measured in radians).+--+-- A large magnitude argument may yield a result with little or no significance.  +--+cos :: Float -> Float+cos = liftFloat F.cosFloat++-- | 'atan' returns the principal value of the arc tangent of x+-- in the range [-pi/2, +pi/2].+--+atan :: Float -> Float+atan = liftFloat F.atanFloat++-- | 'atan2' returns the principal value of the arc tangent of+-- y/x, using the signs of both arguments to determine the quadrant of the+-- return value.+--+foreign import ccall unsafe "atan2f"  atan2 :: Float -> Float -> Float++-- | 'asin' returns the principal value of the arc sine of x in the range [-pi/2, +pi/2].+--+asin :: Float -> Float+asin = liftFloat F.asinFloat++-- | 'acos' returns the principal value of the arc cosine of x in the range [0, pi]+--+acos :: Float -> Float+acos = liftFloat F.acosFloat++-- | 'tanh' returns the hyperbolic tangent of x.+--+tanh :: Float -> Float+tanh = liftFloat F.tanhFloat++-- | 'sinh' returns the hyperbolic sine of x.+--+sinh :: Float -> Float+sinh = liftFloat F.sinhFloat++-- | 'cosh' returns the hyperbolic cosine of x.+--+cosh :: Float -> Float+cosh = liftFloat F.coshFloat++-- | 'atanh' returns the inverse hyperbolic tangent of x.+--+atanh :: Float -> Float+atanh = liftFloat F.atanh++-- | 'asinh' returns the inverse hyperbolic sine of x.+--+asinh :: Float -> Float+asinh = liftFloat F.asinh++-- | 'acosh' returns the inverse hyperbolic cosine of x.+--+acosh :: Float -> Float+acosh = liftFloat F.acosh++++liftFloat :: (F.Float -> F.Float) -> Float -> Float+liftFloat f x = Float $ f x++liftFloat' :: (F.Float -> a) -> Float -> a+liftFloat' f x = f x++liftFloat2 :: (F.Float -> F.Float -> F.Float) -> Float -> Float -> Float+liftFloat2 f x (Float y) = Float $ f x y++liftFloat2' :: (F.Float -> F.Float -> a) -> Float -> Float -> a+liftFloat2' f x (Float y) = f x y+-}
+ src/Data/Prd.hs view
@@ -0,0 +1,659 @@+-- {-# LANGUAGE ConstrainedClassMethods #-}+{-# LANGUAGE ConstraintKinds     #-}+{-# LANGUAGE DeriveDataTypeable  #-}+{-# LANGUAGE DeriveFoldable      #-}+{-# LANGUAGE DeriveFunctor       #-}+{-# LANGUAGE DeriveGeneric       #-}+{-# LANGUAGE DeriveTraversable   #-}+{-# LANGUAGE FlexibleContexts    #-}+module Data.Prd (+    module Data.Prd+  , Down(..)+) where++import Control.Applicative+import Control.Monad+import Data.Data (Data, Typeable)+import Data.Function+import Data.Int as Int (Int, Int8, Int16, Int32, Int64)+import Data.List.NonEmpty (NonEmpty(..))+import Data.Maybe+import Data.Monoid hiding (First, Last)+import Data.Ord (Down(..))+import Data.Ratio+import Data.Word (Word, Word8, Word16, Word32, Word64)+import GHC.Generics (Generic, Generic1)+import GHC.Real+import Numeric.Natural++import qualified Data.Semigroup as S+import qualified Data.Set as Set+import qualified Data.Map as Map+import qualified Data.IntMap as IntMap+import qualified Data.IntSet as IntSet+import qualified Data.Sequence as Seq++infix 4 <~, >~, /~, ~~, =~, ?~, `pgt`, `pge`, `peq`, `pne`, `ple`, `plt`++infix 4 `lt`, `gt`, `le`, `ge`, `eq`, `ne`, `pmax`, `pmin`+++-- | A partial order on the set /a/.+--+-- A poset relation '<~' must satisfy the following three partial order axioms:+--+-- \( \forall x: x \leq x \) (reflexivity)+-- +-- \( \forall a, b: (a \leq b) \Leftrightarrow \neg (b \leq a) \) (anti-symmetry)+--+-- \( \forall a, b, c: ((a \leq b) \wedge (b \leq c)) \Rightarrow (a \leq c) \) (transitivity)+--+-- If a prior equality relation is available, then a valid @Prd a@ instance may be derived from a semiorder relation 'lt' as:+--+-- @+-- x '<~' y = 'lt' x y '||' x '==' y+-- @+--+-- If /a/ is derived from a semiorder then the definition of 'lt' must satisfy +-- the three semiorder axioms:+--+-- \( \forall x, y: x \lt y \Rightarrow \neg y \lt x \) (asymmetry)+--+-- \( \forall x, y, z, w: x \lt y \wedge y \sim z \wedge z \lt w \Rightarrow x \lt w \) (2-2 chain)+--+-- \( \forall x, y, z, w: x \lt y \wedge y \lt z \wedge y \sim w \Rightarrow \neg (x \sim w \wedge z \sim w) \) (3-1 chain)+--+-- The poset axioms on '<~' then follow from the first & second axioms on 'lt',+-- however the converse is not true. While the first semiorder axiom on 'lt' follows, the second +-- and third semiorder axioms forbid partial orders of four items forming two disjoint chains: +--+-- * the second axiom forbids two chains of two items each (the (2+2) free poset)+-- * the third axiom forbids a three-item chain with one unrelated item+--+-- See also the wikipedia definitions of <https://en.wikipedia.org/wiki/Partially_ordered_set partially ordered set>+-- and <https://en.wikipedia.org/wiki/Semiorder semiorder>.+--+class Prd a where+  {-# MINIMAL (<~) | (>~) #-} ++  -- | Non-strict partial order relation on /a/.+  --+  -- '<~' is reflexive, anti-symmetric, and transitive.+  --+  (<~) :: a -> a -> Bool+  (<~) = flip (>~)++  -- | Converse non-strict partial order relation on /a/.+  --+  -- '>~' is reflexive, anti-symmetric, and transitive.+  --+  (>~) :: a -> a -> Bool+  (>~) = flip (<~)++  -- | Equivalence relation on /a/.+  --+  -- '=~' is reflexive, symmetric, and transitive.+  --+  -- @ x =~ y = maybe False (== EQ) (pcomparePrd x y)+  --+  -- If /a/ implements 'Eq' then (ideally) @x =~ y = x == y@.+  --+  (=~) :: Prd a => a -> a -> Bool+  x =~ y = x <~ y && x >~ y++  -- | Comparability relation on /a/. +  --+  -- '?~' is reflexive, symmetric, and transitive.+  --+  -- @ x ?~ y = maybe False (const True) (pcomparePrd x y) @+  --+  -- If /a/ implements 'Ord' then (ideally) @x ?~ y = True@.+  --+  (?~) :: Prd a => a -> a -> Bool+  x ?~ y = x <~ y || x >~ y++  -- | Partial version of 'Data.Ord.compare'.+  --+  pcompare :: Eq a => a -> a -> Maybe Ordering+  pcompare x y+    | x `lt` y  = Just LT+    | x  ==  y  = Just EQ+    | x `gt` y  = Just GT+    | otherwise = Nothing+++-- | Similarity relation on /a/. +--+-- '~~' is reflexive and symmetric, but not necessarily transitive.+--+-- Note this is only equivalent to '==' in a total (i.e. linear) order.+--+(~~) :: Eq a => Prd a => a -> a -> Bool+x ~~ y = not (x `lt` y) && not (x `gt` y)++-- | Negation of '~~'.+--+(/~) :: Eq a => Prd a => a -> a -> Bool+x /~ y = not $ x ~~ y+++-- | Version of 'pcompare' that uses the derived equivalence relation.+--+-- This can be useful if there is no 'Eq' instance or if it is+-- compromised, for example when /a/ is a floating point number.+--+pcomparePrd :: Prd a => a -> a -> Maybe Ordering+pcomparePrd x y +  | x <~ y = Just $ if y <~ x then EQ else LT+  | y <~ x = Just GT+  | otherwise = Nothing++-- | Version of 'pcompare' that uses 'compare'.+--+pcompareOrd :: Ord a => a -> a -> Maybe Ordering+pcompareOrd x y = Just $ x `compare` y++-- | Prefix version of '=~'.+--+-- @ eq x y = maybe False (== EQ) (pcomparePrd x y)+--+eq :: Prd a => a -> a -> Bool+x `eq` y = x <~ y && x >~ y++-- | Negation of 'eq'.+--+-- @ ne x y = maybe False (/= EQ) (pcomparePrd x y)+--+ne :: Prd a => a -> a -> Bool+x `ne` y = not $ x `eq` y++-- | Prefix version of '<~'.+--+-- @ le x y = maybe False (<= EQ) (pcomparePrd x y)+--+le :: Prd a => a -> a -> Bool+x `le` y = x <~ y++-- | Prefix version of '>~'.+--+-- @ ge x y = maybe False (>= EQ) (pcomparePrd x y)+--+ge :: Prd a => a -> a -> Bool+x `ge` y = x >~ y++-- | Strict partial order relation on /a/.+--+-- 'lt' is irreflexive, asymmetric, and transitive.+--+-- @ lt x y = maybe False (< EQ) (pcompare x y) @+--+-- If /a/ implements 'Ord' then (ideally) @x `lt` y = x < y@.+--+lt :: Eq a => Prd a => a -> a -> Bool+x `lt` y | x /= x || y /= y = False -- guard on lawless 0/0 cases+         | otherwise        = x <~ y && x /= y++-- | Converse strict partial order relation on /a/.+--+-- 'gt' is irreflexive, asymmetric, and transitive.+--+-- @ gt x y = maybe False (> EQ) (pcompare x y) @+--+-- If /a/ implements 'Ord' then (ideally) @x `gt` y = x > y@.+--+gt :: Eq a => Prd a => a -> a -> Bool+x `gt` y | x /= x || y /= y = False +         | otherwise        = x >~ y && x /= y++-- | A partial version of ('=~')+--+-- Returns 'Nothing' instead of 'False' when the two values are not comparable.+--+peq  :: Eq a => Prd a => a -> a -> Maybe Bool+peq x y = case x `pcompare` y of+     Just EQ -> Just True+     Just _  -> Just False+     Nothing -> Nothing++-- | A partial version of ('/~')+--+-- Returns 'Nothing' instead of 'False' when the two values are not comparable.+--+pne :: Eq a => Prd a => a -> a -> Maybe Bool+pne x y = case x `pcompare` y of+     Just EQ -> Just False+     Just _  -> Just True+     Nothing -> Nothing++-- | A partial version of ('<~')+--+-- Returns 'Nothing' instead of 'False' when the two values are not comparable.+--+ple :: Eq a => Prd a => a -> a -> Maybe Bool+ple x y = case x `pcompare` y of+     Just GT -> Just False+     Just _  -> Just True+     Nothing -> Nothing++-- | A partial version of ('>~')+--+-- Returns 'Nothing' instead of 'False' when the two values are not comparable.+--+pge :: Eq a => Prd a => a -> a -> Maybe Bool+pge x y = case x `pcompare` y of+     Just LT -> Just False+     Just _  -> Just True+     Nothing -> Nothing++-- | A partial version of ('<')  +-- +-- Returns 'Nothing' instead of 'False' when the two values are not comparable.+--+-- @lt x y == maybe False id $ plt x y@+--+plt :: Eq a => Prd a => a -> a -> Maybe Bool+plt x y = case x `pcompare` y of+     Just LT -> Just True+     Just _  -> Just False+     Nothing -> Nothing++-- | A partial version of ('>')+--+-- Returns 'Nothing' instead of 'False' when the two values are not comparable.+--+-- @gt x y == maybe False id $ pgt x y@+--+pgt :: Eq a => Prd a => a -> a -> Maybe Bool+pgt x y = case x `pcompare` y of+     Just GT -> Just True+     Just _  -> Just False+     Nothing -> Nothing++-- | A partial version of 'Data.Ord.max'. +--+-- Default instance returns the connr argument in the case of equality.+--+pmax :: Eq a => Prd a => a -> a -> Maybe a+pmax x y = do+  o <- pcompare x y+  case o of+    GT -> Just x+    EQ -> Just y+    LT -> Just y++pjoin :: Eq a => Min a => Foldable f => f a -> Maybe a+pjoin = foldM pmax minimal++-- | A partial version of 'Data.Ord.min'. +--+-- Default instance returns the connr argument in the case of equality.+--+pmin :: Eq a => Prd a => a -> a -> Maybe a+pmin x y = do+  o <- pcompare x y+  case o of+    GT -> Just y+    EQ -> Just x+    LT -> Just x++pmeet :: Eq a => Max a => Foldable f => f a -> Maybe a+pmeet = foldM pmin maximal++sign :: Eq a => Num a => Prd a => a -> Maybe Ordering+sign x = pcompare x 0++zero :: Eq a => Num a => Prd a => a -> Bool+zero x = sign x == Just EQ++positive :: Eq a => Num a => Prd a => a -> Bool+positive x = sign x == Just GT++negative :: Eq a => Num a => Prd a => a -> Bool+negative x = sign x == Just LT++indeterminate :: Eq a => Num a => Prd a => a -> Bool+indeterminate x = sign x == Nothing+++---------------------------------------------------------------------+--  Instances+---------------------------------------------------------------------++instance Prd Bool where+    (<~) = (<=)+    pcompare = pcompareOrd++instance Prd Char where+    (<~) = (<=)+    pcompare = pcompareOrd++instance Prd Integer where+    (<~) = (<=)+    pcompare = pcompareOrd++instance Prd Int where +    (<~) = (<=)+    pcompare = pcompareOrd++instance Prd Int8 where+    (<~) = (<=)+    pcompare = pcompareOrd++instance Prd Int16 where+    (<~) = (<=)+    pcompare = pcompareOrd++instance Prd Int32 where+    (<~) = (<=)+    pcompare = pcompareOrd++instance Prd Int64 where+    (<~) = (<=)+    pcompare = pcompareOrd++instance Prd Natural where+    (<~) = (<=)+    pcompare = pcompareOrd++instance Prd Word where+    (<~) = (<=)+    pcompare = pcompareOrd++instance Prd Word8 where+    (<~) = (<=)+    pcompare = pcompareOrd++instance Prd Word16 where+    (<~) = (<=)+    pcompare = pcompareOrd++instance Prd Word32 where+    (<~) = (<=)+    pcompare = pcompareOrd++instance Prd Word64 where+    (<~) = (<=)+    pcompare = pcompareOrd++instance Prd Ordering where+    (<~) = (<=)+    pcompare = pcompareOrd++instance Prd a => Prd [a] where+    {-# SPECIALISE instance Prd [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 Prd a => Prd (NonEmpty a) where+    (x :| xs) <~ (y :| ys) = x <~ y && xs <~ ys++instance Prd a => Prd (Down a) where+    x <~ y = y <~ x++-- Canonically ordered.+instance Prd a => Prd (Dual a) where+    x <~ y = y <~ x++instance Prd Any where+    Any x <~ Any y = x <~ y++instance Prd All where+    All x <~ All y = y <~ x++{-++-- | 'First a' forms a pre-dioid for any semigroup @a@.+instance (Eq a, Semigroup a) => Prd (S.First a) where +    (<~) = (==)++instance Ord a => Prd (S.Max a) where +    pcompare (S.Max x) (S.Max y) = Just $ compare x y++instance Ord a => Prd (S.Min a) where +    pcompare (S.Min x) (S.Min y) = Just $ compare y x++-}++instance Prd Float where+    x <~ y | x /= x && y /= y = True +           | x /= x || y /= y = False+           | otherwise        = x <= y+{-+    pcompare x y | x /= x && y /= y = Just EQ +                 | x /= x || y /= y = Nothing+                 | otherwise        = pcompareOrd x y++    x `eq` y | x /= x && y /= y = True+             | x /= x || y /= y = False+             | otherwise = x == y++    x `lt` y | x /= x || y /= y = False+             | otherwise = shift 2 x P.< y+-}++++instance Prd Double where+    x <~ y | x /= x && y /= y = True +           | x /= x || y /= y = False+           | otherwise        = x <= y++instance  (Prd a, Integral a)  => Prd (Ratio a)  where+    {-# SPECIALIZE instance Prd Rational #-}+    (x:%y) <~ (x':%y') | (x `eq` 0 && y `eq` 0) || (x' `eq` 0 && y' `eq` 0) = False+                         | otherwise = x * y' <~ x' * y++-- Canonical semigroup ordering+instance Prd a => Prd (Maybe a) where+    Just a <~ Just b = a <~ b+    x@Just{} <~ Nothing = False+    Nothing <~ _ = True++-- Canonical semigroup ordering+instance (Prd a, Prd b) => Prd (Either a b) where+    Right a <~ Right b  = a <~ b+    Right _ <~ _        = False+    +    Left e <~ Left f   = e <~ f+    Left _ <~ _        = True+ +instance Prd () where +    pcompare _ _ = Just EQ+    _ <~ _ = True++-- Canonical semigroup ordering+instance (Prd a, Prd b) => Prd (a, b) where +  (a,b) <~ (i,j) = a <~ i && b <~ j++instance (Prd a, Prd b, Prd c) => Prd (a, b, c) where +  (a,b,c) <~ (i,j,k) = a <~ i && b <~ j && c <~ k++instance (Prd a, Prd b, Prd c, Prd d) => Prd (a, b, c, d) where +  (a,b,c,d) <~ (i,j,k,l) = a <~ i && b <~ j && c <~ k && d <~ l++instance (Prd a, Prd b, Prd c, Prd d, Prd e) => Prd (a, b, c, d, e) where +  (a,b,c,d,e) <~ (i,j,k,l,m) = a <~ i && b <~ j && c <~ k && d <~ l && e <~ m++instance Ord a => Prd (Set.Set a) where+    (<~) = Set.isSubsetOf++instance (Ord k, Prd a) => Prd (Map.Map k a) where+    (<~) = Map.isSubmapOfBy (<~)++instance Prd a => Prd (IntMap.IntMap a) where+    (<~) = IntMap.isSubmapOfBy (<~)++instance Prd IntSet.IntSet where+    (<~) = IntSet.isSubsetOf+++-- Helper type for 'DerivingVia'+newtype Ordered a = Ordered { getOrdered :: a }+  deriving ( Eq, Ord, Show, Data, Typeable, Generic, Generic1, Functor, Foldable, Traversable)++instance Ord a => Prd (Ordered a) where+    (<~) = (<=)++type Bound a = (Min a, Max a) ++-- | Min element of a partially ordered set.+-- +-- \( \forall x: x \ge minimal \)+--+-- This means that 'minimal' must be comparable to all values in /a/.+--+class Prd a => Min a where+    minimal :: a++instance Min () where minimal = ()++instance Min Natural where minimal = 0++instance Min Bool where minimal = minBound++instance Min Ordering where minimal = minBound++instance Min Int where minimal = minBound++instance Min Int8 where minimal = minBound++instance Min Int16 where minimal = minBound++instance Min Int32 where minimal = minBound++instance Min Int64 where minimal = minBound++instance Min Word where minimal = minBound++instance Min Word8 where minimal = minBound++instance Min Word16 where minimal = minBound++instance Min Word32 where minimal = minBound++instance Min Word64 where minimal = minBound ++instance Prd a => Min (IntMap.IntMap a) where+    minimal = IntMap.empty++instance Ord a => Min (Set.Set a) where+    minimal = Set.empty++instance (Ord k, Prd a) => Min (Map.Map k a) where+    minimal = Map.empty++instance (Min a, Min b) => Min (a, b) where+    minimal = (minimal, minimal)++instance (Min a, Prd b) => Min (Either a b) where+    minimal = Left minimal++instance Prd a => Min (Maybe a) where+    minimal = Nothing ++instance Max a => Min (Down a) where+    minimal = Down maximal++-- | Max element of a partially ordered set.+--+-- \( \forall x: x \le maximal \)+--+-- This means that 'maximal' must be comparable to all values in /a/.+--+class Prd a => Max a where+    maximal :: a++instance Max () where maximal = ()++instance Max Bool where maximal = maxBound++instance Max Ordering where maximal = maxBound++instance Max Int where maximal = maxBound++instance Max Int8 where maximal = maxBound++instance Max Int16 where maximal = maxBound++instance Max Int32 where maximal = maxBound++instance Max Int64 where maximal = maxBound++instance Max Word where maximal = maxBound++instance Max Word8 where maximal = maxBound++instance Max Word16 where maximal = maxBound++instance Max Word32 where maximal = maxBound++instance Max Word64 where maximal = maxBound++instance (Max a, Max b) => Max (a, b) where+    maximal = (maximal, maximal)++instance (Prd a, Max b) => Max (Either a b) where+    maximal = Right maximal++instance Max a => Max (Maybe a) where+    maximal = Just maximal++instance Min a => Max (Down a) where+    maximal = Down minimal++{-+instance (Universe a, Prd a) => Prd (k -> a) where++instance Min a => Min (k -> a) where+    minimal = const minimal++instance Max a => Max (k -> a) where+    maximal = const maximal+-}+ ++{-# INLINE until #-}+until :: (a -> Bool) -> (a -> a -> Bool) -> (a -> a) -> a -> a+until pred rel f seed = go seed+  where go x | x' `rel` x = x+             | pred x = x+             | otherwise = go x'+          where x' = f x++{-# INLINE while #-}+while :: (a -> Bool) -> (a -> a -> Bool) -> (a -> a) -> a -> a+while pred rel f seed = go seed+  where go x | x' `rel` x = x+             | not (pred x') = x+             | otherwise = go x'+          where x' = f x++{-+while' :: (a -> Bool) -> (a -> a -> Bool) -> (a -> a) -> a -> a+while' pred rel f seed = go seed f+  where go x | x' `rel` x = id+             | not (pred x') = id+             | otherwise = go x' . f+          where x' = f x+-}++-- | Greatest (resp. least) fixed point of a monitone (resp. antitone) function. +--+-- Does not check that the function is monitone (resp. antitone).+--+-- See also < http://en.wikipedia.org/wiki/Kleene_fixed-point_theorem >.+--+{-# INLINE fixed #-}+fixed :: (a -> a -> Bool) -> (a -> a) -> a -> a+fixed = while (\_ -> True)+
+ src/Data/Prd/Lattice.hs view
@@ -0,0 +1,292 @@+{-# LANGUAGE ConstrainedClassMethods #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DeriveDataTypeable  #-}+{-# LANGUAGE Safe #-}++module Data.Prd.Lattice where++import Data.Data (Data, Typeable)+import Data.Foldable+import Data.Function+import Data.Int as Int (Int, Int8, Int16, Int32, Int64)+import Data.Maybe+import Data.Monoid hiding (First, Last)+import Data.Ord+import Data.Prd+import Data.Semigroup.Foldable+import Data.Set (Set)+import Data.Word (Word, Word8, Word16, Word32, Word64)+import GHC.Generics (Generic, Generic1)++import Prelude ++import qualified Data.Map as Map+import qualified Data.Set as Set+import qualified Data.IntMap as IntMap+import qualified Data.IntSet as IntSet+import qualified Data.Sequence as Seq+++{-++A partially ordered set is a directed-complete partial order (dcpo) if each of its directed subsets has a supremum. A subset of a partial order is directed if it is non-empty and every pair of elements has an upper bound in the subset. In the literature, dcpos sometimes also appear under the label up-complete poset.+++distributivity: A join-semilattice is distributive if for all a, b, and x with x ≤ a ∨ b there exist a' ≤ a and b' ≤ b such that x = a' ∨ b' . Distributive meet-semilattices are defined dually. These definitions are justified by the fact that any distributive join-semilattice in which binary meets exist is a distributive lattice++morphisms: Given two join-semilattices (S, ∨) and (T, ∨), a homomorphism of (join-) semilattices is a function f: S → T such that++f(x ∨ y) = f(x) ∨ f(y).+Hence f is just a homomorphism of the two semigroups associated with each semilattice. If S and T both include a least element 0, then f should also be a monoid homomorphism, i.e. we additionally require that++f(0) = 0.+In the order-theoretic formulation, these conditions just state that a homomorphism of join-semilattices is a function that preserves binary joins and least elements, if such there be. The obvious dual—replacing ∧ with ∨ and 0 with 1—transforms this definition of a join-semilattice homomorphism into its meet-semilattice equivalent.++Note that any semilattice homomorphism is necessarily monotone with respect to the associated ordering relation.++-}++--(a ∧ b) ⊗ c = (a ⊗ c) ∧ (b ⊗ c), c ⊗ (a ∧ b) = (c ⊗ a) ∧ (c ⊗ b)+-- (meet x y) /\ z = x /\ z `meet` y /\ z++-- idempotent sup dioids ? complete (join-semi)lattices derived from <~?+--connr-distributivity (the group (E\{ε}, ⊗) is therefore reticulated)+--+-- mon zero = const Nothing++-- bounded meet semilattice+-- need the codistributive property & absorbtion & commutativity++{-+If E is a distributive lattice, then (E, ∨, ∧) is a doublyidempotent dioid, the order relation (canonical) of the dioid being defined as:+a ≤ b ⇔ a ∨ b = b.+Conversely, let (E, ⊕, ⊗) be a doubly-idempotent dioid for which ≤, the canonical+order relation relative to the law ⊕ is also a canonical order relation for ⊗:+x ≤ y ⇔ x ⊗ y = x.+Then E is a distributive lattice.+-}++infixr 6 /\+infixr 5 \/++-- | Lattices.+--+-- A lattice is a partially ordered set in which every two elements have a unique join +-- (least upper bound or supremum) and a unique meet (greatest lower bound or infimum). +--+-- See <http://en.wikipedia.org/wiki/Lattice_(order)> and <http://en.wikipedia.org/wiki/Absorption_law>.+--+--+-- /Laws/+--+-- @+-- x '\/' 'maximal' ≡ x+-- @+--+-- /Corollary/+--+-- @+-- x '\/' 'maximal'+--   ≡⟨ identity ⟩+-- (x '\/' 'maximal') '/\' 'maximal'+--   ≡⟨ absorption ⟩+-- 'maximal'+-- @+--+-- @+-- x '\/' 'minimal' ≡ x+-- @+--+-- /Corollary/+--+-- @+-- x '/\' 'minimal'+--   ≡⟨ identity ⟩+-- (x '/\' 'minimal') '\/' 'minimal'+--   ≡⟨ absorption ⟩+-- 'minimal'+-- @+--+-- /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+-- @+--+class Prd a => Lattice a where++  (\/) :: a -> a -> a++  (/\) :: a -> a -> a++  -- | Lattice morphism.+  fromSubset :: Min a => Set a -> a+  fromSubset = join++-- | The partial ordering induced by the join-semilattice structure+joinLeq :: Lattice a => a -> a -> Bool+joinLeq x y = x \/ y =~ y++meetLeq :: Lattice a => a -> a -> Bool+meetLeq x y = x /\ y =~ x++join :: (Min a, Lattice a, Foldable f) => f a -> a+join = foldr' (\/) minimal++meet :: (Max a, Lattice a, Foldable f) => f a -> a+meet = foldr' (/\) maximal++-- | The join of at a list of join-semilattice elements (of length at least one)+join1 :: (Lattice a, Foldable1 f) => f a -> a+join1 =  unJoin . foldMap1 Join++--+-- | The meet of at a list of meet-semilattice elements (of length at least one)+meet1 :: (Lattice a, Foldable1 f) => f a -> a+meet1 = unMeet . foldMap1 Meet++-- | Birkhoff's self-dual ternary median operation.+--+-- TODO: require a /Dioid/ instance.+--+-- @ median x x y ≡ x @+--+-- @ median x y z ≡ median z x y @+--+-- @ median x y z ≡  median x z y @+--+-- @ median (median x w y) w z ≡ median x w (median y w z) @+--+median :: Lattice a => a -> a -> a -> a+median x y z = (x \/ y) /\ (y \/ z) /\ (z \/ x)+++---------------------------------------------------------------------+--  Instances+---------------------------------------------------------------------++instance Lattice () where+  _ \/ _ = ()+  _ /\ _ = ()++instance (Lattice a, Lattice b) => Lattice (a, b) where+  (x1, y1) \/ (x2, y2) = (x1 \/ x2, y1 \/ y2)+  (x1, y1) /\ (x2, y2) = (x1 /\ x2, y1 /\ y2)++instance (Lattice a, Lattice b) => Lattice (Either a b) where+  Right x \/ Right y = Right $ x \/ y+  x@Right{} \/ _     = x+  Left x  \/ Left y  = Left $ x \/ y+  x@Left{}  \/ y     = y++  Right x /\ Right y = Right $ x /\ y+  x@Right{} /\ y     = y+  Left x  /\ Left y  = Left $ x /\ y+  x@Left{}  /\ _     = x++instance Lattice a => Lattice (Maybe a) where+  Just x \/ Just y    = Just $ x \/ y+  x@Just{} \/ _       = x+  Nothing  \/ Nothing = Nothing+  Nothing  \/ y       = y++  Just x /\ Just y    = Just $ x /\ y+  x@Just{} /\ y       = y+  Nothing  /\ _       = Nothing++instance Lattice Bool where+  (\/) = (||)+  (/\) = (&&)++instance Lattice All where+  All a \/ All b = All $ a \/ b+  All a /\ All b = All $ a /\ b++instance Min All where+  minimal = All False++instance Max All where+  maximal = All True++instance Lattice Any where+  Any a \/ Any b = Any $ a \/ b+  Any a /\ Any b = Any $ a /\ b++instance Min Any where+  minimal = Any False++instance Max Any where+  maximal = Any True++instance Lattice a => Lattice (Down a) where+  Down x \/ Down y = Down (x /\ y)+  Down x /\ Down y = Down (x \/ y)++instance Ord a => Lattice (Ordered a) where+  Ordered x \/ Ordered y = Ordered (max x y)+  Ordered x /\ Ordered y = Ordered (min x y)++instance Ord a => Lattice (Set.Set a) where+  (\/) = Set.union+  (/\) = Set.intersection++instance (Ord k, Lattice a) => Lattice (Map.Map k a) where+  (\/) = Map.unionWith (\/)+  (/\) = Map.intersectionWith (/\)++instance Lattice a => Lattice (IntMap.IntMap a) where+  (\/) = IntMap.unionWith (\/)+  (/\) = IntMap.intersectionWith (/\)++instance Lattice IntSet.IntSet where+  (\/) = IntSet.union+  (/\) = IntSet.intersection++---------------------------------------------------------------------+--  Newtypes+---------------------------------------------------------------------++newtype Join a = Join { unJoin :: a }+  deriving (Eq, Ord, Show, Typeable, Data, Generic)++instance Lattice a => Semigroup (Join a) where+  Join a <> Join b = Join (a \/ b)++instance (Lattice a, Min a) => Monoid (Join a) where+  mempty = Join minimal+  Join a `mappend` Join b = Join (a \/ b)++instance (Eq a, Lattice a) => Prd (Join a) where+  (Join a) <~ (Join b) = joinLeq a b++newtype Meet a = Meet { unMeet :: a }+  deriving (Eq, Ord, Show, Typeable, Data, Generic)++instance Lattice a => Semigroup (Meet a) where+  Meet a <> Meet b = Meet (a /\ b)++instance (Lattice a, Max a) => Monoid (Meet a) where+  mempty = Meet maximal+  Meet a `mappend` Meet b = Meet (a /\ b)
+ src/Data/Prd/Nan.hs view
@@ -0,0 +1,111 @@+{-# LANGUAGE DeriveDataTypeable  #-}+{-# LANGUAGE DeriveFoldable      #-}+{-# LANGUAGE DeriveFunctor       #-}+{-# LANGUAGE DeriveGeneric       #-}+{-# LANGUAGE DeriveTraversable   #-}+{-# LANGUAGE FlexibleContexts    #-}+{-# LANGUAGE Safe                #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE Rank2Types       #-}++module Data.Prd.Nan where++import Control.Applicative+import Data.Data (Data, Typeable)+import Data.Prd+import Data.Connection+import GHC.Generics (Generic, Generic1)++-- A type with an additional element allowing for the possibility of undefined values.+-- Isomorphic to /Maybe a/ but with a different 'Prd' instance.+data Nan a = NaN | Def a+  deriving ( Eq, Ord, Show, Data, Typeable, Generic, Generic1, Functor, Foldable, Traversable)++nan :: b -> (a -> b) -> Nan a -> b+nan _ f (Def y) = f y+nan x _  NaN    = x ++defined :: Nan a -> Bool+defined NaN = False+defined _   = True++mapNan :: (a -> b) -> Nan a -> Nan b+mapNan f = nan NaN $ Def . f++maybeNan :: (forall a. a -> a) -> Maybe a -> Nan a+maybeNan _ Nothing = NaN+maybeNan f (Just x) = Def $ f x++nanMaybe :: (forall a. a -> a) -> Nan a -> Maybe a+nanMaybe _ NaN = Nothing+nanMaybe f (Def x) = Just $ f x++eitherNan :: Either a b -> Nan b+eitherNan = either (const NaN) Def++nanEither :: a -> Nan b -> Either a b+nanEither x = nan (Left x) Right++liftNan :: (Prd a, Fractional a) => (a -> b) -> a -> Nan b+liftNan f x | x =~ (0/0) = NaN+            | otherwise = Def (f x)++liftNan' :: RealFloat a => (a -> b) -> a -> Nan b+liftNan' f x | isNaN x = NaN+             | otherwise = Def (f x)++-- Lift all exceptional values+liftAll :: (RealFloat a, Prd a, Bound b) => (a -> b) -> a -> Nan b+liftAll f x | isNaN x = NaN+            | isInf x = Def maximal+            | isInf (-x) = Def minimal+            | otherwise = Def (f x)++isInf :: (RealFloat a, Prd a) => a -> Bool+isInf x = isInfinite x && gt x 0++floatOrdering :: (RealFloat a, Prd a) => Trip a (Nan Ordering)+floatOrdering = Trip f g h where++  g (Def GT) = 1/0+  g (Def LT) = - 1/0+  g (Def EQ) = 0+  g NaN = 0/0+  +  f x | isNaN x    = NaN+  f x | isInf (-x) = Def LT+  f x | x <~ 0     = Def EQ+  f x | otherwise  = Def GT++  h x | isNaN x    = NaN+  h x | isInf x    = Def GT+  h x | x >~ 0     = Def EQ+  h x | otherwise  = Def LT++instance Prd a => Prd (Nan a) where+    NaN <~ NaN = True+    _   <~ NaN = False+    NaN <~ _   = False+    Def a <~ Def b = a <~ b++instance Applicative Nan where+    pure = Def+    NaN <*> _ = NaN+    Def f <*> x = f <$> x++instance Num a => Num (Nan a) where+    negate      = fmap negate+    (+)         = liftA2 (+)+    (*)         = liftA2 (*)+    fromInteger = pure . fromInteger+    abs         = fmap abs+    signum      = fmap signum++nanflt :: Prd a => Fractional a => Conn (Nan a) a+nanflt = Conn (nan (0/0) id) $ \y -> if y =~ (0/0) then NaN else Def y ++def :: Prd a => Prd b => Conn a b -> Conn (Nan a) (Nan b)+def conn = Conn f g where +  Conn f' g' = _R conn+  f = eitherNan . f' . nanEither ()+  g = eitherNan . g' . nanEither ()
+ src/Data/Prd/Property.hs view
@@ -0,0 +1,164 @@+-- | See <https://en.wikipedia.org/wiki/Binary_relation#Properties>.+module Data.Prd.Property (+  -- * Equivalence relations+    symmetric+  , coreflexive+  , reflexive_eq+  , transitive_eq++  -- * Partial orders+  -- ** Non-strict partial orders+  , antisymmetric+  , reflexive_le+  , transitive_le+  -- ** Connex non-strict partial orders+  , connex+  -- ** Strict partial orders+  , asymmetric+  , transitive_lt+  , irreflexive_lt+  -- ** Semiconnex strict partial orders+  , semiconnex+  , trichotomous+  -- ** Semiorders+  , chain_22+  , chain_31+) where++import Data.Prd+import Data.Prd.Lattice+import Data.Semiring+import Test.Property.Util+import Prelude hiding (Ord(..))++import qualified Prelude as P+import qualified Test.Property.Relation as R++-- | \( \forall a, b: (a \eq b) \Leftrightarrow (b \eq a) \)+--+-- '=~' is a symmetric relation.+--+-- This is a required property.+--+symmetric :: Prd r => r -> r -> Bool+symmetric = R.symmetric (=~)++-- | \( \forall x, y: x \eq y \Leftrightarrow x == y \)+--+-- '=~' is a coreflexive relation.+--+-- See <https://en.wikipedia.org/wiki/Reflexive_relation#Related_terms>.+--+-- This is a required property.+--+coreflexive :: (Eq r, Prd r) => r -> r -> Bool+coreflexive x y = x =~ y ==> x == y++-- | \( \forall a: (a \eq a) \)+--+-- '=~' is a reflexive relation.+--+-- This is a required property.+--+reflexive_eq :: Prd r => r ->  Bool+reflexive_eq = R.reflexive (=~) ++-- | \( \forall a, b, c: ((a \eq b) \wedge (b \eq c)) \Rightarrow (a \eq c) \)+--+-- '=~' is a transitive relation.+--+-- This is a required property.+--+transitive_eq :: Prd r => r -> r -> r -> Bool+transitive_eq = R.transitive (=~)++-- | \( \forall a, b: (a \leq b) \wedge (b \leq a) \Rightarrow a \eq b \)+--+-- '<~' is an antisymmetric relation.+--+-- This is a required property.+--+antisymmetric :: Prd r => r -> r -> Bool+antisymmetric = R.antisymmetric_on (=~) (<~)++-- | \( \forall a: (a \leq a) \)+--+-- '<~' is a reflexive relation.+--+-- This is a required property.+--+reflexive_le :: Prd r => r ->  Bool+reflexive_le = R.reflexive (<~) ++-- | \( \forall a, b, c: ((a \leq b) \wedge (b \leq c)) \Rightarrow (a \leq c) \)+--+-- '<~' is an transitive relation.+--+-- This is a required property.+--+transitive_le :: Prd r => r -> r -> r -> Bool+transitive_le = R.transitive (<~)++-- | \( \forall a, b: ((a \leq b) \vee (b \leq a)) \)+--+-- '<~' is a connex relation.+-- +connex :: Prd r => r -> r -> Bool+connex = R.connex (<~)++-- | \( \forall a, b: (a \lt b) \Rightarrow \neg (b \lt a) \)+--+-- 'lt' is an asymmetric relation.+--+-- This is a required property.+--+asymmetric :: Eq r => Prd r => r -> r -> Bool+asymmetric = R.asymmetric lt++-- | \( \forall a: \neg (a \lt a) \)+--+-- 'lt' is an irreflexive relation.+--+-- This is a required property.+--+irreflexive_lt :: Eq r => Prd r => r ->  Bool+irreflexive_lt = R.irreflexive lt ++-- | \( \forall a, b, c: ((a \lt b) \wedge (b \lt c)) \Rightarrow (a \lt c) \)+--+-- 'lt' is a transitive relation.+--+-- This is a required property.+--+transitive_lt :: Eq r => Prd r => r -> r -> r -> Bool+transitive_lt = R.transitive lt++-- | \( \forall a, b: \neg (a \eq b) \Rightarrow ((a \lt b) \vee (b \lt a)) \)+--+-- 'lt' is a semiconnex relation.+--+semiconnex :: Eq r => Prd r => r -> r -> Bool+semiconnex = R.semiconnex_on (=~) lt++-- | \( \forall a, b, c: ((a \lt b) \vee (a \eq b) \vee (b \lt a)) \wedge \neg ((a \lt b) \wedge (a \eq b) \wedge (b \lt a)) \)+--+-- In other words, exactly one of \(a \lt b\), \(a \eq b\), or \(b \lt a\) holds.+--+-- If 'lt' is a trichotomous relation then the set is totally ordered.+--+trichotomous :: Eq r => Prd r => r -> r -> Bool+trichotomous = R.trichotomous_on (=~) lt++-- | \( \forall x, y, z, w: x \lt y \wedge y \sim z \wedge z \lt w \Rightarrow x \lt w \) +--+-- A semiorder does not allow 2-2 chains.+--+chain_22 :: Eq r => Prd r => r -> r -> r -> r -> Bool+chain_22 x y z w = x `lt` y && y ~~ z && z `lt` w ==> x `lt` w++-- \( \forall x, y, z, w: x \lt y \wedge y \lt z \wedge y \sim w \Rightarrow \neg (x \sim w \wedge z \sim w) \) (3-1 chain)+--+-- A semiorder does not allow 3-1 chains.+--+chain_31 :: Eq r => Prd r => r -> r -> r -> r -> Bool+chain_31 x y z w = x `lt` y && y `lt` z && y ~~ w ==> not (x ~~ w && z ~~ w)
+ src/Data/Semigroup/Quantale.hs view
@@ -0,0 +1,78 @@+module Data.Semigroup.Quantale where++import Data.Connection hiding (floor', ceiling')+import Data.Float+import Data.Group+import Data.Prd+import Data.Prd.Lattice+import Data.Word+import Data.Semigroup.Orphan ()+import Prelude hiding (negate, until)+import Test.Property.Util ((<==>),(==>))+import qualified Prelude as Pr++residuated :: Quantale a => a -> a -> a -> Bool+residuated x y z = x <> y <~ z <==> y <~ x \\ z <==> x <~ z // y++{-++In the interest of usability we abuse terminology slightly and use 'quantale' to describe any residuated, partially ordered semigroup. This admits instances of hoops and triangular (co)-norms.++There are several additional properties that apply when the poset structure is lattice-ordered (i.e. a residuated lattice) or when the semigroup is a monoid or semiring. See the associated 'Properties' module.+++distributive_cross as bs = maybe True (~~ cross as bs) $ pjoin as <> pjoin bs+  where cross = join (liftA2 (<>) a b)++--lattice version+distributive_cross' as bs = cross as bs ~~ join as <> join bs+  where +        cross = join (liftA2 (<>) a b)++join as \\ b ~~ meet (fmap (\\b) as)++a \\ meet bs ~~ meet (fmap (a\\) bs)++ideal_residuated :: (Quantale a, Ideal a, Functor (Rep a)) => a -> a -> Bool+ideal_residuated x y = x \\ y =~ join (fmap (x<>) (connl ideal $ y))++ideal_residuated' :: (Quantale a, Ideal a, Functor (Rep a)) => a -> a -> Bool+ideal_residuated' x y = x // y =~ join (fmap (<>x) (connl ideal $ y))++x \/ y = (x // y) <> y -- unit (minus_plus x) y -- (y // x) + x+x /\ y = x <> (x \\ y) -- (y + x) // x -- x \\ (x + y) ++minimal \\ x =~ maximal =~ x \\ maximal+mempty \\ x ~~ unit+ +-}++class (Semigroup a, Prd a) => Quantale a where+    residr :: a -> Conn a a+    residr x = Conn (x<>) (x\\)++    residl :: a -> Conn a a+    residl x = Conn (<>x) (//x)++    (\\) :: a -> a -> a+    x \\ y = connr (residr x) y++    (//) :: a -> a -> a+    x // y = connl (residl x) y++instance Quantale Float where+    x \\ y = y // x++    --x <> y <~ z iff y <~ x \\ z iff x <~ z // y.+    y // x | y =~ x = 0+           | otherwise = let z = y - x in if z + x <~ y then upper z (x<>) y else lower' z (x<>) y ++-- @'lower'' x@ is the least element /y/ in the descending+-- chain such that @not $ f y '<~' x@.+--+lower' z f x = until (\y -> f y <~ x) ge (shift $ -1) z++-- @'upper' y@ is the greatest element /x/ in the ascending+-- chain such that @g x '<~' y@.+--+upper z g y = while (\x -> g x <~ y) le (shift 1) z
+ test/Test/Data/Connection/Int.hs view
@@ -0,0 +1,130 @@+{-# LANGUAGE TemplateHaskell #-}+module Test.Data.Connection.Int where++import Data.Int+import Data.Word+import Data.Connection+import Data.Connection.Int+import Numeric.Natural+import qualified Data.Connection.Property as Prop++import Hedgehog+import qualified Hedgehog.Gen as G+import qualified Hedgehog.Range as R++ri :: (Integral a, Bounded a) => Range a+ri = R.linearFrom 0 minBound maxBound++rint :: Range Integer+rint = R.linearFrom 0 (- 2^127) (2^127)++rnat :: Range Natural+rnat = R.linear 0 (2^128)++prop_connections_int_wrd :: Property+prop_connections_int_wrd = withTests 1000 . property $ do++  i08 <- forAll $ G.integral (ri @Int8)+  w08 <- forAll $ G.integral (ri @Word8)+  i16 <- forAll $ G.integral (ri @Int16)+  w16 <- forAll $ G.integral (ri @Word16)+  i32 <- forAll $ G.integral (ri @Int32)+  w32 <- forAll $ G.integral (ri @Word32)+  i64 <- forAll $ G.integral (ri @Int64)+  w64 <- forAll $ G.integral (ri @Word64)+  int <- forAll $ G.integral rint+  nat <- forAll $ G.integral rnat++  i08' <- forAll $ G.integral (ri @Int8)+  w08' <- forAll $ G.integral (ri @Word8)+  i16' <- forAll $ G.integral (ri @Int16)+  w16' <- forAll $ G.integral (ri @Word16)+  i32' <- forAll $ G.integral (ri @Int32)+  w32' <- forAll $ G.integral (ri @Word32)+  i64' <- forAll $ G.integral (ri @Int64)+  w64' <- forAll $ G.integral (ri @Word64)+  int' <- forAll $ G.integral rint+  nat' <- forAll $ G.integral rnat++  assert $ Prop.connection intnat  int nat+  assert $ Prop.connection i64w64  i64 w64+  assert $ Prop.connection i64w64' i64 w64+  assert $ Prop.connection i32i64  i32 i64+  assert $ Prop.connection i32w32  i32 w32+  assert $ Prop.connection i32w32' i32 w32+  assert $ Prop.connection i16i64  i16 i64+  assert $ Prop.connection i16i32  i16 i32+  assert $ Prop.connection i16w16  i16 w16+  assert $ Prop.connection i16w16' i16 w16+  assert $ Prop.connection i08i64  i08 i64+  assert $ Prop.connection i08i32  i08 i32+  assert $ Prop.connection i08i16  i08 i16+  assert $ Prop.connection i08w08  i08 w08+  assert $ Prop.connection i08w08' i08 w08++  assert $ Prop.monotone' intnat  int int'+  assert $ Prop.monotone' i64w64  i64 i64'+  assert $ Prop.monotone' i64w64' i64 i64'+  assert $ Prop.monotone' i32i64  i32 i32'+  assert $ Prop.monotone' i32w32  i32 i32'+  assert $ Prop.monotone' i32w32' i32 i32'+  assert $ Prop.monotone' i16i64  i16 i16'+  assert $ Prop.monotone' i16i32  i16 i16'+  assert $ Prop.monotone' i16w16  i16 i16'+  assert $ Prop.monotone' i16w16' i16 i16'+  assert $ Prop.monotone' i08i64  i08 i08'+  assert $ Prop.monotone' i08i32  i08 i08'+  assert $ Prop.monotone' i08i16  i08 i08'+  assert $ Prop.monotone' i08w08  i08 i08'+  assert $ Prop.monotone' i08w08' i08 i08'++  assert $ Prop.monotone intnat  nat nat'+  assert $ Prop.monotone i64w64  w64 w64'+  assert $ Prop.monotone i64w64' w64 w64'+  assert $ Prop.monotone i32i64  i64 i64'+  assert $ Prop.monotone i32w32  w32 w32'+  assert $ Prop.monotone i32w32' w32 w32'+  assert $ Prop.monotone i16i64  i64 i64'+  assert $ Prop.monotone i16i32  i32 i32'+  assert $ Prop.monotone i16w16  w16 w16'+  assert $ Prop.monotone i16w16' w16 w16'+  assert $ Prop.monotone i08i64  i64 i64'+  assert $ Prop.monotone i08i32  i32 i32'+  assert $ Prop.monotone i08i16  i16 i16'+  assert $ Prop.monotone i08w08  w08 w08'+  assert $ Prop.monotone i08w08' w08 w08'++  assert $ Prop.closed intnat  int+  assert $ Prop.closed i64w64  i64+  assert $ Prop.closed i64w64' i64+  assert $ Prop.closed i32i64  i32+  assert $ Prop.closed i32w32  i32+  assert $ Prop.closed i32w32' i32+  assert $ Prop.closed i16i64  i16+  assert $ Prop.closed i16i32  i16+  assert $ Prop.closed i16w16  i16+  assert $ Prop.closed i16w16' i16+  assert $ Prop.closed i08i64  i08+  assert $ Prop.closed i08i32  i08+  assert $ Prop.closed i08i16  i08+  assert $ Prop.closed i08w08  i08+  assert $ Prop.closed i08w08' i08++  assert $ Prop.kernel intnat  nat+  assert $ Prop.kernel i64w64' w64+  assert $ Prop.kernel i64w64  w64+  assert $ Prop.kernel i32i64  i64+  assert $ Prop.kernel i32w32' w32+  assert $ Prop.kernel i32w32  w32+  assert $ Prop.kernel i16i64  i64+  assert $ Prop.kernel i16i32  i32+  assert $ Prop.kernel i16w16' w16+  assert $ Prop.kernel i16w16  w16+  assert $ Prop.kernel i08i64  i64+  assert $ Prop.kernel i08i32  i32+  assert $ Prop.kernel i08i16  i16+  assert $ Prop.kernel i08w08' w08+  assert $ Prop.kernel i08w08  w08++tests :: IO Bool+tests = checkParallel $$(discover)
+ test/Test/Data/Connection/Word.hs view
@@ -0,0 +1,120 @@+{-# LANGUAGE TemplateHaskell #-}+module Test.Data.Connection.Word where++import Data.Int+import Data.Word+import Data.Connection+import Data.Connection.Word+import Numeric.Natural+import qualified Data.Connection.Property as Prop++import Hedgehog+import qualified Hedgehog.Gen as G+import qualified Hedgehog.Range as R++ri :: (Integral a, Bounded a) => Range a+ri = R.linearFrom 0 minBound maxBound++rnat :: Range Natural+rnat = R.linear 0 (2^128)++prop_connections_wrd_int :: Property+prop_connections_wrd_int = withTests 1000 . property $ do++  i08 <- forAll $ G.integral (ri @Int8)+  w08 <- forAll $ G.integral (ri @Word8)+  i16 <- forAll $ G.integral (ri @Int16)+  w16 <- forAll $ G.integral (ri @Word16)+  i32 <- forAll $ G.integral (ri @Int32)+  w32 <- forAll $ G.integral (ri @Word32)+  i64 <- forAll $ G.integral (ri @Int64)+  w64 <- forAll $ G.integral (ri @Word64)+  nat <- forAll $ G.integral rnat++  i08' <- forAll $ G.integral (ri @Int8)+  w08' <- forAll $ G.integral (ri @Word8)+  i16' <- forAll $ G.integral (ri @Int16)+  w16' <- forAll $ G.integral (ri @Word16)+  i32' <- forAll $ G.integral (ri @Int32)+  w32' <- forAll $ G.integral (ri @Word32)+  i64' <- forAll $ G.integral (ri @Int64)+  w64' <- forAll $ G.integral (ri @Word64)+  nat' <- forAll $ G.integral rnat++  assert $ Prop.connection w64nat w64 nat+  assert $ Prop.connection w64i64 w64 i64+  assert $ Prop.connection w32nat w32 nat+  assert $ Prop.connection w32w64 w32 w64+  assert $ Prop.connection w32i32 w32 i32+  assert $ Prop.connection w16nat w16 nat+  assert $ Prop.connection w16w64 w16 w64+  assert $ Prop.connection w16w32 w16 w32+  assert $ Prop.connection w16i16 w16 i16+  assert $ Prop.connection w08nat w08 nat+  assert $ Prop.connection w08w64 w08 w64+  assert $ Prop.connection w08w32 w08 w32+  assert $ Prop.connection w08w16 w08 w16+  assert $ Prop.connection w08i08 w08 i08++  assert $ Prop.monotone' w64nat w64 w64'+  assert $ Prop.monotone' w64i64 w64 w64'+  assert $ Prop.monotone' w32nat w32 w32'+  assert $ Prop.monotone' w32w64 w32 w32'+  assert $ Prop.monotone' w32i32 w32 w32'+  assert $ Prop.monotone' w16nat w16 w16'+  assert $ Prop.monotone' w16w64 w16 w16'+  assert $ Prop.monotone' w16w32 w16 w16'+  assert $ Prop.monotone' w16i16 w16 w16'+  assert $ Prop.monotone' w08nat w08 w08'+  assert $ Prop.monotone' w08w64 w08 w08'+  assert $ Prop.monotone' w08w32 w08 w08'+  assert $ Prop.monotone' w08w16 w08 w08'+  assert $ Prop.monotone' w08i08 w08 w08'++  assert $ Prop.monotone w64nat nat nat'+  assert $ Prop.monotone w64i64 i64 i64'+  assert $ Prop.monotone w32nat nat nat'+  assert $ Prop.monotone w32w64 w64 w64'+  assert $ Prop.monotone w32i32 i32 i32'+  assert $ Prop.monotone w16nat nat nat'+  assert $ Prop.monotone w16w64 w64 w64'+  assert $ Prop.monotone w16w32 w32 w32'+  assert $ Prop.monotone w16i16 i16 i16'+  assert $ Prop.monotone w08nat nat nat'+  assert $ Prop.monotone w08w64 w64 w64'+  assert $ Prop.monotone w08w32 w32 w32'+  assert $ Prop.monotone w08w16 w16 w16'+  assert $ Prop.monotone w08i08 i08 i08'++  assert $ Prop.closed w64nat w64+  assert $ Prop.closed w64i64 w64+  assert $ Prop.closed w32nat w32+  assert $ Prop.closed w32w64 w32+  assert $ Prop.closed w32i32 w32+  assert $ Prop.closed w16nat w16+  assert $ Prop.closed w16w64 w16+  assert $ Prop.closed w16w32 w16+  assert $ Prop.closed w16i16 w16+  assert $ Prop.closed w08nat w08+  assert $ Prop.closed w08w64 w08+  assert $ Prop.closed w08w32 w08+  assert $ Prop.closed w08w16 w08+  assert $ Prop.closed w08i08 w08++  assert $ Prop.kernel w64nat nat+  assert $ Prop.kernel w64i64 i64+  assert $ Prop.kernel w32nat nat+  assert $ Prop.kernel w32w64 w64+  assert $ Prop.kernel w32i32 i32+  assert $ Prop.kernel w16nat nat+  assert $ Prop.kernel w16w64 w64+  assert $ Prop.kernel w16w32 w32+  assert $ Prop.kernel w16i16 i16+  assert $ Prop.kernel w08nat nat+  assert $ Prop.kernel w08w64 w64+  assert $ Prop.kernel w08w32 w32+  assert $ Prop.kernel w08w16 w16+  assert $ Prop.kernel w08i08 i08++tests :: IO Bool+tests = checkParallel $$(discover)
+ test/Test/Data/Dioid/Signed.hs view
@@ -0,0 +1,206 @@+{-# LANGUAGE TemplateHaskell #-}+module Test.Data.Dioid.Signed where++import Prelude ++import Data.Ord (Down(..))+import Data.Prd+import Data.Semiring+import Data.Connection+import Data.Dioid.Signed+import Data.Float+import Data.Semigroup.Quantale++import qualified Data.Prd.Property as Prop+import qualified Data.Semiring.Property as Prop+import qualified Data.Connection.Property as Prop++import Hedgehog+import Test.Data.Float+import Test.Property.Util+import qualified Hedgehog.Gen as G+import qualified Hedgehog.Range as R++gen_sign :: Gen Sign+gen_sign = G.choice $ fmap pure [Zero, Positive, Negative, Indeterminate]++gen_signed :: Gen Signed+gen_signed = Signed <$> gen_flt32'++gen_unsigned :: Gen Unsigned+gen_unsigned = Unsigned <$> gen_flt32++gen_unsigned' :: Gen Unsigned+gen_unsigned' = Unsigned <$> gen_flt32'++prop_prd_signed :: Property+prop_prd_signed = withTests 1 $ property $ do+  x <- forAll gen_signed+  y <- forAll gen_signed+  z <- forAll gen_signed++  assert $ Prop.reflexive_eq x+  assert $ Prop.reflexive_le x+  assert $ Prop.irreflexive_lt x+  assert $ Prop.symmetric x y+  assert $ Prop.asymmetric x y+  assert $ Prop.antisymmetric x y+  assert $ Prop.transitive_lt x y z+  assert $ Prop.transitive_le x y z+  assert $ Prop.transitive_eq x y z++prop_connection_flt32_signed :: Property+prop_connection_flt32_signed = withTests 1 $ property $ do+  x <- forAll gen_flt32'+  y <- forAll gen_signed+  x' <- forAll gen_flt32'+  y' <- forAll gen_signed++  assert $ Prop.connection f32sgn x y+  assert $ Prop.monotone' f32sgn x x'+  assert $ Prop.monotone  f32sgn y y'+  assert $ Prop.closed f32sgn x+  assert $ Prop.kernel f32sgn y ++prop_prd_unsigned :: Property+prop_prd_unsigned = withTests 1000 $ property $ do+  x <- forAll gen_unsigned'+  y <- forAll gen_unsigned'+  z <- forAll gen_unsigned'+  w <- forAll gen_unsigned'++  assert $ Prop.reflexive_eq x+  assert $ Prop.reflexive_le x+  assert $ Prop.irreflexive_lt x+  assert $ Prop.symmetric x y+  assert $ Prop.asymmetric x y+  assert $ Prop.antisymmetric x y+  assert $ Prop.transitive_lt x y z+  assert $ Prop.transitive_le x y z+  assert $ Prop.transitive_eq x y z++  assert $ Prop.connex x y+  assert $ Prop.semiconnex x y+  assert $ Prop.trichotomous x y+  assert $ Prop.chain_22 x y z w+  assert $ Prop.chain_31 x y z w++prop_semiring_unsigned :: Property+prop_semiring_unsigned = withTests 1000 $ property $ do+  x <- forAll gen_unsigned'+  y <- forAll gen_unsigned'+  z <- forAll gen_unsigned'++  assert $ Prop.annihilative_multiplication x+  assert $ Prop.neutral_addition' x+  assert $ Prop.neutral_multiplication' x+  assert $ Prop.associative_addition x y z+  assert $ Prop.associative_multiplication x y z+  assert $ Prop.distributive x y z++prop_quantale_unsigned :: Property+prop_quantale_unsigned = withTests 1000 . withShrinks 0 $ property $ do+  x <- forAll gen_unsigned -- we do not require `residr pInf` etc+  y <- forAll gen_unsigned'+  z <- forAll gen_unsigned'++  --assert $ Prop.connection (residl x) y z+  assert $ Prop.connection (residr x) y z++  --assert $ Prop.monotone' (residl x) y z+  assert $ Prop.monotone' (residr x) y z++  --assert $ Prop.monotone (residl x) y z+  assert $ Prop.monotone (residr x) y z++  --assert $ Prop.closed (residl x) y+  assert $ Prop.closed (residr x) y++  --assert $ Prop.kernel (residl x) y+  assert $ Prop.kernel (residr x) y++  assert $ residuated x y z+++f32ugn :: Conn Float Unsigned+f32ugn = Conn f g where+  f x | finite x  = Unsigned $ max 0 $ x+      | otherwise = Unsigned x+  g (Unsigned x) = x++mono f x y = x <~ y ==> f x <~ f y++{-+u = Unsigned+f = id :: Float -> Float++x = u 2.3380933+y = u 6.049403++x = u 0.37794903+y = u 0.3269925++x = f 2.3380933+y = f 6.049403++x = f 0.37794903+y = f 0.3269925++counit (residl x) y+++residl x = Conn (<>x) . (//x) $ y++(//x) . (<>x) $ y++x = u 1+shift' n (Unsigned x) = Unsigned $ shift n x+xs = flip shift' x <$> [-4,-3,-2,-1,0,1,2,3,4]+fmap (cvn x) xs+y = shift' 2 x+z = shift' 4 x+Prop.transitive_eq x y z+++fmap (cvn x) xs+λ> fmap (Prop.semiconnex x) xs+[True,True,False,False,True,False,False,True,True]+λ> fmap (<~ x) xs+[True,True,False,False,True,False,False,False,False]+λ> fmap (~~ x) xs+[False,False,True,True,True,True,True,False,False]+-}++{-+prop_connection_flt32_unsigned :: Property+prop_connection_flt32_unsigned = withTests 1000 $ property $ do+  x <- forAll gen_flt32+  y <- forAll gen_unsigned+  x' <- forAll gen_flt32+  y' <- forAll gen_unsigned++  assert $ Prop.connection f32ugn x y+  assert $ Prop.monotone' f32ugn x x'+  assert $ mono (connr f32ugn) y y'+  assert $ Prop.closed f32ugn x+  assert $ Prop.kernel f32ugn y +-}++{-+prop_connection_unsigned_signed :: Property+prop_connection_unsigned_signed = withTests 10000 $ property $ do+  x <- forAll gen_unsigned+  y <- forAll gen_signed+  x' <- forAll gen_unsigned+  y' <- forAll gen_signed++  assert $ Prop.connection ugnsgn x y+  assert $ Prop.monotone' ugnsgn x x'+  assert $ Prop.monotone  ugnsgn y y'+  assert $ Prop.closed ugnsgn x+  assert $ Prop.kernel ugnsgn y +-}+++tests :: IO Bool+tests = checkParallel $$(discover)
+ test/Test/Data/Float.hs view
@@ -0,0 +1,184 @@+{-# LANGUAGE TemplateHaskell #-}+module Test.Data.Float where++import Data.Prd.Nan+import Data.Int+import Data.Word+import Data.Float+import Data.Prd+import Data.Semiring+import Data.Connection+import Data.Connection.Filter+import Data.Connection.Float+import Data.Semigroup.Quantale++import qualified Data.Prd.Property as Prop+import qualified Data.Semiring.Property as Prop+import qualified Data.Connection.Property as Prop++import Hedgehog+import qualified Hedgehog.Gen as G+import qualified Hedgehog.Range as R++ri :: (Integral a, Bounded a) => Range a+ri = R.exponentialFrom 0 minBound maxBound++rf :: Range Float+rf = R.exponentialFloatFrom 0 (-3.4028235e38) 3.4028235e38++gen_flt32' :: Gen Float+gen_flt32' = G.frequency [(99, gen_flt32), (1, G.element [nInf, pInf, aNan])] ++gen_flt32 :: Gen Float+gen_flt32 = G.float rf++gen_nan :: Gen a -> Gen (Nan a)+gen_nan gen = G.frequency [(9, Def <$> gen), (1, pure NaN)]++prop_prd_ulp32 :: Property+prop_prd_ulp32 = withTests 1000 . property $ do+  x <- connl f32u32 <$> forAll gen_flt32'+  y <- connl f32u32 <$> forAll gen_flt32'+  z <- connl f32u32 <$> forAll gen_flt32'+  assert $ Prop.reflexive_eq x+  assert $ Prop.reflexive_le x+  assert $ Prop.irreflexive_lt x+  assert $ Prop.symmetric x y+  assert $ Prop.asymmetric x y+  assert $ Prop.antisymmetric x y+  assert $ Prop.transitive_lt x y z+  assert $ Prop.transitive_le x y z+  assert $ Prop.transitive_eq x y z++prop_prd_flt32 :: Property+prop_prd_flt32 = withTests 100000 . property $ do+  x <- forAll gen_flt32'+  y <- forAll gen_flt32'+  z <- forAll gen_flt32'+  w <- forAll gen_flt32'+  assert $ Prop.reflexive_eq x+  assert $ Prop.reflexive_le x+  assert $ Prop.irreflexive_lt x+  assert $ Prop.symmetric x y+  assert $ Prop.asymmetric x y+  assert $ Prop.antisymmetric x y+  assert $ Prop.transitive_lt x y z+  assert $ Prop.transitive_le x y z+  assert $ Prop.transitive_eq x y z+  assert $ Prop.chain_22 x y z w+  --assert $ Prop.chain_31 x y z w++{-+prop_semigroup_float :: Property+prop_semigroup_float = withTests 20000 $ property $ do+  x <- forAll gen_flt32'+  y <- forAll gen_flt32'+  z <- forAll gen_flt32'++  assert $ Prop.neutral_addition' x+  assert $ Prop.associative_addition (abs x) (abs y) (abs z)+-}++prop_connections_flt32_wrd64 :: Property+prop_connections_flt32_wrd64 = withTests 1000 . property $ do+  x <- forAll gen_flt32'+  y <- forAll gen_flt32'+  x' <- forAll gen_flt32'+  y' <- forAll gen_flt32'+  z <- forAll (gen_nan $ G.integral @_ @Word64 ri)+  w <- forAll (gen_nan $ G.integral @_ @Word64 ri)+  z' <- forAll (gen_nan $ G.integral @_ @Word64 ri)+  w' <- forAll (gen_nan $ G.integral @_ @Word64 ri)+  exy <- forAll $ G.element [Left x, Right y]+  exy' <- forAll $ G.element [Left x', Right y']+  ezw <- forAll $ G.element [Left z, Right w]+  ezw' <- forAll $ G.element [Left z', Right w']++  assert $ Prop.closed (idx @Float) x+  assert $ Prop.kernel (idx @Float) z+  assert $ Prop.monotone' (idx @Float) x x'+  assert $ Prop.monotone (idx @Float) z z'+  assert $ Prop.connection (idx @Float) x z++  assert $ Prop.closed (idx @(Float,Float)) (x,y)+  assert $ Prop.kernel (idx @(Float,Float)) (z,w)+  assert $ Prop.monotone' (idx @(Float,Float)) (x,y) (x',y')+  assert $ Prop.monotone (idx @(Float,Float)) (z,w) (z',w')+  assert $ Prop.connection (idx @(Float,Float)) (x,y)(z,w)++  assert $ Prop.closed (idx @(Either Float Float)) exy+  assert $ Prop.kernel (idx @(Either Float Float)) ezw+  assert $ Prop.monotone' (idx @(Either Float Float)) exy exy'+  assert $ Prop.monotone (idx @(Either Float Float)) ezw ezw'+  assert $ Prop.connection (idx @(Either Float Float)) exy ezw++prop_connections_flt32_ulp32 :: Property+prop_connections_flt32_ulp32 = withTests 1000 . property $ do+  x <- forAll gen_flt32'+  y <- Ulp32 <$> forAll (G.integral ri)+  x' <- forAll gen_flt32'+  y' <- Ulp32 <$> forAll (G.integral ri)++  assert $ Prop.connection f32u32 x y+  assert $ Prop.connection u32f32 y x++  assert $ Prop.monotone' f32u32 x x'+  assert $ Prop.monotone' u32f32 y y'++  assert $ Prop.monotone f32u32 y y'+  assert $ Prop.monotone u32f32 x x'++  assert $ Prop.closed f32u32 x+  assert $ Prop.closed u32f32 y++  assert $ Prop.kernel u32f32 x+  assert $ Prop.kernel f32u32 y++prop_connections_flt32_int64 :: Property+prop_connections_flt32_int64 = withTests 1000 . property $ do+  x <- forAll gen_flt32'+  y <- forAll (gen_nan $ G.integral ri)+  x' <- forAll gen_flt32'+  y' <- forAll (gen_nan $ G.integral ri)+ +  assert $ Prop.connection f32i64 x y+  assert $ Prop.connection i64f32 y x++  assert $ Prop.monotone' f32i64 x x'+  assert $ Prop.monotone' i64f32 y y'++  assert $ Prop.monotone f32i64 y y'+  assert $ Prop.monotone i64f32 x x'++  assert $ Prop.closed f32i64 x+  assert $ Prop.closed i64f32 y++  assert $ Prop.kernel i64f32 x+  assert $ Prop.kernel f32i64 y+++prop_quantale_flt32 :: Property+prop_quantale_flt32 = withTests 1000 . withShrinks 0 $ property $ do+  x <- forAll gen_flt32 -- we do not require `residr pInf` etc+  y <- forAll gen_flt32'+  z <- forAll gen_flt32'++  assert $ Prop.connection (residl x) y z+  assert $ Prop.connection (residr x) y z++  assert $ Prop.monotone' (residl x) y z+  assert $ Prop.monotone' (residr x) y z++  assert $ Prop.monotone (residl x) y z+  assert $ Prop.monotone (residr x) y z++  assert $ Prop.closed (residl x) y+  assert $ Prop.closed (residr x) y++  assert $ Prop.kernel (residl x) y+  assert $ Prop.kernel (residr x) y++  assert $ residuated x y z++tests :: IO Bool+tests = checkParallel $$(discover)
+ test/test.hs view
@@ -0,0 +1,22 @@+import Control.Monad+import System.Exit (exitFailure)+import System.IO (BufferMode(..), hSetBuffering, stdout, stderr)+++import qualified Test.Data.Float as F+import qualified Test.Data.Dioid.Signed as S+import qualified Test.Data.Connection.Int as CI+import qualified Test.Data.Connection.Word as CW+++tests :: IO [Bool]+tests = sequence [S.tests] -- [CI.tests, CW.tests, F.tests] ++main :: IO ()+main = do+  hSetBuffering stdout LineBuffering+  hSetBuffering stderr LineBuffering++  results <- tests++  unless (and results) exitFailure