{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE Safe #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ViewPatterns #-}

module Data.Connection.Conn (
    -- * Conn
    Kan (..),
    Conn (),
    pattern Conn,
    embed,
    range,
    identity,

    -- * Connection k
    ConnK,
    half,
    midpoint,
    roundWith,
    roundWith1,
    roundWith2,
    truncateWith,
    truncateWith1,
    truncateWith2,

    -- * Connection L
    ConnL,
    pattern ConnL,
    upL,
    downL,
    swapL,
    counit,
    upper,
    upper1,
    upper2,
    filterWith,
    ceilingWith,
    ceilingWith1,
    ceilingWith2,

    -- * Connection R
    ConnR,
    pattern ConnR,
    upR,
    downR,
    swapR,
    unit,
    lower,
    lower1,
    lower2,
    idealWith,
    floorWith,
    floorWith1,
    floorWith2,

    -- * Combinators
    (>>>),
    (<<<),
    choice,
    strong,
) 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.Order
import safe Prelude hiding (Ord (..))

-- $setup
-- >>> :set -XTypeApplications
-- >>> import Data.Int
-- >>> import Data.Ord (Down(..))
-- >>> 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:
--
-- * /L/-tagged types are low / increasing (e.g. 'Data.Connection.Class.minimal', 'Data.Connection.Class.upper', 'Data.Connection.Class.ceiling', 'Data.Connection.Class.join')
--
-- * /R/-tagged types are high / decreasing (e.g. 'Data.Connection.Class.maximal', 'Data.Connection.Class.lower', 'Data.Connection.Class.floor', 'Data.Connection.Class.meet')
data Kan = L | R

-- | An < https://ncatlab.org/nlab/show/adjoint+string adjoint string > 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
-- (0.125,0.125)
-- >>> range (conn @_ @Rational @Float) (1 :% 7) -- sevenths are not
-- (0.14285713,0.14285715)
data Conn (k :: Kan) a b = Galois (a -> (b, b)) (b -> a)

instance Category (Conn k) where
    id :: Conn k a a
id = Conn k a a
forall (k :: Kan) a. Conn k a a
identity
    {-# INLINE id #-}

    Galois b -> (c, c)
f1 c -> b
g1 . :: Conn k b c -> Conn k a b -> Conn k a c
. Galois a -> (b, b)
f2 b -> a
g2 = (a -> (c, c)) -> (c -> a) -> Conn k a c
forall (k :: Kan) a b. (a -> (b, b)) -> (b -> a) -> Conn k a b
Galois (((c, c) -> c
forall a b. (a, b) -> a
fst ((c, c) -> c) -> (b -> (c, c)) -> b -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> (c, c)
f1) (b -> c) -> (a -> b) -> a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((b, b) -> b
forall a b. (a, b) -> a
fst ((b, b) -> b) -> (a -> (b, b)) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> (b, b)
f2) (a -> c) -> (a -> c) -> a -> (c, c)
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& ((c, c) -> c
forall a b. (a, b) -> b
snd ((c, c) -> c) -> (b -> (c, c)) -> b -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> (c, c)
f1) (b -> c) -> (a -> b) -> a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((b, b) -> b
forall a b. (a, b) -> b
snd ((b, b) -> b) -> (a -> (b, b)) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> (b, b)
f2)) (b -> a
g2 (b -> a) -> (c -> b) -> c -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. c -> b
g1)
    {-# INLINE (.) #-}

-- | Obtain a /Conn/ from an adjoint triple of monotone functions.
--
--  This is a view pattern for an arbitrary 'Conn'. When applied to a 'ConnL'
--  or 'ConnR', the two functions of type @a -> b@ returned will be identical.
--
--  /Caution/: /Conn f g h/ must obey \(f \dashv g \dashv h\). This condition is not checked.
--
--  For detailed properties see 'Data.Connection.Property'.
pattern Conn :: (a -> b) -> (b -> a) -> (a -> b) -> Conn k a b
pattern $bConn :: (a -> b) -> (b -> a) -> (a -> b) -> Conn k a b
$mConn :: forall r a b (k :: Kan).
Conn k a b
-> ((a -> b) -> (b -> a) -> (a -> b) -> r) -> (Void# -> r) -> r
Conn f g h <- (embed &&& _1 &&& _2 -> (g, (h, f))) where Conn a -> b
f b -> a
g a -> b
h = (a -> (b, b)) -> (b -> a) -> Conn k a b
forall (k :: Kan) a b. (a -> (b, b)) -> (b -> a) -> Conn k a b
Galois (a -> b
h (a -> b) -> (a -> b) -> a -> (b, b)
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& a -> b
f) b -> a
g

{-# COMPLETE Conn #-}

-- Internal floor function. When \(f \dashv g \dashv h \) this is h.
_1 :: Conn k a b -> a -> b
_1 :: Conn k a b -> a -> b
_1 (Galois a -> (b, b)
f b -> a
_) = (b, b) -> b
forall a b. (a, b) -> a
fst ((b, b) -> b) -> (a -> (b, b)) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> (b, b)
f
{-# INLINE _1 #-}

-- Internal ceiling function. When \(f \dashv g \dashv h \) this is f.
_2 :: Conn k a b -> a -> b
_2 :: Conn k a b -> a -> b
_2 (Galois a -> (b, b)
f b -> a
_) = (b, b) -> b
forall a b. (a, b) -> b
snd ((b, b) -> b) -> (a -> (b, b)) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> (b, b)
f
{-# INLINE _2 #-}

-- | The identity 'Conn'.
identity :: Conn k a a
identity :: Conn k a a
identity = (a -> (a, a)) -> (a -> a) -> Conn k a a
forall (k :: Kan) a b. (a -> (b, b)) -> (b -> a) -> Conn k a b
Galois (a -> a
forall a. a -> a
id (a -> a) -> (a -> a) -> a -> (a, a)
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& a -> a
forall a. a -> a
id) a -> a
forall a. a -> a
id
{-# INLINE identity #-}

-- | Obtain the center of a 'ConnK', upper adjoint of a 'ConnL', or lower adjoint of a 'ConnR'.
embed :: Conn k a b -> b -> a
embed :: Conn k a b -> b -> a
embed (Galois a -> (b, b)
_ b -> a
g) = b -> a
g
{-# INLINE embed #-}

-- | Obtain the upper and/or lower adjoints of a connection.
--
-- > range c = floorWith c &&& ceilingWith c
--
-- >>> range f64f32 pi
-- (3.1415925,3.1415927)
-- >>> range f64f32 (0/0)
-- (NaN,NaN)
range :: Conn k a b -> a -> (b, b)
range :: Conn k a b -> a -> (b, b)
range (Galois a -> (b, b)
f b -> a
_) = a -> (b, b)
f
{-# INLINE range #-}

---------------------------------------------------------------------
-- ConnK
---------------------------------------------------------------------

-- | An <https://ncatlab.org/nlab/show/adjoint+triple adjoint triple> of Galois connections.
--
-- An adjoint triple is a chain of connections of length 3:
--
-- \(f \dashv g \dashv h \)
--
-- For detailed properties see 'Data.Connection.Property'.
type ConnK a b = forall k. Conn k a b

-- | Determine which half of the interval between 2 representations of /a/ a particular value lies.
--
-- @ 'half' t x = 'pcompare' (x - 'lower' t x) ('upper' t x - x) @
--
-- >>> maybe False (== EQ) $ half f64f32 (midpoint f64f32 pi)
-- True
half :: (Num a, Preorder a) => ConnK a b -> a -> Maybe Ordering
half :: ConnK a b -> a -> Maybe Ordering
half ConnK a b
c a
x = a -> a -> Maybe Ordering
forall a. Preorder a => a -> a -> Maybe Ordering
pcompare (a
x a -> a -> a
forall a. Num a => a -> a -> a
- ConnR a b -> a -> a
forall a b. ConnR a b -> a -> a
lower ConnR a b
ConnK a b
c a
x) (ConnL a b -> a -> a
forall a b. ConnL a b -> a -> a
upper ConnL a b
ConnK a b
c a
x a -> a -> a
forall a. Num a => a -> a -> a
- a
x)
{-# INLINE half #-}

-- | Return the midpoint of the interval containing x.
--
-- >>> pi - midpoint f64f32 pi
-- 3.1786509424591713e-8
midpoint :: Fractional a => ConnK a b -> a -> a
midpoint :: ConnK a b -> a -> a
midpoint ConnK a b
c a
x = ConnR a b -> a -> a
forall a b. ConnR a b -> a -> a
lower ConnR a b
ConnK a b
c a
x a -> a -> a
forall a. Fractional a => a -> a -> a
/ a
2 a -> a -> a
forall a. Num a => a -> a -> a
+ ConnL a b -> a -> a
forall a b. ConnL a b -> a -> a
upper ConnL a b
ConnK a b
c a
x a -> a -> a
forall a. Fractional a => a -> a -> a
/ a
2
{-# INLINE midpoint #-}

-- | Return the nearest value to x.
--
-- > roundWith 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).
--
-- See <https://en.wikipedia.org/wiki/Rounding>.
roundWith :: forall a b. (Num a, Preorder a) => ConnK a b -> a -> b
roundWith :: ConnK a b -> a -> b
roundWith ConnK a b
c a
x = case ConnK a b -> a -> Maybe Ordering
forall a b. (Num a, Preorder a) => ConnK a b -> a -> Maybe Ordering
half ConnK a b
c a
x of
    Just Ordering
GT -> ConnL a b -> a -> b
forall a b. ConnL a b -> a -> b
ceilingWith ConnL a b
ConnK a b
c a
x
    Just Ordering
LT -> ConnR a b -> a -> b
forall a b. ConnR a b -> a -> b
floorWith ConnR a b
ConnK a b
c a
x
    Maybe Ordering
_ -> ConnK a b -> a -> b
forall a b. (Num a, Preorder a) => ConnK a b -> a -> b
truncateWith ConnK a b
c a
x
{-# INLINE roundWith #-}

-- | Lift a unary function over a 'ConnK'.
--
-- Results are rounded to the nearest value with ties away from 0.
roundWith1 :: (Num a, Preorder a) => ConnK a b -> (a -> a) -> b -> b
roundWith1 :: ConnK a b -> (a -> a) -> b -> b
roundWith1 ConnK a b
c a -> a
f b
x = ConnK a b -> a -> b
forall a b. (Num a, Preorder a) => ConnK a b -> a -> b
roundWith ConnK a b
c (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ a -> a
f (b -> a
g b
x) where Conn a -> b
_ b -> a
g a -> b
_ = Conn Any a b
ConnK a b
c
{-# INLINE roundWith1 #-}

-- | Lift a binary function over a 'ConnK'.
--
-- 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
-- >>> roundWith2 ratf32 f maxOdd32 2.0
-- 2.0
roundWith2 :: (Num a, Preorder a) => ConnK a b -> (a -> a -> a) -> b -> b -> b
roundWith2 :: ConnK a b -> (a -> a -> a) -> b -> b -> b
roundWith2 ConnK a b
c a -> a -> a
f b
x b
y = ConnK a b -> a -> b
forall a b. (Num a, Preorder a) => ConnK a b -> a -> b
roundWith ConnK a b
c (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ a -> a -> a
f (b -> a
g b
x) (b -> a
g b
y) where Conn a -> b
_ b -> a
g a -> b
_ = Conn Any a b
ConnK a b
c
{-# INLINE roundWith2 #-}

-- | Truncate towards zero.
--
-- > truncateWith identity = id
truncateWith :: (Num a, Preorder a) => ConnK a b -> a -> b
truncateWith :: ConnK a b -> a -> b
truncateWith ConnK a b
c a
x = if a
x a -> a -> Bool
forall a. Preorder a => a -> a -> Bool
>~ a
0 then ConnR a b -> a -> b
forall a b. ConnR a b -> a -> b
floorWith ConnR a b
ConnK a b
c a
x else ConnL a b -> a -> b
forall a b. ConnL a b -> a -> b
ceilingWith ConnL a b
ConnK a b
c a
x
{-# INLINE truncateWith #-}

-- | Lift a unary function over a 'ConnK'.
--
-- Results are truncated towards zero.
--
-- > truncateWith1 identity = id
truncateWith1 :: (Num a, Preorder a) => ConnK a b -> (a -> a) -> b -> b
truncateWith1 :: ConnK a b -> (a -> a) -> b -> b
truncateWith1 ConnK a b
c a -> a
f b
x = ConnK a b -> a -> b
forall a b. (Num a, Preorder a) => ConnK a b -> a -> b
truncateWith ConnK a b
c (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ a -> a
f (b -> a
g b
x) where Conn a -> b
_ b -> a
g a -> b
_ = Conn Any a b
ConnK a b
c
{-# INLINE truncateWith1 #-}

truncateWith2 :: (Num a, Preorder a) => ConnK a b -> (a -> a -> a) -> b -> b -> b
truncateWith2 :: ConnK a b -> (a -> a -> a) -> b -> b -> b
truncateWith2 ConnK a b
c a -> a -> a
f b
x b
y = ConnK a b -> a -> b
forall a b. (Num a, Preorder a) => ConnK a b -> a -> b
truncateWith ConnK a b
c (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ a -> a -> a
f (b -> a
g b
x) (b -> a
g b
y) where Conn a -> b
_ b -> a
g a -> b
_ = Conn Any a b
ConnK a b
c
{-# INLINE truncateWith2 #-}

---------------------------------------------------------------------
-- ConnL
---------------------------------------------------------------------

-- | A <https://ncatlab.org/nlab/show/Galois+connection Galois connection> between two monotone functions.
--
-- A Galois connection between /f/ and /g/, written \(f \dashv g \)
-- is an adjunction in the category of preorders.
--
-- Each side of the connection may be defined in terms of the other:
--
--  \( g(x) = \sup \{y \in E \mid f(y) \leq x \} \)
--
--  \( f(x) = \inf \{y \in E \mid g(y) \geq x \} \)
--
-- For further information see 'Data.Connection.Property'.
--
-- /Caution/: Monotonicity is not checked.
type ConnL = Conn 'L

-- | A view pattern for a 'ConnL'.
--
-- /Caution/: /ConnL f g/ must obey \(f \dashv g \). This condition is not checked.
pattern ConnL :: (a -> b) -> (b -> a) -> ConnL a b
pattern $bConnL :: (a -> b) -> (b -> a) -> ConnL a b
$mConnL :: forall r a b.
ConnL a b -> ((a -> b) -> (b -> a) -> r) -> (Void# -> r) -> r
ConnL f g <- (_2 &&& embed -> (f, g)) where ConnL a -> b
f b -> a
g = (a -> (b, b)) -> (b -> a) -> ConnL a b
forall (k :: Kan) a b. (a -> (b, b)) -> (b -> a) -> Conn k a b
Galois (a -> b
f (a -> b) -> (a -> b) -> a -> (b, b)
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& a -> b
f) b -> a
g

{-# COMPLETE ConnL #-}

-- | Convert an inverted 'ConnL' to a 'ConnL'.
--
-- > upL . downL = downL . upL = id
upL :: ConnL (Down a) (Down b) -> ConnL b a
upL :: ConnL (Down a) (Down b) -> ConnL b a
upL (ConnL Down a -> Down b
f Down b -> Down a
g) = (b -> a) -> (a -> b) -> ConnL b a
forall a b. (a -> b) -> (b -> a) -> ConnL a b
ConnL b -> a
g' a -> b
f'
  where
    f' :: a -> b
f' a
x = let (Down b
y) = Down a -> Down b
f (a -> Down a
forall a. a -> Down a
Down a
x) in b
y
    g' :: b -> a
g' b
x = let (Down a
y) = Down b -> Down a
g (b -> Down b
forall a. a -> Down a
Down b
x) in a
y
{-# INLINE upL #-}

-- | Convert a 'ConnL' to an inverted 'ConnL'.
--
-- >>> upper (downL $ conn @_ @() @Ordering) (Down LT)
-- Down LT
-- >>> upper (downL $ conn @_ @() @Ordering) (Down GT)
-- Down LT
downL :: ConnL a b -> ConnL (Down b) (Down a)
downL :: ConnL a b -> ConnL (Down b) (Down a)
downL (ConnL a -> b
f b -> a
g) = (Down b -> Down a) -> (Down a -> Down b) -> ConnL (Down b) (Down a)
forall a b. (a -> b) -> (b -> a) -> ConnL a b
ConnL (\(Down b
x) -> a -> Down a
forall a. a -> Down a
Down (a -> Down a) -> a -> Down a
forall a b. (a -> b) -> a -> b
$ b -> a
g b
x) (\(Down a
x) -> b -> Down b
forall a. a -> Down a
Down (b -> Down b) -> b -> Down b
forall a b. (a -> b) -> a -> b
$ a -> b
f a
x)
{-# INLINE downL #-}

-- | Witness to the symmetry between 'ConnL' and 'ConnR'.
--
-- > swapL . swapR = id
-- > swapR . swapL = id
swapL :: ConnR a b -> ConnL b a
swapL :: ConnR a b -> ConnL b a
swapL (ConnR b -> a
f a -> b
g) = (b -> a) -> (a -> b) -> ConnL b a
forall a b. (a -> b) -> (b -> a) -> ConnL a b
ConnL b -> a
f a -> b
g
{-# INLINE swapL #-}

-- | Reverse round trip through a 'ConnK' or 'ConnL'.
--
-- This is the counit of the resulting comonad:
--
-- > x >~ counit c x
--
-- >>> counit (conn @_ @() @Ordering) LT
-- LT
-- >>> counit (conn @_ @() @Ordering) GT
-- LT
counit :: ConnL a b -> b -> b
counit :: ConnL a b -> b -> b
counit ConnL a b
c = ConnL a b -> (a -> a) -> b -> b
forall a b. ConnL a b -> (a -> a) -> b -> b
ceilingWith1 ConnL a b
c a -> a
forall a. a -> a
id
{-# INLINE counit #-}

-- | Round trip through a 'ConnK' or 'ConnL'.
--
-- > upper c = upper1 c id = embed c . ceilingWith c
-- > x <= upper c x
--
-- >>> compare pi $ upper f64f32 pi
-- LT
upper :: ConnL a b -> a -> a
upper :: ConnL a b -> a -> a
upper ConnL a b
c = ConnL a b -> (b -> b) -> a -> a
forall a b. ConnL a b -> (b -> b) -> a -> a
upper1 ConnL a b
c b -> b
forall a. a -> a
id
{-# INLINE upper #-}

-- | Map over a 'ConnK' or 'ConnL' from the right.
upper1 :: ConnL a b -> (b -> b) -> a -> a
upper1 :: ConnL a b -> (b -> b) -> a -> a
upper1 (ConnL a -> b
f b -> a
g) b -> b
h a
a = b -> a
g (b -> a) -> b -> a
forall a b. (a -> b) -> a -> b
$ b -> b
h (a -> b
f a
a)
{-# INLINE upper1 #-}

-- | Zip over a 'ConnK' or 'ConnL' from the right.
upper2 :: ConnL a b -> (b -> b -> b) -> a -> a -> a
upper2 :: ConnL a b -> (b -> b -> b) -> a -> a -> a
upper2 (ConnL a -> b
f b -> a
g) b -> b -> b
h a
a1 a
a2 = b -> a
g (b -> a) -> b -> a
forall a b. (a -> b) -> a -> b
$ b -> b -> b
h (a -> b
f a
a1) (a -> b
f a
a2)
{-# INLINE upper2 #-}

-- | Obtain the principal filter in /B/ generated by an element of /A/.
--
-- A subset /B/ of a lattice is an filter if and only if it is an upper set
-- that is closed under finite meets, i.e., it is nonempty and for all
-- /x/, /y/ in /B/, the element @x `meet` y@ is also in /b/.
--
-- /filterWith/ and /idealWith/ commute with /Down/:
--
-- > filterWith c a b <=> idealWith c (Down a) (Down b)
--
-- > filterWith c (Down a) (Down b) <=> idealWith c a b
--
-- /filterWith c a/ is upward-closed for all /a/:
--
-- > a <= b1 && b1 <= b2 => a <= b2
--
-- > a1 <= b && inf a2 <= b => ceiling a1 `meet` ceiling a2 <= b
--
-- See <https://en.wikipedia.org/wiki/Filter_(mathematics)>
filterWith :: Preorder b => ConnL a b -> a -> b -> Bool
filterWith :: ConnL a b -> a -> b -> Bool
filterWith ConnL a b
c a
a b
b = ConnL a b -> a -> b
forall a b. ConnL a b -> a -> b
ceilingWith ConnL a b
c a
a b -> b -> Bool
forall a. Preorder a => a -> a -> Bool
<~ b
b
{-# INLINE filterWith #-}

-- | Extract the left half of a 'ConnK' or 'ConnL'.
--
-- >>> floorWith f64f32 pi
-- 3.1415925
-- >>> ceilingWith f64f32 pi
-- 3.1415927
ceilingWith :: ConnL a b -> a -> b
ceilingWith :: ConnL a b -> a -> b
ceilingWith (ConnL a -> b
f b -> a
_) = a -> b
f
{-# INLINE ceilingWith #-}

-- | Map over a 'ConnK' or 'ConnL' from the left.
ceilingWith1 :: ConnL a b -> (a -> a) -> b -> b
ceilingWith1 :: ConnL a b -> (a -> a) -> b -> b
ceilingWith1 (ConnL a -> b
f b -> a
g) a -> a
h b
b = a -> b
f (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ a -> a
h (b -> a
g b
b)
{-# INLINE ceilingWith1 #-}

-- | Zip over a 'ConnK' or 'ConnL' from the left.
ceilingWith2 :: ConnL a b -> (a -> a -> a) -> b -> b -> b
ceilingWith2 :: ConnL a b -> (a -> a -> a) -> b -> b -> b
ceilingWith2 (ConnL a -> b
f b -> a
g) a -> a -> a
h b
b1 b
b2 = a -> b
f (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ a -> a -> a
h (b -> a
g b
b1) (b -> a
g b
b2)
{-# INLINE ceilingWith2 #-}

---------------------------------------------------------------------
-- ConnR
---------------------------------------------------------------------

-- | A Galois connection between two monotone functions.
--
-- 'ConnR' is the mirror image of 'ConnL':
--
-- > swapR :: ConnL a b -> ConnR b a
--
-- If you only require one connection there is no particular reason to
-- use one version over the other.
--
-- However some use cases (e.g. rounding) require an adjoint triple
-- of connections (i.e. a 'ConnK') that can lower into a standard
-- connection in either of two ways.
type ConnR = Conn 'R

-- | A view pattern for a 'ConnR'.
--
-- /Caution/: /ConnR f g/ must obey \(f \dashv g \). This condition is not checked.
pattern ConnR :: (b -> a) -> (a -> b) -> ConnR a b
pattern $bConnR :: (b -> a) -> (a -> b) -> ConnR a b
$mConnR :: forall r b a.
ConnR a b -> ((b -> a) -> (a -> b) -> r) -> (Void# -> r) -> r
ConnR f g <- (embed &&& _1 -> (f, g)) where ConnR b -> a
f a -> b
g = (a -> (b, b)) -> (b -> a) -> ConnR a b
forall (k :: Kan) a b. (a -> (b, b)) -> (b -> a) -> Conn k a b
Galois (a -> b
g (a -> b) -> (a -> b) -> a -> (b, b)
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& a -> b
g) b -> a
f

{-# COMPLETE ConnR #-}

-- | Convert an inverted 'ConnR' to a 'ConnR'.
--
-- > upR . downR = downR . upR = id
upR :: ConnR (Down a) (Down b) -> ConnR b a
upR :: ConnR (Down a) (Down b) -> ConnR b a
upR (ConnR Down b -> Down a
f Down a -> Down b
g) = (a -> b) -> (b -> a) -> ConnR b a
forall b a. (b -> a) -> (a -> b) -> ConnR a b
ConnR a -> b
g' b -> a
f'
  where
    f' :: b -> a
f' b
x = let (Down a
y) = Down b -> Down a
f (b -> Down b
forall a. a -> Down a
Down b
x) in a
y
    g' :: a -> b
g' a
x = let (Down b
y) = Down a -> Down b
g (a -> Down a
forall a. a -> Down a
Down a
x) in b
y
{-# INLINE upR #-}

-- | Convert a 'ConnR' to an inverted 'ConnR'.
--
-- >>> lower (downR $ conn @_ @() @Ordering) (Down LT)
-- Down GT
-- >>> lower (downR $ conn @_ @() @Ordering) (Down GT)
-- Down GT
downR :: ConnR a b -> ConnR (Down b) (Down a)
downR :: ConnR a b -> ConnR (Down b) (Down a)
downR (ConnR b -> a
f a -> b
g) = (Down a -> Down b) -> (Down b -> Down a) -> ConnR (Down b) (Down a)
forall b a. (b -> a) -> (a -> b) -> ConnR a b
ConnR (\(Down a
x) -> b -> Down b
forall a. a -> Down a
Down (b -> Down b) -> b -> Down b
forall a b. (a -> b) -> a -> b
$ a -> b
g a
x) (\(Down b
x) -> a -> Down a
forall a. a -> Down a
Down (a -> Down a) -> a -> Down a
forall a b. (a -> b) -> a -> b
$ b -> a
f b
x)
{-# INLINE downR #-}

-- | Witness to the symmetry between 'ConnL' and 'ConnR'.
--
-- > swapL . swapR = id
-- > swapR . swapL = id
swapR :: ConnL a b -> ConnR b a
swapR :: ConnL a b -> ConnR b a
swapR (ConnL a -> b
f b -> a
g) = (a -> b) -> (b -> a) -> ConnR b a
forall b a. (b -> a) -> (a -> b) -> ConnR a b
ConnR a -> b
f b -> a
g
{-# INLINE swapR #-}

-- | Round trip through a 'ConnK' or 'ConnR'.
--
-- This is the unit of the resulting monad:
--
-- > x <~ unit c x
-- > unit c = floorWith1 c id = floorWith c . embed c
--
-- >>> unit (conn @_ @() @Ordering) LT
-- GT
-- >>> unit (conn @_ @() @Ordering) GT
-- GT
unit :: ConnR a b -> b -> b
unit :: ConnR a b -> b -> b
unit ConnR a b
c = ConnR a b -> (a -> a) -> b -> b
forall a b. ConnR a b -> (a -> a) -> b -> b
floorWith1 ConnR a b
c a -> a
forall a. a -> a
id
{-# INLINE unit #-}

-- | Reverse round trip through a 'ConnK' or 'ConnR'.
--
-- > x >~ lower c x
--
-- >>> compare pi $ lower f64f32 pi
-- GT
lower :: ConnR a b -> a -> a
lower :: ConnR a b -> a -> a
lower ConnR a b
c = ConnR a b -> (b -> b) -> a -> a
forall a b. ConnR a b -> (b -> b) -> a -> a
lower1 ConnR a b
c b -> b
forall a. a -> a
id
{-# INLINE lower #-}

-- | Map over a 'ConnK' or 'ConnR' from the left.
lower1 :: ConnR a b -> (b -> b) -> a -> a
lower1 :: ConnR a b -> (b -> b) -> a -> a
lower1 (ConnR b -> a
f a -> b
g) b -> b
h a
a = b -> a
f (b -> a) -> b -> a
forall a b. (a -> b) -> a -> b
$ b -> b
h (a -> b
g a
a)
{-# INLINE lower1 #-}

-- | Zip over a 'ConnK' or 'ConnR' from the left.
lower2 :: ConnR a b -> (b -> b -> b) -> a -> a -> a
lower2 :: ConnR a b -> (b -> b -> b) -> a -> a -> a
lower2 (ConnR b -> a
f a -> b
g) b -> b -> b
h a
a1 a
a2 = b -> a
f (b -> a) -> b -> a
forall a b. (a -> b) -> a -> b
$ b -> b -> b
h (a -> b
g a
a1) (a -> b
g a
a2)
{-# INLINE lower2 #-}

-- | Obtain the principal ideal in /B/ generated by an element of /A/.
--
-- A subset /B/ of a lattice is an ideal if and only if it is a lower set
-- that is closed under finite joins, i.e., it is nonempty and for all
-- /x/, /y/ in /B/, the element /x `join` y/ is also in /B/.
--
-- /idealWith c a/ is downward-closed for all /a/:
--
-- > a >= b1 && b1 >= b2 => a >= b2
--
-- > a1 >= b && a2 >= b => floor a1 `join` floor a2 >= b
--
-- See <https://en.wikipedia.org/wiki/Ideal_(order_theory)>
idealWith :: Preorder b => ConnR a b -> a -> b -> Bool
idealWith :: ConnR a b -> a -> b -> Bool
idealWith ConnR a b
c a
a b
b = b
b b -> b -> Bool
forall a. Preorder a => a -> a -> Bool
<~ ConnR a b -> a -> b
forall a b. ConnR a b -> a -> b
floorWith ConnR a b
c a
a
{-# INLINE idealWith #-}

-- | Extract the right half of a 'ConnK' or 'ConnR'
--
-- This is the adjoint functor theorem for preorders.
--
-- >>> floorWith f64f32 pi
-- 3.1415925
-- >>> ceilingWith f64f32 pi
-- 3.1415927
floorWith :: ConnR a b -> a -> b
floorWith :: ConnR a b -> a -> b
floorWith (ConnR b -> a
_ a -> b
g) = a -> b
g
{-# INLINE floorWith #-}

-- | Map over a 'ConnK' or 'ConnR' from the right.
floorWith1 :: ConnR a b -> (a -> a) -> b -> b
floorWith1 :: ConnR a b -> (a -> a) -> b -> b
floorWith1 (ConnR b -> a
f a -> b
g) a -> a
h b
b = a -> b
g (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ a -> a
h (b -> a
f b
b)
{-# INLINE floorWith1 #-}

-- | Zip over a 'ConnK' or 'ConnR' from the right.
floorWith2 :: ConnR a b -> (a -> a -> a) -> b -> b -> b
floorWith2 :: ConnR a b -> (a -> a -> a) -> b -> b -> b
floorWith2 (ConnR b -> a
f a -> b
g) a -> a -> a
h b
b1 b
b2 = a -> b
g (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ a -> a -> a
h (b -> a
f b
b1) (b -> a
f b
b2)
{-# INLINE floorWith2 #-}

---------------------------------------------------------------------
-- Combinators
---------------------------------------------------------------------

-- | Lift two 'Conn's into a 'Conn' on the <https://en.wikibooks.org/wiki/Category_Theory/Categories_of_ordered_sets coproduct order>
--
-- > (choice id) (ab >>> cd) = (choice id) ab >>> (choice id) cd
-- > (flip choice id) (ab >>> cd) = (flip choice id) ab >>> (flip choice id) cd
choice :: Conn k a b -> Conn k c d -> Conn k (Either a c) (Either b d)
choice :: Conn k a b -> Conn k c d -> Conn k (Either a c) (Either b d)
choice (Conn a -> b
ab b -> a
ba a -> b
ab') (Conn c -> d
cd d -> c
dc c -> d
cd') = (Either a c -> Either b d)
-> (Either b d -> Either a c)
-> (Either a c -> Either b d)
-> Conn k (Either a c) (Either b d)
forall a b (k :: Kan).
(a -> b) -> (b -> a) -> (a -> b) -> Conn k a b
Conn Either a c -> Either b d
f Either b d -> Either a c
g Either a c -> Either b d
h
  where
    f :: Either a c -> Either b d
f = (a -> Either b d) -> (c -> Either b d) -> Either a c -> Either b d
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (b -> Either b d
forall a b. a -> Either a b
Left (b -> Either b d) -> (a -> b) -> a -> Either b d
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
ab) (d -> Either b d
forall a b. b -> Either a b
Right (d -> Either b d) -> (c -> d) -> c -> Either b d
forall b c a. (b -> c) -> (a -> b) -> a -> c
. c -> d
cd)
    g :: Either b d -> Either a c
g = (b -> Either a c) -> (d -> Either a c) -> Either b d -> Either a c
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (a -> Either a c
forall a b. a -> Either a b
Left (a -> Either a c) -> (b -> a) -> b -> Either a c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> a
ba) (c -> Either a c
forall a b. b -> Either a b
Right (c -> Either a c) -> (d -> c) -> d -> Either a c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. d -> c
dc)
    h :: Either a c -> Either b d
h = (a -> Either b d) -> (c -> Either b d) -> Either a c -> Either b d
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (b -> Either b d
forall a b. a -> Either a b
Left (b -> Either b d) -> (a -> b) -> a -> Either b d
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
ab') (d -> Either b d
forall a b. b -> Either a b
Right (d -> Either b d) -> (c -> d) -> c -> Either b d
forall b c a. (b -> c) -> (a -> b) -> a -> c
. c -> d
cd')
{-# INLINE choice #-}

-- | Lift two 'Conn's into a 'Conn' on the <https://en.wikibooks.org/wiki/Order_Theory/Preordered_classes_and_poclasses#product_order product order>
--
-- > (strong id) (ab >>> cd) = (strong id) ab >>> (strong id) cd
-- > (flip strong id) (ab >>> cd) = (flip strong id) ab >>> (flip strong id) cd
strong :: Conn k a b -> Conn k c d -> Conn k (a, c) (b, d)
strong :: Conn k a b -> Conn k c d -> Conn k (a, c) (b, d)
strong (Conn a -> b
ab b -> a
ba a -> b
ab') (Conn c -> d
cd d -> c
dc c -> d
cd') = ((a, c) -> (b, d))
-> ((b, d) -> (a, c)) -> ((a, c) -> (b, d)) -> Conn k (a, c) (b, d)
forall a b (k :: Kan).
(a -> b) -> (b -> a) -> (a -> b) -> Conn k a b
Conn (a, c) -> (b, d)
f (b, d) -> (a, c)
g (a, c) -> (b, d)
h
  where
    f :: (a, c) -> (b, d)
f = (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap a -> b
ab c -> d
cd
    g :: (b, d) -> (a, c)
g = (b -> a) -> (d -> c) -> (b, d) -> (a, c)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap b -> a
ba d -> c
dc
    h :: (a, c) -> (b, d)
h = (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap a -> b
ab' c -> d
cd'
{-# INLINE strong #-}