diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,389 @@ +# connections + +[![Build Status](https://travis-ci.com/cmk/connections.svg?branch=master)](https://travis-ci.com/cmk/connections) + +`connections` is a library for working with Galois connections on various common preorders. + +Hosted on [Hackage](https://hackage.haskell.org/package/connections). + +* [What is a connection?](#intro) +* [What can you do with them?](#what) +* [What's wrong with the numeric conversions in `base`?](#base) + + + +### What is a connection? + +A [Galois connection](https://en.wikipedia.org/wiki/Galois_connection) between preorders P and Q is a pair of monotone maps `f :: p -> q` and `g :: q -> p` such that `f x <= y` if and only if `x <= g y`. We say that `f` is the left or lower adjoint, and `g` is the right or upper adjoint of the connection. + +For illustration, here is a simple example from [7 Sketches](https://math.mit.edu/~dspivak/teaching/sp18/7Sketches.pdf): + +![](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). + +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` + +Lastly, it provides [lattices and algebras](https://hackage.haskell.org/package/connections/docs/Data-Lattice.html). + +### How do connections work? + +Let's look at a simple connection between `Ordering` and `Bool`: + +``` +ordbin :: Conn 'L Ordering Bool +ordbin = ConnL f g where + f LT = False + f _ = True + + g False = LT + g True = GT +``` + +The two component functions are each monotonic (i.e. `x1 <= x2` implies `f x1 <= f x2`), and are 'interlocked' or adjoint in the specific way outlined above: `f x <= y` if and only if `x <= g y`. + +We can easily verify the adjointness property by hand in this case: + +`f`/`g`| `False` | `True` | +------ | ------- | ------- | + `LT` | `=`/`=` | `<`/`<` | + `EQ` | `>`/`>` | `=`/`<` | + `GT` | `>`/`>` | `=`/`=` | + +Each cell represents a pairing of (`x`,`y`) with the two relations `f x _ y` and `x _ g y`. A cell with either `=`/`>`, `>`/`=`, or arrows facing in opposite directions would indictate a failure. See the `test` folder for further examples. + +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 + g False = LT + g True = GT + + h GT = True + h _ = False +``` + +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`). + +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 + where + f LT = False + f _ = True + + g False = LT + g True = GT + + h GT = True + h _ = False +``` + +Once again we can check the adjointness property for each of the two connections (`f`/`g` or `g`/`h`): + + `f`/`g`/`h` | `False` | `True` | +------------ | ----------- | ----------- | + `LT` | `=`/`=`/`=` | `<`/`<`/`<` | + `EQ` | `>`/`>`/`=` | `=`/`<`/`<` | + `GT` | `>`/`>`/`>` | `=`/`=`/`=` | + + +See [`Data.Connection.Property`](https://hackage.haskell.org/package/connections/docs/Data-Connection-Property.html) for a list of properties that all connections should satisfy. + + +### What can you do with them? + +Lots of things! + +At a basic level connections can tell you interesting things about the underlying types themselves: + +``` +λ> import Data.Connection +λ> 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) +``` + +You can use them to safely convert between types obviously: + +``` +λ> :t ceiling f64w32 +ceiling f64w32 :: Double -> Extended Word32 +λ> ceiling f64w32 pi +Finite 4 +λ> ceiling f64w32 (0/0) +PosInf +λ> floor f64w32 (0/0) +NegInf +``` + +... as well as to round, truncate, take medians, etc. + +``` +λ> round f64w32 pi +Finite 3 +λ> round f64w32 (-pi) +Finite 0 +λ> round f64i32 (-pi) +Finite (-3) +λ> median f32f32 1 9 7 +7.0 +λ> median f32f32 1 9 (-1/0) +1.0 +λ> median f32f32 1 9 (0/0) +9.0 +λ> median f32f32 1 9 (1/0) +9.0 +``` + +You can also lift functions over connections: + +``` +λ> :t round1 f64f32 +round1 f64f32 :: (Double -> Double) -> Float -> Float +λ> f x = let m = 16777215 in (m + x) - m +λ> f 2.0 :: Float +1.0 +λ> round1 f64f32 f 2.0 -- Avoid loss of precision +2.0 +``` + +... and use various combinators to combine them: + +``` +λ> :t divide rati16 f32i16 +divide rati16 f32i16 :: Conn k (Rational, Float) (Extended Int16) +λ> maximize (divide rati16 f32i16) 2.99 3.01 +Finite 4 +λ> maximize (divide rati16 f32i16) 2.99 (0/0) +PosInf +λ> minimize (divide rati16 f32i16) 2.99 (0/0) +NegInf +``` + +In particular connections form a category, which means they compose: + +``` +λ> :t MkSystemTime +MkSystemTime :: Int64 -> Word32 -> SystemTime +λ> :t connL ratf64 >>> ratsys +connL ratf64 >>> ratsys :: Conn 'L Double (Extended SystemTime) +λ> ceiling (connL ratf64 >>> ratsys) pi +Finite (MkSystemTime {systemSeconds = 3, systemNanoseconds = 141592654}) +λ> diffSystemTime x y = inner (connL ratf64 >>> ratsys) $ round2 ratsys (-) (Finite x) (Finite y) +λ> :t diffSystemTime +diffSystemTime :: SystemTime -> SystemTime -> Double +λ> diffSystemTime (MkSystemTime 0 0) (MkSystemTime 0 maxBound) +-4.294967295 +λ> divMod (maxBound @Word32) (10^9) +(4,294967295) +``` + + + +### What's wrong with the numeric conversions in `base`? + +From an industrial user's perspective, `base` is unfortunately in pretty bad shape. Every class in the image below not colored yellow or orange has problems in my opinion. Every 'numerical' class (blue or pink) has serious problems either in the interface, the instances, or both. + +![](img/haskell-typeclasses.png) + +With respect to numerical conversions there are two classes of problem: + +* the non-integral instances of `Ord` (e.g. `Float`, `Double`, `Rational`, `Scientific`, etc.) +* the interfaces of `Integral`, `Num`, `Real`, `Fractional`, and `RealFrac` + + +#### Orders: total and partial + +The root problem here is quite old: `NaN` values (e.g. `0/0`, `0 * 1/0`, `1/0 - 1/0`, etc) are not comparable to any finite number, so fractional and floating point types cannot be totally ordered. + +However the `Ord` instances of `Float`, `Double`, and `Rational` ignore this, leading to nonsensical behavior: + +``` +λ> import GHC.Real (Ratio(..)) +λ> 0 :% 0 < -1 +False +λ> 0 :% 0 == -1 +False +λ> 0 :% 0 <= -1 +True +λ> compare @Float (0/0) (1/0) +GT +λ> compare @Float (1/0) (0/0) +GT +λ> max @Float 0 (-0.0) +-0.0 +λ> max @Float (-0.0) 0 +0.0 +``` + +The behavior isn't consistent accross types either: + +``` +λ> 0 :% 0 <= 0 :% 0 +True +λ> (0/0 :: Float) <= 0/0 +False +``` + +This is dangerous and can lead to bugs [well outside of numerical applications](https://github.com/ocaml/ocaml/issues/5222). Fortunately the solution is fairly simple: create a [`Preorder`](https://hackage.haskell.org/package/connections/docs/Data-Order.html#t:Preorder) class with lawful instances for types with `NaN` values. Rust does something [similar](https://doc.rust-lang.org/std/cmp/trait.PartialOrd.html). + + + +#### Coercive conversions + +The second set of problems is with the various conversion methods defined in `Integral`, `Num`, `Real` and `Fractional`: + +``` +fromInteger :: Num a => Integer -> a +toInteger :: Integral a => a -> Integer +fromRational :: Fractional a => Rational -> a +toRational :: Real a => a -> Rational +``` + +The problem with the conversion methods is that they are all lawless: the classes do not define any equational laws that the user can expect instances to obey. Predictably, the result is chaos: + +``` +λ> toInteger @Int8 128 +-128 +λ> fromInteger @Int8 128 +-128 +λ> toRational @Float (0/0) +(-510423550381407695195061911147652317184) % 1 +λ> fromRational @Float (0/0) +*** Exception: Ratio has zero denominator +``` + +One could object that the examples above are exceptional. Unfortunately, surprises can occur in completely mundane situations as well: + +``` +λ> fromRational @Float 5000000.2 -- your fintech app is under-charging 20¢ on every $5M transaction +5000000.0 +λ> fromRational @Float 5000000.3 -- or is it over-charging 20¢? +5000000.5 +``` + +Worse, these conversion methods in turn give rise to the aptly-named [coercions](hackage.haskell.org/package/base/docs/src/GHC-Real.html#fromIntegral): + +``` +realToFrac :: (Real a, Fractional b) => a -> b +realToFrac = fromRational . toRational + +fromIntegral :: (Integral a, Num b) => a -> b +fromIntegral = fromInteger . toInteger +``` + +If you're not careful, these 'just make it type-check' functions will get slotted in everywhere in your application. Sometimes that's ok, but if your application has to deal with small, large, infinite, or otherwise exceptional values then the resultant behavior will make your (or somebody's) life miserable: + +``` +λ> realToFrac @Float @Double (1/0) +3.402823669209385e38 +λ> realToFrac @Double @Float (1/0) +Infinity +λ> realToFrac @Rational @Double (1 :% 0) +Infinity +λ> realToFrac @Double @Rational (1/0) +179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216 % 1 +λ> fromIntegral @Int8 @Word8 128 +128 +λ> fromIntegral @Int8 @Word 128 +18446744073709551488 +λ> fromIntegral @Int8 @Natural 128 -- your colleagues will appreciate this _underflow_ exception +*** Exception: arithmetic underflow +``` + +What happened in that last example to create an underflow exception? If anything you would expect overflow. + +This is what happened: + +``` +λ> toInteger @Int8 128 +-128 +λ> fromInteger @Natural (-128) +*** Exception: arithmetic underflow +``` + +It's a good example of why composition is only your friend if it comes with composable guarantees. + + +Finally, let's look at [`RealFrac`](www.hackage.haskell.org/package/base/docs/GHC-Real.html#t:RealFrac): + +``` +-- | Extracting components of fractions. +class (Real a, Fractional a) => RealFrac a where + + -- | The function 'properFraction' takes a real fractional number @x@ + -- and returns a pair @(n,f)@ such that @x = n+f@, and: + -- + -- * @n@ is an integral number with the same sign as @x@; and + -- + -- * @f@ is a fraction with the same type and sign as @x@, + -- and with absolute value less than @1@. + -- + -- The default definitions of the 'ceiling', 'floor', 'truncate' + -- and 'round' functions are in terms of 'properFraction'. + properFraction :: (Integral b) => a -> (b,a) + + -- | @'truncate' x@ returns the integer nearest @x@ between zero and @x@ + truncate :: (Integral b) => a -> b + + -- | @'round' x@ returns the nearest integer to @x@; + -- the even integer if @x@ is equidistant between two integers + round :: (Integral b) => a -> b + + -- | @'ceiling' x@ returns the least integer not less than @x@ + ceiling :: (Integral b) => a -> b + + -- | @'floor' x@ returns the greatest integer not greater than @x@ + floor :: (Integral b) => a -> b + + {-# MINIMAL properFraction #-} +``` + +By now you might be suspicious of these claims. If so, your suspicion would be rewarded: + + +``` +λ> properFraction @Float @Int 3000000.1 +(3000000,0.0) +λ> ceiling @Float @Int 3000000.1 +3000000 +``` + +The situation again is especially bad for floating point types, which are forced to go through `Integer` and/or `Rational`: + +``` +λ> properFraction @Float @Int (1/0) +(0,0.0) +λ> ceiling @Float @Int (1/0) +0 +λ> properFraction @Float @Integer (1/0) +(340282366920938463463374607431768211456,0.0) +λ> ceiling @Float @Integer (1/0) +340282366920938463463374607431768211456 +λ> realToFrac @Float @Rational (1/0) +340282366920938463463374607431768211456 % 1 +``` + +Even conversions between `Float` and `Double`, which should be straightforward, are impacted: + +``` +λ> realToFrac @Float @Double (1/0) +3.402823669209385e38 +λ> import GHC.Float (float2Double) +λ> float2Double (1/0) +Infinity +``` + +The meta-problem behind all of these problems is the mis-specification of the numeric type classes in `base`. Functions that can only be meaningfully given laws in pairs (like `toRational` and `fromRational`) are instead broken up between different classes, laws are either non-existant or (worse) misleading, and users are left to fend for themselves. + diff --git a/connections.cabal b/connections.cabal --- a/connections.cabal +++ b/connections.cabal @@ -1,7 +1,9 @@ name: connections -version: 0.3.0 +version: 0.3.1 synopsis: Orders, Galois connections, and lattices. -description: A library for order manipulation using Galois connections. See the README for a brief overview. +description: A library for working with Galois connections on various common preorders. + . + See the README for an overview. homepage: https://github.com/cmk/connections license: BSD3 license-file: LICENSE @@ -10,8 +12,12 @@ category: Math, Numerical stability: Experimental build-type: Simple -extra-source-files: ChangeLog.md -cabal-version: >=1.10 +extra-source-files: + ChangeLog.md + README.md +extra-doc-files: + img/*.png +cabal-version: 1.18 library hs-source-dirs: src @@ -26,6 +32,7 @@ , Data.Connection.Float , Data.Connection.Int , Data.Connection.Ratio + , Data.Connection.Time , Data.Connection.Word , Data.Connection.Property @@ -33,14 +40,15 @@ , Data.Lattice.Property , Data.Order - , Data.Order.Extended , Data.Order.Interval , Data.Order.Property , Data.Order.Syntax - + build-depends: - base >= 4.10 && < 5.0 - , containers >= 0.4.0 && < 1.0 + base >= 4.10 && < 5.0 + , containers >= 0.4.0 && < 1.0 + , extended-reals >= 0.2.0.0 && < 0.3 + , time >= 1.8.0 && < 2.0 test-suite test type: exitcode-stdio-1.0 @@ -53,10 +61,12 @@ , Test.Data.Connection.Fixed , Test.Data.Connection.Float , Test.Data.Connection.Ratio + , Test.Data.Connection.Time build-depends: base == 4.* , connections -any , hedgehog + , time >= 1.8.0 && < 2.0 default-extensions: ScopedTypeVariables, TypeApplications, @@ -75,7 +85,7 @@ build-depends: base - , doctest >= 0.8 + , doctest >= 0.8 , connections -any default-extensions: diff --git a/img/example.png b/img/example.png new file mode 100644 Binary files /dev/null and b/img/example.png differ diff --git a/img/haskell-typeclasses.png b/img/haskell-typeclasses.png new file mode 100644 Binary files /dev/null and b/img/haskell-typeclasses.png differ diff --git a/src/Data/Connection.hs b/src/Data/Connection.hs --- a/src/Data/Connection.hs +++ b/src/Data/Connection.hs @@ -1,9 +1,312 @@ +{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE Safe #-} +{-# OPTIONS_HADDOCK show-extensions #-} +-- | +-- +-- 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 +-- based on the same construction. +-- +-- /connections/ is extensively tested, and it exports properties for use in testing +-- your own connections. See "Data.Connection.Property" and "Data.Lattice.Property". +-- In addition to the property tests there are several doctests scattered around, +-- these are runnable as a standalone executable. See the /doctest/ stanza in the +-- library's cabal file. module Data.Connection ( - module Data.Connection.Conn, - module Data.Connection.Class, + + -- $example + + -- * Types + Conn, + Side(..), + + -- ** Conn L + ConnL, + connL, + pattern ConnL, + + -- ** Conn R + ConnR, + connR, + pattern ConnR, + + -- ** Conn k + pattern Conn, + + -- * Combinators + (>>>), + (<<<), + mapped, + choice, + select, + strong, + divide, + + -- * Accessors + upper, + lower, + inner, + outer, + + -- ** max/min + maximize, + minimize, + median, + + -- ** ceiling + ceiling, + ceiling1, + ceiling2, + + -- ** floor + floor, + floor1, + floor2, + + -- ** round + round, + round1, + round2, + + -- ** truncate + truncate, + 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, + + -- *** Double + f64f64, + ratf64, + + -- ** 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.Class 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 Prelude hiding (ceiling, floor, round, truncate) + + + +{- $example + + ==== What is a Galois connection? + + A [Galois connection](https://en.wikipedia.org/wiki/Galois_connection) is an + adjunction in the category of preorders: a pair of monotone maps /f :: p -> q/ + and /g :: q -> p/ between preorders /p/ and /q/, such that + + /f x <= y/ if and only if /x <= g y/ + + We say that /f/ is the left or lower adjoint, and /g/ is the right or upper + adjoint of the connection. + + For illustration, here is a simple example from + [7 Sketches](https://math.mit.edu/~dspivak/teaching/sp18/7Sketches.pdf): + + <> + + Note that the two component functions are each monotonic: + + @ x1 'Data.Order.Syntax.<=' x2 implies f x1 'Data.Order.Syntax.<=' f x2 @ + + and furthermore they are are interlocked (i.e. adjoint) in the specific way + outlined above: + + @ f x 'Data.Order.Syntax.<=' y if and only if x 'Data.Order.Syntax.<=' g y @ + + See the [README](https://github.com/cmk/connections/blob/master/README.md) for + a more extensive overview. +-} 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 @@ -12,71 +12,47 @@ {-# LANGUAGE ViewPatterns #-} module Data.Connection.Class ( - -- * Types Left, left, Right, right, Triple, - - -- * Lattices - (\/), - (/\), - lub, - glb, - choose, - divide, - minimal, - maximal, - extremal, - - -- * Connection - Connection (..), - - -- ** RebindableSyntax ConnInteger, + fromInteger, ConnRational, + fromRational, + Connection (..), ) where import safe Control.Category ((>>>)) -import safe Data.Bool (bool) 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.Functor.Identity import safe Data.Int -import safe qualified Data.IntMap as IntMap -import safe qualified Data.IntSet as IntSet -import safe qualified Data.Map as Map import safe Data.Order -import safe Data.Order.Extended -import safe qualified Data.Set as Set import safe Data.Word import safe Numeric.Natural -import safe Prelude hiding (ceiling, floor, round, truncate) +import safe Prelude hiding (ceiling, floor, fromInteger, fromRational, round, truncate) --- $setup --- >>> :set -XTypeApplications --- >>> :set -XFlexibleContexts --- >>> import GHC.Real (Ratio(..)) --- >>> import Data.Set (Set,fromList) --- >>> :load Data.Connection --- >>> import Prelude hiding (round, floor, ceiling, truncate) +-- | 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 @@ -84,191 +60,29 @@ 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 = upper conn . Just :: ConnInteger a => Integer -> a -type ConnInteger a = Left a (Maybe Integer) +fromInteger :: ConnInteger a => Integer -> a +fromInteger = upper conn . Just -- | A constraint kind for 'Rational' conversions. --- --- Usable in conjunction with /RebindableSyntax/: --- --- > fromRational = round conn :: ConnRational a => Rational -> a type ConnRational a = Triple Rational a --- | An < https://ncatlab.org/nlab/show/adjoint+string adjoint string > of Galois connections of length 2 or 3. -class (Preorder a, Preorder b) => Connection k a b where - -- | - -- - -- >>> range (conn @_ @Rational @Float) (22 :% 7) - -- (3.142857,3.1428573) - -- >>> range (conn @_ @Double @Float) pi - -- (3.1415925,3.1415927) - conn :: Conn k a b - -{- --- | Return the nearest value to x. --- --- > round @a @a = id --- --- If x lies halfway between two finite values, then return the value --- with the larger absolute value (i.e. round away from zero). --- --- See . -round :: forall a b. (Num a, Triple a b) => a -> b -round x = case pcompare halfR halfL of - Just GT -> ceiling x - Just LT -> floor x - _ -> truncate x - where - halfR = x - right (connR @a @b) x -- dist from lower bound - halfL = left (connL @a @b) x - x -- dist from upper bound - --- | Lift a unary function over a 'Conn'. --- --- Results are rounded to the nearest value with ties away from 0. -round1 :: (Num a, Triple a b) => (a -> a) -> b -> b -round1 f x = round $ f (g x) where Conn _ g _ = connL -{-# INLINE round1 #-} - --- | Lift a binary function over a 'Conn'. --- --- Results are rounded to the nearest value with ties away from 0. --- --- Example avoiding loss-of-precision: --- --- >>> f x y = (x + y) - x --- >>> maxOdd32 = 1.6777215e7 --- >>> f maxOdd32 2.0 :: Float --- 1.0 --- >>> round2 @Rational @Float f maxOdd32 2.0 --- 2.0 --- >>> maxOdd64 = 9.007199254740991e15 --- >>> f maxOdd64 2.0 :: Double --- 1.0 --- >>> round2 @Rational @Double f maxOdd64 2.0 --- 2.0 -round2 :: (Num a, Triple a b) => (a -> a -> a) -> b -> b -> b -round2 f x y = round $ f (g x) (g y) where Conn _ g _ = connL -{-# INLINE round2 #-} - --- | Truncate towards zero. --- --- > truncate @a @a = id -truncate :: (Num a, Triple a b) => a -> b -truncate x = if x >~ 0 then floor x else ceiling x - --- | Lift a unary function over a 'Conn'. --- --- Results are truncated towards 0. -truncate1 :: (Num a, Triple a b) => (a -> a) -> b -> b -truncate1 f x = truncate $ f (g x) where Conn _ g _ = connL -{-# INLINE truncate1 #-} - --- | Lift a binary function over a 'Conn'. --- --- Results are truncated towards 0. -truncate2 :: (Num a, Triple a b) => (a -> a -> a) -> b -> b -> b -truncate2 f x y = truncate $ f (g x) (g y) where Conn _ g _ = connL -{-# INLINE truncate2 #-} --} - ---------------------------------------------------------------------- --- Lattices ---------------------------------------------------------------------- - -infixr 5 \/ - --- | Lattice join. --- --- > (\/) = curry $ lower semilattice -(\/) :: Left (a, a) a => a -> a -> a -(\/) = join conn - -infixr 6 /\ -- comment for the parser - --- | Lattice meet. --- --- > (/\) = curry $ floor semilattice -(/\) :: Right (a, a) a => a -> a -> a -(/\) = meet conn - --- | Least upper bound operator. --- --- The order dual of 'glb'. --- --- >>> lub 1.0 9.0 7.0 --- 7.0 --- >>> lub 1.0 9.0 (0.0 / 0.0) --- 1.0 -lub :: Triple (a, a) a => a -> a -> a -> a -lub x y z = x /\ y \/ y /\ z \/ z /\ x - --- | Greatest lower bound operator. --- --- > glb x x y = x --- > glb x y z = glb z x y --- > glb x y z = glb x z y --- > glb (glb x w y) w z = glb x w (glb y w z) --- --- >>> glb 1.0 9.0 7.0 --- 7.0 --- >>> glb 1.0 9.0 (0.0 / 0.0) --- 9.0 --- >>> glb (fromList [1..3]) (fromList [3..5]) (fromList [5..7]) :: Set Int --- fromList [3,5] -glb :: Triple (a, a) a => a -> a -> a -> a -glb x y z = (x \/ y) /\ (y \/ z) /\ (z \/ x) - -infixr 3 `choose` - --- | A preorder variant of 'Control.Arrow.|||'. -choose :: Conn k c a -> Conn k c b -> Conn k c (Either a b) -choose f g = Conn Left (either id id) Right >>> f `choice` g - -infixr 4 `divide` - --- | A preorder variant of 'Control.Arrow.&&&'. -divide :: Connection k (c, c) c => Conn k a c -> Conn k b c -> Conn k (a, b) c -divide f g = f `strong` g >>> conn - --- | A minimal element of a preorder. --- --- > x /\ minimal = minimal --- > x \/ minimal = x --- --- 'minimal' needn't be unique, but it must obey: --- --- > x <~ minimal => x ~~ minimal -minimal :: Left () a => a -minimal = ceiling conn () - --- | A maximal element of a preorder. --- --- > x /\ maximal = x --- > x \/ maximal = maximal --- --- 'maximal' needn't be unique, but it must obey: +-- | A replacement for the version in /base/. -- --- > x >~ maximal => x ~~ maximal -maximal :: Right () a => a -maximal = floor conn () - --- | The canonical connection with a 'Bool'. -extremal :: Triple () a => Conn k a Bool -extremal = Conn f g h +-- 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 - g False = minimal - g True = maximal - - f i - | i ~~ minimal = False - | otherwise = True - - h i - | i ~~ maximal = True - | otherwise = False + 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 #-} --------------------------------------------------------------------- -- Instances @@ -276,48 +90,33 @@ instance Preorder a => Connection k a a where conn = identity -instance Connection k ((), ()) () where conn = latticeOrd - -instance Connection k () Bool where conn = bounded -instance Connection k Ordering Bool where conn = extremal -instance Connection k Word8 Bool where conn = extremal -instance Connection k Word16 Bool where conn = extremal -instance Connection k Word32 Bool where conn = extremal -instance Connection k Word64 Bool where conn = extremal -instance Connection k Word Bool where conn = extremal -instance Connection k Positive Bool where conn = extremal -instance Connection k Int8 Bool where conn = extremal -instance Connection k Int16 Bool where conn = extremal -instance Connection k Int32 Bool where conn = extremal -instance Connection k Int64 Bool where conn = extremal -instance Connection k Int Bool where conn = extremal -instance Connection k Rational Bool where conn = extremal -instance Connection k Float Bool where conn = extremal -instance Connection k Double Bool where conn = extremal -instance Connection k (Bool, Bool) Bool where conn = latticeOrd - -instance Connection k () Ordering where conn = bounded -instance Connection k (Ordering, Ordering) Ordering where conn = latticeOrd +instance Connection k 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 k () Word8 where conn = bounded instance Connection 'L Int8 Word8 where conn = i08w08 -instance Connection k (Word8, Word8) Word8 where conn = latticeOrd -instance Connection k () Word16 where conn = bounded instance Connection 'L Word8 Word16 where conn = w08w16 instance Connection 'L Int8 Word16 where conn = i08w16 instance Connection 'L Int16 Word16 where conn = i16w16 -instance Connection k (Word16, Word16) Word16 where conn = latticeOrd -instance Connection k () Word32 where conn = bounded instance Connection 'L Word8 Word32 where conn = w08w32 instance Connection 'L Word16 Word32 where conn = w16w32 instance Connection 'L Int8 Word32 where conn = i08w32 instance Connection 'L Int16 Word32 where conn = i16w32 instance Connection 'L Int32 Word32 where conn = i32w32 -instance Connection k (Word32, Word32) Word32 where conn = latticeOrd -instance Connection k () Word64 where conn = bounded instance Connection 'L Word8 Word64 where conn = w08w64 instance Connection 'L Word16 Word64 where conn = w16w64 instance Connection 'L Word32 Word64 where conn = w32w64 @@ -326,9 +125,7 @@ instance Connection 'L Int32 Word64 where conn = i32w64 instance Connection 'L Int64 Word64 where conn = i64w64 instance Connection 'L Int Word64 where conn = ixxw64 -instance Connection k (Word64, Word64) Word64 where conn = latticeOrd -instance Connection k () Word where conn = bounded instance Connection 'L Word8 Word where conn = w08wxx instance Connection 'L Word16 Word where conn = w16wxx instance Connection 'L Word32 Word where conn = w32wxx @@ -338,9 +135,7 @@ instance Connection 'L Int32 Word where conn = i32wxx instance Connection 'L Int64 Word where conn = i64wxx instance Connection 'L Int Word where conn = ixxwxx -instance Connection k (Word, Word) Word where conn = latticeOrd -instance Connection 'L () Natural where conn = ConnL (const 0) (const ()) instance Connection 'L Word8 Natural where conn = w08nat instance Connection 'L Word16 Natural where conn = w16nat instance Connection 'L Word32 Natural where conn = w32nat @@ -352,27 +147,8 @@ instance Connection 'L Int64 Natural where conn = i64nat instance Connection 'L Int Natural where conn = ixxnat instance Connection 'L Integer Natural where conn = intnat -instance Connection k (Natural, Natural) Natural where conn = latticeOrd -instance Connection k () Positive where - conn = Conn (const $ 0 :% 1) (const ()) (const $ 1 :% 0) -instance Connection k (Positive, Positive) Positive where conn = latticeN5 - -instance Connection k () Int8 where conn = bounded -instance Connection k (Int8, Int8) Int8 where conn = latticeOrd -instance Connection k () Int16 where conn = bounded -instance Connection k (Int16, Int16) Int16 where conn = latticeOrd -instance Connection k () Int32 where conn = bounded -instance Connection k (Int32, Int32) Int32 where conn = latticeOrd -instance Connection k () Int64 where conn = bounded -instance Connection k (Int64, Int64) Int64 where conn = latticeOrd -instance Connection k () Int where conn = bounded -instance Connection k (Int, Int) Int where conn = latticeOrd -instance Connection k (Integer, Integer) Integer where conn = latticeOrd - -instance Connection k () Rational where - conn = Conn (const $ -1 :% 0) (const ()) (const $ 1 :% 0) -instance Connection k (Rational, Rational) Rational where conn = latticeN5 +instance Connection k Uni Integer where conn = f00int instance Connection k Deci Uni where conn = f01f00 instance Connection k Centi Uni where conn = f02f00 @@ -401,16 +177,10 @@ instance Connection k Pico Nano where conn = f12f09 -instance Connection k (Fixed e, Fixed e) (Fixed e) where conn = latticeOrd - -instance Connection k () Float where conn = extremalN5 instance Connection k Double Float where conn = f64f32 instance Connection k Rational Float where conn = ratf32 -instance Connection k (Float, Float) Float where conn = latticeN5 -instance Connection k () Double where conn = extremalN5 instance Connection k Rational Double where conn = ratf64 -instance Connection k (Double, Double) Double where conn = latticeN5 instance Connection 'L Word8 (Maybe Int16) where conn = w08i16 instance Connection 'L Int8 (Maybe Int16) where conn = i08i16 @@ -434,6 +204,7 @@ 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 'L Word8 (Maybe Integer) where conn = w08int instance Connection 'L Word16 (Maybe Integer) where conn = w16int @@ -447,7 +218,12 @@ instance Connection 'L Int32 (Maybe Integer) where conn = i32int instance Connection 'L Int64 (Maybe Integer) where conn = i64int instance Connection 'L Int (Maybe Integer) where conn = ixxint + instance Connection 'L Integer (Maybe Integer) where + -- | + -- + -- 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 @@ -457,53 +233,35 @@ shiftL x = x - m m = 9223372036854775808 +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 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 HasResolution prec => Connection k Rational (Extended (Fixed prec)) where conn = ratfix - -instance Connection 'L Float (Extended Word8) where conn = f32i08 >>> mapped i08w08 -instance Connection 'L Float (Extended Word16) where conn = f32i16 >>> mapped i16w16 -instance Connection 'L Float (Extended Word32) where conn = f32i32 >>> mapped i32w32 -instance Connection 'L Float (Extended Word64) where conn = f32i64 >>> mapped i64w64 -instance Connection 'L Float (Extended Word) where conn = f32ixx >>> mapped ixxwxx -instance Connection 'L Float (Extended Natural) where conn = f32int >>> mapped intnat +instance Connection k Rational (Extended SystemTime) where conn = ratsys +instance HasResolution res => Connection k Rational (Extended (Fixed res)) where conn = ratfix --- | All 'Data.Int.Int8' values are exactly representable in a 'Float'. +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 - --- | All 'Data.Int.Int16' values are exactly representable in a 'Float'. instance Connection k Float (Extended Int16) where conn = f32i16 - -instance Connection 'L Float (Extended Int32) where conn = f32i32 -instance Connection 'L Float (Extended Int64) where conn = f32i64 -instance Connection 'L Float (Extended Int) where conn = f32ixx -instance Connection 'L Float (Extended Integer) where conn = f32int -instance HasResolution res => Connection 'L Float (Extended (Fixed res)) where conn = connL ratf32 >>> ratfix - -instance Connection 'L Double (Extended Word8) where conn = f64i08 >>> mapped i08w08 -instance Connection 'L Double (Extended Word16) where conn = f64i16 >>> mapped i16w16 -instance Connection 'L Double (Extended Word32) where conn = f64i32 >>> mapped i32w32 -instance Connection 'L Double (Extended Word64) where conn = f64i64 >>> mapped i64w64 -instance Connection 'L Double (Extended Word) where conn = f64ixx >>> mapped ixxwxx -instance Connection 'L Double (Extended Natural) where conn = f64int >>> mapped intnat +instance HasResolution res => Connection 'L Float (Extended (Fixed res)) where conn = f32fix --- | All 'Data.Int.Int8' values are exactly representable in a 'Double'. +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 - --- | All 'Data.Int.Int16' values are exactly representable in a 'Double'. instance Connection k Double (Extended Int16) where conn = f64i16 - --- | All 'Data.Int.Int32' values are exactly representable in a 'Double'. instance Connection k Double (Extended Int32) where conn = f64i32 - -instance Connection 'L Double (Extended Int64) where conn = f64i64 -instance Connection 'L Double (Extended Int) where conn = f64ixx -instance Connection 'L Double (Extended Integer) where conn = f64int -instance HasResolution res => Connection 'L Double (Extended (Fixed res)) where conn = connL ratf64 >>> ratfix +instance HasResolution res => Connection 'L Double (Extended (Fixed res)) where conn = f64fix instance Connection k a b => Connection k (Identity a) b where conn = Conn runIdentity Identity runIdentity >>> conn @@ -511,161 +269,23 @@ instance Connection k a b => Connection k a (Identity b) where conn = conn >>> Conn Identity runIdentity Identity -instance (Triple () a, Triple () b) => Connection k () (a, b) where - conn = Conn (const (minimal, minimal)) (const ()) (const (maximal, maximal)) - -instance Preorder a => Connection 'L () (Maybe a) where - conn = ConnL (const Nothing) (const ()) - -instance Right () a => Connection 'R () (Maybe a) where - conn = ConnR (const ()) (const $ Just maximal) - -instance Preorder a => Connection k () (Extended a) where - conn = Conn (const Bottom) (const ()) (const Top) - -instance (Left () a, Preorder b) => Connection 'L () (Either a b) where - conn = ConnL (const $ Left minimal) (const ()) - -instance (Preorder a, Right () b) => Connection 'R () (Either a b) where - conn = ConnR (const ()) (const $ Right maximal) - -instance (Preorder a, Triple () b) => Connection k (Maybe a) (Either a b) where - conn = maybeL - -instance (Triple () a, Preorder b) => Connection k (Maybe b) (Either a b) where - conn = maybeR - -instance (Total a) => Connection 'L () (Set.Set a) where - conn = ConnL (const Set.empty) (const ()) - -instance Total a => Connection k (Set.Set a, Set.Set a) (Set.Set a) where - conn = Conn (uncurry Set.union) fork (uncurry Set.intersection) - -instance Connection 'L () IntSet.IntSet where - conn = ConnL (const IntSet.empty) (const ()) - -instance Connection k (IntSet.IntSet, IntSet.IntSet) IntSet.IntSet where - conn = Conn (uncurry IntSet.union) fork (uncurry IntSet.intersection) - -instance (Total a, Preorder b) => Connection 'L () (Map.Map a b) where - conn = ConnL (const Map.empty) (const ()) - -instance (Total a, Left (b, b) b) => Connection 'L (Map.Map a b, Map.Map a b) (Map.Map a b) where - conn = ConnL (uncurry $ Map.unionWith (join conn)) fork - -instance (Total a, Right (b, b) b) => Connection 'R (Map.Map a b, Map.Map a b) (Map.Map a b) where - conn = ConnR fork (uncurry $ Map.intersectionWith (meet conn)) - -instance Preorder a => Connection 'L () (IntMap.IntMap a) where - conn = ConnL (const IntMap.empty) (const ()) - -instance Left (a, a) a => Connection 'L (IntMap.IntMap a, IntMap.IntMap a) (IntMap.IntMap a) where - conn = ConnL (uncurry $ IntMap.unionWith (join conn)) fork - -instance Right (a, a) a => Connection 'R (IntMap.IntMap a, IntMap.IntMap a) (IntMap.IntMap a) where - conn = ConnR fork (uncurry $ IntMap.intersectionWith (meet conn)) - -- Internal ------------------------- -fork :: a -> (a, a) -fork x = (x, x) - -bounded :: Bounded a => Conn k () a -bounded = Conn (const minBound) (const ()) (const maxBound) - -latticeN5 :: (Total a, Fractional a) => Conn k (a, a) a -latticeN5 = Conn (uncurry joinN5) fork (uncurry meetN5) - where - joinN5 x y = maybe (1 / 0) (bool y x . (>= EQ)) (pcompare x y) - - meetN5 x y = maybe (-1 / 0) (bool y x . (<= EQ)) (pcompare x y) - -extremalN5 :: (Total a, Fractional a) => Conn k () a -extremalN5 = Conn (const $ -1 / 0) (const ()) (const $ 1 / 0) - -latticeOrd :: (Total a) => Conn k (a, a) a -latticeOrd = Conn (uncurry max) fork (uncurry min) - -maybeL :: Triple () b => Conn k (Maybe a) (Either a b) -maybeL = Conn f g h - where - f = maybe (Right minimal) Left - g = either Just (const Nothing) - h = maybe (Right maximal) Left +bounds' :: (Eq a, Bounded a) => Conn k a Bool +bounds' = bounds minBound maxBound -maybeR :: Triple () a => Conn k (Maybe b) (Either a b) -maybeR = Conn f g h +bounds :: Eq a => a -> a -> Conn k a Bool +bounds x y = Conn f g h where - f = maybe (Left minimal) Right - g = either (const Nothing) Just - h = maybe (Left maximal) Right - -{- -instance (Triple (a, a) a, Triple (b, b) b) => Connection k ((a, b), (a, b)) (a, b) where - conn = Conn (uncurry joinTuple) fork (uncurry meetTuple) - -instance Left (a, a) a => Connection 'L (Maybe a, Maybe a) (Maybe a) where - conn = ConnL (uncurry joinMaybe) fork - -instance Right (a, a) a => Connection 'R (Maybe a, Maybe a) (Maybe a) where - conn = ConnR fork (uncurry meetMaybe) - -instance Left (a, a) a => Connection 'L (Extended a, Extended a) (Extended a) where - conn = ConnL (uncurry joinExtended) fork - -instance Right (a, a) a => Connection 'R (Extended a, Extended a) (Extended a) where - conn = ConnR fork (uncurry meetExtended) - --- | All minimal elements of the upper lattice cover all maximal elements of the lower lattice. -instance (Left (a, a) a, Left (b, b) b) => Connection 'L (Either a b, Either a b) (Either a b) where - conn = ConnL (uncurry joinEither) fork - -instance (Right (a, a) a, Right (b, b) b) => Connection 'R (Either a b, Either a b) (Either a b) where - conn = ConnR fork (uncurry meetEither) - -joinMaybe :: Connection 'L (a, a) a => Maybe a -> Maybe a -> Maybe a -joinMaybe (Just x) (Just y) = Just (x `join` y) -joinMaybe u@(Just _) _ = u -joinMaybe _ u@(Just _) = u -joinMaybe Nothing Nothing = Nothing - -meetMaybe :: Right (a, a) a => Maybe a -> Maybe a -> Maybe a -meetMaybe Nothing Nothing = Nothing -meetMaybe Nothing _ = Nothing -meetMaybe _ Nothing = Nothing -meetMaybe (Just x) (Just y) = Just (x `meet` y) - -joinExtended :: Connection 'L (a, a) a => Extended a -> Extended a -> Extended a -joinExtended Top _ = Top -joinExtended _ Top = Top -joinExtended (Extended x) (Extended y) = Extended (x `join` y) -joinExtended Bottom y = y -joinExtended x Bottom = x - -meetExtended :: Right (a, a) a => Extended a -> Extended a -> Extended a -meetExtended Top y = y -meetExtended x Top = x -meetExtended (Extended x) (Extended y) = Extended (x `meet` y) -meetExtended Bottom _ = Bottom -meetExtended _ Bottom = Bottom - -joinEither :: (Connection 'L (a, a) a, Connection 'L (b, b) b) => Either a b -> Either a b -> Either a b -joinEither (Right x) (Right y) = Right (x `join` y) -joinEither u@(Right _) _ = u -joinEither _ u@(Right _) = u -joinEither (Left x) (Left y) = Left (x `join` y) - -meetEither :: (Right (a, a) a, Right (b, b) b) => Either a b -> Either a b -> Either a b -meetEither (Left x) (Left y) = Left (x `meet` y) -meetEither l@(Left _) _ = l -meetEither _ l@(Left _) = l -meetEither (Right x) (Right y) = Right (x `meet` y) + g False = x + g True = y -joinTuple :: (Connection 'L (a, a) a, Connection 'L (b, b) b) => (a, b) -> (a, b) -> (a, b) -joinTuple (x1, y1) (x2, y2) = (x1 `join` x2, y1 `join` y2) + f i + | i == x = False + | otherwise = True -meetTuple :: (Right (a, a) a, Right (b, b) b) => (a, b) -> (a, b) -> (a, b) -meetTuple (x1, y1) (x2, y2) = (x1 `meet` x2, y1 `meet` y2) --} + h i + | i == y = True + | otherwise = False diff --git a/src/Data/Connection/Conn.hs b/src/Data/Connection/Conn.hs --- a/src/Data/Connection/Conn.hs +++ b/src/Data/Connection/Conn.hs @@ -12,43 +12,47 @@ module Data.Connection.Conn ( -- * Conn - Kan (..), + Side (..), Conn (), - embed, - range, - identity, (>>>), (<<<), mapped, choice, + select, strong, + divide, + bounded, + ordered, + identity, - -- * Connection L + -- * Conn 'L ConnL, pattern ConnL, connL, upper, upper1, upper2, - join, ceiling, ceiling1, ceiling2, + maximize, - -- * Connection R + -- * Conn 'R ConnR, pattern ConnR, connR, lower, lower1, lower2, - meet, floor, floor1, floor2, + minimize, -- * Connection k pattern Conn, + outer, + inner, half, midpoint, round, @@ -57,6 +61,7 @@ truncate, truncate1, truncate2, + median, -- * Down upL, @@ -66,49 +71,69 @@ 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 --- >>> ratf32 = conn @_ @Rational @Float --- >>> f64f32 = conn @_ @Double @Float --- | A data kind distinguishing the directionality of a Galois 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 low / increasing (e.g. 'Data.Connection.Class.minimal', 'Data.Connection.Class.ceiling', 'Data.Connection.Class.join') +-- * /L/-tagged types are increasing (e.g. 'Data.Connection.Conn.ceiling', 'Data.Connection.Conn.maximize') -- --- * /R/-tagged types are high / decreasing (e.g. 'Data.Connection.Class.maximal', 'Data.Connection.Class.floor', 'Data.Connection.Class.meet') -data Kan = L | R - --- | A (chain of) Galois connections. +-- * /R/-tagged types are decreasing (e.g. 'Data.Connection.Conn.floor', 'Data.Connection.Conn.minimize') -- --- A [Galois connection](https://en.wikipedia.org/wiki/Galois_connection) between preorders P and Q --- is a pair of monotone maps `f :: p -> q` and `g :: q -> p` such that: +-- 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/. -- --- > f x <= y iff x <= g y +-- This is useful because it enables rounding, truncation, medians, etc. -- --- We say that `f` is the left or right adjoint, and `g` is the right or left adjoint of the connection. +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: -- --- >>> range (conn @_ @Rational @Float) (1 :% 8) -- eighths are exactly representable in a float +-- >>> inner ratf32 (1 / 8) -- eighths are exactly representable in a float +-- 1 % 8 +-- >>> outer ratf32 (1 % 8) -- (0.125,0.125) --- >>> range (conn @_ @Rational @Float) (1 :% 7) -- sevenths are not +-- >>> 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 :: Kan) a b = Conn_ (a -> (b, b)) (b -> a) +data Conn (k :: Side) a b = Conn_ (a -> (b, b)) (b -> a) instance Category (Conn k) where id = identity @@ -127,37 +152,15 @@ _2 (Conn_ f _) = snd . f {-# INLINE _2 #-} --- | Retrieve the upper adjoint of a 'ConnL', or lower adjoint of a 'ConnR'. -embed :: Conn k a b -> b -> a -embed (Conn_ _ g) = g -{-# INLINE embed #-} - --- | Retrieve the left and/or right adjoints of a connection. --- --- > range c = floor c &&& ceiling c --- --- >>> range f64f32 pi --- (3.1415925,3.1415927) --- >>> range f64f32 (0/0) --- (NaN,NaN) -range :: Conn k a b -> a -> (b, b) -range (Conn_ f _) = f -{-# INLINE range #-} - --- | The identity 'Conn'. -identity :: Conn k a a -identity = Conn_ (id &&& id) id -{-# INLINE identity #-} - -- | Lift a 'Conn' into a functor. -- -- /Caution/: This function will result in an invalid connection --- if the functor alters the internal preorder (i.e. 'Data.Ord.Down'). +-- 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 'Conn's into a 'Conn' on the +-- | 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 @@ -169,7 +172,13 @@ h = either (Left . ab') (Right . cd') {-# INLINE choice #-} --- | Lift two 'Conn's into a 'Conn' on the +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 @@ -181,6 +190,30 @@ 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 --------------------------------------------------------------------- @@ -201,22 +234,22 @@ -- /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) -> ConnL a b +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 symmetry between 'ConnL' and 'ConnR'. +-- | Witness to the mirror symmetry between 'ConnL' and 'ConnR'. -- -- > connL . connR = id -- > connR . connL = id -connL :: ConnR a b -> ConnL b a +connL :: Conn 'R a b -> Conn 'L b a connL (ConnR f g) = ConnL f g {-# INLINE connL #-} --- | Obtain the upper adjoint of a 'ConnL', or lower adjoint of a 'ConnR'. -upper :: ConnL a b -> b -> a -upper = embed +-- | 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. @@ -227,22 +260,15 @@ -- -- >>> compare pi $ upper1 f64f32 id pi -- LT -upper1 :: ConnL a b -> (b -> b) -> a -> a +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 :: ConnL a b -> (b -> b -> b) -> a -> a -> a +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 #-} -infixr 5 `join` - --- | Semigroup operation on a join-semilattice. -join :: ConnL (a, a) b -> a -> a -> b -join = curry . ceiling -{-# INLINE join #-} - -- | Extract the lower half of a 'ConnL'. -- -- > ceiling identity = id @@ -252,35 +278,36 @@ -- -- >>> Data.Connection.ceiling ratf32 (0 :% 0) -- NaN --- >>> Data.Connection.ceiling ratf32 (1 :% 0) --- Infinity -- >>> Data.Connection.ceiling ratf32 (13 :% 10) -- 1.3000001 -- >>> Data.Connection.ceiling f64f32 pi -- 3.1415927 -ceiling :: ConnL a b -> a -> b +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 @_ @() @Ordering) id LT --- LT --- >>> ceiling1 (conn @_ @() @Ordering) id GT --- LT -ceiling1 :: ConnL a b -> (a -> a) -> b -> b +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 :: ConnL a b -> (a -> a -> a) -> b -> b -> b +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 --------------------------------------------------------------------- @@ -301,22 +328,22 @@ -- /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) -> ConnR a b +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 symmetry between 'ConnL' and 'ConnR'. +-- | Witness to the mirror symmetry between 'ConnL' and 'ConnR'. -- -- > connL . connR = id -- > connR . connL = id -connR :: ConnL a b -> ConnR b a +connR :: Conn 'L a b -> Conn 'R b a connR (ConnL f g) = ConnR f g {-# INLINE connR #-} --- | Obtain the lower adjoint of a 'ConnR'. -lower :: ConnR a b -> b -> a -lower = embed +-- | 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. @@ -327,22 +354,15 @@ -- -- >>> compare pi $ lower1 f64f32 id pi -- GT -lower1 :: ConnR a b -> (b -> b) -> a -> a +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 :: ConnR a b -> (b -> b -> b) -> a -> a -> a +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 #-} -infixr 6 `meet` - --- | Semigroup operation on a meet-semilattice. -meet :: ConnR (a, a) b -> a -> a -> b -meet = curry . floor -{-# INLINE meet #-} - -- | Extract the upper half of a 'ConnR' -- -- > floor identity = id @@ -352,35 +372,36 @@ -- -- >>> Data.Connection.floor ratf32 (0 :% 0) -- NaN --- >>> Data.Connection.floor ratf32 (1 :% 0) --- Infinity -- >>> Data.Connection.floor ratf32 (13 :% 10) -- 1.3 -- >>> Data.Connection.floor f64f32 pi -- 3.1415925 -floor :: ConnR a b -> a -> b +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 @_ @() @Ordering) id LT --- GT --- >>> floor1 (conn @_ @() @Ordering) id GT --- GT -floor1 :: ConnR a b -> (a -> a) -> b -> b +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 :: ConnR a b -> (a -> a -> a) -> b -> b -> b +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 --------------------------------------------------------------------- @@ -397,10 +418,36 @@ -- -- For detailed properties see 'Data.Connection.Property'. pattern Conn :: (a -> b) -> (b -> a) -> (a -> b) -> Conn k a b -pattern Conn f g h <- (embed &&& _1 &&& _2 -> (g, (h, f))) where Conn f g h = Conn_ (h &&& f) g +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) @ @@ -424,7 +471,7 @@ -- > round identity = id -- -- If x lies halfway between two finite values, then return the value --- with the larger absolute value (i.e. round away from zero). +-- 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 @@ -434,15 +481,19 @@ _ -> truncate c x {-# INLINE round #-} --- | Lift a unary function over a 'Trip'. +-- | 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 a 'Trip'. +-- | 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: @@ -464,19 +515,42 @@ truncate c x = if x >~ 0 then floor c x else ceiling c x {-# INLINE truncate #-} --- | Lift a unary function over a 'Trip'. --- --- Results are truncated towards zero. +-- | 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 --------------------------------------------------------------------- @@ -484,7 +558,7 @@ -- | Convert an inverted 'ConnL' to a 'ConnL'. -- -- > upL . downL = downL . upL = id -upL :: ConnL (Down a) (Down b) -> ConnL b a +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 @@ -494,7 +568,7 @@ -- | Convert an inverted 'ConnR' to a 'ConnR'. -- -- > upR . downR = downR . upR = id -upR :: ConnR (Down a) (Down b) -> ConnR b a +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 @@ -503,23 +577,23 @@ -- | Convert a 'ConnL' to an inverted 'ConnL'. -- --- >>> let counit = upper1 (downL $ conn @_ @() @Ordering) id +-- >>> let counit = upper1 (downL $ bounded @Ordering) id -- >>> counit (Down LT) -- Down LT -- >>> counit (Down GT) -- Down LT -downL :: ConnL a b -> ConnL (Down b) (Down a) +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 $ conn @_ @() @Ordering) id +-- >>> let unit = lower1 (downR $ bounded @Ordering) id -- >>> unit (Down LT) -- Down GT -- >>> unit (Down GT) -- Down GT -downR :: ConnR a b -> ConnR (Down b) (Down a) +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 #-} @@ -531,17 +605,17 @@ -- -- /filterL/ and /filterR/ commute with /Down/: -- --- > filterL c a b <=> ideal c (Down a) (Down b) +-- > filterL c a b <=> filterR c (Down a) (Down b) -- --- > filterL c (Down a) (Down b) <=> ideal c a 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 => meet c (ceiling c a1) (ceiling c a2) <= b +-- > a1 <= b && a2 <= b => minimize c (ceiling c a1) (ceiling c a2) <= b -- -- See -filterL :: Preorder b => ConnL a b -> a -> b -> Bool +filterL :: Preorder b => Conn 'L a b -> a -> b -> Bool filterL c a b = ceiling c a <~ b {-# INLINE filterL #-} @@ -555,9 +629,33 @@ -- -- > a >= b1 && b1 >= b2 => a >= b2 -- --- > a1 >= b && a2 >= b => join c (floor c a1) (floor c a2) >= b +-- > a1 >= b && a2 >= b => maximize c (floor c a1) (floor c a2) >= b -- -- See -filterR :: Preorder b => ConnR a b -> a -> b -> Bool +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 @@ -1,15 +1,14 @@ -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE Safe #-} +{-# LANGUAGE DataKinds #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE Safe #-} module Data.Connection.Fixed ( - Fixed (..), - showFixed, - shiftf, - + -- * Uni Uni, + f00int, -- * Deci Deci, @@ -50,13 +49,23 @@ f12f06, f12f09, - -- * HasResolution + -- * Fixed + f32fix, + f64fix, + ratfix, + shiftf, + showFixed, + Fixed (..), HasResolution (..), ) where import safe Data.Connection.Conn +import safe Data.Connection.Ratio import safe Data.Fixed +import safe Data.Order import safe Data.Order.Syntax +import safe Data.Proxy +import safe GHC.Real (Ratio (..), Rational) import safe Prelude hiding (Eq (..), Ord (..)) -- | Shift by n 'units of least precision' where the ULP is determined by the precision. @@ -65,87 +74,125 @@ shiftf :: Integer -> Fixed a -> Fixed a shiftf j (MkFixed i) = MkFixed (i + j) +-- Uni + +f00int :: Conn k Uni Integer +f00int = Conn f g f + where + f (MkFixed i) = i + g = fromInteger + -- Deci f01f00 :: Conn k Deci Uni -f01f00 = triple 10 +f01f00 = fixfix 10 -- Centi f02f00 :: Conn k Centi Uni -f02f00 = triple 100 +f02f00 = fixfix 100 f02f01 :: Conn k Centi Deci -f02f01 = triple 10 +f02f01 = fixfix 10 -- Milli f03f00 :: Conn k Milli Uni -f03f00 = triple 1000 +f03f00 = fixfix 1000 f03f01 :: Conn k Milli Deci -f03f01 = triple 100 +f03f01 = fixfix 100 f03f02 :: Conn k Milli Centi -f03f02 = triple 10 +f03f02 = fixfix 10 -- Micro f06f00 :: Conn k Micro Uni -f06f00 = triple $ 10 ^ (6 :: Integer) +f06f00 = fixfix $ 10 ^ (6 :: Integer) f06f01 :: Conn k Micro Deci -f06f01 = triple $ 10 ^ (5 :: Integer) +f06f01 = fixfix $ 10 ^ (5 :: Integer) f06f02 :: Conn k Micro Centi -f06f02 = triple $ 10 ^ (4 :: Integer) +f06f02 = fixfix $ 10 ^ (4 :: Integer) f06f03 :: Conn k Micro Milli -f06f03 = triple $ 10 ^ (3 :: Integer) +f06f03 = fixfix $ 10 ^ (3 :: Integer) -- Nano f09f00 :: Conn k Nano Uni -f09f00 = triple $ 10 ^ (9 :: Integer) +f09f00 = fixfix $ 10 ^ (9 :: Integer) f09f01 :: Conn k Nano Deci -f09f01 = triple $ 10 ^ (8 :: Integer) +f09f01 = fixfix $ 10 ^ (8 :: Integer) f09f02 :: Conn k Nano Centi -f09f02 = triple $ 10 ^ (7 :: Integer) +f09f02 = fixfix $ 10 ^ (7 :: Integer) f09f03 :: Conn k Nano Milli -f09f03 = triple $ 10 ^ (6 :: Integer) +f09f03 = fixfix $ 10 ^ (6 :: Integer) f09f06 :: Conn k Nano Micro -f09f06 = triple $ 10 ^ (3 :: Integer) +f09f06 = fixfix $ 10 ^ (3 :: Integer) -- Pico f12f00 :: Conn k Pico Uni -f12f00 = triple $ 10 ^ (12 :: Integer) +f12f00 = fixfix $ 10 ^ (12 :: Integer) f12f01 :: Conn k Pico Deci -f12f01 = triple $ 10 ^ (11 :: Integer) +f12f01 = fixfix $ 10 ^ (11 :: Integer) f12f02 :: Conn k Pico Centi -f12f02 = triple $ 10 ^ (10 :: Integer) +f12f02 = fixfix $ 10 ^ (10 :: Integer) f12f03 :: Conn k Pico Milli -f12f03 = triple $ 10 ^ (9 :: Integer) +f12f03 = fixfix $ 10 ^ (9 :: Integer) f12f06 :: Conn k Pico Micro -f12f06 = triple $ 10 ^ (6 :: Integer) +f12f06 = fixfix $ 10 ^ (6 :: Integer) f12f09 :: Conn k Pico Nano -f12f09 = triple $ 10 ^ (3 :: Integer) +f12f09 = fixfix $ 10 ^ (3 :: Integer) +-- Fixed + +f32fix :: HasResolution e => Conn 'L Float (Extended (Fixed e)) +f32fix = connL ratf32 >>> ratfix + +f64fix :: HasResolution e => Conn 'L Double (Extended (Fixed e)) +f64fix = connL ratf64 >>> ratfix + +ratfix :: forall e k. HasResolution e => Conn k Rational (Extended (Fixed e)) +ratfix = Conn f' g h' + where + prec = resolution (Proxy :: Proxy e) + + f (reduce . (* (toRational prec)) -> n :% d) = MkFixed $ let i = n `div` d in if n `mod` d == 0 then i else i + 1 + + f' = extend (~~ ninf) (\x -> x ~~ nan || x ~~ pinf) f + + g = extended ninf pinf toRational + + h (reduce . (* (toRational prec)) -> n :% d) = MkFixed $ n `div` d + + h' = extend (\x -> x ~~ nan || x ~~ ninf) (~~ pinf) h + + pinf = 1 :% 0 + + ninf = (-1) :% 0 + + nan = 0 :% 0 + + -- Internal ------------------------- -triple :: Integer -> Conn k (Fixed e1) (Fixed e2) -triple prec = Conn f g h +fixfix :: Integer -> Conn k (Fixed e1) (Fixed e2) +fixfix prec = Conn 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 @@ -1,40 +1,33 @@ -{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE DataKinds #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE Safe #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE Safe #-} module Data.Connection.Float ( -- * Float - min32, - max32, - eps32, + f32w08, + f32w16, + f32i08, + f32i16, + f32f32, ulp32, near32, shift32, - f32i08, - f32i16, - f32i32, - f32i64, - f32ixx, - f32int, -- * Double - min64, - max64, - eps64, - ulp64, - near64, - shift64, + f64f64, + f64w08, + f64w16, + f64w32, f64i08, f64i16, f64i32, - f64i64, - f64ixx, - f64int, f64f32, + ulp64, + near64, + shift64, until, ) where @@ -42,8 +35,7 @@ import safe Data.Connection.Conn hiding (ceiling, floor) import safe Data.Int import safe Data.Order -import safe Data.Order.Extended -import safe Data.Order.Syntax hiding (max, min) +import safe Data.Order.Syntax import safe Data.Word import safe GHC.Float as F import safe Prelude hiding (Eq (..), Ord (..), until) @@ -53,34 +45,21 @@ -- Float --------------------------------------------------------------------- --- | A /NaN/-handling min32 function. --- --- > min32 x NaN = x --- > min32 NaN y = y -min32 :: Float -> Float -> Float -min32 x y = case (isNaN x, isNaN y) of - (False, False) -> if x <= y then x else y - (False, True) -> x - (True, False) -> y - (True, True) -> x +f32f32 :: Conn k (Float, Float) Float +f32f32 = fxxfxx --- | A /NaN/-handling max32 function. --- --- > max32 x NaN = x --- > max32 NaN y = y -max32 :: Float -> Float -> Float -max32 x y = case (isNaN x, isNaN y) of - (False, False) -> if x >= y then x else y - (False, True) -> x - (True, False) -> y - (True, True) -> x +f32w08 :: Conn k Float (Extended Word8) +f32w08 = fxxext --- | Compute the difference between a float and its next largest neighbor. --- --- See < https://en.wikipedia.org/wiki/Machine_epsilon >. -eps32 :: Float -> Float -eps32 x = shift32 1 x - x +f32w16 :: Conn k Float (Extended Word16) +f32w16 = fxxext +f32i08 :: Conn k Float (Extended Int8) +f32i08 = fxxext + +f32i16 :: Conn k Float (Extended Int16) +f32i16 = fxxext + -- | Compute the signed distance between two floats in units of least precision. -- -- >>> ulp32 1.0 (shift32 1 1.0) @@ -125,63 +104,53 @@ _ -> 0 / 0 else int32Float . clamp32 . (+ n) . floatInt32 $ x --- | All 'Data.Int.Int08' values are exactly representable in a 'Float'. -f32i08 :: Conn k Float (Extended Int8) -f32i08 = fxxext +--------------------------------------------------------------------- +-- Double +--------------------------------------------------------------------- --- | All 'Data.Int.Int16' values are exactly representable in a 'Float'. --- --- >>> Data.Connection.Conn.ceiling f32i16 32767.0 --- Extended 32767 --- >>> Data.Connection.Conn.ceiling f32i16 32767.1 --- Top -f32i16 :: Conn k Float (Extended Int16) -f32i16 = fxxext +f64f64 :: Conn k (Double, Double) Double +f64f64 = fxxfxx -f32i32 :: Conn 'L Float (Extended Int32) -f32i32 = f32ext +f64w08 :: Conn k Double (Extended Word8) +f64w08 = fxxext -f32i64 :: Conn 'L Float (Extended Int64) -f32i64 = f32ext +f64w16 :: Conn k Double (Extended Word16) +f64w16 = fxxext -f32ixx :: Conn 'L Float (Extended Int) -f32ixx = f32ext +f64w32 :: Conn k Double (Extended Word32) +f64w32 = fxxext -f32int :: Conn 'L Float (Extended Integer) -f32int = f32ext +f64i08 :: Conn k Double (Extended Int8) +f64i08 = fxxext ---------------------------------------------------------------------- --- Double ---------------------------------------------------------------------- +f64i16 :: Conn k Double (Extended Int16) +f64i16 = fxxext --- | A /NaN/-handling min function. --- --- > min64 x NaN = x --- > min64 NaN y = y -min64 :: Double -> Double -> Double -min64 x y = case (isNaN x, isNaN y) of - (False, False) -> if x <= y then x else y - (False, True) -> x - (True, False) -> y - (True, True) -> x +f64i32 :: Conn k Double (Extended Int32) +f64i32 = fxxext --- | A /NaN/-handling max function. --- --- > max64 x NaN = x --- > max64 NaN y = y -max64 :: Double -> Double -> Double -max64 x y = case (isNaN x, isNaN y) of - (False, False) -> if x >= y then x else y - (False, True) -> x - (True, False) -> y - (True, True) -> x +f64f32 :: Conn k Double Float +f64f32 = Conn f g h + where + f x = + let est = double2Float x + in if g est >~ x + then est + else ascend32 est g x --- | Compute the difference between a double and its next largest neighbor. --- --- See < https://en.wikipedia.org/wiki/Machine_epsilon >. -eps64 :: Double -> Double -eps64 x = shift64 1 x - 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 #-} + -- | Compute the signed distance between two doubles in units of least precision. -- -- >>> ulp64 1.0 (shift64 1 1.0) @@ -226,49 +195,6 @@ _ -> 0 / 0 else int64Double . clamp64 . (+ n) . doubleInt64 $ x --- | All 'Data.Int.Int08' values are exactly representable in a 'Double'. -f64i08 :: Conn k Double (Extended Int8) -f64i08 = fxxext - --- | All 'Data.Int.Int16' values are exactly representable in a 'Double'. -f64i16 :: Conn k Double (Extended Int16) -f64i16 = fxxext - --- | All 'Data.Int.Int32' values are exactly representable in a 'Double'. -f64i32 :: Conn k Double (Extended Int32) -f64i32 = fxxext - -f64i64 :: Conn 'L Double (Extended Int64) -f64i64 = f64ext - -f64ixx :: Conn 'L Double (Extended Int) -f64ixx = f64ext - -f64int :: Conn 'L Double (Extended Integer) -f64int = f64ext - -f64f32 :: Conn k Double Float -f64f32 = Conn 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 #-} - --------------------------------------------------------------------- -- Internal --------------------------------------------------------------------- @@ -329,48 +255,25 @@ clamp64 :: Int64 -> Int64 clamp64 = P.max (-9218868437227405313) . P.min 9218868437227405312 -f32ext :: Integral a => Conn 'L Float (Extended a) -f32ext = ConnL f g +fxxfxx :: (Total a, Fractional a) => Conn k (a, a) a +fxxfxx = Conn f g h where - prec = 24 :: Int -- Float loses integer precision beyond 2^prec - f x - | abs x <= 2 ** 24 -1 = Extended (ceiling x) - | otherwise = case pcompare x 0 of - Just LT -> Bottom - _ -> Extended (2 ^ prec) - - g Bottom = -2 ** 24 - g Top = 1 / 0 - g (Extended i) - | abs i P.<= 2 ^ prec -1 = fromIntegral i - | otherwise = if i P.>= 0 then 1 / 0 else -2 ** 24 -{-# INLINE f32ext #-} + -- join + f (x, y) = maybe (1 / 0) (bool y x . (>= EQ)) (pcompare x y) -f64ext :: Integral a => Conn 'L Double (Extended a) -f64ext = ConnL f g - where - prec = 53 :: Int -- Double loses integer precision beyond 2^prec - f x - | abs x <= 2 ** 53 -1 = Extended (ceiling x) - | otherwise = case pcompare x 0 of - Just LT -> Bottom - _ -> Extended (2 ^ prec) + g x = (x, x) - g Bottom = -2 ** 53 - g Top = 1 / 0 - g (Extended i) - | abs i P.<= 2 ^ prec -1 = fromIntegral i - | otherwise = if i P.>= 0 then 1 / 0 else -2 ** 53 -{-# INLINE f64ext #-} + -- 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 where - f = liftExtended (~~ -1 / 0) (\x -> x ~~ 0 / 0 || x > high) $ \x -> if x < low then minBound else ceiling x + f = extend (~~ -1 / 0) (\x -> x ~~ 0 / 0 || x > high) $ \x -> if x < low then minBound else ceiling x g = extended (-1 / 0) (1 / 0) fromIntegral - h = liftExtended (\x -> x ~~ 0 / 0 || x < low) (~~ 1 / 0) $ \x -> if x > high then maxBound else floor x + h = extend (\x -> x ~~ 0 / 0 || x < low) (~~ 1 / 0) $ \x -> if x > high then maxBound else floor x low = fromIntegral $ minBound @b @@ -378,10 +281,51 @@ {-# INLINE fxxext #-} {- +f32i32 :: Conn 'L Float (Extended Int32) +f32i32 = f32ext -frac2fixed :: (RealFrac a, HasResolution b) => a -> Fixed b -frac2fixed (flip approxRational 0 -> (n :% d)) = fromInteger n / fromInteger d +f32i64 :: Conn 'L Float (Extended Int64) +f32i64 = f32ext ---fixed2Float :: forall a . HasResolution a => Fixed a -> Float ---fixed2Float (MkFixed i) = rationalToFloat i $ resolution (Proxy :: Proxy a) +f32ixx :: Conn 'L Float (Extended Int) +f32ixx = f32ext + +f32int :: Conn 'L Float (Extended Integer) +f32int = f32ext + +f64i64 :: Conn 'L Double (Extended Int64) +f64i64 = f64ext + +f64ixx :: Conn 'L Double (Extended Int) +f64ixx = f64ext + +{-# INLINE f64ext #-} +f64int :: Conn 'L Double (Extended Integer) +f64int = f64ext + +f32ext :: Integral a => Conn '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 = 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 + where + f x + | abs x <= 2 ^^ prec -1 = Finite (ceiling x) + | otherwise = case pcompare x 0 of + Just LT -> NegInf + _ -> Finite (2 ^ prec) + + g NegInf = -2 ^^ prec + g PosInf = 1 / 0 + g (Finite i) + | abs i P.<= 2 ^ prec -1 = fromIntegral i + | otherwise = if i P.>= 0 then 1 / 0 else -2 ^^ prec + +{-# INLINE fxxextL #-} + -} 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 @@ -1,6 +1,7 @@ {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE RankNTypes #-} +{-# LANGUAGE Safe #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} @@ -13,42 +14,49 @@ -- \( \forall x : f \dashv g \Rightarrow f \circ g (x) \leq x \) module Data.Connection.Property ( -- * Adjointness + adjoint, adjointL, adjointR, - adjoint, adjunction, -- * Closure + closed, closedL, closedR, - closed, + kernel, kernelL, kernelR, - kernel, invertible, -- * Monotonicity + monotonic, monotonicR, monotonicL, - monotonic, monotone, -- * Idempotence + idempotent, idempotentL, idempotentR, - idempotent, projective, ) where -import Data.Connection -import Data.Order -import Data.Order.Property -import Prelude hiding (Num (..), Ord (..), ceiling, floor) +import safe Data.Connection.Conn +import safe Data.Order +import safe Data.Order.Property +import safe Prelude hiding (Num (..), Ord (..), ceiling, floor) -- Adjointness ------------------------- +adjoint :: (Preorder a, Preorder b) => (forall k. Conn 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 + -- | \( \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. @@ -58,13 +66,6 @@ adjointR :: (Preorder a, Preorder b) => ConnR a b -> a -> b -> Bool adjointR (ConnR f g) = adjunction (>~) (>~) g f -adjoint :: (Preorder a, Preorder b) => (forall k. Conn 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 - -- | \( \forall a: f a \leq b \Leftrightarrow a \leq g b \) -- -- A monotone Galois connection is defined by @adjunction (<~) (<~)@, @@ -76,6 +77,9 @@ ------------------------- +closed :: (Preorder a, Preorder b) => (forall k. Conn 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. @@ -85,8 +89,8 @@ closedR :: (Preorder a, Preorder b) => ConnR a b -> a -> Bool closedR (ConnR f g) = invertible (<~) g f -closed :: (Preorder a, Preorder b) => (forall k. Conn k a b) -> a -> Bool -closed t a = closedL t a && closedR t a +kernel :: (Preorder a, Preorder b) => (forall k. Conn 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) \) -- @@ -97,9 +101,6 @@ kernelR :: (Preorder a, Preorder b) => ConnR a b -> b -> Bool kernelR (ConnR f g) = invertible (>~) f g -kernel :: (Preorder a, Preorder b) => (forall k. Conn k a b) -> b -> Bool -kernel t b = kernelL t b && kernelR t b - -- | \( \forall a: f (g a) \sim a \) invertible :: Rel s b -> (s -> r) -> (r -> s) -> s -> b invertible (#) f g a = g (f a) # a @@ -108,6 +109,9 @@ ------------------------- +monotonic :: (Preorder a, Preorder b) => (forall k. Conn 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. @@ -117,9 +121,6 @@ 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 -monotonic :: (Preorder a, Preorder b) => (forall k. Conn 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 a, b: a \leq b \Rightarrow f(a) \leq f(b) \) monotone :: Rel r Bool -> Rel s Bool -> (r -> s) -> r -> r -> Bool monotone (#) (%) f a b = a # b ==> f a % f b @@ -128,6 +129,9 @@ ------------------------- +idempotent :: (Preorder a, Preorder b) => (forall k. Conn 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 @@ -136,9 +140,6 @@ 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 - -idempotent :: (Preorder a, Preorder b) => (forall k. Conn k a b) -> a -> b -> Bool -idempotent t a b = idempotentL t a b && idempotentR t a 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 @@ -1,42 +1,37 @@ {-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE Safe #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE Safe #-} module Data.Connection.Ratio ( - Ratio (..), - reduce, - shiftr, - -- * Rational + ratw08, + ratw16, + ratw32, + ratw64, + ratwxx, + ratnat, rati08, rati16, rati32, rati64, ratixx, ratint, - ratfix, ratf32, ratf64, - - -- * Positive - posw08, - posw16, - posw32, - posw64, - poswxx, - posnat, + ratrat, + reduce, + shiftr, + Ratio (..), ) where -import safe Data.Connection.Conn hiding (ceiling, floor) -import safe Data.Connection.Fixed +import safe Data.Bool +import safe Data.Connection.Conn hiding (ceiling, floor, lower) import safe Data.Connection.Float as Float import safe Data.Int import safe Data.Order -import safe Data.Order.Extended import safe Data.Order.Syntax -import safe Data.Proxy import safe Data.Ratio import safe Data.Word import safe GHC.Real (Ratio (..), Rational) @@ -58,44 +53,53 @@ -- Ratio Integer --------------------------------------------------------------------- +ratw08 :: Conn k Rational (Extended Word8) +ratw08 = ratext + +ratw16 :: Conn k Rational (Extended Word16) +ratw16 = ratext + +ratw32 :: Conn k Rational (Extended Word32) +ratw32 = ratext + +ratw64 :: Conn k Rational (Extended Word64) +ratw64 = ratext + +ratwxx :: Conn k Rational (Extended Word) +ratwxx = ratext + +ratnat :: Conn k Rational (Extended Natural) +ratnat = Conn f g h + where + f = extend (~~ ninf) (\x -> x ~~ nan || x ~~ pinf) (ceiling . max 0) + + g = extended ninf pinf fromIntegral + + h = extend (\x -> x ~~ nan || x < 0) (~~ pinf) (floor . max 0) + rati08 :: Conn k Rational (Extended Int8) -rati08 = tripleI +rati08 = ratext rati16 :: Conn k Rational (Extended Int16) -rati16 = tripleI +rati16 = ratext rati32 :: Conn k Rational (Extended Int32) -rati32 = tripleI +rati32 = ratext rati64 :: Conn k Rational (Extended Int64) -rati64 = tripleI +rati64 = ratext ratixx :: Conn k Rational (Extended Int) -ratixx = tripleI +ratixx = ratext ratint :: Conn k Rational (Extended Integer) ratint = Conn f g h where - f = liftExtended (~~ ninf) (\x -> x ~~ nan || x ~~ pinf) ceiling + f = extend (~~ ninf) (\x -> x ~~ nan || x ~~ pinf) ceiling g = extended ninf pinf fromIntegral - h = liftExtended (\x -> x ~~ nan || x ~~ ninf) (~~ pinf) floor - -ratfix :: forall e k. HasResolution e => Conn k Rational (Extended (Fixed e)) -ratfix = Conn f' g h' - where - prec = resolution (Proxy :: Proxy e) - - f (reduce . (* (toRational prec)) -> n :% d) = MkFixed $ let i = n `div` d in if n `mod` d == 0 then i else i + 1 - - f' = liftExtended (~~ ninf) (\x -> x ~~ nan || x ~~ pinf) f - - g = extended ninf pinf toRational - - h (reduce . (* (toRational prec)) -> n :% d) = MkFixed $ n `div` d - - h' = liftExtended (\x -> x ~~ nan || x ~~ ninf) (~~ pinf) h + h = extend (\x -> x ~~ nan || x ~~ ninf) (~~ pinf) floor ratf32 :: Conn k Rational Float ratf32 = Conn (toFractional f) (fromFractional g) (toFractional h) @@ -139,33 +143,16 @@ descendf z f1 x = Float.until (\y -> f1 y <~ x) (>~) (Float.shift64 (-1)) z ---------------------------------------------------------------------- --- Ratio Natural ---------------------------------------------------------------------- - -posw08 :: Conn k Positive (Lowered Word8) -posw08 = tripleW - -posw16 :: Conn k Positive (Lowered Word16) -posw16 = tripleW - -posw32 :: Conn k Positive (Lowered Word32) -posw32 = tripleW - -posw64 :: Conn k Positive (Lowered Word64) -posw64 = tripleW - -poswxx :: Conn k Positive (Lowered Word) -poswxx = tripleW - -posnat :: Conn k Positive (Lowered Natural) -posnat = Conn f g h +ratrat :: Conn k (Rational, Rational) Rational +ratrat = Conn f g h where - f = liftEitherR (\x -> x ~~ nan || x ~~ pinf) ceiling + -- join + f (x, y) = maybe (1 / 0) (bool y x . (>= EQ)) (pcompare x y) - g = either fromIntegral (const pinf) + g x = (x, x) - h = liftEitherR (~~ pinf) $ \x -> if x ~~ nan then 0 else floor x + -- meet + h (x, y) = maybe (-1 / 0) (bool y x . (<= EQ)) (pcompare x y) --------------------------------------------------------------------- -- Internal @@ -180,36 +167,20 @@ nan :: Num a => Ratio a nan = 0 :% 0 -tripleW :: forall a k. (Bounded a, Integral a) => Conn k Positive (Lowered a) -tripleW = Conn f g h - where - f x - | x ~~ nan = Right maxBound - | x > high = Right maxBound - | otherwise = Left $ ceiling x - - g = either fromIntegral (const pinf) - - h x - | x ~~ nan = Left minBound - | x ~~ pinf = Right maxBound - | x > high = Left maxBound - | otherwise = Left $ floor x - - high = fromIntegral @a maxBound - -tripleI :: forall a k. (Bounded a, Integral a) => Conn k Rational (Extended a) -tripleI = Conn f g h +ratext :: forall a k. (Bounded a, Integral a) => Conn k Rational (Extended a) +ratext = Conn f g h where - f = liftExtended (~~ ninf) (\x -> x ~~ nan || x > high) $ \x -> if x < low then minBound else ceiling x + f = extend (~~ ninf) (\x -> x ~~ nan || x > high) $ \x -> if x < low then minBound else ceiling x g = extended ninf pinf fromIntegral - h = liftExtended (\x -> x ~~ nan || x < low) (~~ pinf) $ \x -> if x > high then maxBound else floor x + h = extend (\x -> x ~~ nan || x < low) (~~ pinf) $ \x -> if x > high then maxBound else floor x high = fromIntegral @a maxBound - low = -1 - high + low = fromIntegral @a minBound +--low = -1 - high + toFractional :: Fractional a => (Rational -> a) -> Rational -> a toFractional f x | x ~~ nan = 0 / 0 @@ -236,12 +207,4 @@ nanr :: Integral b => (a -> Ratio b) -> Maybe a -> Ratio b nanr f = maybe (0 :% 0) f -ratpos :: Conn k Rational Positive -ratpos = Conn k f g h where - - f = liftExtended (~~ ninf) (\x -> x ~~ nan || x ~~ pinf) ceiling - - g = extended minBound maxBound fromIntegral - - h = liftExtended (\x -> x ~~ nan || x ~~ ninf) (~~ pinf) floor -} diff --git a/src/Data/Connection/Time.hs b/src/Data/Connection/Time.hs new file mode 100644 --- /dev/null +++ b/src/Data/Connection/Time.hs @@ -0,0 +1,114 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE Safe #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE ViewPatterns #-} + +module Data.Connection.Time ( + -- * SystemTime + sysixx, + f32sys, + f64sys, + ratsys, + f09sys, + diffSystemTime, + getSystemTime, + SystemTime (..), +) where + +import safe Data.Connection.Conn +import safe Data.Connection.Fixed +import safe Data.Connection.Ratio +import safe Data.Int +import safe Data.Order.Syntax +import safe Data.Time.Clock.System +import safe Prelude hiding (Eq (..), Ord (..), ceiling) + +-- $setup +-- >>> :set -XTypeApplications +-- >>> import Data.Word + +-- SystemTime + +------------------------- + +-- | The 'Int' is valued in seconds +sysixx :: Conn k SystemTime Int +sysixx = Conn f g h + where + f (normalize -> MkSystemTime s n) = fromIntegral s + if n == 0 then 0 else 1 + g i = MkSystemTime (fromIntegral i) 0 + h (normalize -> MkSystemTime s _) = fromIntegral s + +-- | The 'Float' is valued in seconds. +-- +-- >>> Data.Connection.ceiling f32sys (0/0) +-- PosInf +-- >>> Data.Connection.ceiling f32sys pi +-- Finite (MkSystemTime {systemSeconds = 3, systemNanoseconds = 141592742}) +f32sys :: Conn 'L Float (Extended SystemTime) +f32sys = connL ratf32 >>> ratsys + +-- | The 'Double' is valued in seconds. +-- +-- >>> Data.Connection.ceiling f64sys (0/0) +-- PosInf +-- >>> Data.Connection.ceiling f64sys pi +-- Finite (MkSystemTime {systemSeconds = 3, systemNanoseconds = 141592654}) +f64sys :: Conn 'L Double (Extended SystemTime) +f64sys = connL ratf64 >>> ratsys + +-- | The 'Rational' is valued in seconds. +ratsys :: Conn 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 + where + f NegInf = NegInf + f (Finite i) = extend (const False) (> max64) (fromNanoSecs . clamp) i + f PosInf = PosInf + + g = fmap toNanoSecs + + h NegInf = NegInf + h (Finite i) = extend (< min64) (const False) (fromNanoSecs . clamp) i + h PosInf = PosInf + + min64 = - 2 ^ 63 + max64 = 2 ^ 63 - 1 + + clamp = max min64 . min max64 + +-- | Return the difference between two 'SystemTime's in seconds +-- +-- >>> diffSystemTime (MkSystemTime 0 0) (MkSystemTime 0 maxBound) +-- -4.294967295 +-- >>> divMod (maxBound @Word32) (10^9) +-- (4,294967295) +diffSystemTime :: SystemTime -> SystemTime -> Double +diffSystemTime x y = inner f64sys $ round2 ratsys (-) (Finite x) (Finite y) + +-- Internal + +------------------------- + +s2ns :: Num a => a +s2ns = 10 ^ 9 + +toNanoSecs :: SystemTime -> Nano +toNanoSecs (MkSystemTime (toInteger -> s) (toInteger -> n)) = MkFixed (s * s2ns + n) + +fromNanoSecs :: Nano -> SystemTime +fromNanoSecs (MkFixed i) = MkSystemTime (fromInteger $ q) (fromInteger r) + where + (q, r) = divMod i s2ns + +normalize :: SystemTime -> SystemTime +normalize (MkSystemTime xs xn) + | xn >= s2ns = MkSystemTime (xs + q) (fromIntegral r) + | otherwise = MkSystemTime xs xn + where + (q, r) = fromIntegral xn `divMod` s2ns 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 @@ -1,4 +1,5 @@ {-# LANGUAGE Safe #-} +{-# LANGUAGE DataKinds #-} module Data.Connection.Word ( -- * Word8 @@ -57,128 +58,128 @@ import safe Numeric.Natural -- Word8 -i08w08 :: ConnL Int8 Word8 +i08w08 :: Conn 'L Int8 Word8 i08w08 = unsigned -- Word16 -w08w16 :: ConnL Word8 Word16 +w08w16 :: Conn 'L Word8 Word16 w08w16 = unsigned -i08w16 :: ConnL Int8 Word16 +i08w16 :: Conn 'L Int8 Word16 i08w16 = unsigned -i16w16 :: ConnL Int16 Word16 +i16w16 :: Conn 'L Int16 Word16 i16w16 = unsigned -- Word32 -w08w32 :: ConnL Word8 Word32 +w08w32 :: Conn 'L Word8 Word32 w08w32 = unsigned -w16w32 :: ConnL Word16 Word32 +w16w32 :: Conn 'L Word16 Word32 w16w32 = unsigned -i08w32 :: ConnL Int8 Word32 +i08w32 :: Conn 'L Int8 Word32 i08w32 = unsigned -i16w32 :: ConnL Int16 Word32 +i16w32 :: Conn 'L Int16 Word32 i16w32 = unsigned -i32w32 :: ConnL Int32 Word32 +i32w32 :: Conn 'L Int32 Word32 i32w32 = unsigned -- Word64 -w08w64 :: ConnL Word8 Word64 +w08w64 :: Conn 'L Word8 Word64 w08w64 = unsigned -w16w64 :: ConnL Word16 Word64 +w16w64 :: Conn 'L Word16 Word64 w16w64 = unsigned -w32w64 :: ConnL Word32 Word64 +w32w64 :: Conn 'L Word32 Word64 w32w64 = unsigned -i08w64 :: ConnL Int8 Word64 +i08w64 :: Conn 'L Int8 Word64 i08w64 = unsigned -i16w64 :: ConnL Int16 Word64 +i16w64 :: Conn 'L Int16 Word64 i16w64 = unsigned -i32w64 :: ConnL Int32 Word64 +i32w64 :: Conn 'L Int32 Word64 i32w64 = unsigned -i64w64 :: ConnL Int64 Word64 +i64w64 :: Conn 'L Int64 Word64 i64w64 = unsigned -ixxw64 :: ConnL Int Word64 +ixxw64 :: Conn 'L Int Word64 ixxw64 = unsigned -- Word -w08wxx :: ConnL Word8 Word +w08wxx :: Conn 'L Word8 Word w08wxx = unsigned -w16wxx :: ConnL Word16 Word +w16wxx :: Conn 'L Word16 Word w16wxx = unsigned -w32wxx :: ConnL Word32 Word +w32wxx :: Conn 'L Word32 Word w32wxx = unsigned -- | /Caution/: This assumes that 'Word' on your system is 64 bits. w64wxx :: Conn k Word64 Word w64wxx = Conn fromIntegral fromIntegral fromIntegral -i08wxx :: ConnL Int8 Word +i08wxx :: Conn 'L Int8 Word i08wxx = unsigned -i16wxx :: ConnL Int16 Word +i16wxx :: Conn 'L Int16 Word i16wxx = unsigned -i32wxx :: ConnL Int32 Word +i32wxx :: Conn 'L Int32 Word i32wxx = unsigned -i64wxx :: ConnL Int64 Word +i64wxx :: Conn 'L Int64 Word i64wxx = unsigned -ixxwxx :: ConnL Int Word +ixxwxx :: Conn 'L Int Word ixxwxx = unsigned -- Natural -w08nat :: ConnL Word8 Natural +w08nat :: Conn 'L Word8 Natural w08nat = unsigned -w16nat :: ConnL Word16 Natural +w16nat :: Conn 'L Word16 Natural w16nat = unsigned -w32nat :: ConnL Word32 Natural +w32nat :: Conn 'L Word32 Natural w32nat = unsigned -w64nat :: ConnL Word64 Natural +w64nat :: Conn 'L Word64 Natural w64nat = unsigned -wxxnat :: ConnL Word Natural +wxxnat :: Conn 'L Word Natural wxxnat = unsigned -i08nat :: ConnL Int8 Natural +i08nat :: Conn 'L Int8 Natural i08nat = unsigned -i16nat :: ConnL Int16 Natural +i16nat :: Conn 'L Int16 Natural i16nat = unsigned -i32nat :: ConnL Int32 Natural +i32nat :: Conn 'L Int32 Natural i32nat = unsigned -i64nat :: ConnL Int64 Natural +i64nat :: Conn 'L Int64 Natural i64nat = unsigned -ixxnat :: ConnL Int Natural +ixxnat :: Conn 'L Int Natural ixxnat = unsigned -intnat :: ConnL Integer Natural +intnat :: Conn 'L Integer Natural intnat = ConnL (fromIntegral . max 0) fromIntegral --------------------------------------------------------------------- -- Internal --------------------------------------------------------------------- -unsigned :: (Bounded a, Integral a, Integral b) => ConnL a b +unsigned :: (Bounded a, Integral a, Integral b) => Conn 'L a b unsigned = ConnL f g where f = fromIntegral . max 0 diff --git a/src/Data/Lattice.hs b/src/Data/Lattice.hs --- a/src/Data/Lattice.hs +++ b/src/Data/Lattice.hs @@ -18,11 +18,13 @@ -- ** Meet Meet, (/\), + glb, top, -- ** Join Join, (\/), + lub, bottom, -- * Algebra @@ -60,7 +62,6 @@ import safe Data.Bifunctor (bimap) import safe Data.Bool hiding (not) -import safe Data.Connection.Class hiding ((/\), (\/)) import safe Data.Connection.Conn import safe Data.Either import safe Data.Int @@ -68,13 +69,16 @@ import safe qualified Data.IntSet as IntSet import safe qualified Data.Map as Map import safe Data.Order -import safe Data.Order.Extended import safe Data.Order.Syntax import safe qualified Data.Set as Set import safe Data.Word import safe Prelude hiding (Eq (..), Ord (..), ceiling, floor, not) import safe qualified Prelude as P +-- >>> import safe Data.IntSet (IntSet,fromList) +-- >>> :load Data.Connection +-- >>> import safe Prelude hiding (round, floor, ceiling, truncate) + ------------------------------------------------------------------------------- -- Lattices ------------------------------------------------------------------------------- @@ -92,7 +96,7 @@ -- A lattice is a partially ordered set in which every two elements have a unique join -- (least upper bound or supremum) and a unique meet (greatest lower bound or infimum). -- --- A bounded lattice adds unique elements 'top' and 'bottom', which serve as +-- A bound lattice adds unique elements 'top' and 'bottom', which serve as -- identities to '\/' and '/\', respectively. -- -- /Neutrality/: @@ -142,20 +146,16 @@ -- @ -- -- See < https://en.wikipedia.org/wiki/Lattice_(order) >. -class Order a => Semilattice (k :: Kan) a where - -- | The defining connection of a bounded semilattice. +class Order a => Semilattice k a where + -- | The defining connection of a bound semilattice. -- -- 'bottom' and 'top' are defined by the left and right adjoints to /a -> ()/. - bounded :: Conn k () a - default bounded :: Connection k () a => Conn k () a - bounded = conn + bound :: Conn 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 - default semilattice :: Connection k (a, a) a => Conn k (a, a) a - semilattice = conn infixr 6 /\ -- comment for the parser @@ -165,12 +165,28 @@ (/\) :: Meet a => a -> a -> a (/\) = curry $ floor semilattice --- | The unique top element of a bounded lattice +-- | Greatest lower bound operator. -- +-- > glb x x y = x +-- > glb x y z = glb z x y +-- > glb x y z = glb x z y +-- > glb (glb x w y) w z = glb x w (glb y w z) +-- +-- >>> glb 1.0 9.0 7.0 +-- 7.0 +-- >>> glb 1.0 9.0 (0.0 / 0.0) +-- 9.0 +-- >>> glb (fromList [1..3]) (fromList [3..5]) (fromList [5..7]) :: IntSet +-- fromList [3,5] +glb :: Lattice a => a -> a -> a -> a +glb x y z = (x \/ y) /\ (y \/ z) /\ (z \/ x) + +-- | The unique top element of a bound lattice +-- -- > x /\ top = x -- > x \/ top = top top :: Meet a => a -top = floor bounded () +top = floor bound () infixr 5 \/ @@ -180,12 +196,23 @@ (\/) :: Join a => a -> a -> a (\/) = curry $ ceiling semilattice --- | The unique bottom element of a bounded lattice +-- | Least upper bound operator. -- +-- The order dual of 'glb'. +-- +-- >>> lub 1.0 9.0 7.0 +-- 7.0 +-- >>> lub 1.0 9.0 (0.0 / 0.0) +-- 1.0 +lub :: Lattice a => a -> a -> a -> a +lub x y z = x /\ y \/ y /\ z \/ z /\ x + +-- | The unique bottom element of a bound lattice +-- -- > x /\ bottom = bottom -- > x \/ bottom = x bottom :: Join a => a -bottom = ceiling bounded () +bottom = ceiling bound () ------------------------------------------------------------------------------- -- Heyting algebras @@ -208,7 +235,7 @@ -- | Heyting and co-Heyting algebras -- --- A Heyting algebra is a bounded, distributive lattice equipped with an +-- A Heyting algebra is a bound, distributive lattice equipped with an -- implication operation. -- -- * The complete of closed subsets of a topological space is the primordial @@ -227,7 +254,7 @@ -- -- > EQ /\ non EQ = EQ /\ GT \\ EQ = EQ /\ GT = EQ /= LT -- --- See < https://ncatlab.org/nlab/show/co-Algebra+algebra > +-- See < https://ncatlab.org/nlab/show/co-Heyting+algebra > -- -- /Heyting/: -- @@ -302,7 +329,7 @@ -- > neg (neg (neg x)) = neg x -- > neg (neg (x \/ neg x)) = top -- --- Some logics may in addition obey < https://ncatlab.org/nlab/show/De+Morgan+Algebra+algebra De Morgan conditions >. +-- Some logics may in addition obey < https://ncatlab.org/nlab/show/De+Morgan+Heyting+algebra De Morgan conditions >. neg :: Heyting a => a -> a neg x = x // bottom @@ -318,11 +345,11 @@ -- -- Double negation is a meet-preserving monad. booleanR :: Heyting a => ConnR a a -booleanR = - let -- Check that /x/ is a regular element - -- See https://ncatlab.org/nlab/show/regular+element - inj x = if x ~~ (neg . neg) x then x else bottom - in ConnR (neg . neg) inj +booleanR = ConnR (neg . neg) inj + where + -- Check that /x/ is a regular element + -- See https://ncatlab.org/nlab/show/regular+element + inj x = if x ~~ (neg . neg) x then x else bottom ------------------------------------------------------------------------------- -- Coheyting @@ -403,11 +430,11 @@ -- -- Double negation is a join-preserving comonad. booleanL :: Coheyting a => ConnL a a -booleanL = - let -- Check that /x/ is a regular element - -- See https://ncatlab.org/nlab/show/regular+element - inj x = if x ~~ (non . non) x then x else top - in ConnL inj (non . non) +booleanL = ConnL inj (non . non) + where + -- Check that /x/ is a regular element + -- See https://ncatlab.org/nlab/show/regular+element + inj x = if x ~~ (non . non) x then x else top ------------------------------------------------------------------------------- -- Symmetric @@ -415,7 +442,7 @@ -- | Symmetric Heyting algebras -- --- A symmetric Heyting algebra is a +-- A symmetric Heyting algebra is a -- bi-Algebra algebra with an idempotent, antitone negation operator. -- -- /Laws/: @@ -494,19 +521,28 @@ -- Instances ------------------------------------------------------------------------------- -instance Semilattice k () +instance Semilattice k () where + bound = bounded + semilattice = ordered + instance Algebra 'L () where algebra = coheyting impliesL instance Algebra 'R () where algebra = heyting impliesR instance Symmetric () where not = id instance Boolean () -instance Semilattice k Bool +instance Semilattice k Bool where + bound = bounded + semilattice = ordered + instance Algebra 'L Bool where algebra = coheyting impliesL instance Algebra 'R Bool where algebra = heyting impliesR instance Symmetric Bool where not = P.not instance Boolean Bool -instance Semilattice k Ordering +instance Semilattice k Ordering where + bound = bounded + semilattice = ordered + instance Algebra 'L Ordering where algebra = coheyting impliesL instance Algebra 'R Ordering where algebra = heyting impliesR instance Symmetric Ordering where @@ -514,52 +550,99 @@ not EQ = EQ not GT = LT -instance Semilattice k Word8 +instance Semilattice k Word8 where + bound = bounded + semilattice = ordered + instance Algebra 'L Word8 where algebra = coheyting impliesL instance Algebra 'R Word8 where algebra = heyting impliesR -instance Semilattice k Word16 +instance Semilattice k Word16 where + bound = bounded + semilattice = ordered + instance Algebra 'L Word16 where algebra = coheyting impliesL instance Algebra 'R Word16 where algebra = heyting impliesR -instance Semilattice k Word32 +instance Semilattice k Word32 where + bound = bounded + semilattice = ordered + instance Algebra 'L Word32 where algebra = coheyting impliesL instance Algebra 'R Word32 where algebra = heyting impliesR -instance Semilattice k Word64 +instance Semilattice k Word64 where + bound = bounded + semilattice = ordered + instance Algebra 'L Word64 where algebra = coheyting impliesL instance Algebra 'R Word64 where algebra = heyting impliesR -instance Semilattice k Word +instance Semilattice k Word where + bound = bounded + semilattice = ordered + instance Algebra 'L Word where algebra = coheyting impliesL instance Algebra 'R Word where algebra = heyting impliesR -instance Semilattice k Int8 +instance Semilattice k Int8 where + bound = bounded + semilattice = ordered + instance Algebra 'L Int8 where algebra = coheyting impliesL instance Algebra 'R Int8 where algebra = heyting impliesR -instance Semilattice k Int16 +instance Semilattice k Int16 where + bound = bounded + semilattice = ordered + instance Algebra 'L Int16 where algebra = coheyting impliesL instance Algebra 'R Int16 where algebra = heyting impliesR -instance Semilattice k Int32 +instance Semilattice k Int32 where + bound = bounded + semilattice = ordered + instance Algebra 'L Int32 where algebra = coheyting impliesL instance Algebra 'R Int32 where algebra = heyting impliesR -instance Semilattice k Int64 +instance Semilattice k Int64 where + bound = bounded + semilattice = ordered + instance Algebra 'L Int64 where algebra = coheyting impliesL instance Algebra 'R Int64 where algebra = heyting impliesR -instance Semilattice k Int +instance Semilattice k Int where + bound = bounded + semilattice = ordered + instance Algebra 'L Int where algebra = coheyting impliesL instance Algebra 'R Int where algebra = heyting impliesR +{- +instance Semilattice k Float where + bound = conn + semilattice = conn + +instance Semilattice k Double where + bound = conn + semilattice = conn + +instance Semilattice k Rational where + bound = conn + semilattice = conn + +instance Semilattice k Positive where + bound = conn + semilattice = conn +-} ------------------------------------------------------------------------------- -- Instances: product types ------------------------------------------------------------------------------- instance (Lattice a, Lattice b) => Semilattice k (a, b) where - bounded = Conn (const (bottom, bottom)) (const ()) (const (top, top)) + bound = Conn (const (bottom, bottom)) (const ()) (const (top, top)) semilattice = Conn (uncurry joinTuple) fork (uncurry meetTuple) instance (Heyting a, Heyting b) => Algebra 'R (a, b) where @@ -578,11 +661,11 @@ ------------------------------------------------------------------------------- instance Join a => Semilattice 'L (Maybe a) where - bounded = ConnL (const Nothing) (const ()) + bound = ConnL (const Nothing) (const ()) semilattice = ConnL (uncurry joinMaybe) fork instance Meet a => Semilattice 'R (Maybe a) where - bounded = ConnR (const ()) (const $ Just top) + bound = ConnR (const ()) (const $ Just top) semilattice = ConnR fork (uncurry meetMaybe) instance Heyting a => Algebra 'R (Maybe a) where @@ -593,36 +676,36 @@ f _ Nothing = Nothing instance Join a => Semilattice 'L (Extended a) where - bounded = Conn (const Bottom) (const ()) (const Top) + bound = Conn (const NegInf) (const ()) (const PosInf) semilattice = ConnL (uncurry joinExtended) fork instance Meet a => Semilattice 'R (Extended a) where - bounded = Conn (const Bottom) (const ()) (const Top) + bound = Conn (const NegInf) (const ()) (const PosInf) semilattice = ConnR fork (uncurry meetExtended) instance Heyting a => Algebra 'R (Extended a) where algebra = heyting f where - Extended a `f` Extended b - | a <~ b = Top - | otherwise = Extended (a // b) - Top `f` a = a - _ `f` Top = Top - Bottom `f` _ = Top - _ `f` Bottom = Bottom + Finite a `f` Finite b + | a <~ b = PosInf + | otherwise = Finite (a // b) + PosInf `f` a = a + _ `f` PosInf = PosInf + NegInf `f` _ = PosInf + _ `f` NegInf = NegInf -- | All minimal elements of the upper lattice cover all maximal elements of the lower lattice. instance (Join a, Join b) => Semilattice 'L (Either a b) where - bounded = ConnL (const $ Left bottom) (const ()) + bound = ConnL (const $ Left bottom) (const ()) semilattice = ConnL (uncurry joinEither) fork instance (Meet a, Meet b) => Semilattice 'R (Either a b) where - bounded = ConnR (const ()) (const $ Right top) + bound = ConnR (const ()) (const $ Right top) semilattice = ConnR fork (uncurry meetEither) -- | -- Subdirectly irreducible Algebra algebra. -instance Heyting a => Algebra 'R (Lowered a) where +instance Heyting a => Algebra 'R (Either a ()) where algebra = heyting f where (Left a) `f` (Left b) @@ -631,7 +714,7 @@ (Right _) `f` a = a _ `f` (Right _) = top -instance Heyting a => Algebra 'R (Lifted a) where +instance Heyting a => Algebra 'R (Either () a) where algebra = heyting f where f (Right a) (Right b) = Right (a // b) @@ -642,8 +725,39 @@ -- Instances: collections ------------------------------------------------------------------------------- -instance Total a => Semilattice 'L (Set.Set a) +{- +instance Total a => Connection k (Set.Set a, Set.Set a) (Set.Set a) where + semilattice = Conn (uncurry Set.union) fork (uncurry Set.intersection) +instance Connection 'L () IntSet.IntSet where + bound = ConnL (const IntSet.empty) (const ()) + +instance Connection k (IntSet.IntSet, IntSet.IntSet) IntSet.IntSet where + semilattice = Conn (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 ()) + +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 + +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) + +instance Preorder a => Connection 'L () (IntMap.IntMap a) where + bound = ConnL (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 + +instance Right (a, a) a => Connection 'R (IntMap.IntMap a, IntMap.IntMap a) (IntMap.IntMap a) where + semilattice = ConnR 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 + instance Total a => Algebra 'L (Set.Set a) where algebra = coheyting (Set.\\) @@ -655,11 +769,20 @@ --instance (Total a, U.Finite a) => Boolean (Set.Set a) where -instance Semilattice 'L IntSet.IntSet +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) instance Algebra 'L IntSet.IntSet where algebra = coheyting (IntSet.\\) +instance Algebra 'R IntSet.IntSet where + --heyting = heyting $ \x y -> non x \/ y + algebra = symmetricR + +instance Symmetric IntSet.IntSet where + not = non --(U.universe IntSet.\\) + {- instance Algebra 'R IntSet.IntSet where --heyting = heyting $ \x y -> non x \/ y @@ -673,100 +796,25 @@ -} instance (Total k, Join a) => Semilattice 'L (Map.Map k a) where - bounded = ConnL (const Map.empty) (const ()) + bound = ConnL (const Map.empty) (const ()) semilattice = ConnL f fork where - f = uncurry $ Map.unionWith (curry $ ceiling semilattice) + f = uncurry $ Map.unionWith (\/) instance (Total k, Join a) => Algebra 'L (Map.Map k a) where algebra = coheyting (Map.\\) instance (Join a) => Semilattice 'L (IntMap.IntMap a) where - bounded = ConnL (const IntMap.empty) (const ()) + bound = ConnL (const IntMap.empty) (const ()) semilattice = ConnL f fork where - f = uncurry $ IntMap.unionWith (curry $ ceiling semilattice) + f = uncurry $ IntMap.unionWith (\/) instance (Join a) => Algebra 'L (IntMap.IntMap a) where algebra = coheyting (IntMap.\\) -{- TODO pick an instance either key-aware or no - -instance (Total a, U.Finite a, Heyting b) => Algebra 'R (Map.Map a b) where - - algebra = heyting $ \a b -> - let - x = Map.merge - Map.dropMissing -- drop if an element is missing in @b@ - (Map.mapMissing (\_ _ -> true)) -- put @true@ if an element is missing in @a@ - (Map.zipWithMatched (\_ -> (//) )) -- merge matching elements with @`implies`@ - a b - - y = Map.fromList [(k, true) | k <- U.universeF, not (Map.member k a), not (Map.member k b) ] - -- for elements which are not in a, nor in b add - -- a @true@ key - in - Map.union x y - --- TODO: compare performance -impliesMap a b = - Map.intersection (`implies`) a b - `Map.union` Map.map (const true) (Map.difference b a) - `Map.union` Map.fromList [(k, true) | k <- universeF, not (Map.member k a), not (Map.member k b)] - --} - -{- - --- A symmetric Heyting algebra --- --- λ> implies (False ... True) (False ... True) --- Interval True True --- λ> implies (False ... True) (singleton False) --- Interval False False --- λ> implies (singleton True) (False ... True) --- Interval False True --- --- λ> implies ([EQ,GT] ... [EQ,GT]) ([LT] ... [LT,EQ]) :: Interval (Set.Set Ordering) --- Interval (fromList [LT]) (fromList [LT,EQ]) --- --- TODO: may need /a/ to be boolean here. -implies :: Symmetric a => Interval a -> Interval a -> Interval a -implies i1 i2 = maybe iempty (uncurry (...)) $ liftA2 f (endpts i1) (endpts i2) where - f (x1,x2) (y1,y2) = (x1 // y1 /\ x2 // y2, x2 // y2) - - --TODO: would this work for interval orders? - f (x1,x2) (y1,y2) = (x1 // y1 /\ x2 // y2, x1 // y1 \/ x2 // y2) - -coimplies i1 i2 = not (not i1 `implies` not i2) - --- The symmetry --- neg x = top \\ not x --- non x = not x // bottom --- λ> not ([LT] ... [LT,GT]) :: Interval (Set.Set Ordering) --- Interval (fromList [EQ]) (fromList [EQ,GT]) --- -not :: Symmetric a => Interval a -> Interval a -not = maybe iempty (\(x1, x2) -> neg x2 ... neg x1) . endpts - --- λ> neg' (False ... True) --- Interval False False --- λ> (False ... True) `implies` (singleton False) --- Interval False False --- -neg' x = (bottom ... top) `coimplies` (not x) - --- λ> non' (False ... True) --- Interval False False --- λ> (singleton True) `coimplies` (False ... True) --- Interval False False --- -non' x = not x `implies` (singleton bottom) - --} - -- Internal ------------------------- @@ -798,18 +846,18 @@ meetMaybe (Just x) (Just y) = Just (x /\ y) joinExtended :: Join a => Extended a -> Extended a -> Extended a -joinExtended Top _ = Top -joinExtended _ Top = Top -joinExtended (Extended x) (Extended y) = Extended (x \/ y) -joinExtended Bottom y = y -joinExtended x Bottom = x +joinExtended PosInf _ = PosInf +joinExtended _ PosInf = PosInf +joinExtended (Finite x) (Finite y) = Finite (x \/ y) +joinExtended NegInf y = y +joinExtended x NegInf = x meetExtended :: Meet a => Extended a -> Extended a -> Extended a -meetExtended Top y = y -meetExtended x Top = x -meetExtended (Extended x) (Extended y) = Extended (x /\ y) -meetExtended Bottom _ = Bottom -meetExtended _ Bottom = Bottom +meetExtended PosInf y = y +meetExtended x PosInf = x +meetExtended (Finite x) (Finite y) = Finite (x /\ y) +meetExtended NegInf _ = NegInf +meetExtended _ NegInf = NegInf joinEither :: (Join a, Join b) => Either a b -> Either a b -> Either a b joinEither (Right x) (Right y) = Right (x \/ y) 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 @@ -1,15 +1,72 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE Safe #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} module Data.Lattice.Property where -import Data.Lattice -import Data.Order.Property -import Data.Order.Syntax -import Prelude hiding (Bounded, Eq (..), Ord (..), not) +import safe Data.Lattice +import safe Data.Order.Property +import safe Data.Order.Syntax +import safe Prelude hiding (Bounded, Eq (..), Ord (..), not) + +heyting0 :: Heyting a => a -> a -> a -> Bool +heyting0 x y z = x /\ y <= z <=> x <= y // z + +heyting1 :: Heyting a => a -> a -> a -> Bool +heyting1 x y z = x // y <= x // (y \/ z) + +heyting2 :: Heyting a => a -> a -> a -> Bool +heyting2 x y z = (x \/ z) // y <= x // y + +heyting3 :: Heyting a => a -> a -> a -> Bool +heyting3 x y z = x <= y ==> z // x <= z // y + +heyting4 :: Heyting a => a -> a -> a -> Bool +heyting4 x y z = (x /\ y) // z == x // y // z + +heyting5 :: Heyting a => a -> a -> a -> Bool +heyting5 x y z = x // (y /\ z) == x // y /\ x // z + +heyting6 :: Heyting a => a -> a -> Bool +heyting6 x y = y <= x // (x /\ y) + +heyting7 :: Heyting a => a -> a -> Bool +heyting7 x y = x /\ x // y == x /\ y + +heyting8 :: forall a. Heyting a => a -> Bool +heyting8 _ = neg bottom == top @a && neg top == bottom @a + +heyting9 :: Heyting a => a -> a -> Bool +heyting9 x y = neg x \/ y <= x // y + +heyting10 :: Heyting a => a -> a -> Bool +heyting10 x y = x <= y <=> x // y == top + +heyting11 :: Heyting a => a -> a -> Bool +heyting11 x y = neg (x \/ y) <= neg x + +heyting12 :: Heyting a => a -> a -> Bool +heyting12 x y = neg (x // y) == neg (neg x) /\ neg y + +heyting13 :: Heyting a => a -> a -> Bool +heyting13 x y = neg (x \/ y) == neg x /\ neg y + +heyting14 :: Heyting a => a -> Bool +heyting14 x = x /\ neg x == bottom + +heyting15 :: Heyting a => a -> Bool +heyting15 x = neg (neg (neg x)) == neg x + +heyting16 :: Heyting a => a -> Bool +heyting16 x = neg (neg (x \/ neg x)) == top + +-- Double negation is a monad. +heyting17 :: Heyting a => a -> Bool +heyting17 x = x <= neg (neg x) + coheyting0 :: Coheyting a => a -> a -> a -> Bool coheyting0 x y z = x \\ y <= z <=> x <= y \/ z @@ -37,7 +94,6 @@ coheyting8 :: forall a. Coheyting a => a -> Bool coheyting8 _ = non bottom == top @a && non top == bottom @a --- Double co-negation is a co-monad. coheyting9 :: Coheyting a => a -> a -> Bool coheyting9 x y = x /\ non y >= x \\ y @@ -62,73 +118,20 @@ coheyting16 :: Coheyting a => a -> Bool coheyting16 x = non (non (x /\ non x)) == bottom +-- Double co-negation is a co-monad. coheyting17 :: Coheyting a => a -> Bool coheyting17 x = x >= non (non x) coheyting18 :: Coheyting c => c -> Bool coheyting18 x = x == boundary x \/ (non . non) x +-- Leibniz rule coheyting19 :: Coheyting a => a -> a -> Bool -coheyting19 x y = boundary (x /\ y) == (boundary x /\ y) \/ (x /\ boundary y) -- (Leibniz rule) +coheyting19 x y = boundary (x /\ y) == (boundary x /\ y) \/ (x /\ boundary y) coheyting20 :: Coheyting a => a -> a -> Bool coheyting20 x y = boundary (x \/ y) \/ boundary (x /\ y) == boundary x \/ boundary y -heyting0 :: Heyting a => a -> a -> a -> Bool -heyting0 x y z = x /\ y <= z <=> x <= y // z - -heyting1 :: Heyting a => a -> a -> a -> Bool -heyting1 x y z = x // y <= x // (y \/ z) - -heyting2 :: Heyting a => a -> a -> a -> Bool -heyting2 x y z = (x \/ z) // y <= x // y - -heyting3 :: Heyting a => a -> a -> a -> Bool -heyting3 x y z = x <= y ==> z // x <= z // y - -heyting4 :: Heyting a => a -> a -> a -> Bool -heyting4 x y z = (x /\ y) // z == x // y // z - -heyting5 :: Heyting a => a -> a -> a -> Bool -heyting5 x y z = x // (y /\ z) == x // y /\ x // z - -heyting6 :: Heyting a => a -> a -> Bool -heyting6 x y = y <= x // (x /\ y) - -heyting7 :: Heyting a => a -> a -> Bool -heyting7 x y = x /\ x // y == x /\ y - -heyting8 :: forall a. Heyting a => a -> Bool -heyting8 _ = neg bottom == top @a && neg top == bottom @a - --- Double negation is a monad. -heyting9 :: Heyting a => a -> a -> Bool -heyting9 x y = neg x \/ y <= x // y - -heyting10 :: Heyting a => a -> a -> Bool -heyting10 x y = x <= y <=> x // y == top - -heyting11 :: Heyting a => a -> a -> Bool -heyting11 x y = neg (x \/ y) <= neg x - -heyting12 :: Heyting a => a -> a -> Bool -heyting12 x y = neg (x // y) == neg (neg x) /\ neg y - -heyting13 :: Heyting a => a -> a -> Bool -heyting13 x y = neg (x \/ y) == neg x /\ neg y - -heyting14 :: Heyting a => a -> Bool -heyting14 x = x /\ neg x == bottom - -heyting15 :: Heyting a => a -> Bool -heyting15 x = neg (neg (neg x)) == neg x - -heyting16 :: Heyting a => a -> Bool -heyting16 x = neg (neg (x \/ neg x)) == top - -heyting17 :: Heyting a => a -> Bool -heyting17 x = x <= neg (neg x) - -- -- x '\\' x = 'top' -- x '/\' (x '\\' y) = x '/\' y @@ -207,182 +210,3 @@ boolean6 :: Biheyting a => a -> a -> Bool boolean6 x y = x // y == non (non y \\ non x) -{- -infix 4 `joinLe` --- | The partial ordering induced by the join-semilattice structure. --- --- --- Normally when /a/ implements 'Ord' we should have: --- @ 'joinLe' x y = x '<=' y @ --- -joinLe :: Lattice a => a -> a -> Bool -joinLe x y = y == x \/ y - -infix 4 `joinGe` --- | The partial ordering induced by the join-semilattice structure. --- --- Normally when /a/ implements 'Ord' we should have: --- @ 'joinGe' x y = x '>=' y @ --- -joinGe :: Lattice a => a -> a -> Bool -joinGe x y = x == x \/ y - --- | Partial version of 'Data.Ord.compare'. --- --- Normally when /a/ implements 'Preorder' we should have: --- @ 'pcompareJoin' x y = 'pcompare' x y @ --- -pcompareJoin :: Lattice a => a -> a -> Maybe Ordering -pcompareJoin x y - | x == y = Just EQ - | joinLe x y && x /= y = Just LT - | joinGe x y && x /= y = Just GT - | otherwise = Nothing - -infix 4 `meetLe` --- | The partial ordering induced by the meet-semilattice structure. --- --- Normally when /a/ implements 'Preorder' we should have: --- @ 'meetLe' x y = x '<~' y @ --- -meetLe :: Lattice a => a -> a -> Bool -meetLe x y = x == x /\ y - -infix 4 `meetGe` --- | The partial ordering induced by the meet-semilattice structure. --- --- Normally when /a/ implements 'Preorder' we should have: --- @ 'meetGe' x y = x '>~' y @ --- -meetGe :: Lattice a => a -> a -> Bool -meetGe x y = y == x /\ y - --- | Partial version of 'Data.Ord.compare'. --- --- Normally when /a/ implements 'Preorder' we should have: --- @ 'pcompareJoin' x y = 'pcompare' x y @ --- -pcompareMeet :: Lattice a => a -> a -> Maybe Ordering -pcompareMeet x y - | x == y = Just EQ - | meetLe x y && x /= y = Just LT - | meetGe x y && x /= y = Just GT - | otherwise = Nothing - --- | \( \forall a \in R: a \/ a = a \) --- --- @ 'idempotent_join' = 'absorbative' 'top' @ --- --- See < https:\\en.wikipedia.org/wiki/Band_(mathematics) >. --- --- This is a required property. --- -idempotent_join :: Lattice r => r -> Bool -idempotent_join = idempotent_join_on (~~) - -idempotent_join_on :: Semilattice 'L r => Rel r b -> r -> b -idempotent_join_on (~~) r = (\/) r r ~~ r - --- | \( \forall a, b, c \in R: (a \/ b) \/ c = a \/ (b \/ c) \) --- --- This is a required property. --- -associative_join :: Lattice r => r -> r -> r -> Bool -associative_join = associative_on (~~) (\/) - -associative_join_on :: Semilattice 'L r => Rel r b -> r -> r -> r -> b -associative_join_on (=~) = associative_on (=~) (\/) - --- | \( \forall a, b, c: (a \# b) \# c \doteq a \# (b \# c) \) --- -associative_on :: Rel r b -> (r -> r -> r) -> (r -> r -> r -> b) -associative_on (~~) (#) a b c = ((a # b) # c) ~~ (a # (b # c)) - --- | \( \forall a, b \in R: a \/ b = b \/ a \) --- --- This is a required property. --- -commutative_join :: Lattice r => r -> r -> Bool -commutative_join = commutative_join_on (~~) - -commutative_join_on :: Semilattice 'L r => Rel r b -> r -> r -> b -commutative_join_on (=~) = commutative_on (=~) (\/) - --- | \( \forall a, b: a \# b \doteq b \# a \) --- -commutative_on :: Rel r b -> (r -> r -> r) -> r -> r -> b -commutative_on (=~) (#) a b = (a # b) =~ (b # a) - --- | \( \forall a, b \in R: a /\ b \/ b = b \) --- --- Absorbativity is a generalized form of idempotency: --- --- @ --- 'absorbative' 'top' a = a \/ a = a --- @ --- --- This is a required property. --- -absorbative_on :: Lattice r => Rel r Bool -> r -> r -> Bool -absorbative_on (=~) x y = (x /\ y \/ y) =~ y - --- | \( \forall a, b \in R: a \/ b /\ b = b \) --- --- Absorbativity is a generalized form of idempotency: --- --- @ --- 'absorbative'' 'bottom' a = a \/ a = a --- @ --- --- This is a required property. --- -absorbative_on' :: Lattice r => Rel r Bool -> r -> r -> Bool -absorbative_on' (=~) x y = ((x \/ y) /\ y) =~ y - -distributive :: Lattice r => r -> r -> r -> Bool -distributive = distributive_on (~~) (/\) (\/) - -codistributive :: Lattice r => r -> r -> r -> Bool -codistributive = distributive_on (~~) (\/) (/\) - -distributive_on :: Rel r b -> (r -> r -> r) -> (r -> r -> r) -> (r -> r -> r -> b) -distributive_on (=~) (#) (%) a b c = ((a # b) % c) =~ ((a % c) # (b % c)) - -distributive_on' :: Rel r b -> (r -> r -> r) -> (r -> r -> r) -> (r -> r -> r -> b) -distributive_on' (=~) (#) (%) a b c = (c % (a # b)) =~ ((c % a) # (c % b)) - --- | @ 'glb' x x y = x @ --- --- See < https:\\en.wikipedia.org/wiki/Median_algebra >. -majority_glb :: Lattice r => r -> r -> Bool -majority_glb x y = glb x y y ~~ y - --- | @ 'glb' x y z = 'glb' z x y @ --- -commutative_glb :: Lattice r => r -> r -> r -> Bool -commutative_glb x y z = glb x y z ~~ glb z x y - --- | @ 'glb' x y z = 'glb' x z y @ --- -commutative_glb' :: Lattice r => r -> r -> r -> Bool -commutative_glb' x y z = glb x y z ~~ glb x z y - --- | @ 'glb' ('glb' x w y) w z = 'glb' x w ('glb' y w z) @ --- -associative_glb :: Lattice r => r -> r -> r -> r -> Bool -associative_glb x y z w = glb (glb x w y) w z ~~ glb x w (glb y w z) - -distributive_glb :: (Bounded r, Lattice r) => r -> r -> r -> Bool -distributive_glb x y z = glb x y z ~~ lub x y z - -interval_glb :: Lattice r => r -> r -> r -> Bool -interval_glb x y z = glb x y z ~~ y ==> (x <~ y && y <~ z) || (z <~ y && y <~ x) - --- | \( \forall a, b, c: a \leq b \Rightarrow a \/ (c /\ b) \eq (a \/ c) /\ b \) --- --- See < https:\\en.wikipedia.org/wiki/Distributivity_(order_theory)#Distributivity_for_semilattices > --- -modular :: Lattice r => r -> r -> r -> Bool -modular a b c = a \/ (c /\ b) ~~ (a \/ c) /\ b - --} diff --git a/src/Data/Order.hs b/src/Data/Order.hs --- a/src/Data/Order.hs +++ b/src/Data/Order.hs @@ -11,6 +11,7 @@ {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} +{-# LANGUAGE ViewPatterns #-} module Data.Order ( -- * Constraint kinds @@ -28,7 +29,6 @@ -- * Re-exports Ordering (..), Down (..), - Positive, ) where import safe Control.Applicative @@ -36,6 +36,7 @@ import safe Data.Complex import safe Data.Either import safe qualified Data.Eq as Eq +import safe Data.ExtendedReal import safe Data.Fixed import safe Data.Functor.Identity import safe Data.Int @@ -48,6 +49,7 @@ import safe qualified Data.Ord as Ord import safe Data.Semigroup import safe qualified Data.Set as Set +import safe Data.Time.Clock.System import safe Data.Void import safe Data.Word import safe GHC.Real @@ -349,28 +351,30 @@ pcompareRat (x :% 0) _ = Just $ Ord.compare x 0 pcompareRat x y = Just $ Ord.compare x y --- | Positive rationals, extended with an absorbing zero. --- --- 'Positive' is the canonical < https://en.wikipedia.org/wiki/Semifield#Examples semifield >. -type Positive = Ratio Natural - --- N5 lattice comparison -pcomparePos :: Positive -> Positive -> Maybe Ordering -pcomparePos (0 :% 0) (x :% 0) = Just $ Ord.compare 0 x -pcomparePos (x :% 0) (0 :% 0) = Just $ Ord.compare x 0 -pcomparePos (_ :% 0) (_ :% 0) = Just EQ -- all non-nan infs are equal -pcomparePos (0 :% 0) (0 :% _) = Just $ GT -pcomparePos (0 :% _) (0 :% 0) = Just $ LT -pcomparePos (0 :% 0) _ = Nothing -pcomparePos _ (0 :% 0) = Nothing -pcomparePos (x :% y) (x' :% y') = Just $ Ord.compare (x * y') (x' * y) - instance Preorder Rational where pcompare = pcompareRat -instance Preorder Positive where - pcompare = pcomparePos +--deriving via (Base SystemTime) instance Preorder SystemTime +instance Preorder SystemTime where + pcompare = fmap Just . compareSys +compareSys :: SystemTime -> SystemTime -> Ordering +compareSys (norm -> MkSystemTime xs xn) (norm -> MkSystemTime ys yn) + | EQ == os = Ord.compare xn yn + | otherwise = os + where + os = Ord.compare xs ys + +s2ns :: Num a => a +s2ns = 10 ^ 9 + +norm :: SystemTime -> SystemTime +norm (MkSystemTime xs xn) + | xn Ord.>= s2ns = MkSystemTime (xs + q) (fromIntegral r) + | otherwise = MkSystemTime xs xn + where + (q, r) = fromIntegral xn `divMod` s2ns + instance (Preorder a, Num a) => Preorder (Complex a) where pcompare = pcomparing $ \(x :+ y) -> x * x + y * y @@ -418,6 +422,13 @@ instance Preorder a => Preorder (NonEmpty a) where (x :| xs) <~ (y :| ys) = x <~ y && xs <~ ys + +instance Preorder a => Preorder (Extended a) where + _ <~ PosInf = True + PosInf <~ _ = False + NegInf <~ _ = True + _ <~ NegInf = False + Finite x <~ Finite y = x <~ y instance (Preorder a, Preorder b) => Preorder (Either a b) where Right a <~ Right b = a <~ b diff --git a/src/Data/Order/Extended.hs b/src/Data/Order/Extended.hs deleted file mode 100644 --- a/src/Data/Order/Extended.hs +++ /dev/null @@ -1,106 +0,0 @@ -{-# LANGUAGE DeriveFunctor #-} -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE Safe #-} - -module Data.Order.Extended ( - -- * Lattice extensions - Lifted, - Lowered, - Extended (..), - extended, - --, retract - - -- * Lattice Extensions - liftMaybe, - liftEitherL, - liftEitherR, - liftExtended, -) where - -import safe Data.Order -import safe Data.Order.Syntax -import safe GHC.Generics -import safe Prelude hiding (Bounded, Eq (..), Ord (..)) - -type Lifted = Either () - -type Lowered a = Either a () - --- | Add a bottom and top to a lattice. --- --- The top is the absorbing element for the join, and the bottom is the absorbing --- element for the meet. -data Extended a = Bottom | Extended a | Top - deriving (Eq, Ord, Show, Generic, Functor, Generic1) - --- | Eliminate an 'Extended'. -extended :: b -> b -> (a -> b) -> Extended a -> b -extended b _ _ Bottom = b -extended _ t _ Top = t -extended _ _ f (Extended x) = f x - -------------------------------------------------------------------------------- --- Lattice extensions -------------------------------------------------------------------------------- - -{- -lifts :: Minimal a => Eq a => (a -> b) -> a -> Lifted b -lifts = liftEitherL (== minimal) - -lifted :: Minimal b => (a -> b) -> Lifted a -> b -lifted f = either (const minimal) f - -lowered :: Maximal b => (a -> b) -> Lowered a -> b -lowered f = either f (const maximal) - -lowers :: Maximal a => Eq a => (a -> b) -> a -> Lowered b -lowers = liftEitherR (== maximal) --} - -liftMaybe :: (a -> Bool) -> (a -> b) -> a -> Maybe b -liftMaybe p f = g - where - g i - | p i = Nothing - | otherwise = Just $ f i - -liftEitherL :: (a -> Bool) -> (a -> b) -> a -> Lifted b -liftEitherL p f = g - where - g i - | p i = Left () - | otherwise = Right $ f i - -liftEitherR :: (a -> Bool) -> (a -> b) -> a -> Lowered b -liftEitherR p f = g - where - g i - | p i = Right () - | otherwise = Left $ f i - -liftExtended :: (a -> Bool) -> (a -> Bool) -> (a -> b) -> a -> Extended b -liftExtended p q f = g - where - g i - | p i = Bottom - | q i = Top - | otherwise = Extended $ f i - ---------------------------------------------------------------------- --- Instances ---------------------------------------------------------------------- - -instance Preorder a => Preorder (Extended a) where - _ <~ Top = True - Top <~ _ = False - Bottom <~ _ = True - _ <~ Bottom = False - Extended x <~ Extended y = x <~ y - -{- -instance Universe a => Universe (Extended a) where - universe = Top : Bottom : map Extended universe -instance Finite a => Finite (Extended a) where - universeF = Top : Bottom : map Extended universeF - cardinality = fmap (2 +) (retag (cardinality :: Tagged a Natural)) --} diff --git a/src/Data/Order/Property.hs b/src/Data/Order/Property.hs --- a/src/Data/Order/Property.hs +++ b/src/Data/Order/Property.hs @@ -1,4 +1,5 @@ {-# LANGUAGE DataKinds #-} +{-# LANGUAGE Safe #-} -- | See . module Data.Order.Property ( @@ -50,10 +51,10 @@ antisymmetric, ) where -import Data.Lattice hiding (not) -import Data.Order -import Data.Order.Syntax -import Prelude hiding (Eq (..), Ord (..)) +import safe Data.Lattice hiding (not) +import safe Data.Order +import safe Data.Order.Syntax +import safe Prelude hiding (Eq (..), Ord (..)) -- | See . -- diff --git a/src/Data/Order/Syntax.hs b/src/Data/Order/Syntax.hs --- a/src/Data/Order/Syntax.hs +++ b/src/Data/Order/Syntax.hs @@ -31,7 +31,7 @@ import safe qualified Data.Ord as Ord import safe Data.Order -import Prelude hiding (Eq (..), Ord (..)) +import safe Prelude hiding (Eq (..), Ord (..)) infix 4 <, > diff --git a/test/Test/Data/Connection.hs b/test/Test/Data/Connection.hs --- a/test/Test/Data/Connection.hs +++ b/test/Test/Data/Connection.hs @@ -1,42 +1,36 @@ -{-# LANGUAGE TemplateHaskell #-} -{-# LANGUAGE RankNTypes #-} {-# LANGUAGE DataKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TemplateHaskell #-} + module Test.Data.Connection where import Control.Applicative hiding (empty) import Data.Connection -import Data.Connection.Conn +import Data.Connection.Property as Prop import Data.Connection.Ratio -import Data.Foldable -import Data.Lattice -import Data.Int -import Data.Word import Data.Fixed import Data.Order -import Data.Order.Extended import Data.Order.Interval -import GHC.Real hiding (Fractional(..), (^^), (^), div) +import Data.Order.Property +import Data.Order.Syntax +import GHC.Real hiding (Fractional (..), div, (^), (^^)) import Hedgehog -import Numeric.Natural -import Prelude hiding (Eq(..),Ord(..)) import qualified Hedgehog.Gen as G import qualified Hedgehog.Range as R -import Data.Connection.Property as Prop -import Data.Lattice.Property -import Data.Order.Property -import Data.Order.Syntax +import Numeric.Natural +import Prelude hiding (Eq (..), Ord (..)) ri :: (Integral a, Bounded a) => Range a ri = R.linearFrom 0 minBound maxBound ri' :: Range Integer -ri' = R.linearFrom 0 (- 2^127) (2^127) +ri' = R.linearFrom 0 (- 2 ^ 127) (2 ^ 127) ri'' :: Range Integer ri'' = R.exponentialFrom 0 (-340282366920938463463374607431768211456) 340282366920938463463374607431768211456 rn :: Range Natural -rn = R.linear 0 (2^128) +rn = R.linear 0 (2 ^ 128) rf :: Range Float rf = R.exponentialFloatFrom 0 (-3.4028235e38) 3.4028235e38 @@ -53,35 +47,35 @@ f64 :: Gen Double f64 = gen_flt $ G.double rd +fxx :: Gen (Fixed k) +fxx = MkFixed <$> G.integral ri' + rat :: Gen (Ratio Integer) -rat = G.realFrac_ $ R.linearFracFrom 0 (- 2^(127 :: Integer)) (2^(127 :: Integer)) +rat = G.realFrac_ $ R.linearFracFrom 0 (- 2 ^ (127 :: Integer)) (2 ^ (127 :: Integer)) rat' :: Gen (Ratio Integer) rat' = G.frequency [(49, rat), (1, G.element [-1 :% 0, 1 :% 0, 0 :% 0])] -pos :: Gen (Ratio Natural) -pos = G.frequency [(49, gen), (1, G.element [1 :% 0, 0 :% 0])] - where gen = G.realFrac_ (R.linearFracFrom 0 0 (2^127)) - -- potentially ineffiecient gen_ivl :: Preorder a => Gen a -> Gen a -> Gen (Interval a) -gen_ivl g1 g2 = liftA2 (...) g1 g2 +gen_ivl g1 g2 = liftA2 (...) g1 g2 gen_maybe :: Gen a -> Gen (Maybe a) gen_maybe gen = G.frequency [(9, Just <$> gen), (1, pure Nothing)] -gen_lifted :: Gen a -> Gen (Lifted a) +gen_lifted :: Gen a -> Gen (Either () a) gen_lifted gen = G.frequency [(9, Right <$> gen), (1, pure $ Left ())] -gen_lowered :: Gen a -> Gen (Lowered a) +gen_lowered :: Gen a -> Gen (Either a ()) gen_lowered gen = G.frequency [(9, Left <$> gen), (1, pure $ Right ())] gen_extended :: Gen a -> Gen (Extended a) -gen_extended gen = G.frequency [(18, Extended <$> gen), (1, pure Bottom), (1, pure Top)] +gen_extended gen = G.frequency [(18, Finite <$> gen), (1, pure NegInf), (1, pure PosInf)] -gen_flt :: Floating a => Gen a -> Gen a -gen_flt gen = G.frequency [(49, gen), (1, G.element [(-1/0), 1/0, 0/0])] +gen_flt :: Floating a => Gen a -> Gen a +gen_flt gen = G.frequency [(49, gen), (1, G.element [(-1 / 0), 1 / 0, 0 / 0])] +{- prop_connection_extremal :: Property prop_connection_extremal = withTests 1000 . property $ do x <- forAll f32 @@ -90,7 +84,28 @@ o' <- forAll ord r <- forAll rat' r' <- forAll rat' + b <- forAll G.bool + b' <- forAll G.bool + {- + assert $ Prop.adjoint extremal o b + assert $ Prop.closed extremal o + assert $ Prop.kernel (extremal @Ordering) b + assert $ Prop.monotonic extremal o o' b b' + assert $ Prop.idempotent extremal o b + + assert $ Prop.adjoint extremal x b + assert $ Prop.closed extremal x + assert $ Prop.kernel (extremal @Float) b + assert $ Prop.monotonic extremal x x' b b' + assert $ Prop.idempotent extremal x b + + assert $ Prop.adjoint extremal r b + assert $ Prop.closed extremal r + assert $ Prop.kernel (extremal @Rational) b + assert $ Prop.monotonic extremal r r' b b' + assert $ Prop.idempotent extremal r b + assert $ Prop.adjoint (conn @_ @() @Ordering) () o assert $ Prop.closed (conn @_ @() @Ordering) () assert $ Prop.kernel (conn @_ @() @Ordering) o @@ -102,6 +117,7 @@ assert $ Prop.kernel (conn @_ @() @Float) x assert $ Prop.monotonic (conn @_ @() @Float) () () x x' assert $ Prop.idempotent (conn @_ @() @Float) () x + -} assert $ Prop.adjoint (conn @_ @() @Rational) () r assert $ Prop.closed (conn @_ @() @Rational) () @@ -111,3 +127,4 @@ tests :: IO Bool tests = checkParallel $$(discover) +-} 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 @@ -1,15 +1,54 @@ {-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE ScopedTypeVariables #-} module Test.Data.Connection.Fixed where import Data.Connection.Fixed import qualified Data.Connection.Property as Prop +import Data.Fixed import Hedgehog import qualified Hedgehog.Gen as G import Test.Data.Connection -fxx :: Gen (Fixed k) -fxx = MkFixed <$> G.integral ri' +prop_connection_ratf06 :: Property +prop_connection_ratf06 = withTests 1000 . property $ do + x <- forAll rat + x' <- forAll rat + y <- forAll $ gen_extended fxx + y' <- forAll $ gen_extended fxx + + assert $ Prop.adjoint (ratfix @E6) x y + assert $ Prop.closed (ratfix @E6) x + assert $ Prop.kernel (ratfix @E6) y + assert $ Prop.monotonic (ratfix @E6) x x' y y' + assert $ Prop.idempotent (ratfix @E6) x y + +prop_connection_ratf09 :: Property +prop_connection_ratf09 = withTests 1000 . property $ do + x <- forAll rat + x' <- forAll rat + y <- forAll $ gen_extended fxx + y' <- forAll $ gen_extended fxx + + assert $ Prop.adjoint (ratfix @E9) x y + assert $ Prop.closed (ratfix @E9) x + assert $ Prop.kernel (ratfix @E9) y + assert $ Prop.monotonic (ratfix @E9) x x' y y' + assert $ Prop.idempotent (ratfix @E9) x y + +prop_connection_ratf12 :: Property +prop_connection_ratf12 = withTests 1000 . property $ do + x <- forAll rat + x' <- forAll rat + y <- forAll $ gen_extended fxx + y' <- forAll $ gen_extended fxx + + assert $ Prop.adjoint (ratfix @E12) x y + assert $ Prop.closed (ratfix @E12) x + assert $ Prop.kernel (ratfix @E12) y + assert $ Prop.monotonic (ratfix @E12) x x' y y' + assert $ Prop.idempotent (ratfix @E12) x y prop_connections_micro :: Property prop_connections_micro = withTests 1000 . property $ do 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 @@ -4,17 +4,40 @@ module Test.Data.Connection.Float where -import Data.Connection.Conn import Data.Connection.Float -import Data.Fixed -import Data.Int -import Data.Order - import qualified Data.Connection.Property as Prop +import Data.Int +import Data.Word import Hedgehog import qualified Hedgehog.Gen as G import Test.Data.Connection +prop_connection_f32w08 :: Property +prop_connection_f32w08 = withTests 1000 . property $ do + x <- forAll f32 + x' <- forAll f32 + y <- forAll $ gen_extended $ G.integral (ri @Word8) + y' <- forAll $ gen_extended $ G.integral (ri @Word8) + + assert $ Prop.adjoint f32w08 x y + assert $ Prop.closed f32w08 x + assert $ Prop.kernel f32w08 y + assert $ Prop.monotonic f32w08 x x' y y' + assert $ Prop.idempotent f32w08 x y + +prop_connection_f32w16 :: Property +prop_connection_f32w16 = withTests 1000 . property $ do + x <- forAll f32 + x' <- forAll f32 + y <- forAll $ gen_extended $ G.integral (ri @Word16) + y' <- forAll $ gen_extended $ G.integral (ri @Word16) + + assert $ Prop.adjoint f32w16 x y + assert $ Prop.closed f32w16 x + assert $ Prop.kernel f32w16 y + assert $ Prop.monotonic f32w16 x x' y y' + assert $ Prop.idempotent f32w16 x y + prop_connection_f32i08 :: Property prop_connection_f32i08 = withTests 1000 . property $ do x <- forAll f32 @@ -41,57 +64,44 @@ 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) +prop_connection_f64w08 :: Property +prop_connection_f64w08 = withTests 1000 . property $ do + x <- forAll f64 + x' <- forAll f64 + y <- forAll $ gen_extended $ G.integral (ri @Word8) + y' <- forAll $ gen_extended $ G.integral (ri @Word8) - 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 + assert $ Prop.adjoint f64w08 x y + assert $ Prop.closed f64w08 x + assert $ Prop.kernel f64w08 y + assert $ Prop.monotonic f64w08 x x' y y' + assert $ Prop.idempotent f64w08 x y -prop_connection_f32ixx :: Property -prop_connection_f32ixx = withTests 1000 . property $ do - x <- forAll f32 - x' <- forAll f32 - y <- forAll $ gen_extended $ G.integral (ri @Int) - y' <- forAll $ gen_extended $ G.integral (ri @Int) +prop_connection_f64w16 :: Property +prop_connection_f64w16 = withTests 1000 . property $ do + x <- forAll f64 + x' <- forAll f64 + y <- forAll $ gen_extended $ G.integral (ri @Word16) + y' <- forAll $ gen_extended $ G.integral (ri @Word16) - assert $ Prop.adjointL f32ixx x y - assert $ Prop.closedL f32ixx x - assert $ Prop.kernelL f32ixx y - assert $ Prop.monotonicL f32ixx x x' y y' - assert $ Prop.idempotentL f32ixx x y + assert $ Prop.adjoint f64w16 x y + assert $ Prop.closed f64w16 x + assert $ Prop.kernel f64w16 y + assert $ Prop.monotonic f64w16 x x' y y' + assert $ Prop.idempotent f64w16 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' +prop_connection_f64w32 :: Property +prop_connection_f64w32 = withTests 1000 . property $ do + x <- forAll f64 + x' <- forAll f64 + y <- forAll $ gen_extended $ G.integral (ri @Word32) + y' <- forAll $ gen_extended $ G.integral (ri @Word32) - 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 + assert $ Prop.adjoint f64w32 x y + assert $ Prop.closed f64w32 x + assert $ Prop.kernel f64w32 y + assert $ Prop.monotonic f64w32 x x' y y' + assert $ Prop.idempotent f64w32 x y prop_connection_f64i08 :: Property prop_connection_f64i08 = withTests 1000 . property $ do @@ -131,45 +141,6 @@ assert $ Prop.kernel f64i32 y assert $ Prop.monotonic f64i32 x x' y y' assert $ Prop.idempotent f64i32 x y - -prop_connection_f64i64 :: Property -prop_connection_f64i64 = withTests 1000 . property $ do - x <- forAll f64 - x' <- forAll f64 - y <- forAll $ gen_extended $ G.integral (ri @Int64) - y' <- forAll $ gen_extended $ G.integral (ri @Int64) - - 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_f64ixx :: Property -prop_connection_f64ixx = withTests 1000 . property $ do - x <- forAll f64 - x' <- forAll f64 - y <- forAll $ gen_extended $ G.integral (ri @Int) - y' <- forAll $ gen_extended $ G.integral (ri @Int) - - assert $ Prop.adjointL f64ixx x y - assert $ Prop.closedL f64ixx x - assert $ Prop.kernelL f64ixx y - assert $ Prop.monotonicL f64ixx x x' y y' - assert $ Prop.idempotentL f64ixx 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_f64f32 :: Property prop_connection_f64f32 = withTests 1000 . property $ do 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 @@ -1,89 +1,96 @@ {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeApplications #-} +{-# LANGUAGE ScopedTypeVariables #-} module Test.Data.Connection.Ratio where import qualified Data.Connection.Property as Prop import Data.Connection.Ratio -import Data.Fixed import Data.Int -import Data.Order.Extended import Data.Word -import GHC.Real hiding (Fractional (..), div, (^), (^^)) import Hedgehog import qualified Hedgehog.Gen as G -import qualified Hedgehog.Range as R -import Numeric.Natural import Test.Data.Connection -fxx :: Gen (Extended (Fixed k)) -fxx = gen_extended $ MkFixed <$> G.integral ri' -prop_connection_ratf06 :: Property -prop_connection_ratf06 = withTests 1000 . property $ do - x <- forAll rat - x' <- forAll rat - y <- forAll fxx - y' <- forAll fxx +prop_connection_ratw08 :: Property +prop_connection_ratw08 = withTests 1000 . property $ do + x <- forAll rat' + x' <- forAll rat' + y <- forAll $ gen_extended $ G.integral (ri @Word8) + y' <- forAll $ gen_extended $ G.integral (ri @Word8) - assert $ Prop.adjoint (ratfix @E6) x y - assert $ Prop.closed (ratfix @E6) x - assert $ Prop.kernel (ratfix @E6) y - assert $ Prop.monotonic (ratfix @E6) x x' y y' - assert $ Prop.idempotent (ratfix @E6) x y + assert $ Prop.adjoint (ratw08) x y + assert $ Prop.closed (ratw08) x + assert $ Prop.kernel (ratw08) y + assert $ Prop.monotonic (ratw08) x x' y y' + assert $ Prop.idempotent (ratw08) x y -prop_connection_ratf09 :: Property -prop_connection_ratf09 = withTests 1000 . property $ do - x <- forAll rat - x' <- forAll rat - y <- forAll fxx - y' <- forAll fxx +prop_connection_ratw16 :: Property +prop_connection_ratw16 = withTests 1000 . property $ do + x <- forAll rat' + x' <- forAll rat' + y <- forAll $ gen_extended $ G.integral (ri @Word16) + y' <- forAll $ gen_extended $ G.integral (ri @Word16) - assert $ Prop.adjoint (ratfix @E9) x y - assert $ Prop.closed (ratfix @E9) x - assert $ Prop.kernel (ratfix @E9) y - assert $ Prop.monotonic (ratfix @E9) x x' y y' - assert $ Prop.idempotent (ratfix @E9) x y + assert $ Prop.adjoint (ratw16) x y + assert $ Prop.closed (ratw16) x + assert $ Prop.kernel (ratw16) y + assert $ Prop.monotonic (ratw16) x x' y y' + assert $ Prop.idempotent (ratw16) x y -prop_connection_ratf12 :: Property -prop_connection_ratf12 = withTests 1000 . property $ do - x <- forAll rat - x' <- forAll rat - y <- forAll fxx - y' <- forAll fxx +prop_connection_ratw32 :: Property +prop_connection_ratw32 = withTests 1000 . property $ do + x <- forAll rat' + x' <- forAll rat' + y <- forAll $ gen_extended $ G.integral (ri @Word32) + y' <- forAll $ gen_extended $ G.integral (ri @Word32) - assert $ Prop.adjoint (ratfix @E12) x y - assert $ Prop.closed (ratfix @E12) x - assert $ Prop.kernel (ratfix @E12) y - assert $ Prop.monotonic (ratfix @E12) x x' y y' - assert $ Prop.idempotent (ratfix @E12) x y + assert $ Prop.adjoint (ratw32) x y + assert $ Prop.closed (ratw32) x + assert $ Prop.kernel (ratw32) y + assert $ Prop.monotonic (ratw32) x x' y y' + assert $ Prop.idempotent (ratw32) x y -prop_connection_ratf32 :: Property -prop_connection_ratf32 = withTests 1000 . property $ do +prop_connection_ratw64 :: Property +prop_connection_ratw64 = withTests 1000 . property $ do x <- forAll rat' x' <- forAll rat' - y <- forAll f32 - y' <- forAll f32 + y <- forAll $ gen_extended $ G.integral (ri @Word64) + y' <- forAll $ gen_extended $ G.integral (ri @Word64) - 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 + assert $ Prop.adjoint (ratw64) x y + assert $ Prop.closed (ratw64) x + assert $ Prop.kernel (ratw64) y + assert $ Prop.monotonic (ratw64) x x' y y' + assert $ Prop.idempotent (ratw64) x y -prop_connection_ratf64 :: Property -prop_connection_ratf64 = withTests 1000 . property $ do +prop_connection_ratwxx :: Property +prop_connection_ratwxx = withTests 1000 . property $ do x <- forAll rat' x' <- forAll rat' - y <- forAll f64 - y' <- forAll f64 + y <- forAll $ gen_extended $ G.integral (ri @Word) + y' <- forAll $ gen_extended $ G.integral (ri @Word) - 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 + assert $ Prop.adjoint (ratwxx) x y + assert $ Prop.closed (ratwxx) x + assert $ Prop.kernel (ratwxx) y + assert $ Prop.monotonic (ratwxx) x x' y y' + assert $ Prop.idempotent (ratwxx) x y +prop_connection_ratnat :: Property +prop_connection_ratnat = withTests 1000 . property $ do + x <- forAll rat + x' <- forAll rat + y <- forAll $ gen_extended $ G.integral rn + y' <- forAll $ gen_extended $ G.integral rn + + assert $ Prop.adjoint ratnat x y + assert $ Prop.closed ratnat x + assert $ Prop.kernel ratnat y + assert $ Prop.monotonic ratnat x x' y y' + assert $ Prop.idempotent ratnat x y + prop_connection_rati08 :: Property prop_connection_rati08 = withTests 1000 . property $ do x <- forAll rat' @@ -149,70 +156,31 @@ assert $ Prop.monotonic (ratint) x x' y y' assert $ Prop.idempotent (ratint) x y -prop_connection_posw08 :: Property -prop_connection_posw08 = withTests 1000 . property $ do - x <- forAll pos - x' <- forAll pos - y <- forAll $ gen_lowered $ G.integral (ri @Word8) - y' <- forAll $ gen_lowered $ G.integral (ri @Word8) - - assert $ Prop.adjoint (posw08) x y - assert $ Prop.closed (posw08) x - assert $ Prop.kernel (posw08) y - assert $ Prop.monotonic (posw08) x x' y y' - assert $ Prop.idempotent (posw08) x y - -prop_connection_posw16 :: Property -prop_connection_posw16 = withTests 1000 . property $ do - x <- forAll pos - x' <- forAll pos - y <- forAll $ gen_lowered $ G.integral (ri @Word16) - y' <- forAll $ gen_lowered $ G.integral (ri @Word16) - - assert $ Prop.adjoint (posw16) x y - assert $ Prop.closed (posw16) x - assert $ Prop.kernel (posw16) y - assert $ Prop.monotonic (posw16) x x' y y' - assert $ Prop.idempotent (posw16) x y - -prop_connection_posw32 :: Property -prop_connection_posw32 = withTests 1000 . property $ do - x <- forAll pos - x' <- forAll pos - y <- forAll $ gen_lowered $ G.integral (ri @Word32) - y' <- forAll $ gen_lowered $ G.integral (ri @Word32) - - assert $ Prop.adjoint (posw32) x y - assert $ Prop.closed (posw32) x - assert $ Prop.kernel (posw32) y - assert $ Prop.monotonic (posw32) x x' y y' - assert $ Prop.idempotent (posw32) x y - -prop_connection_posw64 :: Property -prop_connection_posw64 = withTests 1000 . property $ do - x <- forAll pos - x' <- forAll pos - y <- forAll $ gen_lowered $ G.integral (ri @Word64) - y' <- forAll $ gen_lowered $ G.integral (ri @Word64) +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 (posw64) x y - assert $ Prop.closed (posw64) x - assert $ Prop.kernel (posw64) y - assert $ Prop.monotonic (posw64) x x' y y' - assert $ Prop.idempotent (posw64) x y + 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_posnat :: Property -prop_connection_posnat = withTests 1000 . property $ do - x <- forAll pos - x' <- forAll pos - y <- forAll $ gen_lowered $ G.integral rn - y' <- forAll $ gen_lowered $ G.integral rn +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 (posnat) x y - assert $ Prop.closed (posnat) x - assert $ Prop.kernel (posnat) y - assert $ Prop.monotonic (posnat) x x' y y' - assert $ Prop.idempotent (posnat) x y + 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/Time.hs b/test/Test/Data/Connection/Time.hs new file mode 100644 --- /dev/null +++ b/test/Test/Data/Connection/Time.hs @@ -0,0 +1,81 @@ +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} + +module Test.Data.Connection.Time where + +import qualified Data.Connection.Property as Prop +import Data.Connection.Time +import Hedgehog +import qualified Hedgehog.Gen as G +import Test.Data.Connection + +sys :: Gen SystemTime +sys = MkSystemTime <$> G.int64 ri <*> G.word32 ri + +prop_connection_sysixx :: Property +prop_connection_sysixx = withTests 1000 . property $ do + x <- forAll sys + x' <- forAll sys + y <- forAll $ G.int ri + y' <- forAll $ G.int ri + + assert $ Prop.adjoint sysixx x y + assert $ Prop.closed sysixx x + assert $ Prop.kernel sysixx y + assert $ Prop.monotonic sysixx x x' y y' + assert $ Prop.idempotent sysixx x y + +prop_connection_f32sys :: Property +prop_connection_f32sys = withTests 1000 . property $ do + x <- forAll f32 + x' <- forAll f32 + y <- forAll $ gen_extended sys + y' <- forAll $ gen_extended sys + + assert $ Prop.adjointL f32sys x y + assert $ Prop.closedL f32sys x + assert $ Prop.kernelL f32sys y + assert $ Prop.monotonicL f32sys x x' y y' + assert $ Prop.idempotentL f32sys x y + +prop_connection_f64sys :: Property +prop_connection_f64sys = withTests 1000 . property $ do + x <- forAll f64 + x' <- forAll f64 + y <- forAll $ gen_extended sys + y' <- forAll $ gen_extended sys + + assert $ Prop.adjointL f64sys x y + assert $ Prop.closedL f64sys x + assert $ Prop.kernelL f64sys y + assert $ Prop.monotonicL f64sys x x' y y' + assert $ Prop.idempotentL f64sys x y + +prop_connection_ratsys :: Property +prop_connection_ratsys = withTests 1000 . property $ do + x <- forAll rat' + x' <- forAll rat' + y <- forAll $ gen_extended sys + y' <- forAll $ gen_extended sys + + assert $ Prop.adjoint ratsys x y + assert $ Prop.closed ratsys x + assert $ Prop.kernel ratsys y + assert $ Prop.monotonic ratsys x x' y y' + assert $ Prop.idempotent ratsys x y + +prop_connection_f09sys :: Property +prop_connection_f09sys = withTests 1000 . property $ do + x <- forAll $ gen_extended fxx + x' <- forAll $ gen_extended fxx + y <- forAll $ gen_extended sys + y' <- forAll $ gen_extended sys + + assert $ Prop.adjoint f09sys x y + assert $ Prop.closed f09sys x + assert $ Prop.kernel f09sys y + assert $ Prop.monotonic f09sys x x' y y' + assert $ Prop.idempotent f09sys x y + +tests :: IO Bool +tests = checkParallel $$(discover) diff --git a/test/Test/Data/Order.hs b/test/Test/Data/Order.hs --- a/test/Test/Data/Order.hs +++ b/test/Test/Data/Order.hs @@ -267,25 +267,6 @@ assert $ Prop.transitive_eq x y z assert $ Prop.chain_22 x y z w -prop_order_pos :: Property -prop_order_pos = withTests 1000 . property $ do - x <- forAll pos - y <- forAll pos - z <- forAll pos - w <- forAll pos - assert $ Prop.preorder x y - assert $ Prop.order z w - assert $ Prop.reflexive_eq x - assert $ Prop.reflexive_le x - assert $ Prop.irreflexive_lt x - assert $ Prop.symmetric_eq x y - assert $ Prop.asymmetric_lt x y - assert $ Prop.antisymmetric_le x y - assert $ Prop.transitive_lt x y z - assert $ Prop.transitive_le x y z - assert $ Prop.transitive_eq x y z - assert $ Prop.chain_22 x y z w - prop_order_f32 :: Property prop_order_f32 = withTests 1000 . property $ do x <- forAll f32 diff --git a/test/test.hs b/test/test.hs --- a/test/test.hs +++ b/test/test.hs @@ -2,11 +2,11 @@ import System.Exit (exitFailure) import System.IO (BufferMode (..), hSetBuffering, stderr, stdout) -import qualified Test.Data.Connection as C import qualified Test.Data.Connection.Fixed as CX import qualified Test.Data.Connection.Float as CF import qualified Test.Data.Connection.Int as CI import qualified Test.Data.Connection.Ratio as CR +import qualified Test.Data.Connection.Time as CT import qualified Test.Data.Connection.Word as CW import qualified Test.Data.Lattice as L import qualified Test.Data.Order as P @@ -16,12 +16,12 @@ sequence [ P.tests , L.tests - , C.tests , CI.tests , CW.tests , CF.tests , CX.tests , CR.tests + , CT.tests ] main :: IO ()