connections 0.3.1 → 0.3.2

raw patch · 22 files changed

+1706/−1753 lines, 22 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• ChangeLog.md +24/−7
• README.md +15/−14
• connections.cabal +2/−2
• src/Data/Connection.hs +40/−224
• src/Data/Connection/Cast.hs +634/−0
• src/Data/Connection/Class.hs +159/−231
• src/Data/Connection/Conn.hs +0/−661
• src/Data/Connection/Fixed.hs +33/−32
• src/Data/Connection/Float.hs +172/−47
• src/Data/Connection/Int.hs +90/−73
• src/Data/Connection/Property.hs +28/−28
• src/Data/Connection/Ratio.hs +19/−78
• src/Data/Connection/Time.hs +16/−16
• src/Data/Connection/Word.hs +100/−77
• src/Data/Lattice.hs +49/−49
• src/Data/Lattice/Property.hs +1/−1
• src/Data/Order/Interval.hs +2/−2
• test/Test/Data/Connection/Fixed.hs +0/−1
• test/Test/Data/Connection/Float.hs +165/−9
• test/Test/Data/Connection/Int.hs +156/−173
• test/Test/Data/Connection/Ratio.hs +0/−26
• test/doctest.hs +1/−2

@@ -1,16 +1,21 @@ # Revision history for connections -## 0.0.3  -- 2020-02-17+## 0.3.2  -- 2021-xx-xx -* `Data.Connection.Float` : float utils-* `Data.Connection.Ratio` : add rational connections+* Add left-hand float and double connections. -## 0.1.0  -- 2020-07-07+## 0.3.1  -- 2021-05-30 -* Unify `Connection` and `Triple` into a single class-* Add `Heyting`, `Symmetric`, and `Boolean` algebras-* Add misc new instances+* Add `Data.Connection.Time`.+* Add float-word connections.+* Move infix join/meet to `Data.Lattice`+* Re-organize top-level exports.+* New dependencies on `time` and `extended-reals`. +## 0.3.0  -- 2021-03-14++* Add `Data.Connection.Fixed`.+ ## 0.2.0  -- 2021-02-21  * Change integral connection instances to non-shifting behavior.@@ -20,3 +25,15 @@ * Move `<` and `>` to `Syntax.hs`. * Remove niche instances w/ upstream dependencies. * Add misc new instances.++## 0.1.0  -- 2020-07-07++* Unify `Connection` and `Triple` into a single class+* Add `Heyting`, `Symmetric`, and `Boolean` algebras+* Add misc new instances++## 0.0.3  -- 2020-02-17++* `Data.Connection.Float` : float utils+* `Data.Connection.Ratio` : add rational connections+

