diff --git a/ChangeLog.md b/ChangeLog.md --- a/ChangeLog.md +++ b/ChangeLog.md @@ -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 + diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -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? @@ -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) diff --git a/connections.cabal b/connections.cabal --- a/connections.cabal +++ b/connections.cabal @@ -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 diff --git a/src/Data/Connection.hs b/src/Data/Connection.hs --- a/src/Data/Connection.hs +++ b/src/Data/Connection.hs @@ -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? diff --git a/src/Data/Connection/Cast.hs b/src/Data/Connection/Cast.hs new file mode 100644 --- /dev/null +++ b/src/Data/Connection/Cast.hs @@ -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 +-- +-- > (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 +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 +-- +-- > (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 +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 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 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 . +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 +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 +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 diff --git a/src/Data/Connection/Class.hs b/src/Data/Connection/Class.hs --- a/src/Data/Connection/Class.hs +++ b/src/Data/Connection/Class.hs @@ -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 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 diff --git a/src/Data/Connection/Conn.hs b/src/Data/Connection/Conn.hs deleted file mode 100644 --- a/src/Data/Connection/Conn.hs +++ /dev/null @@ -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 --- --- > (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 -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 --- --- > (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 -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 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 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 . -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 -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 -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 diff --git a/src/Data/Connection/Fixed.hs b/src/Data/Connection/Fixed.hs --- a/src/Data/Connection/Fixed.hs +++ b/src/Data/Connection/Fixed.hs @@ -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 diff --git a/src/Data/Connection/Float.hs b/src/Data/Connection/Float.hs --- a/src/Data/Connection/Float.hs +++ b/src/Data/Connection/Float.hs @@ -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) diff --git a/src/Data/Connection/Int.hs b/src/Data/Connection/Int.hs --- a/src/Data/Connection/Int.hs +++ b/src/Data/Connection/Int.hs @@ -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 + diff --git a/src/Data/Connection/Property.hs b/src/Data/Connection/Property.hs --- a/src/Data/Connection/Property.hs +++ b/src/Data/Connection/Property.hs @@ -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 -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 diff --git a/src/Data/Connection/Ratio.hs b/src/Data/Connection/Ratio.hs --- a/src/Data/Connection/Ratio.hs +++ b/src/Data/Connection/Ratio.hs @@ -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 diff --git a/src/Data/Connection/Time.hs b/src/Data/Connection/Time.hs --- a/src/Data/Connection/Time.hs +++ b/src/Data/Connection/Time.hs @@ -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 diff --git a/src/Data/Connection/Word.hs b/src/Data/Connection/Word.hs --- a/src/Data/Connection/Word.hs +++ b/src/Data/Connection/Word.hs @@ -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) diff --git a/src/Data/Lattice.hs b/src/Data/Lattice.hs --- a/src/Data/Lattice.hs +++ b/src/Data/Lattice.hs @@ -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 (\/) diff --git a/src/Data/Lattice/Property.hs b/src/Data/Lattice/Property.hs --- a/src/Data/Lattice/Property.hs +++ b/src/Data/Lattice/Property.hs @@ -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 diff --git a/src/Data/Order/Interval.hs b/src/Data/Order/Interval.hs --- a/src/Data/Order/Interval.hs +++ b/src/Data/Order/Interval.hs @@ -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 diff --git a/test/Test/Data/Connection/Fixed.hs b/test/Test/Data/Connection/Fixed.hs --- a/test/Test/Data/Connection/Fixed.hs +++ b/test/Test/Data/Connection/Fixed.hs @@ -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 diff --git a/test/Test/Data/Connection/Float.hs b/test/Test/Data/Connection/Float.hs --- a/test/Test/Data/Connection/Float.hs +++ b/test/Test/Data/Connection/Float.hs @@ -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) diff --git a/test/Test/Data/Connection/Int.hs b/test/Test/Data/Connection/Int.hs --- a/test/Test/Data/Connection/Int.hs +++ b/test/Test/Data/Connection/Int.hs @@ -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 diff --git a/test/Test/Data/Connection/Ratio.hs b/test/Test/Data/Connection/Ratio.hs --- a/test/Test/Data/Connection/Ratio.hs +++ b/test/Test/Data/Connection/Ratio.hs @@ -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) diff --git a/test/doctest.hs b/test/doctest.hs --- a/test/doctest.hs +++ b/test/doctest.hs @@ -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" ]