@@ -10,7 +10,8 @@ * [What can you do with them?](#what) * [What's wrong with the numeric conversions in `base`?](#base) -+Note that this file contains markdown syntax that doesn't render on Hackage.+A fully rendered version is hosted on Github [here](https://github.com/cmk/connections/blob/master/README.md).  ### What is a connection? <a name="intro"></a> @@ -20,7 +21,7 @@  ![](img/example.png) -Connections are useful for performing lawful conversions between different types [among other things](#what). This library provides connections between common types, combinators & accessors, including lawful versions of [`floor`](https://hackage.haskell.org/package/connections/docs/Data-Connection-Conn.html#v:floor), [`ceiling`](https://hackage.haskell.org/package/connections/docs/Data-Connection-Conn.html#v:ceiling), [`round`](https://hackage.haskell.org/package/connections/docs/Data-Connection-Conn.html#v:round), and [`truncate`](https://hackage.haskell.org/package/connections/docs/Data-Connection-Conn.html#v:truncate).+Connections are useful for performing lawful conversions between different types [among other things](#what). This library provides connections between common types, combinators & accessors, including lawful versions of [`floor`](https://hackage.haskell.org/package/connections/docs/Data-Connection-Cast.html#v:floor), [`ceiling`](https://hackage.haskell.org/package/connections/docs/Data-Connection-Cast.html#v:ceiling), [`round`](https://hackage.haskell.org/package/connections/docs/Data-Connection-Cast.html#v:round), and [`truncate`](https://hackage.haskell.org/package/connections/docs/Data-Connection-Cast.html#v:truncate).  There is also a [class](https://hackage.haskell.org/package/connections/docs/Data-Connection-Class.html#t:Connection) with lawful versions of `fromInteger` and `fromRational`, suitable for use with `-XRebindableSyntax` @@ -31,8 +32,8 @@ Let's look at a simple connection between `Ordering` and `Bool`:  ```-ordbin :: Conn 'L Ordering Bool-ordbin = ConnL f g where+ordbin :: Cast 'L Ordering Bool+ordbin = CastL f g where   f LT = False   f _  = True  @@ -55,8 +56,8 @@ Interestingly, there is a second 'flipped' connection available as well, where the same `g` can serve as the lower end:  ```-binord :: Conn 'L Bool Ordering-binord = ConnL g h where+binord :: Cast 'L Bool Ordering+binord = CastL g h where   g False = LT   g True  = GT   @@ -66,13 +67,13 @@  It turns out that this situation happens fairly frequently- the three functions are called an adjoint [string](https://ncatlab.org/nlab/show/adjoint+string) or chain of length 3 (i.e. `f` is adjoint to `g` is adjoint to `h`). It is useful to be able to work with these length-3 chains directly, because the choice of two routes back from P to Q is what enables lawful rounding and truncation.  -Therefore the connection type in `Data.Connection.Conn` is parametrized over a data kind (e.g. `'L`) that specifies which pair we are talking about (`f`/`g` or `g`/`h`). When a chain is available the data kind is existentialized (see the view pattern `Conn`).+Therefore the connection type in `Data.Connection.Cast` is parametrized over a data kind (e.g. `'L`) that specifies which pair we are talking about (`f`/`g` or `g`/`h`). When a chain is available the data kind is existentialized (see the view pattern `Cast`).  In our example above, it turns out that a small change in the adjoints on each side enables such a chain:  ```-ordbin :: Conn k Ordering Bool-ordbin = Conn f g h+ordbin :: Cast k Ordering Bool+ordbin = Cast f g h   where     f LT = False     f _  = True@@ -162,7 +163,7 @@  ``` λ> :t divide rati16 f32i16-divide rati16 f32i16 :: Conn k (Rational, Float) (Extended Int16)+divide rati16 f32i16 :: Cast k (Rational, Float) (Extended Int16) λ> maximize (divide rati16 f32i16) 2.99 3.01 Finite 4 λ> maximize (divide rati16 f32i16) 2.99 (0/0)@@ -176,11 +177,11 @@ ``` λ> :t MkSystemTime MkSystemTime :: Int64 -> Word32 -> SystemTime-λ> :t connL ratf64 >>> ratsys-connL ratf64 >>> ratsys :: Conn 'L Double (Extended SystemTime)-λ> ceiling (connL ratf64 >>> ratsys) pi+λ> :t swapL ratf64 >>> ratsys+swapL ratf64 >>> ratsys :: Cast 'L Double (Extended SystemTime)+λ> ceiling (swapL ratf64 >>> ratsys) pi Finite (MkSystemTime {systemSeconds = 3, systemNanoseconds = 141592654})-λ> diffSystemTime x y = inner (connL ratf64 >>> ratsys) $ round2 ratsys (-) (Finite x) (Finite y)+λ> diffSystemTime x y = inner (swapL ratf64 >>> ratsys) $ round2 ratsys (-) (Finite x) (Finite y) λ> :t diffSystemTime diffSystemTime :: SystemTime -> SystemTime -> Double λ> diffSystemTime (MkSystemTime 0 0) (MkSystemTime 0 maxBound)

@@ -1,5 +1,5 @@ name:                connections-version:             0.3.1+version:             0.3.2 synopsis:            Orders, Galois connections, and lattices. description:         A library for working with Galois connections on various common preorders.                      .@@ -26,7 +26,7 @@   exposed-modules:        Data.Connection-    , Data.Connection.Conn+    , Data.Connection.Cast     , Data.Connection.Class     , Data.Connection.Fixed     , Data.Connection.Float

@@ -6,10 +6,8 @@ -- -- This library provides connections between common types, combinators & accessors, -- including lawful versions of 'floor', 'ceiling', 'round', and 'truncate'. There--- is also a separately exported 'Data.Connection.Class.Connection' class, along--- with lawful versions of 'Data.Connection.Class.fromInteger' and--- 'Data.Connection.Class.fromRational', suitable for use with /-XRebindableSyntax/.--- Lastly, there are 'Data.Lattice.Semilattice' and 'Data.Lattice.Algebra' classes+-- is also a separately exported 'Data.Connection.Class.Connection' class. Lastly,+-- there are 'Data.Lattice.Semilattice' and 'Data.Lattice.Algebra' classes -- based on the same construction. -- -- /connections/ is extensively tested, and it exports properties for use in testing@@ -21,42 +19,36 @@         -- $example     -    -- * Types-    Conn,     Side(..),     -    -- ** Conn L-    ConnL,-    connL,-    pattern ConnL,-   -    -- ** Conn R-    ConnR,-    connR,-    pattern ConnR,+    -- * Types++    -- ** CastL+    castL,+    pattern CastL,     -    -- ** Conn k-    pattern Conn,+    -- ** CastR+    castR,+    pattern CastR,     -    -- * Combinators-    (>>>),-    (<<<),-    mapped,-    choice,-    select,-    strong,-    divide,+    -- ** Cast+    cast,+    pattern Cast,+    Cast,          -- * Accessors+    midpoint,+    interval,+    +    -- ** upper     upper,-    lower,-    inner,-    outer,+    upper1,+    upper2,     -    -- ** max/min-    maximize,-    minimize,-    median,+    -- ** lower+    lower,+    lower1,+    lower2,          -- ** ceiling     ceiling,@@ -78,208 +70,32 @@     truncate1,     truncate2,     -    -- * Connections-    bounded,-    ordered,-    identity,-    -    -- ** Unsigned ints-    -    -- *** Word8-    i08w08,-    f32w08,-    f64w08,-    ratw08,--    -- *** Word16-    w08w16,-    i08w16,-    i16w16,-    f32w16,-    f64w16,-    ratw16,--    -- *** Word32-    w08w32,-    w16w32,-    i08w32,-    i16w32,-    i32w32,-    f64w32,-    ratw32,--    -- *** Word64-    w08w64,-    w16w64,-    w32w64,-    i08w64,-    i16w64,-    i32w64,-    i64w64,-    ixxw64,-    ratw64,--    -- *** Word-    w08wxx,-    w16wxx,-    w32wxx,-    w64wxx,-    i08wxx,-    i16wxx,-    i32wxx,-    i64wxx,-    ixxwxx,-    ratwxx,--    -- *** Natural-    w08nat,-    w16nat,-    w32nat,-    w64nat,-    wxxnat,-    i08nat,-    i16nat,-    i32nat,-    i64nat,-    ixxnat,-    intnat,-    ratnat,-    -    -- ** Signed ints-    -    -- *** Int8-    f32i08,-    f64i08,-    rati08,-    -    -- *** Int16-    w08i16,-    i08i16,-    f32i16,-    f64i16,-    rati16,--    -- *** Int32-    w08i32,-    w16i32,-    i08i32,-    i16i32,-    f64i32,-    rati32,--    -- *** Int64-    w08i64,-    w16i64,-    w32i64,-    i08i64,-    i16i64,-    i32i64,-    rati64,--    -- *** Int-    w08ixx,-    w16ixx,-    w32ixx,-    i08ixx,-    i16ixx,-    i32ixx,-    i64ixx,-    ratixx,-    sysixx,--    -- *** Integer-    w08int,-    w16int,-    w32int,-    w64int,-    wxxint,-    natint,-    i08int,-    i16int,-    i32int,-    i64int,-    ixxint,-    f00int,-    ratint,--    -- ** Rational-    ratrat,--    -- ** Floating point- -    -- *** Float-    f32f32,-    f64f32,-    ratf32,+    -- ** max/min+    maximize,+    minimize,+    median, -    -- *** Double-    f64f64,-    ratf64,+    -- * Combinators+    (>>>),+    (<<<),+    swapL,+    swapR,+    mapped,+    choice,+    select,+    strong,+    divide,     -    -- ** Fixed point-    f32fix,-    f64fix,-    ratfix,--    -- *** Uni-    f01f00,-    f02f00,-    f03f00,-    f06f00,-    f09f00,-    f12f00,--    -- *** Deci-    f02f01,-    f03f01,-    f06f01,-    f09f01,-    f12f01,--    -- *** Centi-    f03f02,-    f06f02,-    f09f02,-    f12f02,--    -- *** Milli-    f06f03,-    f09f03,-    f12f03,--    -- *** Micro-    f09f06,-    f12f06,--    -- *** Nano-    f12f09,--    -- ** Time--    -- *** SystemTime-    f32sys,-    f64sys,-    f09sys,-    ratsys,-     -- * Extended     extended,     Extended (..),  ) where -import safe Data.Connection.Conn-import safe Data.Connection.Fixed-import safe Data.Connection.Float-import safe Data.Connection.Int-import safe Data.Connection.Ratio-import safe Data.Connection.Time-import safe Data.Connection.Word-+import safe Data.Connection.Cast+import safe Data.Connection.Class import safe Prelude hiding (ceiling, floor, round, truncate) --  {- $example    ==== What is a Galois connection?

@@ -0,0 +1,634 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE Safe #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE ViewPatterns #-}++module Data.Connection.Cast (+    -- * Cast+    Side (..),+    Cast (),+    (>>>),+    (<<<),+    mapped,+    choice,+    select,+    strong,+    divide,+    bounded,+    ordered,+    identity,++    -- * Cast 'L+    pattern CastL,+    swapL,+    upper,+    upper1,+    upper2,+    ceiling,+    ceiling1,+    ceiling2,+    maximize,++    -- * Cast 'R+    pattern CastR,+    swapR,+    lower,+    lower1,+    lower2,+    floor,+    floor1,+    floor2,+    minimize,++    -- * Cast k+    pattern Cast,+    midpoint,+    interval,+    round,+    round1,+    round2,+    truncate,+    truncate1,+    truncate2,+    median,++    -- * Down+    upL,+    upR,+    downL,+    downR,+    filterL,+    filterR,++    -- * Extended+    extend,+    extended,+    Extended (..),+) where++import safe Control.Arrow ((&&&))+import safe Control.Category (Category, (<<<), (>>>))+import safe qualified Control.Category as C+import safe Data.Bifunctor (bimap)+import safe Data.ExtendedReal+import safe Data.Order+import safe Prelude hiding (ceiling, floor, round, truncate)++-- $setup+-- >>> :set -XTypeApplications+-- >>> import Control.Arrow ((&&&))+-- >>> import Data.Int+-- >>> import Data.Ord (Down(..))+-- >>> import Data.Ratio ((%))+-- >>> import GHC.Real (Ratio(..))+-- >>> import Data.Connection.Cast+-- >>> import Data.Connection.Float+-- >>> import Data.Connection.Ratio+-- >>> import Prelude hiding (floor, ceiling, round, truncate)+++-- | A data kind distinguishing links in a < https://ncatlab.org/nlab/show/adjoint+string chain > of Galois connections of length 2 or 3.+--+-- * /L/-tagged types are increasing (e.g. 'Data.Connection.Cast.ceiling', 'Data.Connection.Cast.maximize')+--+-- * /R/-tagged types are decreasing (e.g. 'Data.Connection.Cast.floor', 'Data.Connection.Cast.minimize')+--+--  If a connection is existentialized over this value (i.e. has type /forall k. Cast k a b/) then it can+--  provide either of two functions /f, h :: a -> b/.+--+--  This is useful because it enables rounding, truncation, medians, etc. +--+data Side = L | R++-- | A < https://ncatlab.org/nlab/show/adjoint+string chain > of Galois connections of length 2 or 3.+--+-- Connections have many nice properties wrt numerical conversion:+--+-- >>> upper ratf32 (1 / 8)    -- eighths are exactly representable in a float+-- 1 % 8+-- >>> upper ratf32 (1 / 7)    -- sevenths are not+-- 9586981 % 67108864+-- >>> floor ratf32 &&& ceiling ratf32 $ 1 % 8+-- (0.125,0.125)+-- >>> floor ratf32 &&& ceiling ratf32 $ 1 % 7+-- (0.14285713,0.14285715)+--+-- Another example avoiding loss-of-precision:+--+-- >>> f x y = (x + y) - x+-- >>> maxOdd32 = 1.6777215e7+-- >>> f maxOdd32 2.0 :: Float+-- 1.0+-- >>> round2 f64f32 f maxOdd32 2.0+-- 2.0+data Cast (k :: Side) a b = Cast_ (a -> (b, b)) (b -> a)++instance Category (Cast k) where+    id = identity+    {-# INLINE id #-}++    Cast_ f1 g1 . Cast_ f2 g2 = Cast_ ((fst . f1) . (fst . f2) &&& (snd . f1) . (snd . f2)) (g2 . g1)+    {-# INLINE (.) #-}++-- Internal floor function. When \(f \dashv g \dashv h \) this is h.+_1 :: Cast k a b -> a -> b+_1 (Cast_ f _) = fst . f+{-# INLINE _1 #-}++-- Internal ceiling function. When \(f \dashv g \dashv h \) this is f.+_2 :: Cast k a b -> a -> b+_2 (Cast_ f _) = snd . f+{-# INLINE _2 #-}++-- Extract the upper adjoint of a 'CastL', or lower adjoint of a 'CastR'.+inner :: Cast k a b -> b -> a+inner (Cast_ _ g) = g+{-# INLINE inner #-}++-- | Lift a 'Cast' into a functor.+--+-- /Caution/: This function will result in an invalid connection+-- if the functor alters the internal preorder (e.g. 'Data.Ord.Down').+mapped :: Functor f => Cast k a b -> Cast k (f a) (f b)+mapped (Cast f g h) = Cast (fmap f) (fmap g) (fmap h)+{-# INLINE mapped #-}++-- | Lift two connections into a connection on the <https://en.wikibooks.org/wiki/Category_Theory/Categories_of_ordered_sets coproduct order>+--+-- > (choice id) (ab >>> cd) = (choice id) ab >>> (choice id) cd+-- > (flip choice id) (ab >>> cd) = (flip choice id) ab >>> (flip choice id) cd+choice :: Cast k a b -> Cast k c d -> Cast k (Either a c) (Either b d)+choice (Cast ab ba ab') (Cast cd dc cd') = Cast f g h+  where+    f = either (Left . ab) (Right . cd)+    g = either (Left . ba) (Right . dc)+    h = either (Left . ab') (Right . cd')+{-# INLINE choice #-}++infixr 3 `select`++-- | Lift two connections into a connection on the <https://en.wikibooks.org/wiki/Category_Theory/Categories_of_ordered_sets coproduct order>+select :: Cast k c a -> Cast k c b -> Cast k c (Either a b)+select f g = Cast Left (either id id) Right >>> f `choice` g++-- | Lift two connections into a connection on the <https://en.wikibooks.org/wiki/Order_Theory/Preordered_classes_and_poclasses#product_order product order>+--+-- > (strong id) (ab >>> cd) = (strong id) ab >>> (strong id) cd+-- > (flip strong id) (ab >>> cd) = (flip strong id) ab >>> (flip strong id) cd+strong :: Cast k a b -> Cast k c d -> Cast k (a, c) (b, d)+strong (Cast ab ba ab') (Cast cd dc cd') = Cast f g h+  where+    f = bimap ab cd+    g = bimap ba dc+    h = bimap ab' cd'+{-# INLINE strong #-}++infixr 4 `divide`++-- | Lift two connections into a connection on the <https://en.wikibooks.org/wiki/Order_Theory/Preordered_classes_and_poclasses#product_order product order>+divide :: Ord c => Cast k a c -> Cast k b c -> Cast k (a, b) c+divide f g = f `strong` g >>> ordered+{-# INLINE divide #-}++-- | The defining connections of a bounded preorder.+bounded :: Bounded a => Cast k () a+bounded = Cast (const minBound) (const ()) (const maxBound)+{-# INLINE bounded #-}++-- | The defining connections of a total order.+--+-- >>> floor ordered &&& ceiling ordered $ (True, False)+-- (False,True)+ordered :: Ord a => Cast k (a, a) a+ordered = Cast (uncurry max) (id &&& id) (uncurry min)+{-# INLINE ordered #-}++-- | The identity connection.+identity :: Cast k a a+identity = Cast_ (id &&& id) id+{-# INLINE identity #-}++---------------------------------------------------------------------+-- Cast 'L+---------------------------------------------------------------------++-- | A <https://ncatlab.org/nlab/show/Galois+connection Galois connection> between two monotone functions.+--+-- A Galois connection between /f/ and /g/, written \(f \dashv g \)+-- is an adjunction in the category of preorders.+--+-- Each side of the connection may be defined in terms of the other:+--+--  \( g(x) = \sup \{y \in E \mid f(y) \leq x \} \)+--+--  \( f(x) = \inf \{y \in E \mid g(y) \geq x \} \)+--+-- /Caution/: /CastL f g/ must obey \(f \dashv g \). This condition is not checked.+--+-- For further information see 'Data.Connection.Property'.+pattern CastL :: (a -> b) -> (b -> a) -> Cast 'L a b+pattern CastL f g <- (_2 &&& upper -> (f, g)) where CastL f g = Cast_ (f &&& f) g++{-# COMPLETE CastL #-}++-- | Witness to the mirror symmetry between 'CastL' and 'CastR'.+--+-- > swapL . swapR = id+-- > swapR . swapL = id+swapL :: Cast 'R a b -> Cast 'L b a+swapL (CastR f g) = CastL f g+{-# INLINE swapL #-}++-- | Extract the upper half of a 'CastL'.+--+-- >>> upper ratf32 (1 / 8)    -- eighths are exactly representable in a float+-- 1 % 8+-- >>> upper ratf32 (1 / 7)    -- sevenths are not+-- 9586981 % 67108864+upper :: Cast 'L a b -> b -> a+upper = inner+{-# INLINE upper #-}++-- | Map over a 'CastL' from the right.+--+-- This is the unit of the resulting monad:+--+-- > x <~ upper1 c id x+--+-- >>> compare pi $ upper1 f64f32 id pi+-- LT+upper1 :: Cast 'L a b -> (b -> b) -> a -> a+upper1 (CastL f g) h a = g $ h (f a)+{-# INLINE upper1 #-}++-- | Zip over a 'CastL' from the right.+upper2 :: Cast 'L a b -> (b -> b -> b) -> a -> a -> a+upper2 (CastL f g) h a1 a2 = g $ h (f a1) (f a2)+{-# INLINE upper2 #-}++-- | Extract the lower half of a 'CastL'.+--+-- > ceiling identity = id+-- > ceiling c (x \/ y) = ceiling c x \/ ceiling c y+--+-- The latter law is the adjoint functor theorem for preorders.+--+-- >>> ceiling ratf32 (0 :% 0)+-- NaN+-- >>> ceiling ratf32 (13 :% 10)+-- 1.3000001+-- >>> ceiling f64f32 pi+-- 3.1415927+ceiling :: Cast 'L a b -> a -> b+ceiling (CastL f _) = f+{-# INLINE ceiling #-}++-- | Map over a 'CastL' from the left.+--+-- > ceiling1 identity = id+--+-- This is the counit of the resulting comonad:+--+-- > x >~ ceiling1 c id x+--+ceiling1 :: Cast 'L a b -> (a -> a) -> b -> b+ceiling1 (CastL f g) h b = f $ h (g b)+{-# INLINE ceiling1 #-}++-- | Zip over a 'CastL' from the left.+ceiling2 :: Cast 'L a b -> (a -> a -> a) -> b -> b -> b+ceiling2 (CastL f g) h b1 b2 = f $ h (g b1) (g b2)+{-# INLINE ceiling2 #-}++-- | Generalized maximum.+maximize :: Cast 'L (a, b) c -> a -> b -> c+maximize = curry . ceiling+{-# INLINE maximize #-}++---------------------------------------------------------------------+-- Cast 'R+---------------------------------------------------------------------++-- | A Galois connection between two monotone functions.+--+-- 'CastR' is the mirror image of 'CastL'.+--+-- If you only require one connection there is no particular reason to+-- use one version over the other. However many use cases (e.g. rounding)+-- require an adjoint triple of connections that can lower into a standard+-- connection in either of two ways.+--+-- /Caution/: /CastR f g/ must obey \(f \dashv g \). This condition is not checked.+--+-- For further information see 'Data.Connection.Property'.+pattern CastR :: (b -> a) -> (a -> b) -> Cast 'R a b+pattern CastR f g <- (lower &&& _1 -> (f, g)) where CastR f g = Cast_ (g &&& g) f++{-# COMPLETE CastR #-}++-- | Witness to the mirror symmetry between 'CastL' and 'CastR'.+--+-- > swapL . swapR = id+-- > swapR . swapL = id+swapR :: Cast 'L a b -> Cast 'R b a+swapR (CastL f g) = CastR f g+{-# INLINE swapR #-}++-- | Extract the lower half of a 'CastR'.+lower :: Cast 'R a b -> b -> a+lower = inner+{-# INLINE lower #-}++-- | Map over a 'CastR' from the left.+--+-- This is the counit of the resulting comonad:+--+-- > x >~ lower1 c id x+--+-- >>> compare pi $ lower1 f64f32 id pi+-- GT+lower1 :: Cast 'R a b -> (b -> b) -> a -> a+lower1 (CastR f g) h a = f $ h (g a)+{-# INLINE lower1 #-}++-- | Zip over a 'CastR' from the left.+lower2 :: Cast 'R a b -> (b -> b -> b) -> a -> a -> a+lower2 (CastR f g) h a1 a2 = f $ h (g a1) (g a2)+{-# INLINE lower2 #-}++-- | Extract the upper half of a 'CastR'+--+-- > floor identity = id+-- > floor c (x /\ y) = floor c x /\ floor c y+--+-- The latter law is the adjoint functor theorem for preorders.+--+-- >>> floor ratf32 (0 :% 0)+-- NaN+-- >>> floor ratf32 (13 :% 10)+-- 1.3+-- >>> floor f64f32 pi+-- 3.1415925+floor :: Cast 'R a b -> a -> b+floor (CastR _ g) = g+{-# INLINE floor #-}++-- | Map over a 'CastR' from the right.+--+-- > floor1 identity = id+--+-- This is the unit of the resulting monad:+--+-- > x <~ floor1 c id x+--+floor1 :: Cast 'R a b -> (a -> a) -> b -> b+floor1 (CastR f g) h b = g $ h (f b)+{-# INLINE floor1 #-}++-- | Zip over a 'CastR' from the right.+floor2 :: Cast 'R a b -> (a -> a -> a) -> b -> b -> b+floor2 (CastR f g) h b1 b2 = g $ h (f b1) (f b2)+{-# INLINE floor2 #-}++-- | Generalized minimum.+minimize :: Cast 'R (a, b) c -> a -> b -> c+minimize = curry . floor+{-# INLINE minimize #-}++---------------------------------------------------------------------+-- Cast k+---------------------------------------------------------------------++-- | An <https://ncatlab.org/nlab/show/adjoint+triple adjoint triple> of Galois connections.+--+-- An adjoint triple is a chain of connections of length 3:+--+-- \(f \dashv g \dashv h \)+--+-- When applied to a 'CastL' or 'CastR', the two functions of type @a -> b@ returned will be identical.+--+-- /Caution/: /Cast f g h/ must obey \(f \dashv g \dashv h\). This condition is not checked.+--+-- For detailed properties see 'Data.Connection.Property'.+pattern Cast :: (a -> b) -> (b -> a) -> (a -> b) -> Cast k a b+pattern Cast f g h <- (inner &&& _1 &&& _2 -> (g, (h, f))) where Cast f g h = Cast_ (h &&& f) g++{-# COMPLETE Cast #-}++-- | Determine which half of the interval between 2 representations of /a/ a particular value lies.+--+-- @ 'interval' c x = 'pcompare' (x - 'lower1' c 'id' x) ('upper1' c 'id' x - x) @+--+-- >>> maybe False (== EQ) $ interval f64f32 (midpoint f64f32 pi)+-- True+interval :: (Num a, Preorder a) => (forall k. Cast k a b) -> a -> Maybe Ordering+interval c x = pcompare (x - lower1 c id x) (upper1 c id x - x)+{-# INLINE interval #-}++-- | Return the midpoint of the interval containing x.+--+-- For example, the (double-precision) error of the single-precision floating+-- point approximation of pi is:+--+-- >>> pi - midpoint f64f32 pi+-- 3.1786509424591713e-8+midpoint :: Fractional a => (forall k. Cast k a b) -> a -> a+midpoint c x = lower1 c id x / 2 + upper1 c id x / 2+{-# INLINE midpoint #-}++-- | Return the nearest value to x.+--+-- > round identity = id+--+-- If x lies halfway between two finite values, then return the value+-- with the smaller absolute value (i.e. round towards from zero).+--+-- See <https://en.wikipedia.org/wiki/Rounding>.+round :: (Num a, Preorder a) => (forall k. Cast k a b) -> a -> b+round c x = case interval c x of+    Just GT -> ceiling c x+    Just LT -> floor c x+    _ -> truncate c x+{-# INLINE round #-}++-- | Lift a unary function over an adjoint triple.+--+-- > round1 identity = id+--+-- Results are rounded to the nearest value with ties away from 0.+round1 :: (Num a, Preorder a) => (forall k. Cast k a b) -> (a -> a) -> b -> b+round1 c f x = round c $ f (inner c x)+{-# INLINE round1 #-}++-- | Lift a binary function over an adjoint triple.+--+-- > round2 identity = id+--+-- Results are rounded to the nearest value with ties away from 0.+--+-- For example, to avoid a loss of precision:+--+-- >>> f x y = (x + y) - x+-- >>> maxOdd32 = 1.6777215e7+-- >>> f maxOdd32 2.0 :: Float+-- 1.0+-- >>> round2 ratf32 f maxOdd32 2.0+-- 2.0+round2 :: (Num a, Preorder a) => (forall k. Cast k a b) -> (a -> a -> a) -> b -> b -> b+round2 c f x y = round c $ f (inner c x) (inner c y)+{-# INLINE round2 #-}++-- | Truncate towards zero.+--+-- > truncate identity = id+truncate :: (Num a, Preorder a) => (forall k. Cast k a b) -> a -> b+truncate c x = if x >~ 0 then floor c x else ceiling c x+{-# INLINE truncate #-}++-- | Lift a unary function over an adjoint triple.+--+-- > truncate1 identity = id+--+-- Results are truncated towards zero.+truncate1 :: (Num a, Preorder a) => (forall k. Cast k a b) -> (a -> a) -> b -> b+truncate1 c f x = truncate c $ f (inner c x)+{-# INLINE truncate1 #-}++-- | Lift a binary function over an adjoint triple.+--+-- > truncate2 identity = id+--+-- Results are truncated towards zero.+truncate2 :: (Num a, Preorder a) => (forall k. Cast k a b) -> (a -> a -> a) -> b -> b -> b+truncate2 c f x y = truncate c $ f (inner c x) (inner c y)+{-# INLINE truncate2 #-}++-- | Birkoff's < https://en.wikipedia.org/wiki/Median_algebra median > operator.+--+-- > 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 f32f32 1.0 9.0 7.0+-- 7.0+-- >>> median f32f32 1.0 9.0 (0.0 / 0.0)+-- 9.0+median :: (forall k. Cast k (a, a) a) -> a -> a -> a -> a+median c x y z = (x `join` y) `meet` (y `join` z) `meet` (z `join` x)+  where+    join = maximize c+    meet = minimize c+{-# INLINE median #-}++---------------------------------------------------------------------+-- Down+---------------------------------------------------------------------++-- | Invert a 'Cast'.+--+-- > upL . downL = downL . upL = id+upL :: Cast 'L (Down a) (Down b) -> Cast 'L b a+upL (CastL f g) = CastL g' f'+  where+    f' x = let (Down y) = f (Down x) in y+    g' x = let (Down y) = g (Down x) in y+{-# INLINE upL #-}++-- | Invert a 'Cast'.+--+-- > upR . downR = downR . upR = id+upR :: Cast 'R (Down a) (Down b) -> Cast 'R b a+upR (CastR f g) = CastR g' f'+  where+    f' x = let (Down y) = f (Down x) in y+    g' x = let (Down y) = g (Down x) in y+{-# INLINE upR #-}++-- | Invert a 'Cast'.+--+-- >>> let counit = upper1 (downL $ bounded @Ordering) id+-- >>> counit (Down LT)+-- Down LT+-- >>> counit (Down GT)+-- Down LT+downL :: Cast 'L a b -> Cast 'L (Down b) (Down a)+downL (CastL f g) = CastL (\(Down x) -> Down $ g x) (\(Down x) -> Down $ f x)+{-# INLINE downL #-}++-- | Invert a 'Cast'.+--+-- >>> let unit = lower1 (downR $ bounded @Ordering) id+-- >>> unit (Down LT)+-- Down GT+-- >>> unit (Down GT)+-- Down GT+downR :: Cast 'R a b -> Cast 'R (Down b) (Down a)+downR (CastR f g) = CastR (\(Down x) -> Down $ g x) (\(Down x) -> Down $ f x)+{-# INLINE downR #-}++-- | Obtain the principal filter in /B/ generated by an element of /A/.+--+-- A subset /B/ of a lattice is an filter if and only if it is an upper set+-- that is closed under finite meets, i.e., it is nonempty and for all+-- /x/, /y/ in /B/, the element @meet c x y@ is also in /b/.+--+-- /filterL/ and /filterR/ commute with /Down/:+--+-- > filterL c a b <=> filterR c (Down a) (Down b)+--+-- > filterL c (Down a) (Down b) <=> filterR c a b+--+-- /filterL c a/ is upward-closed for all /a/:+--+-- > a <= b1 && b1 <= b2 => a <= b2+-- > a1 <= b && a2 <= b => minimize c (ceiling c a1) (ceiling c a2) <= b+--+-- See <https://en.wikipedia.org/wiki/Filter_(mathematics)>+filterL :: Preorder b => Cast 'L a b -> a -> b -> Bool+filterL c a b = ceiling c a <~ b+{-# INLINE filterL #-}++-- | Obtain the principal ideal in /B/ generated by an element of /A/.+--+-- A subset /B/ of a lattice is an ideal if and only if it is a lower set+-- that is closed under finite joins, i.e., it is nonempty and for all+-- /x/, /y/ in /B/, the element /join c x y/ is also in /B/.+--+-- /filterR c a/ is downward-closed for all /a/:+--+-- > a >= b1 && b1 >= b2 => a >= b2+--+-- > a1 >= b && a2 >= b => maximize c (floor c a1) (floor c a2) >= b+--+-- See <https://en.wikipedia.org/wiki/Ideal_(order_theory)>+filterR :: Preorder b => Cast 'R a b -> a -> b -> Bool+filterR c a b = b <~ floor c a+{-# INLINE filterR #-}++---------------------------------------------------------------------+-- Extended+---------------------------------------------------------------------++{-# INLINE extend #-}+extend :: (a -> Bool) -> (a -> Bool) -> (a -> b) -> a -> Extended b+extend p q f = g+  where+    g i+        | p i = NegInf+        | q i = PosInf+        | otherwise = Finite $ f i++-- | Eliminate an 'Extended'.+{-# INLINE extended #-}+extended :: b -> b -> (a -> b) -> Extended a -> b+extended b _ _ NegInf = b+extended _ t _ PosInf = t+extended _ _ f (Finite x) = f x

@@ -1,291 +1,219 @@-{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-}+{-# LANGUAGE KindSignatures #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE KindSignatures #-} {-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE PatternSynonyms #-}-{-# LANGUAGE RankNTypes #-} {-# LANGUAGE Safe #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-}-{-# LANGUAGE ViewPatterns #-}  module Data.Connection.Class (-    Left,-    left,-    Right,-    right,-    Triple,-    ConnInteger,-    fromInteger,-    ConnRational,-    fromRational,+    castL,+    castR,     Connection (..), ) where -import safe Control.Category ((>>>))-import safe Data.Connection.Conn+import safe Data.Connection.Cast import safe Data.Connection.Fixed import safe Data.Connection.Float import safe Data.Connection.Int import safe Data.Connection.Ratio import safe Data.Connection.Time import safe Data.Connection.Word-import safe Data.Functor.Identity import safe Data.Int-import safe Data.Order import safe Data.Word import safe Numeric.Natural-import safe Prelude hiding (ceiling, floor, fromInteger, fromRational, round, truncate) --- | A < https://ncatlab.org/nlab/show/adjoint+string chain > of Galois connections of length 2 or 3.-class (Preorder a, Preorder b) => Connection k a b where-    -    conn :: Conn k a b--type Left = Connection 'L---- | A specialization of /conn/ to left-side connections.-left :: Left a b => ConnL a b-left = conn @ 'L--type Right = Connection 'R---- | A specialization of /conn/ to right-side connections.-right :: Right a b => ConnR a b-right = conn @ 'R---- | A constraint kind representing an <https://ncatlab.org/nlab/show/adjoint+triple adjoint triple> of Galois connections.-type Triple a b = (Left a b, Right a b)---- | A constraint kind for 'Integer' conversions.-type ConnInteger a = Left a (Maybe Integer)---- | A replacement for the version in /base/.------  Usable in conjunction with /RebindableSyntax/:-fromInteger :: ConnInteger a => Integer -> a-fromInteger = upper conn . Just+castL :: Connection 'L a b => Cast 'L a b+castL = cast @'L --- | A constraint kind for 'Rational' conversions.-type ConnRational a = Triple Rational a+castR :: Connection 'R a b => Cast 'R a b+castR = cast @'R --- | A replacement for the version in /base/.------ Usable in conjunction with /RebindableSyntax/:-fromRational :: forall a. ConnRational a => Rational -> a-fromRational x = case pcompare r l of-    Just GT -> ceiling left x-    Just LT -> floor right x-    _ -> if x >~ 0 then floor right x else ceiling left x-  where-    r = x - lower1 (right @Rational @a) id x -- dist from lower bound-    l = upper1 (left @Rational @a) id x - x -- dist from upper bound-{-# INLINE fromRational #-}+-- | A < https://ncatlab.org/nlab/show/adjoint+string chain > of Galois connections of length 2 or 3.+class Connection (k :: Side) a b where+    cast :: Cast k a b  --------------------------------------------------------------------- -- Instances --------------------------------------------------------------------- -instance Preorder a => Connection k a a where conn = identity--instance Connection k Ordering Bool where conn = bounds'-instance Connection k Word8 Bool where conn = bounds'-instance Connection k Word16 Bool where conn = bounds'-instance Connection k Word32 Bool where conn = bounds'-instance Connection k Word64 Bool where conn = bounds'-instance Connection k Word Bool where conn = bounds'-instance Connection k Int8 Bool where conn = bounds'-instance Connection k Int16 Bool where conn = bounds'-instance Connection k Int32 Bool where conn = bounds'-instance Connection k Int64 Bool where conn = bounds'-instance Connection k Int Bool where conn = bounds'-instance Connection k Rational Bool where conn = bounds (-1 :% 0) (1 :% 0)-instance Connection k Float Bool where conn = bounds (-1 / 0) (1 / 0)-instance Connection k Double Bool where conn = bounds (-1 / 0) (1 / 0)--instance Connection 'L Int8 Word8 where conn = i08w08--instance Connection 'L Word8 Word16 where conn = w08w16-instance Connection 'L Int8 Word16 where conn = i08w16-instance Connection 'L Int16 Word16 where conn = i16w16--instance Connection 'L Word8 Word32 where conn = w08w32-instance Connection 'L Word16 Word32 where conn = w16w32-instance Connection 'L Int8 Word32 where conn = i08w32-instance Connection 'L Int16 Word32 where conn = i16w32-instance Connection 'L Int32 Word32 where conn = i32w32--instance Connection 'L Word8 Word64 where conn = w08w64-instance Connection 'L Word16 Word64 where conn = w16w64-instance Connection 'L Word32 Word64 where conn = w32w64-instance Connection 'L Int8 Word64 where conn = i08w64-instance Connection 'L Int16 Word64 where conn = i16w64-instance Connection 'L Int32 Word64 where conn = i32w64-instance Connection 'L Int64 Word64 where conn = i64w64-instance Connection 'L Int Word64 where conn = ixxw64+instance Connection k a a where cast = identity -instance Connection 'L Word8 Word where conn = w08wxx-instance Connection 'L Word16 Word where conn = w16wxx-instance Connection 'L Word32 Word where conn = w32wxx-instance Connection k Word64 Word where conn = w64wxx-instance Connection 'L Int8 Word where conn = i08wxx-instance Connection 'L Int16 Word where conn = i16wxx-instance Connection 'L Int32 Word where conn = i32wxx-instance Connection 'L Int64 Word where conn = i64wxx-instance Connection 'L Int Word where conn = ixxwxx+instance Connection k Ordering Bool where cast = bndbin+instance Connection k Word8 Bool where cast = bndbin+instance Connection k Word16 Bool where cast = bndbin+instance Connection k Word32 Bool where cast = bndbin+instance Connection k Word64 Bool where cast = bndbin+instance Connection k Word Bool where cast = bndbin+instance Connection k Int8 Bool where cast = bndbin+instance Connection k Int16 Bool where cast = bndbin+instance Connection k Int32 Bool where cast = bndbin+instance Connection k Int64 Bool where cast = bndbin+instance Connection k Int Bool where cast = bndbin -instance Connection 'L Word8 Natural where conn = w08nat-instance Connection 'L Word16 Natural where conn = w16nat-instance Connection 'L Word32 Natural where conn = w32nat-instance Connection 'L Word64 Natural where conn = w64nat-instance Connection 'L Word Natural where conn = wxxnat-instance Connection 'L Int8 Natural where conn = i08nat-instance Connection 'L Int16 Natural where conn = i16nat-instance Connection 'L Int32 Natural where conn = i32nat-instance Connection 'L Int64 Natural where conn = i64nat-instance Connection 'L Int Natural where conn = ixxnat-instance Connection 'L Integer Natural where conn = intnat+instance Connection 'L Int8 Word8 where cast = i08w08 -instance Connection k Uni Integer where conn = f00int+instance Connection 'L Word8 Word16 where cast = w08w16+instance Connection 'L Int8 Word16 where cast = i08w16+instance Connection 'L Int16 Word16 where cast = i16w16 -instance Connection k Deci Uni where conn = f01f00-instance Connection k Centi Uni where conn = f02f00-instance Connection k Milli Uni where conn = f03f00-instance Connection k Micro Uni where conn = f06f00-instance Connection k Nano Uni where conn = f09f00-instance Connection k Pico Uni where conn = f12f00+instance Connection 'L Word8 Word32 where cast = w08w32+instance Connection 'L Word16 Word32 where cast = w16w32+instance Connection 'L Int8 Word32 where cast = i08w32+instance Connection 'L Int16 Word32 where cast = i16w32+instance Connection 'L Int32 Word32 where cast = i32w32 -instance Connection k Centi Deci where conn = f02f01-instance Connection k Milli Deci where conn = f03f01-instance Connection k Micro Deci where conn = f06f01-instance Connection k Nano Deci where conn = f09f01-instance Connection k Pico Deci where conn = f12f01+instance Connection 'L Word8 Word64 where cast = w08w64+instance Connection 'L Word16 Word64 where cast = w16w64+instance Connection 'L Word32 Word64 where cast = w32w64+instance Connection k Word Word64 where cast = wxxw64+instance Connection 'L Int8 Word64 where cast = i08w64+instance Connection 'L Int16 Word64 where cast = i16w64+instance Connection 'L Int32 Word64 where cast = i32w64+instance Connection 'L Int64 Word64 where cast = i64w64+instance Connection 'L Int Word64 where cast = ixxw64 -instance Connection k Milli Centi where conn = f03f02-instance Connection k Micro Centi where conn = f06f02-instance Connection k Nano Centi where conn = f09f02-instance Connection k Pico Centi where conn = f12f02+instance Connection 'L Word8 Word where cast = w08wxx+instance Connection 'L Word16 Word where cast = w16wxx+instance Connection 'L Word32 Word where cast = w32wxx+instance Connection k Word64 Word where cast = w64wxx+instance Connection 'L Int8 Word where cast = i08wxx+instance Connection 'L Int16 Word where cast = i16wxx+instance Connection 'L Int32 Word where cast = i32wxx+instance Connection 'L Int64 Word where cast = i64wxx+instance Connection 'L Int Word where cast = ixxwxx -instance Connection k Micro Milli where conn = f06f03-instance Connection k Nano Milli where conn = f09f03-instance Connection k Pico Milli where conn = f12f03+instance Connection 'L Word8 Natural where cast = w08nat+instance Connection 'L Word16 Natural where cast = w16nat+instance Connection 'L Word32 Natural where cast = w32nat+instance Connection 'L Word64 Natural where cast = w64nat+instance Connection 'L Word Natural where cast = wxxnat+instance Connection 'L Int8 Natural where cast = i08nat+instance Connection 'L Int16 Natural where cast = i16nat+instance Connection 'L Int32 Natural where cast = i32nat+instance Connection 'L Int64 Natural where cast = i64nat+instance Connection 'L Int Natural where cast = ixxnat+instance Connection 'L Integer Natural where cast = intnat -instance Connection k Nano Micro where conn = f09f06-instance Connection k Pico Micro where conn = f12f06+instance Connection k Uni Integer where cast = f00int -instance Connection k Pico Nano where conn = f12f09+instance Connection k Deci Uni where cast = f01f00+instance Connection k Centi Uni where cast = f02f00+instance Connection k Milli Uni where cast = f03f00+instance Connection k Micro Uni where cast = f06f00+instance Connection k Nano Uni where cast = f09f00+instance Connection k Pico Uni where cast = f12f00 -instance Connection k Double Float where conn = f64f32-instance Connection k Rational Float where conn = ratf32+instance Connection k Centi Deci where cast = f02f01+instance Connection k Milli Deci where cast = f03f01+instance Connection k Micro Deci where cast = f06f01+instance Connection k Nano Deci where cast = f09f01+instance Connection k Pico Deci where cast = f12f01 -instance Connection k Rational Double where conn = ratf64+instance Connection k Milli Centi where cast = f03f02+instance Connection k Micro Centi where cast = f06f02+instance Connection k Nano Centi where cast = f09f02+instance Connection k Pico Centi where cast = f12f02 -instance Connection 'L Word8 (Maybe Int16) where conn = w08i16-instance Connection 'L Int8 (Maybe Int16) where conn = i08i16+instance Connection k Micro Milli where cast = f06f03+instance Connection k Nano Milli where cast = f09f03+instance Connection k Pico Milli where cast = f12f03 -instance Connection 'L Word8 (Maybe Int32) where conn = w08i32-instance Connection 'L Word16 (Maybe Int32) where conn = w16i32-instance Connection 'L Int8 (Maybe Int32) where conn = i08i32-instance Connection 'L Int16 (Maybe Int32) where conn = i16i32+instance Connection k Nano Micro where cast = f09f06+instance Connection k Pico Micro where cast = f12f06 -instance Connection 'L Word8 (Maybe Int64) where conn = w08i64-instance Connection 'L Word16 (Maybe Int64) where conn = w16i64-instance Connection 'L Word32 (Maybe Int64) where conn = w32i64-instance Connection 'L Int8 (Maybe Int64) where conn = i08i64-instance Connection 'L Int16 (Maybe Int64) where conn = i16i64-instance Connection 'L Int32 (Maybe Int64) where conn = i32i64+instance Connection k Pico Nano where cast = f12f09 -instance Connection 'L Word8 (Maybe Int) where conn = w08ixx-instance Connection 'L Word16 (Maybe Int) where conn = w16ixx-instance Connection 'L Word32 (Maybe Int) where conn = w32ixx-instance Connection 'L Int8 (Maybe Int) where conn = i08ixx-instance Connection 'L Int16 (Maybe Int) where conn = i16ixx-instance Connection 'L Int32 (Maybe Int) where conn = i32ixx-instance Connection k Int64 Int where conn = i64ixx-instance Connection k SystemTime Int where conn = sysixx+instance Connection k Double Float where cast = f64f32+instance Connection k Rational Float where cast = ratf32 -instance Connection 'L Word8 (Maybe Integer) where conn = w08int-instance Connection 'L Word16 (Maybe Integer) where conn = w16int-instance Connection 'L Word32 (Maybe Integer) where conn = w32int-instance Connection 'L Word64 (Maybe Integer) where conn = w64int-instance Connection 'L Word (Maybe Integer) where conn = wxxint-instance Connection 'L Natural (Maybe Integer) where conn = natint+instance Connection k Rational Double where cast = ratf64 -instance Connection 'L Int8 (Maybe Integer) where conn = i08int-instance Connection 'L Int16 (Maybe Integer) where conn = i16int-instance Connection 'L Int32 (Maybe Integer) where conn = i32int-instance Connection 'L Int64 (Maybe Integer) where conn = i64int-instance Connection 'L Int (Maybe Integer) where conn = ixxint+instance Connection k (Extended Word8) Int16 where cast = w08i16+instance Connection k (Extended Int8) Int16 where cast = i08i16 -instance Connection 'L Integer (Maybe Integer) where-    -- | -    ---    -- NB: This instance is provided for use with 'fromInteger'.-    -- It is lawful for /abs i <= maxBound @Int64/-    conn = c1 >>> intnat >>> natint >>> c2-      where-        c1 = Conn shiftR shiftL shiftR-        c2 = Conn (fmap shiftL) (fmap shiftR) (fmap shiftL)+instance Connection k (Extended Word8) Int32 where cast = w08i32+instance Connection k (Extended Word16) Int32 where cast = w16i32+instance Connection k (Extended Int8) Int32 where cast = i08i32+instance Connection k (Extended Int16) Int32 where cast = i16i32 -        shiftR x = x + m-        shiftL x = x - m-        m = 9223372036854775808+instance Connection k (Extended Word8) Int64 where cast = w08i64+instance Connection k (Extended Word16) Int64 where cast = w16i64+instance Connection k (Extended Word32) Int64 where cast = w32i64+instance Connection k (Extended Int8) Int64 where cast = i08i64+instance Connection k (Extended Int16) Int64 where cast = i16i64+instance Connection k (Extended Int32) Int64 where cast = i32i64+instance Connection k Int Int64 where cast = ixxi64 -instance Connection k Rational (Extended Word8) where conn = ratw08-instance Connection k Rational (Extended Word16) where conn = ratw16-instance Connection k Rational (Extended Word32) where conn = ratw32-instance Connection k Rational (Extended Word64) where conn = ratw64-instance Connection k Rational (Extended Word) where conn = ratwxx-instance Connection k Rational (Extended Natural) where conn = ratnat+instance Connection k (Extended Word8) Int where cast = w08ixx+instance Connection k (Extended Word16) Int where cast = w16ixx+instance Connection k (Extended Word32) Int where cast = w32ixx+instance Connection k (Extended Int8) Int where cast = i08ixx+instance Connection k (Extended Int16) Int where cast = i16ixx+instance Connection k (Extended Int32) Int where cast = i32ixx+instance Connection k Int64 Int where cast = i64ixx+instance Connection k SystemTime Int where cast = sysixx -instance Connection k Rational (Extended Int8) where conn = rati08-instance Connection k Rational (Extended Int16) where conn = rati16-instance Connection k Rational (Extended Int32) where conn = rati32-instance Connection k Rational (Extended Int64) where conn = rati64-instance Connection k Rational (Extended Int) where conn = ratixx-instance Connection k Rational (Extended Integer) where conn = ratint-instance Connection k Rational (Extended SystemTime) where conn = ratsys-instance HasResolution res => Connection k Rational (Extended (Fixed res)) where conn = ratfix+instance Connection 'L (Extended Word8) (Maybe Integer) where cast = w08int+instance Connection 'L (Extended Word16) (Maybe Integer) where cast = w16int+instance Connection 'L (Extended Word32) (Maybe Integer) where cast = w32int+instance Connection 'L (Extended Word64) (Maybe Integer) where cast = w64int+instance Connection 'L (Extended Word) (Maybe Integer) where cast = wxxint -instance Connection k Float (Extended Word8) where conn = f32w08-instance Connection k Float (Extended Word16) where conn = f32w16-instance Connection k Float (Extended Int8) where conn = f32i08-instance Connection k Float (Extended Int16) where conn = f32i16-instance HasResolution res => Connection 'L Float (Extended (Fixed res)) where conn = f32fix+instance Connection 'L (Extended Int8) (Maybe Integer) where cast = i08int+instance Connection 'L (Extended Int16) (Maybe Integer) where cast = i16int+instance Connection 'L (Extended Int32) (Maybe Integer) where cast = i32int+instance Connection 'L (Extended Int64) (Maybe Integer) where cast = i64int+instance Connection 'L (Extended Int) (Maybe Integer) where cast = ixxint -instance Connection k Double (Extended Word8) where conn = f64w08-instance Connection k Double (Extended Word16) where conn = f64w16-instance Connection k Double (Extended Word32) where conn = f64w32-instance Connection k Double (Extended Int8) where conn = f64i08-instance Connection k Double (Extended Int16) where conn = f64i16-instance Connection k Double (Extended Int32) where conn = f64i32-instance HasResolution res => Connection 'L Double (Extended (Fixed res)) where conn = f64fix+instance Connection k Rational (Extended Word8) where cast = ratw08+instance Connection k Rational (Extended Word16) where cast = ratw16+instance Connection k Rational (Extended Word32) where cast = ratw32+instance Connection k Rational (Extended Word64) where cast = ratw64+instance Connection k Rational (Extended Word) where cast = ratwxx+instance Connection k Rational (Extended Natural) where cast = ratnat -instance Connection k a b => Connection k (Identity a) b where-    conn = Conn runIdentity Identity runIdentity >>> conn+instance Connection k Rational (Extended Int8) where cast = rati08+instance Connection k Rational (Extended Int16) where cast = rati16+instance Connection k Rational (Extended Int32) where cast = rati32+instance Connection k Rational (Extended Int64) where cast = rati64+instance Connection k Rational (Extended Int) where cast = ratixx+instance Connection k Rational (Extended Integer) where cast = ratint+instance Connection k Rational (Extended SystemTime) where cast = ratsys -instance Connection k a b => Connection k a (Identity b) where-    conn = conn >>> Conn Identity runIdentity Identity+instance HasResolution res => Connection k Rational (Extended (Fixed res)) where cast = ratfix --- Internal+instance Connection k Float (Extended Word8) where cast = f32w08+instance Connection k Float (Extended Word16) where cast = f32w16+instance Connection 'L Float (Extended Word32) where cast = f32w32+instance Connection 'L Float (Extended Word64) where cast = f32w64+instance Connection 'L Float (Extended Word) where cast = f32wxx+instance Connection 'L Float (Extended Natural) where cast = f32nat --------------------------+instance Connection k Float (Extended Int8) where cast = f32i08+instance Connection k Float (Extended Int16) where cast = f32i16+instance Connection 'L Float (Extended Int32) where cast = f32i32+instance Connection 'L Float (Extended Int64) where cast = f32i64+instance Connection 'L Float (Extended Int) where cast = f32ixx+instance Connection 'L Float (Extended Integer) where cast = f32int+instance Connection 'L Float (Extended SystemTime) where cast = f32sys -bounds' :: (Eq a, Bounded a) => Conn k a Bool-bounds' = bounds minBound maxBound+instance HasResolution res => Connection 'L Float (Extended (Fixed res)) where cast = f32fix -bounds :: Eq a => a -> a -> Conn k a Bool-bounds x y = Conn f g h-  where-    g False = x-    g True = y+instance Connection k Double (Extended Word8) where cast = f64w08+instance Connection k Double (Extended Word16) where cast = f64w16+instance Connection k Double (Extended Word32) where cast = f64w32+instance Connection 'L Double (Extended Word64) where cast = f64w64+instance Connection 'L Double (Extended Word) where cast = f64wxx+instance Connection 'L Double (Extended Natural) where cast = f64nat -    f i-        | i == x = False-        | otherwise = True+instance Connection k Double (Extended Int8) where cast = f64i08+instance Connection k Double (Extended Int16) where cast = f64i16+instance Connection k Double (Extended Int32) where cast = f64i32+instance Connection 'L Double (Extended Int64) where cast = f64i64+instance Connection 'L Double (Extended Int) where cast = f64ixx+instance Connection 'L Double (Extended Integer) where cast = f64int+instance Connection 'L Double (Extended SystemTime) where cast = f64sys -    h i-        | i == y = True-        | otherwise = False+instance HasResolution res => Connection 'L Double (Extended (Fixed res)) where cast = f64fix

@@ -1,661 +0,0 @@-{-# LANGUAGE AllowAmbiguousTypes #-}-{-# LANGUAGE ConstraintKinds #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE DeriveFunctor #-}-{-# LANGUAGE DeriveGeneric #-}-{-# LANGUAGE PatternSynonyms #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE Safe #-}-{-# LANGUAGE TypeApplications #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE ViewPatterns #-}--module Data.Connection.Conn (-    -- * Conn-    Side (..),-    Conn (),-    (>>>),-    (<<<),-    mapped,-    choice,-    select,-    strong,-    divide,-    bounded,-    ordered,-    identity,--    -- * Conn 'L-    ConnL,-    pattern ConnL,-    connL,-    upper,-    upper1,-    upper2,-    ceiling,-    ceiling1,-    ceiling2,-    maximize,--    -- * Conn 'R-    ConnR,-    pattern ConnR,-    connR,-    lower,-    lower1,-    lower2,-    floor,-    floor1,-    floor2,-    minimize,--    -- * Connection k-    pattern Conn,-    outer,-    inner,-    half,-    midpoint,-    round,-    round1,-    round2,-    truncate,-    truncate1,-    truncate2,-    median,--    -- * Down-    upL,-    upR,-    downL,-    downR,-    filterL,-    filterR,-    Down (..),--    -- * Extended-    Lifted,-    Lowered,-    Extended (..),-    extended,-    extend,-) where--import safe Control.Arrow ((&&&))-import safe Control.Category (Category, (<<<), (>>>))-import safe qualified Control.Category as C-import safe Data.Bifunctor (bimap)-import safe Data.ExtendedReal-import safe Data.Order-import safe Data.Order.Syntax-import safe Prelude hiding (Ord (..), ceiling, floor, round, truncate)---- $setup--- >>> :set -XTypeApplications--- >>> import Data.Int--- >>> import Data.Ord (Down(..))--- >>> import Data.Ratio ((%))--- >>> import GHC.Real (Ratio(..))--- >>> :load Data.Connection---- | A data kind distinguishing links in a < https://ncatlab.org/nlab/show/adjoint+string chain > of Galois connections of length 2 or 3.------ * /L/-tagged types are increasing (e.g. 'Data.Connection.Conn.ceiling', 'Data.Connection.Conn.maximize')------ * /R/-tagged types are decreasing (e.g. 'Data.Connection.Conn.floor', 'Data.Connection.Conn.minimize')------  If a connection is existentialized over this value (i.e. has type /forall k. Conn k a b/) then it can---  provide either of two functions /f, h :: a -> b/.------  This is useful because it enables rounding, truncation, medians, etc. ----data Side = L | R---- | A < https://ncatlab.org/nlab/show/adjoint+string chain > of Galois connections of length 2 or 3.------ Connections have many nice properties wrt numerical conversion:------ >>> inner ratf32 (1 / 8)    -- eighths are exactly representable in a float--- 1 % 8--- >>> outer ratf32 (1 % 8)--- (0.125,0.125)--- >>> inner ratf32 (1 / 7)    -- sevenths are not--- 9586981 % 67108864--- >>> outer ratf32 (1 % 7)--- (0.14285713,0.14285715)------ Another example avoiding loss-of-precision:------ >>> f x y = (x + y) - x--- >>> maxOdd32 = 1.6777215e7--- >>> f maxOdd32 2.0 :: Float--- 1.0--- >>> round2 f64f32 f maxOdd32 2.0--- 2.0------ See the /README/ file for a slightly more in-depth introduction.-data Conn (k :: Side) a b = Conn_ (a -> (b, b)) (b -> a)--instance Category (Conn k) where-    id = identity-    {-# INLINE id #-}--    Conn_ f1 g1 . Conn_ f2 g2 = Conn_ ((fst . f1) . (fst . f2) &&& (snd . f1) . (snd . f2)) (g2 . g1)-    {-# INLINE (.) #-}---- Internal floor function. When \(f \dashv g \dashv h \) this is h.-_1 :: Conn k a b -> a -> b-_1 (Conn_ f _) = fst . f-{-# INLINE _1 #-}---- Internal ceiling function. When \(f \dashv g \dashv h \) this is f.-_2 :: Conn k a b -> a -> b-_2 (Conn_ f _) = snd . f-{-# INLINE _2 #-}---- | Lift a 'Conn' into a functor.------ /Caution/: This function will result in an invalid connection--- if the functor alters the internal preorder (e.g. 'Data.Ord.Down').-mapped :: Functor f => Conn k a b -> Conn k (f a) (f b)-mapped (Conn f g h) = Conn (fmap f) (fmap g) (fmap h)-{-# INLINE mapped #-}---- | Lift two connections into a connection on the <https://en.wikibooks.org/wiki/Category_Theory/Categories_of_ordered_sets coproduct order>------ > (choice id) (ab >>> cd) = (choice id) ab >>> (choice id) cd--- > (flip choice id) (ab >>> cd) = (flip choice id) ab >>> (flip choice id) cd-choice :: Conn k a b -> Conn k c d -> Conn k (Either a c) (Either b d)-choice (Conn ab ba ab') (Conn cd dc cd') = Conn f g h-  where-    f = either (Left . ab) (Right . cd)-    g = either (Left . ba) (Right . dc)-    h = either (Left . ab') (Right . cd')-{-# INLINE choice #-}--infixr 3 `select`---- | Lift two connections into a connection on the <https://en.wikibooks.org/wiki/Category_Theory/Categories_of_ordered_sets coproduct order>-select :: Conn k c a -> Conn k c b -> Conn k c (Either a b)-select f g = Conn Left (either id id) Right >>> f `choice` g---- | Lift two connections into a connection on the <https://en.wikibooks.org/wiki/Order_Theory/Preordered_classes_and_poclasses#product_order product order>------ > (strong id) (ab >>> cd) = (strong id) ab >>> (strong id) cd--- > (flip strong id) (ab >>> cd) = (flip strong id) ab >>> (flip strong id) cd-strong :: Conn k a b -> Conn k c d -> Conn k (a, c) (b, d)-strong (Conn ab ba ab') (Conn cd dc cd') = Conn f g h-  where-    f = bimap ab cd-    g = bimap ba dc-    h = bimap ab' cd'-{-# INLINE strong #-}--infixr 4 `divide`---- | Lift two connections into a connection on the <https://en.wikibooks.org/wiki/Order_Theory/Preordered_classes_and_poclasses#product_order product order>-divide :: Total c => Conn k a c -> Conn k b c -> Conn k (a, b) c-divide f g = f `strong` g >>> ordered---- | The defining connections of a bounded preorder.-bounded :: Bounded a => Conn k () a-bounded = Conn (const minBound) (const ()) (const maxBound)-{-# INLINE bounded #-}---- | The defining connections of a total order.------ >>> outer ordered (True, False)--- (False,True)-ordered :: Total a => Conn k (a, a) a-ordered = Conn (uncurry max) (id &&& id) (uncurry min)-{-# INLINE ordered #-}---- | The identity connection.-identity :: Conn k a a-identity = Conn_ (id &&& id) id-{-# INLINE identity #-}-------------------------------------------------------------------------- Conn 'L------------------------------------------------------------------------type ConnL = Conn 'L---- | A <https://ncatlab.org/nlab/show/Galois+connection Galois connection> between two monotone functions.------ A Galois connection between /f/ and /g/, written \(f \dashv g \)--- is an adjunction in the category of preorders.------ Each side of the connection may be defined in terms of the other:------  \( g(x) = \sup \{y \in E \mid f(y) \leq x \} \)------  \( f(x) = \inf \{y \in E \mid g(y) \geq x \} \)------ /Caution/: /ConnL f g/ must obey \(f \dashv g \). This condition is not checked.------ For further information see 'Data.Connection.Property'.-pattern ConnL :: (a -> b) -> (b -> a) -> Conn 'L a b-pattern ConnL f g <- (_2 &&& upper -> (f, g)) where ConnL f g = Conn_ (f &&& f) g--{-# COMPLETE ConnL #-}---- | Witness to the mirror symmetry between 'ConnL' and 'ConnR'.------ > connL . connR = id--- > connR . connL = id-connL :: Conn 'R a b -> Conn 'L b a-connL (ConnR f g) = ConnL f g-{-# INLINE connL #-}---- | Extract the upper adjoint of a 'ConnL'.-upper :: Conn 'L a b -> b -> a-upper = inner-{-# INLINE upper #-}---- | Map over a 'ConnL' from the right.------ This is the unit of the resulting monad:------ > x <~ upper1 c id x------ >>> compare pi $ upper1 f64f32 id pi--- LT-upper1 :: Conn 'L a b -> (b -> b) -> a -> a-upper1 (ConnL f g) h a = g $ h (f a)-{-# INLINE upper1 #-}---- | Zip over a 'ConnL' from the right.-upper2 :: Conn 'L a b -> (b -> b -> b) -> a -> a -> a-upper2 (ConnL f g) h a1 a2 = g $ h (f a1) (f a2)-{-# INLINE upper2 #-}---- | Extract the lower half of a 'ConnL'.------ > ceiling identity = id--- > ceiling c (x \/ y) = ceiling c x \/ ceiling c y------ The latter law is the adjoint functor theorem for preorders.------ >>> Data.Connection.ceiling ratf32 (0 :% 0)--- NaN--- >>> Data.Connection.ceiling ratf32 (13 :% 10)--- 1.3000001--- >>> Data.Connection.ceiling f64f32 pi--- 3.1415927-ceiling :: Conn 'L a b -> a -> b-ceiling (ConnL f _) = f-{-# INLINE ceiling #-}---- | Map over a 'ConnL' from the left.------ > ceiling1 identity = id------ This is the counit of the resulting comonad:------ > x >~ ceiling1 c id x----ceiling1 :: Conn 'L a b -> (a -> a) -> b -> b-ceiling1 (ConnL f g) h b = f $ h (g b)-{-# INLINE ceiling1 #-}---- | Zip over a 'ConnL' from the left.-ceiling2 :: Conn 'L a b -> (a -> a -> a) -> b -> b -> b-ceiling2 (ConnL f g) h b1 b2 = f $ h (g b1) (g b2)-{-# INLINE ceiling2 #-}---- | Generalized maximum.-maximize :: Conn 'L (a, b) c -> a -> b -> c-maximize = curry . ceiling-{-# INLINE maximize #-}-------------------------------------------------------------------------- Conn 'R------------------------------------------------------------------------type ConnR = Conn 'R---- | A Galois connection between two monotone functions.------ 'ConnR' is the mirror image of 'ConnL':------ > connR :: ConnL a b -> ConnR b a------ If you only require one connection there is no particular reason to--- use one version over the other. However some use cases (e.g. rounding)--- require an adjoint triple of connections that can lower into a standard--- connection in either of two ways.------ /Caution/: /ConnR f g/ must obey \(f \dashv g \). This condition is not checked.------ For further information see 'Data.Connection.Property'.-pattern ConnR :: (b -> a) -> (a -> b) -> Conn 'R a b-pattern ConnR f g <- (lower &&& _1 -> (f, g)) where ConnR f g = Conn_ (g &&& g) f--{-# COMPLETE ConnR #-}---- | Witness to the mirror symmetry between 'ConnL' and 'ConnR'.------ > connL . connR = id--- > connR . connL = id-connR :: Conn 'L a b -> Conn 'R b a-connR (ConnL f g) = ConnR f g-{-# INLINE connR #-}---- | Extract the lower adjoint of a 'ConnR'.-lower :: Conn 'R a b -> b -> a-lower = inner-{-# INLINE lower #-}---- | Map over a 'ConnR' from the left.------ This is the counit of the resulting comonad:------ > x >~ lower1 c id x------ >>> compare pi $ lower1 f64f32 id pi--- GT-lower1 :: Conn 'R a b -> (b -> b) -> a -> a-lower1 (ConnR f g) h a = f $ h (g a)-{-# INLINE lower1 #-}---- | Zip over a 'ConnR' from the left.-lower2 :: Conn 'R a b -> (b -> b -> b) -> a -> a -> a-lower2 (ConnR f g) h a1 a2 = f $ h (g a1) (g a2)-{-# INLINE lower2 #-}---- | Extract the upper half of a 'ConnR'------ > floor identity = id--- > floor c (x /\ y) = floor c x /\ floor c y------ The latter law is the adjoint functor theorem for preorders.------ >>> Data.Connection.floor ratf32 (0 :% 0)--- NaN--- >>> Data.Connection.floor ratf32 (13 :% 10)--- 1.3--- >>> Data.Connection.floor f64f32 pi--- 3.1415925-floor :: Conn 'R a b -> a -> b-floor (ConnR _ g) = g-{-# INLINE floor #-}---- | Map over a 'ConnR' from the right.------ > floor1 identity = id------ This is the unit of the resulting monad:------ > x <~ floor1 c id x----floor1 :: Conn 'R a b -> (a -> a) -> b -> b-floor1 (ConnR f g) h b = g $ h (f b)-{-# INLINE floor1 #-}---- | Zip over a 'ConnR' from the right.-floor2 :: Conn 'R a b -> (a -> a -> a) -> b -> b -> b-floor2 (ConnR f g) h b1 b2 = g $ h (f b1) (f b2)-{-# INLINE floor2 #-}---- | Generalized minimum.-minimize :: Conn 'R (a, b) c -> a -> b -> c-minimize = curry . floor-{-# INLINE minimize #-}-------------------------------------------------------------------------- Conn k-------------------------------------------------------------------------- | An <https://ncatlab.org/nlab/show/adjoint+triple adjoint triple> of Galois connections.------ An adjoint triple is a chain of connections of length 3:------ \(f \dashv g \dashv h \)------ When applied to a 'ConnL' or 'ConnR', the two functions of type @a -> b@ returned will be identical.------ /Caution/: /Conn f g h/ must obey \(f \dashv g \dashv h\). This condition is not checked.------ For detailed properties see 'Data.Connection.Property'.-pattern Conn :: (a -> b) -> (b -> a) -> (a -> b) -> Conn k a b-pattern Conn f g h <- (inner &&& _1 &&& _2 -> (g, (h, f))) where Conn f g h = Conn_ (h &&& f) g--{-# COMPLETE Conn #-}---- | Extract the left and/or right adjoints of a connection.------ When the connection is an adjoint triple the outer functions are returned:------ > outer c = floor c &&& ceiling c------ >>> outer ratf32 (1 % 8)    -- eighths are exactly representable in a float--- (0.125,0.125)--- >>> outer ratf32 (1 % 7)    -- sevenths are not--- (0.14285713,0.14285715)-outer :: Conn k a b -> a -> (b, b)-outer (Conn_ f _) = f-{-# INLINE outer #-}---- | Extract the upper adjoint of a 'ConnL', or lower adjoint of a 'ConnR'.------ When the connection is an adjoint triple the inner function is returned:------ >>> inner ratf32 (1 / 8)    -- eighths are exactly representable in a float--- 1 % 8--- >>> inner ratf32 (1 / 7)    -- sevenths are not--- 9586981 % 67108864-inner :: Conn k a b -> b -> a-inner (Conn_ _ g) = g-{-# INLINE inner #-}---- | Determine which half of the interval between 2 representations of /a/ a particular value lies.------ @ 'half' c x = 'pcompare' (x - 'lower1' c 'id' x) ('upper1' c 'id' x - x) @------ >>> maybe False (== EQ) $ half f64f32 (midpoint f64f32 pi)--- True-half :: (Num a, Preorder a) => (forall k. Conn k a b) -> a -> Maybe Ordering-half c x = pcompare (x - lower1 c id x) (upper1 c id x - x)-{-# INLINE half #-}---- | Return the midpoint of the interval containing x.------ >>> pi - midpoint f64f32 pi--- 3.1786509424591713e-8-midpoint :: Fractional a => (forall k. Conn k a b) -> a -> a-midpoint c x = lower1 c id x / 2 + upper1 c id x / 2-{-# INLINE midpoint #-}---- | Return the nearest value to x.------ > round identity = id------ If x lies halfway between two finite values, then return the value--- with the smaller absolute value (i.e. round towards from zero).------ See <https://en.wikipedia.org/wiki/Rounding>.-round :: (Num a, Preorder a) => (forall k. Conn k a b) -> a -> b-round c x = case half c x of-    Just GT -> ceiling c x-    Just LT -> floor c x-    _ -> truncate c x-{-# INLINE round #-}---- | Lift a unary function over an adjoint triple.------ > round1 identity = id------ Results are rounded to the nearest value with ties away from 0.-round1 :: (Num a, Preorder a) => (forall k. Conn k a b) -> (a -> a) -> b -> b-round1 c f x = round c $ f (g x) where Conn _ g _ = c-{-# INLINE round1 #-}---- | Lift a binary function over an adjoint triple.------ > round2 identity = id------ Results are rounded to the nearest value with ties away from 0.------ Example avoiding loss-of-precision:------ >>> f x y = (x + y) - x--- >>> maxOdd32 = 1.6777215e7--- >>> f maxOdd32 2.0 :: Float--- 1.0--- >>> round2 ratf32 f maxOdd32 2.0--- 2.0-round2 :: (Num a, Preorder a) => (forall k. Conn k a b) -> (a -> a -> a) -> b -> b -> b-round2 c f x y = round c $ f (g x) (g y) where Conn _ g _ = c-{-# INLINE round2 #-}---- | Truncate towards zero.------ > truncate identity = id-truncate :: (Num a, Preorder a) => (forall k. Conn k a b) -> a -> b-truncate c x = if x >~ 0 then floor c x else ceiling c x-{-# INLINE truncate #-}---- | Lift a unary function over an adjoint triple.------ > truncate1 identity = id------ Results are truncated towards zero.-truncate1 :: (Num a, Preorder a) => (forall k. Conn k a b) -> (a -> a) -> b -> b-truncate1 c f x = truncate c $ f (g x) where Conn _ g _ = c-{-# INLINE truncate1 #-}---- | Lift a binary function over an adjoint triple.------ > truncate2 identity = id------ Results are truncated towards zero.-truncate2 :: (Num a, Preorder a) => (forall k. Conn k a b) -> (a -> a -> a) -> b -> b -> b-truncate2 c f x y = truncate c $ f (g x) (g y) where Conn _ g _ = c-{-# INLINE truncate2 #-}---- | Birkoff's < https://en.wikipedia.org/wiki/Median_algebra median > operator.------ > 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 f32f32 1.0 9.0 7.0--- 7.0--- >>> median f32f32 1.0 9.0 (0.0 / 0.0)--- 9.0-median :: (forall k. Conn k (a, a) a) -> a -> a -> a -> a-median c x y z = (x `join` y) `meet` (y `join` z) `meet` (z `join` x)-  where-    join = maximize c-    meet = minimize c-{-# INLINE median #-}-------------------------------------------------------------------------- Down-------------------------------------------------------------------------- | Convert an inverted 'ConnL' to a 'ConnL'.------ > upL . downL = downL . upL = id-upL :: Conn 'L (Down a) (Down b) -> Conn 'L b a-upL (ConnL f g) = ConnL g' f'-  where-    f' x = let (Down y) = f (Down x) in y-    g' x = let (Down y) = g (Down x) in y-{-# INLINE upL #-}---- | Convert an inverted 'ConnR' to a 'ConnR'.------ > upR . downR = downR . upR = id-upR :: Conn 'R (Down a) (Down b) -> Conn 'R b a-upR (ConnR f g) = ConnR g' f'-  where-    f' x = let (Down y) = f (Down x) in y-    g' x = let (Down y) = g (Down x) in y-{-# INLINE upR #-}---- | Convert a 'ConnL' to an inverted 'ConnL'.------ >>> let counit = upper1 (downL $ bounded @Ordering) id--- >>> counit (Down LT)--- Down LT--- >>> counit (Down GT)--- Down LT-downL :: Conn 'L a b -> Conn 'L (Down b) (Down a)-downL (ConnL f g) = ConnL (\(Down x) -> Down $ g x) (\(Down x) -> Down $ f x)-{-# INLINE downL #-}---- | Convert a 'ConnR' to an inverted 'ConnR'.------ >>> let unit = lower1 (downR $ bounded @Ordering) id--- >>> unit (Down LT)--- Down GT--- >>> unit (Down GT)--- Down GT-downR :: Conn 'R a b -> Conn 'R (Down b) (Down a)-downR (ConnR f g) = ConnR (\(Down x) -> Down $ g x) (\(Down x) -> Down $ f x)-{-# INLINE downR #-}---- | Obtain the principal filter in /B/ generated by an element of /A/.------ A subset /B/ of a lattice is an filter if and only if it is an upper set--- that is closed under finite meets, i.e., it is nonempty and for all--- /x/, /y/ in /B/, the element @meet c x y@ is also in /b/.------ /filterL/ and /filterR/ commute with /Down/:------ > filterL c a b <=> filterR c (Down a) (Down b)------ > filterL c (Down a) (Down b) <=> filterR c a b------ /filterL c a/ is upward-closed for all /a/:------ > a <= b1 && b1 <= b2 => a <= b2--- > a1 <= b && a2 <= b => minimize c (ceiling c a1) (ceiling c a2) <= b------ See <https://en.wikipedia.org/wiki/Filter_(mathematics)>-filterL :: Preorder b => Conn 'L a b -> a -> b -> Bool-filterL c a b = ceiling c a <~ b-{-# INLINE filterL #-}---- | Obtain the principal ideal in /B/ generated by an element of /A/.------ A subset /B/ of a lattice is an ideal if and only if it is a lower set--- that is closed under finite joins, i.e., it is nonempty and for all--- /x/, /y/ in /B/, the element /join c x y/ is also in /B/.------ /filterR c a/ is downward-closed for all /a/:------ > a >= b1 && b1 >= b2 => a >= b2------ > a1 >= b && a2 >= b => maximize c (floor c a1) (floor c a2) >= b------ See <https://en.wikipedia.org/wiki/Ideal_(order_theory)>-filterR :: Preorder b => Conn 'R a b -> a -> b -> Bool-filterR c a b = b <~ floor c a-{-# INLINE filterR #-}-------------------------------------------------------------------------- Extended------------------------------------------------------------------------type Lifted = Either ()--type Lowered a = Either a ()---- | Eliminate an 'Extended'.-{-# INLINE extended #-}-extended :: b -> b -> (a -> b) -> Extended a -> b-extended b _ _ NegInf = b-extended _ t _ PosInf = t-extended _ _ f (Finite x) = f x--{-# INLINE extend #-}-extend :: (a -> Bool) -> (a -> Bool) -> (a -> b) -> a -> Extended b-extend p q f = g-  where-    g i-        | p i = NegInf-        | q i = PosInf-        | otherwise = Finite $ f i

@@ -59,7 +59,8 @@     HasResolution (..), ) where -import safe Data.Connection.Conn+import safe Data.Connection.Cast+import safe Data.Connection.Float import safe Data.Connection.Ratio import safe Data.Fixed import safe Data.Order@@ -76,97 +77,97 @@  -- Uni -f00int :: Conn k Uni Integer-f00int = Conn f g f+f00int :: Cast k Uni Integer+f00int = Cast f g f   where     f (MkFixed i) = i     g = fromInteger  -- Deci -f01f00 :: Conn k Deci Uni+f01f00 :: Cast k Deci Uni f01f00 = fixfix 10  -- Centi -f02f00 :: Conn k Centi Uni+f02f00 :: Cast k Centi Uni f02f00 = fixfix 100 -f02f01 :: Conn k Centi Deci+f02f01 :: Cast k Centi Deci f02f01 = fixfix 10  -- Milli -f03f00 :: Conn k Milli Uni+f03f00 :: Cast k Milli Uni f03f00 = fixfix 1000 -f03f01 :: Conn k Milli Deci+f03f01 :: Cast k Milli Deci f03f01 = fixfix 100 -f03f02 :: Conn k Milli Centi+f03f02 :: Cast k Milli Centi f03f02 = fixfix 10  -- Micro -f06f00 :: Conn k Micro Uni+f06f00 :: Cast k Micro Uni f06f00 = fixfix $ 10 ^ (6 :: Integer) -f06f01 :: Conn k Micro Deci+f06f01 :: Cast k Micro Deci f06f01 = fixfix $ 10 ^ (5 :: Integer) -f06f02 :: Conn k Micro Centi+f06f02 :: Cast k Micro Centi f06f02 = fixfix $ 10 ^ (4 :: Integer) -f06f03 :: Conn k Micro Milli+f06f03 :: Cast k Micro Milli f06f03 = fixfix $ 10 ^ (3 :: Integer)  -- Nano -f09f00 :: Conn k Nano Uni+f09f00 :: Cast k Nano Uni f09f00 = fixfix $ 10 ^ (9 :: Integer) -f09f01 :: Conn k Nano Deci+f09f01 :: Cast k Nano Deci f09f01 = fixfix $ 10 ^ (8 :: Integer) -f09f02 :: Conn k Nano Centi+f09f02 :: Cast k Nano Centi f09f02 = fixfix $ 10 ^ (7 :: Integer) -f09f03 :: Conn k Nano Milli+f09f03 :: Cast k Nano Milli f09f03 = fixfix $ 10 ^ (6 :: Integer) -f09f06 :: Conn k Nano Micro+f09f06 :: Cast k Nano Micro f09f06 = fixfix $ 10 ^ (3 :: Integer)  -- Pico -f12f00 :: Conn k Pico Uni+f12f00 :: Cast k Pico Uni f12f00 = fixfix $ 10 ^ (12 :: Integer) -f12f01 :: Conn k Pico Deci+f12f01 :: Cast k Pico Deci f12f01 = fixfix $ 10 ^ (11 :: Integer) -f12f02 :: Conn k Pico Centi+f12f02 :: Cast k Pico Centi f12f02 = fixfix $ 10 ^ (10 :: Integer) -f12f03 :: Conn k Pico Milli+f12f03 :: Cast k Pico Milli f12f03 = fixfix $ 10 ^ (9 :: Integer) -f12f06 :: Conn k Pico Micro+f12f06 :: Cast k Pico Micro f12f06 = fixfix $ 10 ^ (6 :: Integer) -f12f09 :: Conn k Pico Nano+f12f09 :: Cast k Pico Nano f12f09 = fixfix $ 10 ^ (3 :: Integer)  -- Fixed -f32fix :: HasResolution e => Conn 'L Float (Extended (Fixed e))-f32fix = connL ratf32 >>> ratfix+f32fix :: HasResolution e => Cast 'L Float (Extended (Fixed e))+f32fix = swapL ratf32 >>> ratfix -f64fix :: HasResolution e => Conn 'L Double (Extended (Fixed e))-f64fix = connL ratf64 >>> ratfix+f64fix :: HasResolution e => Cast 'L Double (Extended (Fixed e))+f64fix = swapL ratf64 >>> ratfix -ratfix :: forall e k. HasResolution e => Conn k Rational (Extended (Fixed e))-ratfix = Conn f' g h'+ratfix :: forall e k. HasResolution e => Cast k Rational (Extended (Fixed e))+ratfix = Cast f' g h'   where     prec = resolution (Proxy :: Proxy e) @@ -191,8 +192,8 @@  ------------------------- -fixfix :: Integer -> Conn k (Fixed e1) (Fixed e2)-fixfix prec = Conn f g h+fixfix :: Integer -> Cast k (Fixed e1) (Fixed e2)+fixfix prec = Cast f g h   where     f (MkFixed i) = MkFixed $ let j = i `div` prec in if i `mod` prec == 0 then j else j + 1     g (MkFixed i) = MkFixed $ i * prec

@@ -9,35 +9,53 @@     -- * Float     f32w08,     f32w16,+    f32w32,+    f32w64,+    f32wxx,+    f32nat,     f32i08,     f32i16,+    f32i32,+    f32i64,+    f32ixx,+    f32int,     f32f32,+    f64f32,+    ratf32,     ulp32,     near32,     shift32,      -- * Double-    f64f64,     f64w08,     f64w16,     f64w32,+    f64w64,+    f64wxx,+    f64nat,     f64i08,     f64i16,     f64i32,-    f64f32,+    f64i64,+    f64ixx,+    f64int,+    f64f64,+    ratf64,     ulp64,     near64,     shift64,-    until, ) where  import safe Data.Bool-import safe Data.Connection.Conn hiding (ceiling, floor)+import safe Data.Connection.Cast hiding (ceiling, floor)+import safe Data.Connection.Ratio import safe Data.Int import safe Data.Order import safe Data.Order.Syntax+import safe Data.Ratio (approxRational) import safe Data.Word import safe GHC.Float as F+import safe Numeric.Natural import safe Prelude hiding (Eq (..), Ord (..), until) import safe qualified Prelude as P @@ -45,21 +63,88 @@ -- Float --------------------------------------------------------------------- -f32f32 :: Conn k (Float, Float) Float-f32f32 = fxxfxx--f32w08 :: Conn k Float (Extended Word8)+f32w08 :: Cast k Float (Extended Word8) f32w08 = fxxext -f32w16 :: Conn k Float (Extended Word16)+f32w16 :: Cast k Float (Extended Word16) f32w16 = fxxext -f32i08 :: Conn k Float (Extended Int8)+f32w32 :: Cast 'L Float (Extended Word32)+f32w32 = swapL ratf32 >>> ratw32++f32w64 :: Cast 'L Float (Extended Word64)+f32w64 = swapL ratf32 >>> ratw64++f32wxx :: Cast 'L Float (Extended Word)+f32wxx = swapL ratf32 >>> ratwxx++f32nat :: Cast 'L Float (Extended Natural)+f32nat = swapL ratf32 >>> ratnat++f32i32 :: Cast 'L Float (Extended Int32)+f32i32 = swapL ratf32 >>> rati32++f32i64 :: Cast 'L Float (Extended Int64)+f32i64 = swapL ratf32 >>> rati64++f32ixx :: Cast 'L Float (Extended Int)+f32ixx = swapL ratf32 >>> ratixx++f32int :: Cast 'L Float (Extended Integer)+f32int = swapL ratf32 >>> ratint++f32i08 :: Cast k Float (Extended Int8) f32i08 = fxxext -f32i16 :: Conn k Float (Extended Int16)+f32i16 :: Cast k Float (Extended Int16) f32i16 = fxxext +f32f32 :: Cast k (Float, Float) Float+f32f32 = fxxfxx++f64f32 :: Cast k Double Float+f64f32 = Cast f g h+  where+    f x =+        let est = double2Float x+         in if g est >~ x+                then est+                else ascend32 est g x++    g = float2Double++    h x =+        let est = double2Float x+         in if g est <~ x+                then est+                else descend32 est g x++    ascend32 z g1 y = until (\x -> g1 x >~ y) (<~) (shift32 1) z++    descend32 z h1 x = until (\y -> h1 y <~ x) (>~) (shift32 (-1)) z+{-# INLINE f64f32 #-}++ratf32 :: Cast k Rational Float+ratf32 = Cast (toFractional f) (fromFractional g) (toFractional h)+  where+    f x =+        let est = fromRational x+         in if fromFractional g est >~ x+                then est+                else ascendf est (fromFractional g) x++    g = flip approxRational 0++    h x =+        let est = fromRational x+         in if fromFractional g est <~ x+                then est+                else descendf est (fromFractional g) x++    ascendf z g1 y = until (\x -> g1 x >~ y) (<~) (shift32 1) z++    descendf z f1 x = until (\y -> f1 y <~ x) (>~) (shift32 (-1)) z+ -- | Compute the signed distance between two floats in units of least precision. -- -- >>> ulp32 1.0 (shift32 1 1.0)@@ -108,48 +193,65 @@ -- Double --------------------------------------------------------------------- -f64f64 :: Conn k (Double, Double) Double-f64f64 = fxxfxx--f64w08 :: Conn k Double (Extended Word8)+f64w08 :: Cast k Double (Extended Word8) f64w08 = fxxext -f64w16 :: Conn k Double (Extended Word16)+f64w16 :: Cast k Double (Extended Word16) f64w16 = fxxext -f64w32 :: Conn k Double (Extended Word32)+f64w32 :: Cast k Double (Extended Word32) f64w32 = fxxext -f64i08 :: Conn k Double (Extended Int8)+f64w64 :: Cast 'L Double (Extended Word64)+f64w64 = swapL ratf64 >>> ratw64++f64wxx :: Cast 'L Double (Extended Word)+f64wxx = swapL ratf64 >>> ratwxx++f64nat :: Cast 'L Double (Extended Natural)+f64nat = swapL ratf64 >>> ratnat++f64i08 :: Cast k Double (Extended Int8) f64i08 = fxxext -f64i16 :: Conn k Double (Extended Int16)+f64i16 :: Cast k Double (Extended Int16) f64i16 = fxxext -f64i32 :: Conn k Double (Extended Int32)+f64i32 :: Cast k Double (Extended Int32) f64i32 = fxxext -f64f32 :: Conn k Double Float-f64f32 = Conn f g h+f64i64 :: Cast 'L Double (Extended Int64)+f64i64 = swapL ratf64 >>> rati64++f64ixx :: Cast 'L Double (Extended Int)+f64ixx = swapL ratf64 >>> ratixx++f64int :: Cast 'L Double (Extended Integer)+f64int = swapL ratf64 >>> ratint++f64f64 :: Cast k (Double, Double) Double+f64f64 = fxxfxx++ratf64 :: Cast k Rational Double+ratf64 = Cast (toFractional f) (fromFractional g) (toFractional h)   where     f x =-        let est = double2Float x-         in if g est >~ x+        let est = fromRational x+         in if fromFractional g est >~ x                 then est-                else ascend32 est g x+                else ascendf est (fromFractional g) x -    g = float2Double+    g = flip approxRational 0      h x =-        let est = double2Float x-         in if g est <~ x+        let est = fromRational x+         in if fromFractional g est <~ x                 then est-                else descend32 est g x+                else descendf est (fromFractional g) x -    ascend32 z g1 y = until (\x -> g1 x >~ y) (<~) (shift32 1) z+    ascendf z g1 y = until (\x -> g1 x >~ y) (<~) (shift64 1) z -    descend32 z h1 x = until (\y -> h1 y <~ x) (>~) (shift32 (-1)) z-{-# INLINE f64f32 #-}+    descendf z f1 x = until (\y -> f1 y <~ x) (>~) (shift64 (-1)) z  -- | Compute the signed distance between two doubles in units of least precision. --@@ -210,6 +312,29 @@       where         x' = f x +pinf :: Num a => Ratio a+pinf = 1 :% 0++ninf :: Num a => Ratio a+ninf = (-1) :% 0++nan :: Num a => Ratio a+nan = 0 :% 0++toFractional :: Fractional a => (Rational -> a) -> Rational -> a+toFractional f x+    | x ~~ nan = 0 / 0+    | x ~~ ninf = (-1) / 0+    | x ~~ pinf = 1 / 0+    | otherwise = f x++fromFractional :: (Order a, Fractional a) => (a -> Rational) -> a -> Rational+fromFractional f x+    | x ~~ 0 / 0 = nan+    | x ~~ (-1) / 0 = ninf+    | x ~~ 1 / 0 = pinf+    | otherwise = f x+ -- Non-monotonic function signed32 :: Word32 -> Int32 signed32 x@@ -255,8 +380,8 @@ clamp64 :: Int64 -> Int64 clamp64 = P.max (-9218868437227405313) . P.min 9218868437227405312 -fxxfxx :: (Total a, Fractional a) => Conn k (a, a) a-fxxfxx = Conn f g h+fxxfxx :: (Total a, Fractional a) => Cast k (a, a) a+fxxfxx = Cast f g h   where     -- join     f (x, y) = maybe (1 / 0) (bool y x . (>= EQ)) (pcompare x y)@@ -266,8 +391,8 @@     -- meet     h (x, y) = maybe (-1 / 0) (bool y x . (<= EQ)) (pcompare x y) -fxxext :: forall a b k. (RealFrac a, Preorder a, Bounded b, Integral b) => Conn k a (Extended b)-fxxext = Conn f g h+fxxext :: forall a b k. (RealFrac a, Preorder a, Bounded b, Integral b) => Cast k a (Extended b)+fxxext = Cast f g h   where     f = extend (~~ -1 / 0) (\x -> x ~~ 0 / 0 || x > high) $ \x -> if x < low then minBound else ceiling x @@ -281,38 +406,38 @@ {-# INLINE fxxext #-}  {--f32i32 :: Conn 'L Float (Extended Int32)+f32i32 :: Cast 'L Float (Extended Int32) f32i32 = f32ext -f32i64 :: Conn 'L Float (Extended Int64)+f32i64 :: Cast 'L Float (Extended Int64) f32i64 = f32ext -f32ixx :: Conn 'L Float (Extended Int)+f32ixx :: Cast 'L Float (Extended Int) f32ixx = f32ext -f32int :: Conn 'L Float (Extended Integer)+f32int :: Cast 'L Float (Extended Integer) f32int = f32ext -f64i64 :: Conn 'L Double (Extended Int64)+f64i64 :: Cast 'L Double (Extended Int64) f64i64 = f64ext -f64ixx :: Conn 'L Double (Extended Int)+f64ixx :: Cast 'L Double (Extended Int) f64ixx = f64ext  {-# INLINE f64ext #-}-f64int :: Conn 'L Double (Extended Integer)+f64int :: Cast 'L Double (Extended Integer) f64int = f64ext -f32ext :: Integral a => Conn 'L Float (Extended a)+f32ext :: Integral a => Cast 'L Float (Extended a) f32ext = fxxextL 23 -- Float loses integer precision beyond 2^prec  {-# INLINE f32ext #-} -f64ext :: Integral a => Conn 'L Double (Extended a)+f64ext :: Integral a => Cast 'L Double (Extended a) f64ext = fxxextL 52 -- Double loses integer precision beyond 2^prec -fxxextL :: (Preorder a, RealFrac a, Integral b) => b -> ConnL a (Extended b)-fxxextL prec = ConnL f g+fxxextL :: (Preorder a, RealFrac a, Integral b) => b -> CastL a (Extended b)+fxxextL prec = CastL f g   where     f x         | abs x <= 2 ^^ prec -1 = Finite (ceiling x)

@@ -22,6 +22,7 @@     i08i64,     i16i64,     i32i64,+    ixxi64,      -- * Int     w08ixx,@@ -38,7 +39,6 @@     w32int,     w64int,     wxxint,-    natint,     i08int,     i16int,     i32int,@@ -46,119 +46,136 @@     ixxint, ) where -import safe Control.Applicative-import safe Control.Monad-import safe Data.Connection.Conn+import safe Data.Connection.Cast import safe Data.Int import safe Data.Word-import safe Numeric.Natural-import safe Prelude  -- Int16-w08i16 :: Conn 'L Word8 (Maybe Int16)-w08i16 = signed+w08i16 :: Cast k (Extended Word8) Int16+w08i16 = conn -i08i16 :: Conn 'L Int8 (Maybe Int16)-i08i16 = signed+i08i16 :: Cast k (Extended Int8) Int16+i08i16 = conn  -- Int32-w08i32 :: Conn 'L Word8 (Maybe Int32)-w08i32 = signed+w08i32 :: Cast k (Extended Word8) Int32+w08i32 = conn -w16i32 :: Conn 'L Word16 (Maybe Int32)-w16i32 = signed+w16i32 :: Cast k (Extended Word16) Int32+w16i32 = conn -i08i32 :: Conn 'L Int8 (Maybe Int32)-i08i32 = signed+i08i32 :: Cast k (Extended Int8) Int32+i08i32 = conn -i16i32 :: Conn 'L Int16 (Maybe Int32)-i16i32 = signed+i16i32 :: Cast k (Extended Int16) Int32+i16i32 = conn  -- Int64-w08i64 :: Conn 'L Word8 (Maybe Int64)-w08i64 = signed+w08i64 :: Cast k (Extended Word8) Int64+w08i64 = conn -w16i64 :: Conn 'L Word16 (Maybe Int64)-w16i64 = signed+w16i64 :: Cast k (Extended Word16) Int64+w16i64 = conn -w32i64 :: Conn 'L Word32 (Maybe Int64)-w32i64 = signed+w32i64 :: Cast k (Extended Word32) Int64+w32i64 = conn -i08i64 :: Conn 'L Int8 (Maybe Int64)-i08i64 = signed+i08i64 :: Cast k (Extended Int8) Int64+i08i64 = conn -i16i64 :: Conn 'L Int16 (Maybe Int64)-i16i64 = signed+i16i64 :: Cast k (Extended Int16) Int64+i16i64 = conn -i32i64 :: Conn 'L Int32 (Maybe Int64)-i32i64 = signed+i32i64 :: Cast k (Extended Int32) Int64+i32i64 = conn +-- | /Caution/: This assumes that 'Int' on your system is 64 bits.+ixxi64 :: Cast k Int Int64+ixxi64 = Cast fromIntegral fromIntegral fromIntegral+ -- Int-w08ixx :: Conn 'L Word8 (Maybe Int)-w08ixx = signed+w08ixx :: Cast k (Extended Word8) Int+w08ixx = conn -w16ixx :: Conn 'L Word16 (Maybe Int)-w16ixx = signed+w16ixx :: Cast k (Extended Word16) Int+w16ixx = conn -w32ixx :: Conn 'L Word32 (Maybe Int)-w32ixx = signed+w32ixx :: Cast k (Extended Word32) Int+w32ixx = conn -i08ixx :: Conn 'L Int8 (Maybe Int)-i08ixx = signed+i08ixx :: Cast k (Extended Int8) Int+i08ixx = conn -i16ixx :: Conn 'L Int16 (Maybe Int)-i16ixx = signed+i16ixx :: Cast k (Extended Int16) Int+i16ixx = conn -i32ixx :: Conn 'L Int32 (Maybe Int)-i32ixx = signed+i32ixx :: Cast k (Extended Int32) Int+i32ixx = conn  -- | /Caution/: This assumes that 'Int' on your system is 64 bits.-i64ixx :: Conn k Int64 Int-i64ixx = Conn fromIntegral fromIntegral fromIntegral+i64ixx :: Cast k Int64 Int+i64ixx = Cast fromIntegral fromIntegral fromIntegral  -- Integer-w08int :: Conn 'L Word8 (Maybe Integer)-w08int = signed--w16int :: Conn 'L Word16 (Maybe Integer)-w16int = signed+w08int :: Cast 'L (Extended Word8) (Maybe Integer)+w08int = extint -w32int :: Conn 'L Word32 (Maybe Integer)-w32int = signed+w16int :: Cast 'L (Extended Word16) (Maybe Integer)+w16int = extint -w64int :: Conn 'L Word64 (Maybe Integer)-w64int = signed+w32int :: Cast 'L (Extended Word32) (Maybe Integer)+w32int = extint -wxxint :: Conn 'L Word (Maybe Integer)-wxxint = signed+w64int :: Cast 'L (Extended Word64) (Maybe Integer)+w64int = extint -natint :: Conn 'L Natural (Maybe Integer)-natint = ConnL (fmap fromIntegral . fromPred (/= 0)) (maybe 0 $ fromInteger . max 0)+wxxint :: Cast 'L (Extended Word) (Maybe Integer)+wxxint = extint -i08int :: Conn 'L Int8 (Maybe Integer)-i08int = signed+i08int :: Cast 'L (Extended Int8) (Maybe Integer)+i08int = extint -i16int :: Conn 'L Int16 (Maybe Integer)-i16int = signed+i16int :: Cast 'L (Extended Int16) (Maybe Integer)+i16int = extint -i32int :: Conn 'L Int32 (Maybe Integer)-i32int = signed+i32int :: Cast 'L (Extended Int32) (Maybe Integer)+i32int = extint -i64int :: Conn 'L Int64 (Maybe Integer)-i64int = signed+i64int :: Cast 'L (Extended Int64) (Maybe Integer)+i64int = extint -ixxint :: Conn 'L Int (Maybe Integer)-ixxint = signed+ixxint :: Cast 'L (Extended Int) (Maybe Integer)+ixxint = extint  --------------------------------------------------------------------- -- Internal --------------------------------------------------------------------- -fromPred :: (a -> Bool) -> a -> Maybe a-fromPred p a = a <$ guard (p a)+{-# INLINE conn #-}+conn :: forall a b k. (Bounded a, Bounded b, Integral a, Integral b) => Cast k (Extended a) b+conn = Cast f g h +  where+    below = fromIntegral @a minBound - 1+    above = fromIntegral @a maxBound + 1+    +    f = extended minBound above $ fromIntegral+    +    g x | x <= below = NegInf+        | x >= above = PosInf+        | otherwise = Finite $ fromIntegral x -signed :: forall a b. (Bounded a, Integral a, Integral b) => Conn 'L a (Maybe b)-signed = ConnL f g+    h = extended below maxBound $ fromIntegral++{-# INLINE extint #-}+extint :: forall a. (Bounded a, Integral a) => Cast 'L (Extended a) (Maybe Integer)+extint = CastL f $ maybe NegInf g   where-    f = fmap fromIntegral . fromPred (/= minBound)-    g = maybe minBound $ fromIntegral @b . min (fromIntegral @a maxBound) . max (fromIntegral @a minBound)+    below = fromIntegral @a minBound - 1+    above = fromIntegral @a maxBound + 1+    +    f = extended Nothing (Just above) (Just . fromIntegral)+    +    g x | x <= below = NegInf+        | x >= above = PosInf+        | otherwise = Finite $ fromIntegral x+

@@ -41,7 +41,7 @@     projective, ) where -import safe Data.Connection.Conn+import safe Data.Connection.Cast import safe Data.Order import safe Data.Order.Property import safe Prelude hiding (Num (..), Ord (..), ceiling, floor)@@ -50,21 +50,21 @@  ------------------------- -adjoint :: (Preorder a, Preorder b) => (forall k. Conn k a b) -> a -> b -> Bool+adjoint :: (Preorder a, Preorder b) => (forall k. Cast k a b) -> a -> b -> Bool adjoint t a b =     adjointL t a b         && adjointR t a b-        && adjointL (connL t) b a-        && adjointR (connR t) b a+        && adjointL (swapL t) b a+        && adjointR (swapR t) b a  -- | \( \forall x, y : f \dashv g \Rightarrow f (x) \leq y \Leftrightarrow x \leq g (y) \) -- -- A Galois connection is an adjunction of preorders. This is a required property.-adjointL :: (Preorder a, Preorder b) => ConnL a b -> a -> b -> Bool-adjointL (ConnL f g) = adjunction (<~) (<~) f g+adjointL :: (Preorder a, Preorder b) => Cast 'L a b -> a -> b -> Bool+adjointL (CastL f g) = adjunction (<~) (<~) f g -adjointR :: (Preorder a, Preorder b) => ConnR a b -> a -> b -> Bool-adjointR (ConnR f g) = adjunction (>~) (>~) g f+adjointR :: (Preorder a, Preorder b) => Cast 'R a b -> a -> b -> Bool+adjointR (CastR f g) = adjunction (>~) (>~) g f  -- | \( \forall a: f a \leq b \Leftrightarrow a \leq g b \) --@@ -77,29 +77,29 @@  ------------------------- -closed :: (Preorder a, Preorder b) => (forall k. Conn k a b) -> a -> Bool+closed :: (Preorder a, Preorder b) => (forall k. Cast k a b) -> a -> Bool closed t a = closedL t a && closedR t a  -- | \( \forall x : f \dashv g \Rightarrow x \leq g \circ f (x) \) -- -- This is a required property.-closedL :: (Preorder a, Preorder b) => ConnL a b -> a -> Bool-closedL (ConnL f g) = invertible (>~) f g+closedL :: (Preorder a, Preorder b) => Cast 'L a b -> a -> Bool+closedL (CastL f g) = invertible (>~) f g -closedR :: (Preorder a, Preorder b) => ConnR a b -> a -> Bool-closedR (ConnR f g) = invertible (<~) g f+closedR :: (Preorder a, Preorder b) => Cast 'R a b -> a -> Bool+closedR (CastR f g) = invertible (<~) g f -kernel :: (Preorder a, Preorder b) => (forall k. Conn k a b) -> b -> Bool+kernel :: (Preorder a, Preorder b) => (forall k. Cast k a b) -> b -> Bool kernel t b = kernelL t b && kernelR t b  -- | \( \forall x : f \dashv g \Rightarrow x \leq g \circ f (x) \) -- -- This is a required property.-kernelL :: (Preorder a, Preorder b) => ConnL a b -> b -> Bool-kernelL (ConnL f g) = invertible (<~) g f+kernelL :: (Preorder a, Preorder b) => Cast 'L a b -> b -> Bool+kernelL (CastL f g) = invertible (<~) g f -kernelR :: (Preorder a, Preorder b) => ConnR a b -> b -> Bool-kernelR (ConnR f g) = invertible (>~) f g+kernelR :: (Preorder a, Preorder b) => Cast 'R a b -> b -> Bool+kernelR (CastR f g) = invertible (>~) f g  -- | \( \forall a: f (g a) \sim a \) invertible :: Rel s b -> (s -> r) -> (r -> s) -> s -> b@@ -109,17 +109,17 @@  ------------------------- -monotonic :: (Preorder a, Preorder b) => (forall k. Conn k a b) -> a -> a -> b -> b -> Bool+monotonic :: (Preorder a, Preorder b) => (forall k. Cast k a b) -> a -> a -> b -> b -> Bool monotonic t a1 a2 b1 b2 = monotonicL t a1 a2 b1 b2 && monotonicR t a1 a2 b1 b2  -- | \( \forall x, y : x \leq y \Rightarrow f (x) \leq f (y) \) -- -- This is a required property.-monotonicR :: (Preorder a, Preorder b) => ConnR a b -> a -> a -> b -> b -> Bool-monotonicR (ConnR f g) a1 a2 b1 b2 = monotone (<~) (<~) g a1 a2 && monotone (<~) (<~) f b1 b2+monotonicR :: (Preorder a, Preorder b) => Cast 'R a b -> a -> a -> b -> b -> Bool+monotonicR (CastR f g) a1 a2 b1 b2 = monotone (<~) (<~) g a1 a2 && monotone (<~) (<~) f b1 b2 -monotonicL :: (Preorder a, Preorder b) => ConnL a b -> a -> a -> b -> b -> Bool-monotonicL (ConnL f g) a1 a2 b1 b2 = monotone (<~) (<~) f a1 a2 && monotone (<~) (<~) g b1 b2+monotonicL :: (Preorder a, Preorder b) => Cast 'L a b -> a -> a -> b -> b -> Bool+monotonicL (CastL f g) a1 a2 b1 b2 = monotone (<~) (<~) f a1 a2 && monotone (<~) (<~) g b1 b2  -- | \( \forall a, b: a \leq b \Rightarrow f(a) \leq f(b) \) monotone :: Rel r Bool -> Rel s Bool -> (r -> s) -> r -> r -> Bool@@ -129,17 +129,17 @@  ------------------------- -idempotent :: (Preorder a, Preorder b) => (forall k. Conn k a b) -> a -> b -> Bool+idempotent :: (Preorder a, Preorder b) => (forall k. Cast k a b) -> a -> b -> Bool idempotent t a b = idempotentL t a b && idempotentR t a b  -- | \( \forall x: f \dashv g \Rightarrow counit \circ f (x) \sim f (x) \wedge unit \circ g (x) \sim g (x) \) -- -- See <https://ncatlab.org/nlab/show/idempotent+adjunction>-idempotentL :: (Preorder a, Preorder b) => ConnL a b -> a -> b -> Bool-idempotentL c@(ConnL f g) a b = projective (~~) g (upper1 c id) b && projective (~~) f (ceiling1 c id) a+idempotentL :: (Preorder a, Preorder b) => Cast 'L a b -> a -> b -> Bool+idempotentL c@(CastL f g) a b = projective (~~) g (upper1 c id) b && projective (~~) f (ceiling1 c id) a -idempotentR :: (Preorder a, Preorder b) => ConnR a b -> a -> b -> Bool-idempotentR c@(ConnR f g) a b = projective (~~) g (floor1 c id) a && projective (~~) f (lower1 c id) b+idempotentR :: (Preorder a, Preorder b) => Cast 'R a b -> a -> b -> Bool+idempotentR c@(CastR f g) a b = projective (~~) g (floor1 c id) a && projective (~~) f (lower1 c id) b  -- | \( \forall a: g \circ f (a) \sim f (a) \) projective :: Rel s b -> (r -> s) -> (s -> s) -> r -> b

@@ -18,8 +18,6 @@     rati64,     ratixx,     ratint,-    ratf32,-    ratf64,     ratrat,     reduce,     shiftr,@@ -27,12 +25,10 @@ ) where  import safe Data.Bool-import safe Data.Connection.Conn hiding (ceiling, floor, lower)-import safe Data.Connection.Float as Float+import safe Data.Connection.Cast hiding (ceiling, floor, lower) import safe Data.Int import safe Data.Order import safe Data.Order.Syntax-import safe Data.Ratio import safe Data.Word import safe GHC.Real (Ratio (..), Rational) import safe Numeric.Natural@@ -53,23 +49,23 @@ -- Ratio Integer --------------------------------------------------------------------- -ratw08 :: Conn k Rational (Extended Word8)+ratw08 :: Cast k Rational (Extended Word8) ratw08 = ratext -ratw16 :: Conn k Rational (Extended Word16)+ratw16 :: Cast k Rational (Extended Word16) ratw16 = ratext -ratw32 :: Conn k Rational (Extended Word32)+ratw32 :: Cast k Rational (Extended Word32) ratw32 = ratext -ratw64 :: Conn k Rational (Extended Word64)+ratw64 :: Cast k Rational (Extended Word64) ratw64 = ratext -ratwxx :: Conn k Rational (Extended Word)+ratwxx :: Cast k Rational (Extended Word) ratwxx = ratext -ratnat :: Conn k Rational (Extended Natural)-ratnat = Conn f g h+ratnat :: Cast k Rational (Extended Natural)+ratnat = Cast f g h   where     f = extend (~~ ninf) (\x -> x ~~ nan || x ~~ pinf) (ceiling . max 0) @@ -77,23 +73,23 @@      h = extend (\x -> x ~~ nan || x < 0) (~~ pinf) (floor . max 0) -rati08 :: Conn k Rational (Extended Int8)+rati08 :: Cast k Rational (Extended Int8) rati08 = ratext -rati16 :: Conn k Rational (Extended Int16)+rati16 :: Cast k Rational (Extended Int16) rati16 = ratext -rati32 :: Conn k Rational (Extended Int32)+rati32 :: Cast k Rational (Extended Int32) rati32 = ratext -rati64 :: Conn k Rational (Extended Int64)+rati64 :: Cast k Rational (Extended Int64) rati64 = ratext -ratixx :: Conn k Rational (Extended Int)+ratixx :: Cast k Rational (Extended Int) ratixx = ratext -ratint :: Conn k Rational (Extended Integer)-ratint = Conn f g h+ratint :: Cast k Rational (Extended Integer)+ratint = Cast f g h   where     f = extend (~~ ninf) (\x -> x ~~ nan || x ~~ pinf) ceiling @@ -101,50 +97,8 @@      h = extend (\x -> x ~~ nan || x ~~ ninf) (~~ pinf) floor -ratf32 :: Conn k Rational Float-ratf32 = Conn (toFractional f) (fromFractional g) (toFractional h)-  where-    f x =-        let est = fromRational x-         in if fromFractional g est >~ x-                then est-                else ascendf est (fromFractional g) x--    g = flip approxRational 0--    h x =-        let est = fromRational x-         in if fromFractional g est <~ x-                then est-                else descendf est (fromFractional g) x--    ascendf z g1 y = Float.until (\x -> g1 x >~ y) (<~) (Float.shift32 1) z--    descendf z f1 x = Float.until (\y -> f1 y <~ x) (>~) (Float.shift32 (-1)) z--ratf64 :: Conn k Rational Double-ratf64 = Conn (toFractional f) (fromFractional g) (toFractional h)-  where-    f x =-        let est = fromRational x-         in if fromFractional g est >~ x-                then est-                else ascendf est (fromFractional g) x--    g = flip approxRational 0--    h x =-        let est = fromRational x-         in if fromFractional g est <~ x-                then est-                else descendf est (fromFractional g) x--    ascendf z g1 y = Float.until (\x -> g1 x >~ y) (<~) (Float.shift64 1) z--    descendf z f1 x = Float.until (\y -> f1 y <~ x) (>~) (Float.shift64 (-1)) z--ratrat :: Conn k (Rational, Rational) Rational-ratrat = Conn f g h+ratrat :: Cast k (Rational, Rational) Rational+ratrat = Cast f g h   where     -- join     f (x, y) = maybe (1 / 0) (bool y x . (>= EQ)) (pcompare x y)@@ -167,8 +121,8 @@ nan :: Num a => Ratio a nan = 0 :% 0 -ratext :: forall a k. (Bounded a, Integral a) => Conn k Rational (Extended a)-ratext = Conn f g h+ratext :: forall a k. (Bounded a, Integral a) => Cast k Rational (Extended a)+ratext = Cast f g h   where     f = extend (~~ ninf) (\x -> x ~~ nan || x > high) $ \x -> if x < low then minBound else ceiling x @@ -181,19 +135,6 @@  --low = -1 - high -toFractional :: Fractional a => (Rational -> a) -> Rational -> a-toFractional f x-    | x ~~ nan = 0 / 0-    | x ~~ ninf = (-1) / 0-    | x ~~ pinf = 1 / 0-    | otherwise = f x--fromFractional :: (Order a, Fractional a) => (a -> Rational) -> a -> Rational-fromFractional f x-    | x ~~ 0 / 0 = nan-    | x ~~ (-1) / 0 = ninf-    | x ~~ 1 / 0 = pinf-    | otherwise = f x  {- pabs :: (Lattice a, Eq a, Num a) => a -> a

@@ -17,9 +17,9 @@     SystemTime (..), ) where -import safe Data.Connection.Conn+import safe Data.Connection.Cast import safe Data.Connection.Fixed-import safe Data.Connection.Ratio+import safe Data.Connection.Float import safe Data.Int import safe Data.Order.Syntax import safe Data.Time.Clock.System@@ -34,8 +34,8 @@ -------------------------  -- | The 'Int' is valued in seconds-sysixx :: Conn k SystemTime Int-sysixx = Conn f g h+sysixx :: Cast k SystemTime Int+sysixx = Cast f g h   where     f (normalize -> MkSystemTime s n) = fromIntegral s + if n == 0 then 0 else 1     g i = MkSystemTime (fromIntegral i) 0@@ -43,29 +43,29 @@  -- | The 'Float' is valued in seconds. ----- >>> Data.Connection.ceiling f32sys (0/0)+-- >>> Data.Connection.Cast.ceiling f32sys (0/0) -- PosInf--- >>> Data.Connection.ceiling f32sys pi+-- >>> Data.Connection.Cast.ceiling f32sys pi -- Finite (MkSystemTime {systemSeconds = 3, systemNanoseconds = 141592742})-f32sys :: Conn 'L Float (Extended SystemTime)-f32sys = connL ratf32 >>> ratsys+f32sys :: Cast 'L Float (Extended SystemTime)+f32sys = swapL ratf32 >>> ratsys  -- | The 'Double' is valued in seconds. ----- >>> Data.Connection.ceiling f64sys (0/0)+-- >>> Data.Connection.Cast.ceiling f64sys (0/0) -- PosInf--- >>> Data.Connection.ceiling f64sys pi+-- >>> Data.Connection.Cast.ceiling f64sys pi -- Finite (MkSystemTime {systemSeconds = 3, systemNanoseconds = 141592654})-f64sys :: Conn 'L Double (Extended SystemTime)-f64sys = connL ratf64 >>> ratsys+f64sys :: Cast 'L Double (Extended SystemTime)+f64sys = swapL ratf64 >>> ratsys  -- | The 'Rational' is valued in seconds.-ratsys :: Conn k Rational (Extended SystemTime)+ratsys :: Cast k Rational (Extended SystemTime) ratsys = ratfix >>> f09sys  -- | The 'Nano' is valued in seconds (to nanosecond precision).-f09sys :: Conn k (Extended Nano) (Extended SystemTime)-f09sys = Conn f g h+f09sys :: Cast k (Extended Nano) (Extended SystemTime)+f09sys = Cast f g h   where     f NegInf = NegInf     f (Finite i) = extend (const False) (> max64) (fromNanoSecs . clamp) i@@ -89,7 +89,7 @@ -- >>> divMod (maxBound @Word32) (10^9) -- (4,294967295) diffSystemTime :: SystemTime -> SystemTime -> Double-diffSystemTime x y = inner f64sys $ round2 ratsys (-) (Finite x) (Finite y)+diffSystemTime x y = upper f64sys $ round2 ratsys (-) (Finite x) (Finite y)  -- Internal 

@@ -2,6 +2,9 @@ {-# LANGUAGE DataKinds #-}  module Data.Connection.Word (+    -- * Bool+    bndbin,+     -- * Word8     i08w08, @@ -21,6 +24,7 @@     w08w64,     w16w64,     w32w64,+    wxxw64,     i08w64,     i16w64,     i32w64,@@ -52,135 +56,154 @@     intnat, ) where -import safe Data.Connection.Conn+import safe Data.Connection.Cast import safe Data.Int import safe Data.Word import safe Numeric.Natural +{-# INLINEABLE bndbin #-}+bndbin :: (Eq a, Bounded a) => Cast k a Bool+bndbin = Cast f g h+  where+    f i+        | i == minBound = False+        | otherwise = True+    +    g x = if x then maxBound else minBound++    h i+        | i == maxBound = True+        | otherwise = False+ -- Word8-i08w08 :: Conn 'L Int8 Word8-i08w08 = unsigned+i08w08 :: Cast 'L Int8 Word8+i08w08 = conn  -- Word16-w08w16 :: Conn 'L Word8 Word16-w08w16 = unsigned+w08w16 :: Cast 'L Word8 Word16+w08w16 = conn -i08w16 :: Conn 'L Int8 Word16-i08w16 = unsigned+i08w16 :: Cast 'L Int8 Word16+i08w16 = conn -i16w16 :: Conn 'L Int16 Word16-i16w16 = unsigned+i16w16 :: Cast 'L Int16 Word16+i16w16 = conn  -- Word32-w08w32 :: Conn 'L Word8 Word32-w08w32 = unsigned+w08w32 :: Cast 'L Word8 Word32+w08w32 = conn -w16w32 :: Conn 'L Word16 Word32-w16w32 = unsigned+w16w32 :: Cast 'L Word16 Word32+w16w32 = conn -i08w32 :: Conn 'L Int8 Word32-i08w32 = unsigned+i08w32 :: Cast 'L Int8 Word32+i08w32 = conn -i16w32 :: Conn 'L Int16 Word32-i16w32 = unsigned+i16w32 :: Cast 'L Int16 Word32+i16w32 = conn -i32w32 :: Conn 'L Int32 Word32-i32w32 = unsigned+i32w32 :: Cast 'L Int32 Word32+i32w32 = conn  -- Word64-w08w64 :: Conn 'L Word8 Word64-w08w64 = unsigned+w08w64 :: Cast 'L Word8 Word64+w08w64 = conn -w16w64 :: Conn 'L Word16 Word64-w16w64 = unsigned+w16w64 :: Cast 'L Word16 Word64+w16w64 = conn -w32w64 :: Conn 'L Word32 Word64-w32w64 = unsigned+w32w64 :: Cast 'L Word32 Word64+w32w64 = conn -i08w64 :: Conn 'L Int8 Word64-i08w64 = unsigned+-- | /Caution/: This assumes that 'Word' on your system is 64 bits.+wxxw64 :: Cast k Word Word64+wxxw64 = Cast fromIntegral fromIntegral fromIntegral -i16w64 :: Conn 'L Int16 Word64-i16w64 = unsigned+i08w64 :: Cast 'L Int8 Word64+i08w64 = conn -i32w64 :: Conn 'L Int32 Word64-i32w64 = unsigned+i16w64 :: Cast 'L Int16 Word64+i16w64 = conn -i64w64 :: Conn 'L Int64 Word64-i64w64 = unsigned+i32w64 :: Cast 'L Int32 Word64+i32w64 = conn -ixxw64 :: Conn 'L Int Word64-ixxw64 = unsigned+i64w64 :: Cast 'L Int64 Word64+i64w64 = conn +ixxw64 :: Cast 'L Int Word64+ixxw64 = conn+ -- Word-w08wxx :: Conn 'L Word8 Word-w08wxx = unsigned+w08wxx :: Cast 'L Word8 Word+w08wxx = conn -w16wxx :: Conn 'L Word16 Word-w16wxx = unsigned+w16wxx :: Cast 'L Word16 Word+w16wxx = conn -w32wxx :: Conn 'L Word32 Word-w32wxx = unsigned+w32wxx :: Cast 'L Word32 Word+w32wxx = conn  -- | /Caution/: This assumes that 'Word' on your system is 64 bits.-w64wxx :: Conn k Word64 Word-w64wxx = Conn fromIntegral fromIntegral fromIntegral+w64wxx :: Cast k Word64 Word+w64wxx = Cast fromIntegral fromIntegral fromIntegral -i08wxx :: Conn 'L Int8 Word-i08wxx = unsigned+i08wxx :: Cast 'L Int8 Word+i08wxx = conn -i16wxx :: Conn 'L Int16 Word-i16wxx = unsigned+i16wxx :: Cast 'L Int16 Word+i16wxx = conn -i32wxx :: Conn 'L Int32 Word-i32wxx = unsigned+i32wxx :: Cast 'L Int32 Word+i32wxx = conn -i64wxx :: Conn 'L Int64 Word-i64wxx = unsigned+i64wxx :: Cast 'L Int64 Word+i64wxx = conn -ixxwxx :: Conn 'L Int Word-ixxwxx = unsigned+ixxwxx :: Cast 'L Int Word+ixxwxx = conn  -- Natural-w08nat :: Conn 'L Word8 Natural-w08nat = unsigned+w08nat :: Cast 'L Word8 Natural+w08nat = conn -w16nat :: Conn 'L Word16 Natural-w16nat = unsigned+w16nat :: Cast 'L Word16 Natural+w16nat = conn -w32nat :: Conn 'L Word32 Natural-w32nat = unsigned+w32nat :: Cast 'L Word32 Natural+w32nat = conn -w64nat :: Conn 'L Word64 Natural-w64nat = unsigned+w64nat :: Cast 'L Word64 Natural+w64nat = conn -wxxnat :: Conn 'L Word Natural-wxxnat = unsigned+wxxnat :: Cast 'L Word Natural+wxxnat = conn -i08nat :: Conn 'L Int8 Natural-i08nat = unsigned+i08nat :: Cast 'L Int8 Natural+i08nat = conn -i16nat :: Conn 'L Int16 Natural-i16nat = unsigned+i16nat :: Cast 'L Int16 Natural+i16nat = conn -i32nat :: Conn 'L Int32 Natural-i32nat = unsigned+i32nat :: Cast 'L Int32 Natural+i32nat = conn -i64nat :: Conn 'L Int64 Natural-i64nat = unsigned+i64nat :: Cast 'L Int64 Natural+i64nat = conn -ixxnat :: Conn 'L Int Natural-ixxnat = unsigned+ixxnat :: Cast 'L Int Natural+ixxnat = conn -intnat :: Conn 'L Integer Natural-intnat = ConnL (fromIntegral . max 0) fromIntegral+intnat :: Cast 'L Integer Natural+intnat = CastL (fromIntegral . max 0) fromIntegral  --------------------------------------------------------------------- -- Internal --------------------------------------------------------------------- -unsigned :: (Bounded a, Integral a, Integral b) => Conn 'L a b-unsigned = ConnL f g+{-# INLINE conn #-}+conn :: (Bounded a, Integral a, Integral b) => Cast 'L a b+conn = CastL f g   where     f = fromIntegral . max 0     g = fromIntegral . min (f maxBound)

@@ -62,7 +62,7 @@  import safe Data.Bifunctor (bimap) import safe Data.Bool hiding (not)-import safe Data.Connection.Conn+import safe Data.Connection.Cast import safe Data.Either import safe Data.Int import safe qualified Data.IntMap as IntMap@@ -150,12 +150,12 @@     -- | The defining connection of a bound semilattice.     --     -- 'bottom' and 'top' are defined by the left and right adjoints to /a -> ()/.-    bound :: Conn k () a+    bound :: Cast k () a      -- | The defining connection of a semilattice.     --     -- '\/' and '/\' are defined by the left and right adjoints to /a -> (a, a)/.-    semilattice :: Conn k (a, a) a+    semilattice :: Cast k (a, a) a  infixr 6 /\ -- comment for the parser @@ -270,9 +270,9 @@ class Semilattice k a => Algebra k a where     -- | The defining connection of a (co-)Heyting algebra.     ---    -- > algebra @'L x = ConnL (\\ x) (\/ x)-    -- > algebra @'R x = ConnR (x /\) (x //)-    algebra :: a -> Conn k a a+    -- > algebra @'L x = CastL (\\ x) (\/ x)+    -- > algebra @'R x = CastR (x /\) (x //)+    algebra :: a -> Cast k a a  ------------------------------------------------------------------------------- -- Heyting@@ -338,14 +338,14 @@ middle x = x \/ neg x  -- | Default constructor for a Algebra algebra.-heyting :: Meet a => (a -> a -> a) -> a -> ConnR a a-heyting f a = ConnR (a /\) (a `f`)+heyting :: Meet a => (a -> a -> a) -> a -> Cast 'R a a+heyting f a = CastR (a /\) (a `f`)  -- | An adjunction between a Algebra algebra and its Boolean sub-algebra. -- -- Double negation is a meet-preserving monad.-booleanR :: Heyting a => ConnR a a-booleanR = ConnR (neg . neg) inj+booleanR :: Heyting a => Cast 'R a a+booleanR = CastR (neg . neg) inj   where     -- Check that /x/ is a regular element     -- See https://ncatlab.org/nlab/show/regular+element@@ -423,14 +423,14 @@ boundary x = x /\ non x  -- | Default constructor for a co-Heyting algebra.-coheyting :: Join a => (a -> a -> a) -> a -> ConnL a a-coheyting f a = ConnL (`f` a) (\/ a)+coheyting :: Join a => (a -> a -> a) -> a -> Cast 'L a a+coheyting f a = CastL (`f` a) (\/ a)  -- | An adjunction between a co-Heyting algebra and its Boolean sub-algebra. -- -- Double negation is a join-preserving comonad.-booleanL :: Coheyting a => ConnL a a-booleanL = ConnL inj (non . non)+booleanL :: Coheyting a => Cast 'L a a+booleanL = CastL inj (non . non)   where     -- Check that /x/ is a regular element     -- See https://ncatlab.org/nlab/show/regular+element@@ -489,11 +489,11 @@ converseR x = not x // bottom  -- | Default constructor for a Heyting algebra.-symmetricR :: Symmetric a => a -> ConnR a a+symmetricR :: Symmetric a => a -> Cast 'R a a symmetricR = heyting $ \x y -> not (not y \\ not x)  -- | Default constructor for a co-Heyting algebra.-symmetricL :: Symmetric a => a -> ConnL a a+symmetricL :: Symmetric a => a -> Cast 'L a a symmetricL = coheyting $ \x y -> not (not y // not x)  -------------------------------------------------------------------------------@@ -514,8 +514,8 @@ -- > non = not = neg class Symmetric a => Boolean a where     -- | A witness to the lawfulness of a boolean algebra.-    boolean :: Conn k a a-    boolean = Conn (converseR . converseL) id (converseL . converseR)+    boolean :: Cast k a a+    boolean = Cast (converseR . converseL) id (converseL . converseR)  ------------------------------------------------------------------------------- -- Instances@@ -642,8 +642,8 @@ -------------------------------------------------------------------------------  instance (Lattice a, Lattice b) => Semilattice k (a, b) where-    bound = Conn (const (bottom, bottom)) (const ()) (const (top, top))-    semilattice = Conn (uncurry joinTuple) fork (uncurry meetTuple)+    bound = Cast (const (bottom, bottom)) (const ()) (const (top, top))+    semilattice = Cast (uncurry joinTuple) fork (uncurry meetTuple)  instance (Heyting a, Heyting b) => Algebra 'R (a, b) where     algebra (a, b) = algebra a `strong` algebra b@@ -661,12 +661,12 @@ -------------------------------------------------------------------------------  instance Join a => Semilattice 'L (Maybe a) where-    bound = ConnL (const Nothing) (const ())-    semilattice = ConnL (uncurry joinMaybe) fork+    bound = CastL (const Nothing) (const ())+    semilattice = CastL (uncurry joinMaybe) fork  instance Meet a => Semilattice 'R (Maybe a) where-    bound = ConnR (const ()) (const $ Just top)-    semilattice = ConnR fork (uncurry meetMaybe)+    bound = CastR (const ()) (const $ Just top)+    semilattice = CastR fork (uncurry meetMaybe)  instance Heyting a => Algebra 'R (Maybe a) where     algebra = heyting f@@ -676,12 +676,12 @@         f _ Nothing = Nothing  instance Join a => Semilattice 'L (Extended a) where-    bound = Conn (const NegInf) (const ()) (const PosInf)-    semilattice = ConnL (uncurry joinExtended) fork+    bound = Cast (const NegInf) (const ()) (const PosInf)+    semilattice = CastL (uncurry joinExtended) fork  instance Meet a => Semilattice 'R (Extended a) where-    bound = Conn (const NegInf) (const ()) (const PosInf)-    semilattice = ConnR fork (uncurry meetExtended)+    bound = Cast (const NegInf) (const ()) (const PosInf)+    semilattice = CastR fork (uncurry meetExtended)  instance Heyting a => Algebra 'R (Extended a) where     algebra = heyting f@@ -696,12 +696,12 @@  -- | All minimal elements of the upper lattice cover all maximal elements of the lower lattice. instance (Join a, Join b) => Semilattice 'L (Either a b) where-    bound = ConnL (const $ Left bottom) (const ())-    semilattice = ConnL (uncurry joinEither) fork+    bound = CastL (const $ Left bottom) (const ())+    semilattice = CastL (uncurry joinEither) fork  instance (Meet a, Meet b) => Semilattice 'R (Either a b) where-    bound = ConnR (const ()) (const $ Right top)-    semilattice = ConnR fork (uncurry meetEither)+    bound = CastR (const ()) (const $ Right top)+    semilattice = CastR fork (uncurry meetEither)  -- | -- Subdirectly irreducible Algebra algebra.@@ -727,36 +727,36 @@  {- instance Total a => Connection k (Set.Set a, Set.Set a) (Set.Set a) where-    semilattice = Conn (uncurry Set.union) fork (uncurry Set.intersection)+    semilattice = Cast (uncurry Set.union) fork (uncurry Set.intersection)  instance Connection 'L () IntSet.IntSet where-    bound = ConnL (const IntSet.empty) (const ())+    bound = CastL (const IntSet.empty) (const ())  instance Connection k (IntSet.IntSet, IntSet.IntSet) IntSet.IntSet where-    semilattice = Conn (uncurry IntSet.union) fork (uncurry IntSet.intersection)+    semilattice = Cast (uncurry IntSet.union) fork (uncurry IntSet.intersection)  instance (Total a, Preorder b) => Connection 'L () (Map.Map a b) where-    bound = ConnL (const Map.empty) (const ())+    bound = CastL (const Map.empty) (const ())  instance (Total a, Left (b, b) b) => Connection 'L (Map.Map a b, Map.Map a b) (Map.Map a b) where-    semilattice = ConnL (uncurry $ Map.unionWith join) fork+    semilattice = CastL (uncurry $ Map.unionWith join) fork  instance (Total a, Right (b, b) b) => Connection 'R (Map.Map a b, Map.Map a b) (Map.Map a b) where-    semilattice = ConnR fork (uncurry $ Map.intersectionWith meet)+    semilattice = CastR fork (uncurry $ Map.intersectionWith meet)  instance Preorder a => Connection 'L () (IntMap.IntMap a) where-    bound = ConnL (const IntMap.empty) (const ())+    bound = CastL (const IntMap.empty) (const ())  instance Left (a, a) a => Connection 'L (IntMap.IntMap a, IntMap.IntMap a) (IntMap.IntMap a) where-    semilattice = ConnL (uncurry $ IntMap.unionWith join) fork+    semilattice = CastL (uncurry $ IntMap.unionWith join) fork  instance Right (a, a) a => Connection 'R (IntMap.IntMap a, IntMap.IntMap a) (IntMap.IntMap a) where-    semilattice = ConnR fork (uncurry $ IntMap.intersectionWith meet)+    semilattice = CastR fork (uncurry $ IntMap.intersectionWith meet) -}  instance Total a => Semilattice 'L (Set.Set a) where-    bound = ConnL (const Set.empty) (const ())-    semilattice = ConnL (uncurry Set.union) fork+    bound = CastL (const Set.empty) (const ())+    semilattice = CastL (uncurry Set.union) fork  instance Total a => Algebra 'L (Set.Set a) where     algebra = coheyting (Set.\\)@@ -770,8 +770,8 @@ --instance (Total a, U.Finite a) => Boolean (Set.Set a) where  instance Semilattice k IntSet.IntSet where-    bound = Conn (const IntSet.empty) (const ()) (const $ IntSet.fromList [minBound .. maxBound])-    semilattice = Conn (uncurry IntSet.union) fork (uncurry IntSet.intersection)+    bound = Cast (const IntSet.empty) (const ()) (const $ IntSet.fromList [minBound .. maxBound])+    semilattice = Cast (uncurry IntSet.union) fork (uncurry IntSet.intersection)  instance Algebra 'L IntSet.IntSet where     algebra = coheyting (IntSet.\\)@@ -796,9 +796,9 @@ -}  instance (Total k, Join a) => Semilattice 'L (Map.Map k a) where-    bound = ConnL (const Map.empty) (const ())+    bound = CastL (const Map.empty) (const ()) -    semilattice = ConnL f fork+    semilattice = CastL f fork       where         f = uncurry $ Map.unionWith (\/) @@ -806,9 +806,9 @@     algebra = coheyting (Map.\\)  instance (Join a) => Semilattice 'L (IntMap.IntMap a) where-    bound = ConnL (const IntMap.empty) (const ())+    bound = CastL (const IntMap.empty) (const ()) -    semilattice = ConnL f fork+    semilattice = CastL f fork       where         f = uncurry $ IntMap.unionWith (\/) 

@@ -149,7 +149,7 @@ -- -- --- adjointL $ ConnL (\x -> y \\ not x) (\z -> not z // not y)+-- adjointL $ CastL (\x -> y \\ not x) (\z -> not z // not y) symmetric1 :: Biheyting a => a -> Bool symmetric1 x = neg x <= non x 

@@ -92,13 +92,13 @@  {- instance Bounded 'L a => Connection k (Maybe a) (Interval a) where-  conn = Conn f g h where+  conn = Cast f g h where     f = maybe iempty singleton     g = maybe Nothing (Just . uncurry (\/)) . endpts     h = maybe iempty $ \x -> minimal ... x  instance Lattice a => Connection k (Interval a) (Maybe a) where-  conn = Conn f g h where+  conn = Cast f g h where     f = maybe Nothing (Just . uncurry (\/)) . endpts     g = maybe iempty singleton     h = maybe Nothing (Just . uncurry (/\)) . endpts

@@ -8,7 +8,6 @@ import qualified Data.Connection.Property as Prop import Data.Fixed import Hedgehog-import qualified Hedgehog.Gen as G import Test.Data.Connection  prop_connection_ratf06 :: Property

@@ -38,6 +38,45 @@     assert $ Prop.monotonic f32w16 x x' y y'     assert $ Prop.idempotent f32w16 x y +prop_connection_f32w32 :: Property+prop_connection_f32w32 = withTests 1000 . property $ do+    x <- forAll f32+    x' <- forAll f32+    y <- forAll $ gen_extended $ G.integral (ri @Word32)+    y' <- forAll $ gen_extended $ G.integral (ri @Word32)++    assert $ Prop.adjointL f32w32 x y+    assert $ Prop.closedL f32w32 x+    assert $ Prop.kernelL f32w32 y+    assert $ Prop.monotonicL f32w32 x x' y y'+    assert $ Prop.idempotentL f32w32 x y++prop_connection_f32w64 :: Property+prop_connection_f32w64 = withTests 1000 . property $ do+    x <- forAll f32+    x' <- forAll f32+    y <- forAll $ gen_extended $ G.integral (ri @Word64)+    y' <- forAll $ gen_extended $ G.integral (ri @Word64)++    assert $ Prop.adjointL f32w64 x y+    assert $ Prop.closedL f32w64 x+    assert $ Prop.kernelL f32w64 y+    assert $ Prop.monotonicL f32w64 x x' y y'+    assert $ Prop.idempotentL f32w64 x y++prop_connection_f32nat :: Property+prop_connection_f32nat = withTests 1000 . property $ do+    x <- forAll f32+    x' <- forAll f32+    y <- forAll $ gen_extended $ G.integral rn+    y' <- forAll $ gen_extended $ G.integral rn++    assert $ Prop.adjointL f32nat x y+    assert $ Prop.closedL f32nat x+    assert $ Prop.kernelL f32nat y+    assert $ Prop.monotonicL f32nat x x' y y'+    assert $ Prop.idempotentL f32nat x y+ prop_connection_f32i08 :: Property prop_connection_f32i08 = withTests 1000 . property $ do     x <- forAll f32@@ -64,6 +103,71 @@     assert $ Prop.monotonic f32i16 x x' y y'     assert $ Prop.idempotent f32i16 x y +prop_connection_f32i32 :: Property+prop_connection_f32i32 = withTests 1000 . property $ do+    x <- forAll f32+    x' <- forAll f32+    y <- forAll $ gen_extended $ G.integral (ri @Int32)+    y' <- forAll $ gen_extended $ G.integral (ri @Int32)++    assert $ Prop.adjointL f32i32 x y+    assert $ Prop.closedL f32i32 x+    assert $ Prop.kernelL f32i32 y+    assert $ Prop.monotonicL f32i32 x x' y y'+    assert $ Prop.idempotentL f32i32 x y++prop_connection_f32i64 :: Property+prop_connection_f32i64 = withTests 1000 . property $ do+    x <- forAll f32+    x' <- forAll f32+    y <- forAll $ gen_extended $ G.integral (ri @Int64)+    y' <- forAll $ gen_extended $ G.integral (ri @Int64)++    assert $ Prop.adjointL f32i64 x y+    assert $ Prop.closedL f32i64 x+    assert $ Prop.kernelL f32i64 y+    assert $ Prop.monotonicL f32i64 x x' y y'+    assert $ Prop.idempotentL f32i64 x y++prop_connection_f32int :: Property+prop_connection_f32int = withTests 1000 . property $ do+    x <- forAll f32+    x' <- forAll f32+    y <- forAll $ gen_extended $ G.integral ri'+    y' <- forAll $ gen_extended $ G.integral ri'++    assert $ Prop.adjointL f32int x y+    assert $ Prop.closedL f32int x+    assert $ Prop.kernelL f32int y+    assert $ Prop.monotonicL f32int x x' y y'+    assert $ Prop.idempotentL f32int x y++prop_connection_f64f32 :: Property+prop_connection_f64f32 = withTests 1000 . property $ do+    x <- forAll f64+    x' <- forAll f64+    y <- forAll f32+    y' <- forAll f32++    assert $ Prop.adjoint (f64f32) x y+    assert $ Prop.closed (f64f32) x+    assert $ Prop.kernel (f64f32) y+    assert $ Prop.monotonic (f64f32) x x' y y'+    assert $ Prop.idempotent (f64f32) x y++prop_connection_ratf32 :: Property+prop_connection_ratf32 = withTests 1000 . property $ do+    x <- forAll rat'+    x' <- forAll rat'+    y <- forAll f32+    y' <- forAll f32++    assert $ Prop.adjoint (ratf32) x y+    assert $ Prop.closed (ratf32) x+    assert $ Prop.kernel (ratf32) y+    assert $ Prop.monotonic (ratf32) x x' y y'+    assert $ Prop.idempotent (ratf32) x y+ prop_connection_f64w08 :: Property prop_connection_f64w08 = withTests 1000 . property $ do     x <- forAll f64@@ -103,6 +207,32 @@     assert $ Prop.monotonic f64w32 x x' y y'     assert $ Prop.idempotent f64w32 x y +prop_connection_f64w64 :: Property+prop_connection_f64w64 = withTests 1000 . property $ do+    x <- forAll f64+    x' <- forAll f64+    y <- forAll $ gen_extended $ G.integral (ri @Word64)+    y' <- forAll $ gen_extended $ G.integral (ri @Word64)++    assert $ Prop.adjointL f64w64 x y+    assert $ Prop.closedL f64w64 x+    assert $ Prop.kernelL f64w64 y+    assert $ Prop.monotonicL f64w64 x x' y y'+    assert $ Prop.idempotentL f64w64 x y++prop_connection_f64nat :: Property+prop_connection_f64nat = withTests 1000 . property $ do+    x <- forAll f64+    x' <- forAll f64+    y <- forAll $ gen_extended $ G.integral rn+    y' <- forAll $ gen_extended $ G.integral rn++    assert $ Prop.adjointL f64nat x y+    assert $ Prop.closedL f64nat x+    assert $ Prop.kernelL f64nat y+    assert $ Prop.monotonicL f64nat x x' y y'+    assert $ Prop.idempotentL f64nat x y+ prop_connection_f64i08 :: Property prop_connection_f64i08 = withTests 1000 . property $ do     x <- forAll f64@@ -142,18 +272,44 @@     assert $ Prop.monotonic f64i32 x x' y y'     assert $ Prop.idempotent f64i32 x y -prop_connection_f64f32 :: Property-prop_connection_f64f32 = withTests 1000 . property $ do+prop_connection_f64i64 :: Property+prop_connection_f64i64 = withTests 1000 . property $ do     x <- forAll f64     x' <- forAll f64-    y <- forAll f32-    y' <- forAll f32+    y <- forAll $ gen_extended $ G.integral (ri @Int64)+    y' <- forAll $ gen_extended $ G.integral (ri @Int64) -    assert $ Prop.adjoint (f64f32) x y-    assert $ Prop.closed (f64f32) x-    assert $ Prop.kernel (f64f32) y-    assert $ Prop.monotonic (f64f32) x x' y y'-    assert $ Prop.idempotent (f64f32) x y+    assert $ Prop.adjointL f64i64 x y+    assert $ Prop.closedL f64i64 x+    assert $ Prop.kernelL f64i64 y+    assert $ Prop.monotonicL f64i64 x x' y y'+    assert $ Prop.idempotentL f64i64 x y++prop_connection_f64int :: Property+prop_connection_f64int = withTests 1000 . property $ do+    x <- forAll f64+    x' <- forAll f64+    y <- forAll $ gen_extended $ G.integral ri'+    y' <- forAll $ gen_extended $ G.integral ri'++    assert $ Prop.adjointL f64int x y+    assert $ Prop.closedL f64int x+    assert $ Prop.kernelL f64int y+    assert $ Prop.monotonicL f64int x x' y y'+    assert $ Prop.idempotentL f64int x y++prop_connection_ratf64 :: Property+prop_connection_ratf64 = withTests 1000 . property $ do+    x <- forAll rat'+    x' <- forAll rat'+    y <- forAll f64+    y' <- forAll f64++    assert $ Prop.adjoint (ratf64) x y+    assert $ Prop.closed (ratf64) x+    assert $ Prop.kernel (ratf64) y+    assert $ Prop.monotonic (ratf64) x x' y y'+    assert $ Prop.idempotent (ratf64) x y  tests :: IO Bool tests = checkParallel $$(discover)

@@ -1,4 +1,6 @@ {-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE DataKinds #-} module Test.Data.Connection.Int where  import Data.Connection.Int@@ -12,213 +14,201 @@ prop_connections_int16 :: Property prop_connections_int16 = withTests 1000 . property $ do -  i08 <- forAll $ G.integral (ri @Int8)-  w08 <- forAll $ G.integral (ri @Word8)-  i16 <- forAll $ gen_maybe $ G.integral (ri @Int16)+  i08 <- forAll $ gen_extended $ G.integral (ri @Int8)+  w08 <- forAll $ gen_extended $ G.integral (ri @Word8)+  i16 <- forAll $ G.integral (ri @Int16) -  i08' <- forAll $ G.integral (ri @Int8)-  w08' <- forAll $ G.integral (ri @Word8)-  i16' <- forAll $ gen_maybe $ G.integral (ri @Int16)+  i08' <- forAll $ gen_extended $ G.integral (ri @Int8)+  w08' <- forAll $ gen_extended $ G.integral (ri @Word8)+  i16' <- forAll $ G.integral (ri @Int16) -  assert $ Prop.adjointL w08i16 w08 i16-  assert $ Prop.closedL w08i16 w08-  assert $ Prop.kernelL w08i16 i16-  assert $ Prop.monotonicL w08i16 w08 w08' i16 i16'-  assert $ Prop.idempotentL w08i16 w08 i16+  assert $ Prop.adjoint w08i16 w08 i16+  assert $ Prop.closed w08i16 w08+  assert $ Prop.kernel w08i16 i16+  assert $ Prop.monotonic w08i16 w08 w08' i16 i16'+  assert $ Prop.idempotent w08i16 w08 i16 -  assert $ Prop.adjointL i08i16 i08 i16-  assert $ Prop.closedL i08i16 i08-  assert $ Prop.kernelL i08i16 i16-  assert $ Prop.monotonicL i08i16 i08 i08' i16 i16'-  assert $ Prop.idempotentL i08i16 i08 i16+  assert $ Prop.adjoint i08i16 i08 i16+  assert $ Prop.closed i08i16 i08+  assert $ Prop.kernel i08i16 i16+  assert $ Prop.monotonic i08i16 i08 i08' i16 i16'+  assert $ Prop.idempotent i08i16 i08 i16  prop_connections_int32 :: Property prop_connections_int32 = 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 $ gen_maybe $ G.integral (ri @Int32)+  i08 <- forAll $ gen_extended $ G.integral (ri @Int8)+  w08 <- forAll $ gen_extended $ G.integral (ri @Word8)+  i16 <- forAll $ gen_extended $ G.integral (ri @Int16)+  w16 <- forAll $ gen_extended $ G.integral (ri @Word16)+  i32 <- forAll $ G.integral (ri @Int32) -  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 $ gen_maybe $ G.integral (ri @Int32)+  i08' <- forAll $ gen_extended $ G.integral (ri @Int8)+  w08' <- forAll $ gen_extended $ G.integral (ri @Word8)+  i16' <- forAll $ gen_extended $ G.integral (ri @Int16)+  w16' <- forAll $ gen_extended $ G.integral (ri @Word16)+  i32' <- forAll $ G.integral (ri @Int32) -  assert $ Prop.adjointL w08i32 w08 i32-  assert $ Prop.closedL w08i32 w08-  assert $ Prop.kernelL w08i32 i32-  assert $ Prop.monotonicL w08i32 w08 w08' i32 i32'-  assert $ Prop.idempotentL w08i32 w08 i32+  assert $ Prop.adjoint w08i32 w08 i32+  assert $ Prop.closed w08i32 w08+  assert $ Prop.kernel w08i32 i32+  assert $ Prop.monotonic w08i32 w08 w08' i32 i32'+  assert $ Prop.idempotent w08i32 w08 i32   -  assert $ Prop.adjointL w16i32 w16 i32-  assert $ Prop.closedL w16i32 w16-  assert $ Prop.kernelL w16i32 i32-  assert $ Prop.monotonicL w16i32 w16 w16' i32 i32'-  assert $ Prop.idempotentL w16i32 w16 i32+  assert $ Prop.adjoint w16i32 w16 i32+  assert $ Prop.closed w16i32 w16+  assert $ Prop.kernel w16i32 i32+  assert $ Prop.monotonic w16i32 w16 w16' i32 i32'+  assert $ Prop.idempotent w16i32 w16 i32 -  assert $ Prop.adjointL i08i32 i08 i32-  assert $ Prop.closedL i08i32 i08-  assert $ Prop.kernelL i08i32 i32-  assert $ Prop.monotonicL i08i32 i08 i08' i32 i32'-  assert $ Prop.idempotentL i08i32 i08 i32+  assert $ Prop.adjoint i08i32 i08 i32+  assert $ Prop.closed i08i32 i08+  assert $ Prop.kernel i08i32 i32+  assert $ Prop.monotonic i08i32 i08 i08' i32 i32'+  assert $ Prop.idempotent i08i32 i08 i32   -  assert $ Prop.adjointL i16i32 i16 i32-  assert $ Prop.closedL i16i32 i16-  assert $ Prop.kernelL i16i32 i32-  assert $ Prop.monotonicL i16i32 i16 i16' i32 i32'-  assert $ Prop.idempotentL i16i32 i16 i32+  assert $ Prop.adjoint i16i32 i16 i32+  assert $ Prop.closed i16i32 i16+  assert $ Prop.kernel i16i32 i32+  assert $ Prop.monotonic i16i32 i16 i16' i32 i32'+  assert $ Prop.idempotent i16i32 i16 i32  prop_connections_int64 :: Property prop_connections_int64 = 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 $ gen_maybe $ G.integral (ri @Int64)+  i08 <- forAll $ gen_extended $ G.integral (ri @Int8)+  w08 <- forAll $ gen_extended $ G.integral (ri @Word8)+  i16 <- forAll $ gen_extended $ G.integral (ri @Int16)+  w16 <- forAll $ gen_extended $ G.integral (ri @Word16)+  i32 <- forAll $ gen_extended $ G.integral (ri @Int32)+  w32 <- forAll $ gen_extended $ G.integral (ri @Word32)+  i64 <- forAll $ G.integral (ri @Int64) -  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 $ gen_maybe $ G.integral (ri @Int64)+  i08' <- forAll $ gen_extended $ G.integral (ri @Int8)+  w08' <- forAll $ gen_extended $ G.integral (ri @Word8)+  i16' <- forAll $ gen_extended $ G.integral (ri @Int16)+  w16' <- forAll $ gen_extended $ G.integral (ri @Word16)+  i32' <- forAll $ gen_extended $ G.integral (ri @Int32)+  w32' <- forAll $ gen_extended $ G.integral (ri @Word32)+  i64' <- forAll $ G.integral (ri @Int64) -  assert $ Prop.adjointL w08i64 w08 i64-  assert $ Prop.closedL w08i64 w08-  assert $ Prop.kernelL w08i64 i64-  assert $ Prop.monotonicL w08i64 w08 w08' i64 i64'-  assert $ Prop.idempotentL w08i64 w08 i64+  assert $ Prop.adjoint w08i64 w08 i64+  assert $ Prop.closed w08i64 w08+  assert $ Prop.kernel w08i64 i64+  assert $ Prop.monotonic w08i64 w08 w08' i64 i64'+  assert $ Prop.idempotent w08i64 w08 i64   -  assert $ Prop.adjointL w16i64 w16 i64-  assert $ Prop.closedL w16i64 w16-  assert $ Prop.kernelL w16i64 i64-  assert $ Prop.monotonicL w16i64 w16 w16' i64 i64'-  assert $ Prop.idempotentL w16i64 w16 i64+  assert $ Prop.adjoint w16i64 w16 i64+  assert $ Prop.closed w16i64 w16+  assert $ Prop.kernel w16i64 i64+  assert $ Prop.monotonic w16i64 w16 w16' i64 i64'+  assert $ Prop.idempotent w16i64 w16 i64   -  assert $ Prop.adjointL w32i64 w32 i64-  assert $ Prop.closedL w32i64 w32-  assert $ Prop.kernelL w32i64 i64-  assert $ Prop.monotonicL w32i64 w32 w32' i64 i64'-  assert $ Prop.idempotentL w32i64 w32 i64+  assert $ Prop.adjoint w32i64 w32 i64+  assert $ Prop.closed w32i64 w32+  assert $ Prop.kernel w32i64 i64+  assert $ Prop.monotonic w32i64 w32 w32' i64 i64'+  assert $ Prop.idempotent w32i64 w32 i64 -  assert $ Prop.adjointL i08i64 i08 i64-  assert $ Prop.closedL i08i64 i08-  assert $ Prop.kernelL i08i64 i64-  assert $ Prop.monotonicL i08i64 i08 i08' i64 i64'-  assert $ Prop.idempotentL i08i64 i08 i64+  assert $ Prop.adjoint i08i64 i08 i64+  assert $ Prop.closed i08i64 i08+  assert $ Prop.kernel i08i64 i64+  assert $ Prop.monotonic i08i64 i08 i08' i64 i64'+  assert $ Prop.idempotent i08i64 i08 i64   -  assert $ Prop.adjointL i16i64 i16 i64-  assert $ Prop.closedL i16i64 i16-  assert $ Prop.kernelL i16i64 i64-  assert $ Prop.monotonicL i16i64 i16 i16' i64 i64'-  assert $ Prop.idempotentL i16i64 i16 i64+  assert $ Prop.adjoint i16i64 i16 i64+  assert $ Prop.closed i16i64 i16+  assert $ Prop.kernel i16i64 i64+  assert $ Prop.monotonic i16i64 i16 i16' i64 i64'+  assert $ Prop.idempotent i16i64 i16 i64   -  assert $ Prop.adjointL i32i64 i32 i64-  assert $ Prop.closedL i32i64 i32-  assert $ Prop.kernelL i32i64 i64-  assert $ Prop.monotonicL i32i64 i32 i32' i64 i64'-  assert $ Prop.idempotentL i32i64 i32 i64+  assert $ Prop.adjoint i32i64 i32 i64+  assert $ Prop.closed i32i64 i32+  assert $ Prop.kernel i32i64 i64+  assert $ Prop.monotonic i32i64 i32 i32' i64 i64'+  assert $ Prop.idempotent i32i64 i32 i64  prop_connections_int :: Property prop_connections_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)-  ixx <- forAll $ gen_maybe $ G.integral (ri @Int)-  int <- forAll $ G.integral (ri @Int)+  i08 <- forAll $ gen_extended $ G.integral (ri @Int8)+  w08 <- forAll $ gen_extended $ G.integral (ri @Word8)+  i16 <- forAll $ gen_extended $ G.integral (ri @Int16)+  w16 <- forAll $ gen_extended $ G.integral (ri @Word16)+  i32 <- forAll $ gen_extended $ G.integral (ri @Int32)+  w32 <- forAll $ gen_extended $ G.integral (ri @Word32)+  ixx <- forAll $ G.integral (ri @Int) -  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)-  ixx' <- forAll $ gen_maybe $ G.integral (ri @Int)-  int' <- forAll $ G.integral (ri @Int)+  i08' <- forAll $ gen_extended $ G.integral (ri @Int8)+  w08' <- forAll $ gen_extended $ G.integral (ri @Word8)+  i16' <- forAll $ gen_extended $ G.integral (ri @Int16)+  w16' <- forAll $ gen_extended $ G.integral (ri @Word16)+  i32' <- forAll $ gen_extended $ G.integral (ri @Int32)+  w32' <- forAll $ gen_extended $ G.integral (ri @Word32)+  ixx' <- forAll $ G.integral (ri @Int) -  assert $ Prop.adjointL w08ixx w08 ixx-  assert $ Prop.closedL w08ixx w08-  assert $ Prop.kernelL w08ixx ixx-  assert $ Prop.monotonicL w08ixx w08 w08' ixx ixx'-  assert $ Prop.idempotentL w08ixx w08 ixx+  assert $ Prop.adjoint w08ixx w08 ixx+  assert $ Prop.closed w08ixx w08+  assert $ Prop.kernel w08ixx ixx+  assert $ Prop.monotonic w08ixx w08 w08' ixx ixx'+  assert $ Prop.idempotent w08ixx w08 ixx   -  assert $ Prop.adjointL w16ixx w16 ixx-  assert $ Prop.closedL w16ixx w16-  assert $ Prop.kernelL w16ixx ixx-  assert $ Prop.monotonicL w16ixx w16 w16' ixx ixx'-  assert $ Prop.idempotentL w16ixx w16 ixx+  assert $ Prop.adjoint w16ixx w16 ixx+  assert $ Prop.closed w16ixx w16+  assert $ Prop.kernel w16ixx ixx+  assert $ Prop.monotonic w16ixx w16 w16' ixx ixx'+  assert $ Prop.idempotent w16ixx w16 ixx   -  assert $ Prop.adjointL w32ixx w32 ixx-  assert $ Prop.closedL w32ixx w32-  assert $ Prop.kernelL w32ixx ixx-  assert $ Prop.monotonicL w32ixx w32 w32' ixx ixx'-  assert $ Prop.idempotentL w32ixx w32 ixx+  assert $ Prop.adjoint w32ixx w32 ixx+  assert $ Prop.closed w32ixx w32+  assert $ Prop.kernel w32ixx ixx+  assert $ Prop.monotonic w32ixx w32 w32' ixx ixx'+  assert $ Prop.idempotent w32ixx w32 ixx -  assert $ Prop.adjointL i08ixx i08 ixx-  assert $ Prop.closedL i08ixx i08-  assert $ Prop.kernelL i08ixx ixx-  assert $ Prop.monotonicL i08ixx i08 i08' ixx ixx'-  assert $ Prop.idempotentL i08ixx i08 ixx-  -  assert $ Prop.adjointL i16ixx i16 ixx-  assert $ Prop.closedL i16ixx i16-  assert $ Prop.kernelL i16ixx ixx-  assert $ Prop.monotonicL i16ixx i16 i16' ixx ixx'-  assert $ Prop.idempotentL i16ixx i16 ixx+  assert $ Prop.adjoint i08ixx i08 ixx+  assert $ Prop.closed i08ixx i08+  assert $ Prop.kernel i08ixx ixx+  assert $ Prop.monotonic i08ixx i08 i08' ixx ixx'+  assert $ Prop.idempotent i08ixx i08 ixx   -  assert $ Prop.adjointL i32ixx i32 ixx-  assert $ Prop.closedL i32ixx i32-  assert $ Prop.kernelL i32ixx ixx-  assert $ Prop.monotonicL i32ixx i32 i32' ixx ixx'-  assert $ Prop.idempotentL i32ixx i32 ixx+  assert $ Prop.adjoint i16ixx i16 ixx+  assert $ Prop.closed i16ixx i16+  assert $ Prop.kernel i16ixx ixx+  assert $ Prop.monotonic i16ixx i16 i16' ixx ixx'+  assert $ Prop.idempotent i16ixx i16 ixx   -  assert $ Prop.adjoint i64ixx i64 int-  assert $ Prop.closed i64ixx i64-  assert $ Prop.kernel i64ixx int-  assert $ Prop.monotonic i64ixx i64 i64' int int'-  assert $ Prop.idempotent i64ixx i64 int+  assert $ Prop.adjoint i32ixx i32 ixx+  assert $ Prop.closed i32ixx i32+  assert $ Prop.kernel i32ixx ixx+  assert $ Prop.monotonic i32ixx i32 i32' ixx ixx'+  assert $ Prop.idempotent i32ixx i32 ixx  prop_connections_integer :: Property prop_connections_integer = 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)-  ixx <- forAll $ G.integral (ri @Int)-  wxx <- forAll $ G.integral (ri @Word)+  i08 <- forAll $ gen_extended $ G.integral (ri @Int8)+  w08 <- forAll $ gen_extended $ G.integral (ri @Word8)+  i16 <- forAll $ gen_extended $ G.integral (ri @Int16)+  w16 <- forAll $ gen_extended $ G.integral (ri @Word16)+  i32 <- forAll $ gen_extended $ G.integral (ri @Int32)+  w32 <- forAll $ gen_extended $ G.integral (ri @Word32)+  i64 <- forAll $ gen_extended $ G.integral (ri @Int64)+  w64 <- forAll $ gen_extended $ G.integral (ri @Word64)+  ixx <- forAll $ gen_extended $ G.integral (ri @Int)+  wxx <- forAll $ gen_extended $ G.integral (ri @Word)   int <- forAll $ gen_maybe $ G.integral ri'-  nat <- forAll $ G.integral rn -  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)-  ixx' <- forAll $ G.integral (ri @Int)-  wxx' <- forAll $ G.integral (ri @Word)+  i08' <- forAll $ gen_extended $ G.integral (ri @Int8)+  w08' <- forAll $ gen_extended $ G.integral (ri @Word8)+  i16' <- forAll $ gen_extended $ G.integral (ri @Int16)+  w16' <- forAll $ gen_extended $ G.integral (ri @Word16)+  i32' <- forAll $ gen_extended $ G.integral (ri @Int32)+  w32' <- forAll $ gen_extended $ G.integral (ri @Word32)+  i64' <- forAll $ gen_extended $ G.integral (ri @Int64)+  w64' <- forAll $ gen_extended $ G.integral (ri @Word64)+  ixx' <- forAll $ gen_extended $ G.integral (ri @Int)+  wxx' <- forAll $ gen_extended $ G.integral (ri @Word)   int' <- forAll $ gen_maybe (G.integral ri')-  nat' <- forAll $ G.integral rn      assert $ Prop.adjointL w08int w08 int   assert $ Prop.closedL w08int w08@@ -249,13 +239,6 @@   assert $ Prop.kernelL wxxint int   assert $ Prop.monotonicL wxxint wxx wxx' int int'   assert $ Prop.idempotentL wxxint wxx int--  assert $ Prop.adjointL natint nat int-  assert $ Prop.closedL natint nat-  assert $ Prop.kernelL natint int-  assert $ Prop.monotonicL natint nat nat' int int'-  assert $ Prop.idempotentL natint nat int-       assert $ Prop.adjointL i08int i08 int   assert $ Prop.closedL i08int i08

@@ -156,31 +156,5 @@     assert $ Prop.monotonic (ratint) x x' y y'     assert $ Prop.idempotent (ratint) x y -prop_connection_ratf32 :: Property-prop_connection_ratf32 = withTests 1000 . property $ do-    x <- forAll rat'-    x' <- forAll rat'-    y <- forAll f32-    y' <- forAll f32--    assert $ Prop.adjoint (ratf32) x y-    assert $ Prop.closed (ratf32) x-    assert $ Prop.kernel (ratf32) y-    assert $ Prop.monotonic (ratf32) x x' y y'-    assert $ Prop.idempotent (ratf32) x y--prop_connection_ratf64 :: Property-prop_connection_ratf64 = withTests 1000 . property $ do-    x <- forAll rat'-    x' <- forAll rat'-    y <- forAll f64-    y' <- forAll f64--    assert $ Prop.adjoint (ratf64) x y-    assert $ Prop.closed (ratf64) x-    assert $ Prop.kernel (ratf64) y-    assert $ Prop.monotonic (ratf64) x x' y y'-    assert $ Prop.idempotent (ratf64) x y- tests :: IO Bool tests = checkParallel $$(discover)

@@ -7,8 +7,7 @@ main =     doctest         [ "-isrc"-        , "src/Data/Connection.hs"-        , "src/Data/Connection/Conn.hs"+        , "src/Data/Connection/Cast.hs"         , "src/Data/Connection/Class.hs"         , "src/Data/Connection/Float.hs"         ]