{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE Safe #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ViewPatterns #-}

module Data.Connection.Class (
    -- * Conn
    Conn (),
    identity,

    -- * Connection k
    Triple,
    pattern Conn,
    ConnK,
    embed,
    extremal,
    lub,
    glb,
    half,
    midpoint,
    range,
    round,
    round1,
    round2,
    truncate,
    truncate1,
    truncate2,

    -- * Connection L
    Left,
    pattern ConnL,
    ConnL,
    connL,
    embedL,
    minimal,
    join,
    ceiling,
    ceiling1,
    ceiling2,

    -- * Connection R
    Right,
    pattern ConnR,
    ConnR,
    connR,
    embedR,
    maximal,
    meet,
    floor,
    floor1,
    floor2,

    -- * Combinators
    (>>>),
    (<<<),
    (/|\),
    (\|/),
    choice,
    strong,

    -- * Connection
    Kan (..),
    ConnInteger,
    ConnRational,
    ConnExtended,
    Connection (..),
) where

import safe Control.Category ((>>>))
import safe Data.Bool (bool)
import safe Data.Connection.Conn
import safe Data.Connection.Float
import safe Data.Connection.Int
import safe Data.Connection.Ratio
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)

-- $setup
-- >>> :set -XTypeApplications
-- >>> :set -XFlexibleContexts
-- >>> import GHC.Real (Ratio(..))
-- >>> import Data.Set (Set,fromList)
-- >>> :load Data.Connection
-- >>> import Prelude hiding (round, floor, ceiling, truncate)

type Left = Connection 'L

type Right = Connection 'R

-- | A constraint kind representing an <https://ncatlab.org/nlab/show/adjoint+triple adjoint triple> of Galois connections.
type Triple a b = (Left a b, Right a b)

-- | A constraint kind for 'Integer' conversions.
--
--  Usable in conjunction with /RebindableSyntax/:
--
--  > fromInteger = embedL . Just :: ConnInteger a => Integer -> a
type ConnInteger a = Left a (Maybe Integer)

-- | A constraint kind for 'Rational' conversions.
--
-- Usable in conjunction with /RebindableSyntax/:
--
--  > fromRational = round :: ConnRational a => Rational -> a
type ConnRational a = Triple Rational a

type ConnExtended a b = Triple a (Extended b)

-- | 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

infixr 3 \|/

-- | A preorder variant of 'Control.Arrow.|||'.
(\|/) :: Conn k c a -> Conn k c b -> Conn k c (Either a b)
Conn k c a
f \|/ :: Conn k c a -> Conn k c b -> Conn k c (Either a b)
\|/ Conn k c b
g = (c -> Either c c)
-> (Either c c -> c) -> (c -> Either c c) -> Conn k c (Either c c)
forall a b (k :: Kan).
(a -> b) -> (b -> a) -> (a -> b) -> Conn k a b
Conn c -> Either c c
forall a b. a -> Either a b
Left ((c -> c) -> (c -> c) -> Either c c -> c
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either c -> c
forall a. a -> a
id c -> c
forall a. a -> a
id) c -> Either c c
forall a b. b -> Either a b
Right Conn k c (Either c c)
-> Conn k (Either c c) (Either a b) -> Conn k c (Either a b)
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> Conn k c a
f Conn k c a -> Conn k c b -> Conn k (Either c c) (Either a b)
forall (k :: Kan) a b c d.
Conn k a b -> Conn k c d -> Conn k (Either a c) (Either b d)
`choice` Conn k c b
g

infixr 4 /|\

-- | A preorder variant of 'Control.Arrow.&&&'.
(/|\) :: Connection k (c, c) c => Conn k a c -> Conn k b c -> Conn k (a, b) c
Conn k a c
f /|\ :: Conn k a c -> Conn k b c -> Conn k (a, b) c
/|\ Conn k b c
g = Conn k a c
f Conn k a c -> Conn k b c -> Conn k (a, b) (c, c)
forall (k :: Kan) a b c d.
Conn k a b -> Conn k c d -> Conn k (a, c) (b, d)
`strong` Conn k b c
g Conn k (a, b) (c, c) -> Conn k (c, c) c -> Conn k (a, b) c
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> Conn k (c, c) c
forall (k :: Kan) a b. Connection k a b => Conn k a b
conn

---------------------------------------------------------------------
-- Connection k
---------------------------------------------------------------------

-- | The canonical connections against a 'Bool'.
extremal :: Triple () a => Conn k a Bool
extremal :: Conn k a Bool
extremal = (a -> Bool) -> (Bool -> a) -> (a -> Bool) -> Conn k a Bool
forall a b (k :: Kan).
(a -> b) -> (b -> a) -> (a -> b) -> Conn k a b
Conn a -> Bool
forall a. Connection 'L () a => a -> Bool
f Bool -> a
forall p. (Connection 'L () p, Connection 'R () p) => Bool -> p
g a -> Bool
forall a. Connection 'R () a => a -> Bool
h
  where
    g :: Bool -> p
g Bool
False = p
forall a. Left () a => a
minimal
    g Bool
True = p
forall a. Right () a => a
maximal

    f :: a -> Bool
f a
i
        | a
i a -> a -> Bool
forall a. Preorder a => a -> a -> Bool
~~ a
forall a. Left () a => a
minimal = Bool
False
        | Bool
otherwise = Bool
True

    h :: a -> Bool
h a
i
        | a
i a -> a -> Bool
forall a. Preorder a => a -> a -> Bool
~~ a
forall a. Right () a => a
maximal = Bool
True
        | Bool
otherwise = Bool
False

-- | 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 :: a -> a -> a -> a
lub a
x a
y a
z = (a
x a -> a -> a
forall a. Right (a, a) a => a -> a -> a
`meet` a
y) a -> a -> a
forall a. Left (a, a) a => a -> a -> a
`join` (a
y a -> a -> a
forall a. Right (a, a) a => a -> a -> a
`meet` a
z) a -> a -> a
forall a. Left (a, a) a => a -> a -> a
`join` (a
z a -> a -> a
forall a. Right (a, a) a => a -> a -> a
`meet` a
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 :: a -> a -> a -> a
glb a
x a
y a
z = (a
x a -> a -> a
forall a. Left (a, a) a => a -> a -> a
`join` a
y) a -> a -> a
forall a. Right (a, a) a => a -> a -> a
`meet` (a
y a -> a -> a
forall a. Left (a, a) a => a -> a -> a
`join` a
z) a -> a -> a
forall a. Right (a, a) a => a -> a -> a
`meet` (a
z a -> a -> a
forall a. Left (a, a) a => a -> a -> a
`join` a
x)

-- | 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 <https://en.wikipedia.org/wiki/Rounding>.
round :: forall a b. (Num a, Triple a b) => a -> b
round :: a -> b
round a
x = case a -> a -> Maybe Ordering
forall a. Preorder a => a -> a -> Maybe Ordering
pcompare a
halfR a
halfL of
    Just Ordering
GT -> a -> b
forall a b. Left a b => a -> b
ceiling a
x
    Just Ordering
LT -> a -> b
forall a b. Right a b => a -> b
floor a
x
    Maybe Ordering
_ -> a -> b
forall a b. (Num a, Triple a b) => a -> b
truncate a
x
  where
    halfR :: a
halfR = 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 (Right a b => ConnR a b
forall a b. Right a b => ConnR a b
connR @a @b) a
x -- dist from lower bound
    halfL :: a
halfL = ConnL a b -> a -> a
forall a b. ConnL a b -> a -> a
upper (Left a b => ConnL a b
forall a b. Left a b => ConnL a b
connL @a @b) a
x a -> a -> a
forall a. Num a => a -> a -> a
- a
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 :: (a -> a) -> b -> b
round1 a -> a
f b
x = a -> b
forall a b. (Num a, Triple a b) => a -> b
round (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 'L a b
forall a b. Left a b => ConnL a b
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 :: (a -> a -> a) -> b -> b -> b
round2 a -> a -> a
f b
x b
y = a -> b
forall a b. (Num a, Triple a b) => a -> b
round (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 'L a b
forall a b. Left a b => ConnL a b
connL
{-# INLINE round2 #-}

-- | Truncate towards zero.
--
-- > truncate @a @a = id
truncate :: (Num a, Triple a b) => a -> b
truncate :: a -> b
truncate a
x = if a
x a -> a -> Bool
forall a. Preorder a => a -> a -> Bool
>~ a
0 then a -> b
forall a b. Right a b => a -> b
floor a
x else a -> b
forall a b. Left a b => a -> b
ceiling a
x

-- | Lift a unary function over a 'Conn'.
--
-- Results are truncated towards 0.
truncate1 :: (Num a, Triple a b) => (a -> a) -> b -> b
truncate1 :: (a -> a) -> b -> b
truncate1 a -> a
f b
x = a -> b
forall a b. (Num a, Triple a b) => a -> b
truncate (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 'L a b
forall a b. Left a b => ConnL a b
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 :: (a -> a -> a) -> b -> b -> b
truncate2 a -> a -> a
f b
x b
y = a -> b
forall a b. (Num a, Triple a b) => a -> b
truncate (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 'L a b
forall a b. Left a b => ConnL a b
connL
{-# INLINE truncate2 #-}

---------------------------------------------------------------------
-- Connection L
---------------------------------------------------------------------

-- | A specialization of /conn/ to left-side connections.
--
-- This is a convenience function provided primarily to avoid needing
-- to enable /DataKinds/.
connL :: Left a b => ConnL a b
connL :: ConnL a b
connL = forall a b. Left a b => ConnL a b
forall (k :: Kan) a b. Connection k a b => Conn k a b
conn @ 'L

-- | Extract the center of a 'Conn' or upper half of a 'ConnL'.
embedL :: Left a b => b -> a
embedL :: b -> a
embedL = Conn 'L a b -> b -> a
forall (k :: Kan) a b. Conn k a b -> b -> a
embed Conn 'L a b
forall a b. Left a b => ConnL a b
connL

-- | A minimal element of a preorder.
--
-- 'minimal' needn't be unique, but it must obey:
--
-- > x <~ minimal => x ~~ minimal
minimal :: Left () a => a
minimal :: a
minimal = () -> a
forall a b. Left a b => a -> b
ceiling ()

infixr 5 `join`

-- | Semigroup operation on a join-lattice.
join :: Left (a, a) a => a -> a -> a
join :: a -> a -> a
join = ((a, a) -> a) -> a -> a -> a
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (a, a) -> a
forall a b. Left a b => a -> b
ceiling

-- | Extract the ceiling of a 'Conn' or lower half of a 'ConnL'.
--
-- > ceiling @a @a = id
-- > ceiling (x1 `join` a2) = ceiling x1 `join` ceiling x2
--
-- The latter law is the adjoint functor theorem for preorders.
--
-- >>> Data.Connection.ceiling @Rational @Float (0 :% 0)
-- NaN
-- >>> Data.Connection.ceiling @Rational @Float (1 :% 0)
-- Infinity
-- >>> Data.Connection.ceiling @Rational @Float (13 :% 10)
-- 1.3000001
ceiling :: Left a b => a -> b
ceiling :: a -> b
ceiling = ConnL a b -> a -> b
forall a b. ConnL a b -> a -> b
ceilingWith ConnL a b
forall (k :: Kan) a b. Connection k a b => Conn k a b
conn

-- | Lift a unary function over a 'ConnL'.
ceiling1 :: Left a b => (a -> a) -> b -> b
ceiling1 :: (a -> a) -> b -> b
ceiling1 = ConnL a b -> (a -> a) -> b -> b
forall a b. ConnL a b -> (a -> a) -> b -> b
ceilingWith1 ConnL a b
forall (k :: Kan) a b. Connection k a b => Conn k a b
conn

-- | Lift a binary function over a 'ConnL'.
ceiling2 :: Left a b => (a -> a -> a) -> b -> b -> b
ceiling2 :: (a -> a -> a) -> b -> b -> b
ceiling2 = ConnL a b -> (a -> a -> a) -> b -> b -> b
forall a b. ConnL a b -> (a -> a -> a) -> b -> b -> b
ceilingWith2 ConnL a b
forall (k :: Kan) a b. Connection k a b => Conn k a b
conn

---------------------------------------------------------------------
-- Connection R
---------------------------------------------------------------------

-- | A specialization of /conn/ to right-side connections.
--
-- This is a convenience function provided primarily to avoid needing
-- to enable /DataKinds/.
connR :: Right a b => ConnR a b
connR :: ConnR a b
connR = forall a b. Right a b => ConnR a b
forall (k :: Kan) a b. Connection k a b => Conn k a b
conn @ 'R

-- | Extract the center of a 'ConnK' or lower half of a 'ConnR'.
embedR :: Right a b => b -> a
embedR :: b -> a
embedR = Conn 'R a b -> b -> a
forall (k :: Kan) a b. Conn k a b -> b -> a
embed Conn 'R a b
forall a b. Right a b => ConnR a b
connR

-- | A maximal element of a preorder.
--
-- 'maximal' needn't be unique, but it must obey:
--
-- > x >~ maximal => x ~~ maximal
maximal :: Right () a => a
maximal :: a
maximal = () -> a
forall a b. Right a b => a -> b
floor ()

infixr 6 `meet`

-- | Semigroup operation on a meet-lattice.
meet :: Right (a, a) a => a -> a -> a
meet :: a -> a -> a
meet = ((a, a) -> a) -> a -> a -> a
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (a, a) -> a
forall a b. Right a b => a -> b
floor

-- | Extract the floor of a 'ConnK' or upper half of a 'ConnL'.
--
-- > floor @a @a = id
-- > floor (x1 `meet` x2) = floor x1 `meet` floor x2
--
-- The latter law is the adjoint functor theorem for preorders.
--
-- >>> Data.Connection.floor @Rational @Float (0 :% 0)
-- NaN
-- >>> Data.Connection.floor @Rational @Float (1 :% 0)
-- Infinity
-- >>> Data.Connection.floor @Rational @Float (13 :% 10)
-- 1.3
floor :: Right a b => a -> b
floor :: a -> b
floor = ConnR a b -> a -> b
forall a b. ConnR a b -> a -> b
floorWith ConnR a b
forall (k :: Kan) a b. Connection k a b => Conn k a b
conn

-- | Lift a unary function over a 'ConnR'.
floor1 :: Right a b => (a -> a) -> b -> b
floor1 :: (a -> a) -> b -> b
floor1 = ConnR a b -> (a -> a) -> b -> b
forall a b. ConnR a b -> (a -> a) -> b -> b
floorWith1 ConnR a b
forall (k :: Kan) a b. Connection k a b => Conn k a b
conn

-- | Lift a binary function over a 'ConnR'.
floor2 :: Right a b => (a -> a -> a) -> b -> b -> b
floor2 :: (a -> a -> a) -> b -> b -> b
floor2 = ConnR a b -> (a -> a -> a) -> b -> b -> b
forall a b. ConnR a b -> (a -> a -> a) -> b -> b -> b
floorWith2 ConnR a b
forall (k :: Kan) a b. Connection k a b => Conn k a b
conn

---------------------------------------------------------------------
-- Instances
---------------------------------------------------------------------

instance Preorder a => Connection k a a where conn :: Conn k a a
conn = Conn k a a
forall (k :: Kan) a. Conn k a a
identity

instance Connection k ((), ()) () where conn :: Conn k ((), ()) ()
conn = Conn k ((), ()) ()
forall a (k :: Kan). Total a => Conn k (a, a) a
latticeOrd

instance Connection k () Bool where conn :: Conn k () Bool
conn = Conn k () Bool
forall a (k :: Kan). Bounded a => Conn k () a
bounded
instance Connection k Ordering Bool where conn :: Conn k Ordering Bool
conn = Conn k Ordering Bool
forall a (k :: Kan). Triple () a => Conn k a Bool
extremal
instance Connection k Word8 Bool where conn :: Conn k Word8 Bool
conn = Conn k Word8 Bool
forall a (k :: Kan). Triple () a => Conn k a Bool
extremal
instance Connection k Word16 Bool where conn :: Conn k Word16 Bool
conn = Conn k Word16 Bool
forall a (k :: Kan). Triple () a => Conn k a Bool
extremal
instance Connection k Word32 Bool where conn :: Conn k Word32 Bool
conn = Conn k Word32 Bool
forall a (k :: Kan). Triple () a => Conn k a Bool
extremal
instance Connection k Word64 Bool where conn :: Conn k Word64 Bool
conn = Conn k Word64 Bool
forall a (k :: Kan). Triple () a => Conn k a Bool
extremal
instance Connection k Word Bool where conn :: Conn k Word Bool
conn = Conn k Word Bool
forall a (k :: Kan). Triple () a => Conn k a Bool
extremal
instance Connection k Positive Bool where conn :: Conn k Positive Bool
conn = Conn k Positive Bool
forall a (k :: Kan). Triple () a => Conn k a Bool
extremal
instance Connection k Int8 Bool where conn :: Conn k Int8 Bool
conn = Conn k Int8 Bool
forall a (k :: Kan). Triple () a => Conn k a Bool
extremal
instance Connection k Int16 Bool where conn :: Conn k Int16 Bool
conn = Conn k Int16 Bool
forall a (k :: Kan). Triple () a => Conn k a Bool
extremal
instance Connection k Int32 Bool where conn :: Conn k Int32 Bool
conn = Conn k Int32 Bool
forall a (k :: Kan). Triple () a => Conn k a Bool
extremal
instance Connection k Int64 Bool where conn :: Conn k Int64 Bool
conn = Conn k Int64 Bool
forall a (k :: Kan). Triple () a => Conn k a Bool
extremal
instance Connection k Int Bool where conn :: Conn k Int Bool
conn = Conn k Int Bool
forall a (k :: Kan). Triple () a => Conn k a Bool
extremal
instance Connection k Rational Bool where conn :: Conn k Rational Bool
conn = Conn k Rational Bool
forall a (k :: Kan). Triple () a => Conn k a Bool
extremal
instance Connection k Float Bool where conn :: Conn k Float Bool
conn = Conn k Float Bool
forall a (k :: Kan). Triple () a => Conn k a Bool
extremal
instance Connection k Double Bool where conn :: Conn k Double Bool
conn = Conn k Double Bool
forall a (k :: Kan). Triple () a => Conn k a Bool
extremal
instance Connection k (Bool, Bool) Bool where conn :: Conn k (Bool, Bool) Bool
conn = Conn k (Bool, Bool) Bool
forall a (k :: Kan). Total a => Conn k (a, a) a
latticeOrd

instance Connection k () Ordering where conn :: Conn k () Ordering
conn = Conn k () Ordering
forall a (k :: Kan). Bounded a => Conn k () a
bounded
instance Connection k (Ordering, Ordering) Ordering where conn :: Conn k (Ordering, Ordering) Ordering
conn = Conn k (Ordering, Ordering) Ordering
forall a (k :: Kan). Total a => Conn k (a, a) a
latticeOrd

instance Connection k () Word8 where conn :: Conn k () Word8
conn = Conn k () Word8
forall a (k :: Kan). Bounded a => Conn k () a
bounded
instance Connection 'L Int8 Word8 where conn :: Conn 'L Int8 Word8
conn = Conn 'L Int8 Word8
i08w08
instance Connection k (Word8, Word8) Word8 where conn :: Conn k (Word8, Word8) Word8
conn = Conn k (Word8, Word8) Word8
forall a (k :: Kan). Total a => Conn k (a, a) a
latticeOrd

instance Connection k () Word16 where conn :: Conn k () Word16
conn = Conn k () Word16
forall a (k :: Kan). Bounded a => Conn k () a
bounded
instance Connection 'L Word8 Word16 where conn :: Conn 'L Word8 Word16
conn = Conn 'L Word8 Word16
w08w16
instance Connection 'L Int8 Word16 where conn :: Conn 'L Int8 Word16
conn = Conn 'L Int8 Word16
i08w16
instance Connection 'L Int16 Word16 where conn :: Conn 'L Int16 Word16
conn = Conn 'L Int16 Word16
i16w16
instance Connection k (Word16, Word16) Word16 where conn :: Conn k (Word16, Word16) Word16
conn = Conn k (Word16, Word16) Word16
forall a (k :: Kan). Total a => Conn k (a, a) a
latticeOrd

instance Connection k () Word32 where conn :: Conn k () Word32
conn = Conn k () Word32
forall a (k :: Kan). Bounded a => Conn k () a
bounded
instance Connection 'L Word8 Word32 where conn :: Conn 'L Word8 Word32
conn = Conn 'L Word8 Word32
w08w32
instance Connection 'L Word16 Word32 where conn :: Conn 'L Word16 Word32
conn = Conn 'L Word16 Word32
w16w32
instance Connection 'L Int8 Word32 where conn :: Conn 'L Int8 Word32
conn = Conn 'L Int8 Word32
i08w32
instance Connection 'L Int16 Word32 where conn :: Conn 'L Int16 Word32
conn = Conn 'L Int16 Word32
i16w32
instance Connection 'L Int32 Word32 where conn :: Conn 'L Int32 Word32
conn = Conn 'L Int32 Word32
i32w32
instance Connection k (Word32, Word32) Word32 where conn :: Conn k (Word32, Word32) Word32
conn = Conn k (Word32, Word32) Word32
forall a (k :: Kan). Total a => Conn k (a, a) a
latticeOrd

instance Connection k () Word64 where conn :: Conn k () Word64
conn = Conn k () Word64
forall a (k :: Kan). Bounded a => Conn k () a
bounded
instance Connection 'L Word8 Word64 where conn :: Conn 'L Word8 Word64
conn = Conn 'L Word8 Word64
w08w64
instance Connection 'L Word16 Word64 where conn :: Conn 'L Word16 Word64
conn = Conn 'L Word16 Word64
w16w64
instance Connection 'L Word32 Word64 where conn :: Conn 'L Word32 Word64
conn = Conn 'L Word32 Word64
w32w64
instance Connection 'L Int8 Word64 where conn :: Conn 'L Int8 Word64
conn = Conn 'L Int8 Word64
i08w64
instance Connection 'L Int16 Word64 where conn :: Conn 'L Int16 Word64
conn = Conn 'L Int16 Word64
i16w64
instance Connection 'L Int32 Word64 where conn :: Conn 'L Int32 Word64
conn = Conn 'L Int32 Word64
i32w64
instance Connection 'L Int64 Word64 where conn :: Conn 'L Int64 Word64
conn = Conn 'L Int64 Word64
i64w64
instance Connection 'L Int Word64 where conn :: Conn 'L Int Word64
conn = Conn 'L Int Word64
ixxw64
instance Connection k (Word64, Word64) Word64 where conn :: Conn k (Word64, Word64) Word64
conn = Conn k (Word64, Word64) Word64
forall a (k :: Kan). Total a => Conn k (a, a) a
latticeOrd

instance Connection k () Word where conn :: Conn k () Word
conn = Conn k () Word
forall a (k :: Kan). Bounded a => Conn k () a
bounded
instance Connection 'L Word8 Word where conn :: Conn 'L Word8 Word
conn = Conn 'L Word8 Word
w08wxx
instance Connection 'L Word16 Word where conn :: Conn 'L Word16 Word
conn = Conn 'L Word16 Word
w16wxx
instance Connection 'L Word32 Word where conn :: Conn 'L Word32 Word
conn = Conn 'L Word32 Word
w32wxx
instance Connection k Word64 Word where conn :: Conn k Word64 Word
conn = Conn k Word64 Word
forall (k :: Kan). Conn k Word64 Word
w64wxx
instance Connection 'L Int8 Word where conn :: Conn 'L Int8 Word
conn = Conn 'L Int8 Word
i08wxx
instance Connection 'L Int16 Word where conn :: Conn 'L Int16 Word
conn = Conn 'L Int16 Word
i16wxx
instance Connection 'L Int32 Word where conn :: Conn 'L Int32 Word
conn = Conn 'L Int32 Word
i32wxx
instance Connection 'L Int64 Word where conn :: Conn 'L Int64 Word
conn = Conn 'L Int64 Word
i64wxx
instance Connection 'L Int Word where conn :: Conn 'L Int Word
conn = Conn 'L Int Word
ixxwxx
instance Connection k (Word, Word) Word where conn :: Conn k (Word, Word) Word
conn = Conn k (Word, Word) Word
forall a (k :: Kan). Total a => Conn k (a, a) a
latticeOrd

instance Connection 'L () Natural where conn :: Conn 'L () Natural
conn = (() -> Natural) -> (Natural -> ()) -> Conn 'L () Natural
forall a b. (a -> b) -> (b -> a) -> ConnL a b
ConnL (Natural -> () -> Natural
forall a b. a -> b -> a
const Natural
0) (() -> Natural -> ()
forall a b. a -> b -> a
const ())
instance Connection 'L Word8 Natural where conn :: Conn 'L Word8 Natural
conn = Conn 'L Word8 Natural
w08nat
instance Connection 'L Word16 Natural where conn :: Conn 'L Word16 Natural
conn = Conn 'L Word16 Natural
w16nat
instance Connection 'L Word32 Natural where conn :: Conn 'L Word32 Natural
conn = Conn 'L Word32 Natural
w32nat
instance Connection 'L Word64 Natural where conn :: Conn 'L Word64 Natural
conn = Conn 'L Word64 Natural
w64nat
instance Connection 'L Word Natural where conn :: Conn 'L Word Natural
conn = Conn 'L Word Natural
wxxnat
instance Connection 'L Int8 Natural where conn :: Conn 'L Int8 Natural
conn = Conn 'L Int8 Natural
i08nat
instance Connection 'L Int16 Natural where conn :: Conn 'L Int16 Natural
conn = Conn 'L Int16 Natural
i16nat
instance Connection 'L Int32 Natural where conn :: Conn 'L Int32 Natural
conn = Conn 'L Int32 Natural
i32nat
instance Connection 'L Int64 Natural where conn :: Conn 'L Int64 Natural
conn = Conn 'L Int64 Natural
i64nat
instance Connection 'L Int Natural where conn :: Conn 'L Int Natural
conn = Conn 'L Int Natural
ixxnat
instance Connection 'L Integer Natural where conn :: Conn 'L Integer Natural
conn = Conn 'L Integer Natural
intnat
instance Connection k (Natural, Natural) Natural where conn :: Conn k (Natural, Natural) Natural
conn = Conn k (Natural, Natural) Natural
forall a (k :: Kan). Total a => Conn k (a, a) a
latticeOrd

instance Connection k () Positive where
    conn :: Conn k () Positive
conn = (() -> Positive)
-> (Positive -> ()) -> (() -> Positive) -> Conn k () Positive
forall a b (k :: Kan).
(a -> b) -> (b -> a) -> (a -> b) -> Conn k a b
Conn (Positive -> () -> Positive
forall a b. a -> b -> a
const (Positive -> () -> Positive) -> Positive -> () -> Positive
forall a b. (a -> b) -> a -> b
$ Natural
0 Natural -> Natural -> Positive
forall a. a -> a -> Ratio a
:% Natural
1) (() -> Positive -> ()
forall a b. a -> b -> a
const ()) (Positive -> () -> Positive
forall a b. a -> b -> a
const (Positive -> () -> Positive) -> Positive -> () -> Positive
forall a b. (a -> b) -> a -> b
$ Natural
1 Natural -> Natural -> Positive
forall a. a -> a -> Ratio a
:% Natural
0)
instance Connection k (Positive, Positive) Positive where conn :: Conn k (Positive, Positive) Positive
conn = Conn k (Positive, Positive) Positive
forall a (k :: Kan). (Total a, Fractional a) => Conn k (a, a) a
latticeN5

instance Connection k () Int8 where conn :: Conn k () Int8
conn = Conn k () Int8
forall a (k :: Kan). Bounded a => Conn k () a
bounded
instance Connection k (Int8, Int8) Int8 where conn :: Conn k (Int8, Int8) Int8
conn = Conn k (Int8, Int8) Int8
forall a (k :: Kan). Total a => Conn k (a, a) a
latticeOrd
instance Connection k () Int16 where conn :: Conn k () Int16
conn = Conn k () Int16
forall a (k :: Kan). Bounded a => Conn k () a
bounded
instance Connection k (Int16, Int16) Int16 where conn :: Conn k (Int16, Int16) Int16
conn = Conn k (Int16, Int16) Int16
forall a (k :: Kan). Total a => Conn k (a, a) a
latticeOrd
instance Connection k () Int32 where conn :: Conn k () Int32
conn = Conn k () Int32
forall a (k :: Kan). Bounded a => Conn k () a
bounded
instance Connection k (Int32, Int32) Int32 where conn :: Conn k (Int32, Int32) Int32
conn = Conn k (Int32, Int32) Int32
forall a (k :: Kan). Total a => Conn k (a, a) a
latticeOrd
instance Connection k () Int64 where conn :: Conn k () Int64
conn = Conn k () Int64
forall a (k :: Kan). Bounded a => Conn k () a
bounded
instance Connection k (Int64, Int64) Int64 where conn :: Conn k (Int64, Int64) Int64
conn = Conn k (Int64, Int64) Int64
forall a (k :: Kan). Total a => Conn k (a, a) a
latticeOrd
instance Connection k () Int where conn :: Conn k () Int
conn = Conn k () Int
forall a (k :: Kan). Bounded a => Conn k () a
bounded
instance Connection k (Int, Int) Int where conn :: Conn k (Int, Int) Int
conn = Conn k (Int, Int) Int
forall a (k :: Kan). Total a => Conn k (a, a) a
latticeOrd
instance Connection k (Integer, Integer) Integer where conn :: Conn k (Integer, Integer) Integer
conn = Conn k (Integer, Integer) Integer
forall a (k :: Kan). Total a => Conn k (a, a) a
latticeOrd

instance Connection k () Rational where
    conn :: Conn k () Rational
conn = (() -> Rational)
-> (Rational -> ()) -> (() -> Rational) -> Conn k () Rational
forall a b (k :: Kan).
(a -> b) -> (b -> a) -> (a -> b) -> Conn k a b
Conn (Rational -> () -> Rational
forall a b. a -> b -> a
const (Rational -> () -> Rational) -> Rational -> () -> Rational
forall a b. (a -> b) -> a -> b
$ -Integer
1 Integer -> Integer -> Rational
forall a. a -> a -> Ratio a
:% Integer
0) (() -> Rational -> ()
forall a b. a -> b -> a
const ()) (Rational -> () -> Rational
forall a b. a -> b -> a
const (Rational -> () -> Rational) -> Rational -> () -> Rational
forall a b. (a -> b) -> a -> b
$ Integer
1 Integer -> Integer -> Rational
forall a. a -> a -> Ratio a
:% Integer
0)
instance Connection k (Rational, Rational) Rational where conn :: Conn k (Rational, Rational) Rational
conn = Conn k (Rational, Rational) Rational
forall a (k :: Kan). (Total a, Fractional a) => Conn k (a, a) a
latticeN5

instance Connection k () Float where conn :: Conn k () Float
conn = Conn k () Float
forall a (k :: Kan). (Total a, Fractional a) => Conn k () a
extremalN5
instance Connection k Double Float where conn :: Conn k Double Float
conn = Conn k Double Float
forall (k :: Kan). Conn k Double Float
f64f32
instance Connection k Rational Float where conn :: Conn k Rational Float
conn = Conn k Rational Float
forall (k :: Kan). Conn k Rational Float
ratf32
instance Connection k (Float, Float) Float where conn :: Conn k (Float, Float) Float
conn = Conn k (Float, Float) Float
forall a (k :: Kan). (Total a, Fractional a) => Conn k (a, a) a
latticeN5

instance Connection k () Double where conn :: Conn k () Double
conn = Conn k () Double
forall a (k :: Kan). (Total a, Fractional a) => Conn k () a
extremalN5
instance Connection k Rational Double where conn :: Conn k Rational Double
conn = Conn k Rational Double
forall (k :: Kan). Conn k Rational Double
ratf64
instance Connection k (Double, Double) Double where conn :: Conn k (Double, Double) Double
conn = Conn k (Double, Double) Double
forall a (k :: Kan). (Total a, Fractional a) => Conn k (a, a) a
latticeN5

instance Connection 'L Word8 (Maybe Int16) where conn :: Conn 'L Word8 (Maybe Int16)
conn = Conn 'L Word8 (Maybe Int16)
w08i16
instance Connection 'L Int8 (Maybe Int16) where conn :: Conn 'L Int8 (Maybe Int16)
conn = Conn 'L Int8 (Maybe Int16)
i08i16

instance Connection 'L Word8 (Maybe Int32) where conn :: Conn 'L Word8 (Maybe Int32)
conn = Conn 'L Word8 (Maybe Int32)
w08i32
instance Connection 'L Word16 (Maybe Int32) where conn :: Conn 'L Word16 (Maybe Int32)
conn = Conn 'L Word16 (Maybe Int32)
w16i32
instance Connection 'L Int8 (Maybe Int32) where conn :: Conn 'L Int8 (Maybe Int32)
conn = Conn 'L Int8 (Maybe Int32)
i08i32
instance Connection 'L Int16 (Maybe Int32) where conn :: Conn 'L Int16 (Maybe Int32)
conn = Conn 'L Int16 (Maybe Int32)
i16i32

instance Connection 'L Word8 (Maybe Int64) where conn :: Conn 'L Word8 (Maybe Int64)
conn = Conn 'L Word8 (Maybe Int64)
w08i64
instance Connection 'L Word16 (Maybe Int64) where conn :: Conn 'L Word16 (Maybe Int64)
conn = Conn 'L Word16 (Maybe Int64)
w16i64
instance Connection 'L Word32 (Maybe Int64) where conn :: Conn 'L Word32 (Maybe Int64)
conn = Conn 'L Word32 (Maybe Int64)
w32i64
instance Connection 'L Int8 (Maybe Int64) where conn :: Conn 'L Int8 (Maybe Int64)
conn = Conn 'L Int8 (Maybe Int64)
i08i64
instance Connection 'L Int16 (Maybe Int64) where conn :: Conn 'L Int16 (Maybe Int64)
conn = Conn 'L Int16 (Maybe Int64)
i16i64
instance Connection 'L Int32 (Maybe Int64) where conn :: Conn 'L Int32 (Maybe Int64)
conn = Conn 'L Int32 (Maybe Int64)
i32i64

instance Connection 'L Word8 (Maybe Int) where conn :: Conn 'L Word8 (Maybe Int)
conn = Conn 'L Word8 (Maybe Int)
w08ixx
instance Connection 'L Word16 (Maybe Int) where conn :: Conn 'L Word16 (Maybe Int)
conn = Conn 'L Word16 (Maybe Int)
w16ixx
instance Connection 'L Word32 (Maybe Int) where conn :: Conn 'L Word32 (Maybe Int)
conn = Conn 'L Word32 (Maybe Int)
w32ixx
instance Connection 'L Int8 (Maybe Int) where conn :: Conn 'L Int8 (Maybe Int)
conn = Conn 'L Int8 (Maybe Int)
i08ixx
instance Connection 'L Int16 (Maybe Int) where conn :: Conn 'L Int16 (Maybe Int)
conn = Conn 'L Int16 (Maybe Int)
i16ixx
instance Connection 'L Int32 (Maybe Int) where conn :: Conn 'L Int32 (Maybe Int)
conn = Conn 'L Int32 (Maybe Int)
i32ixx
instance Connection k Int64 Int where conn :: Conn k Int64 Int
conn = Conn k Int64 Int
forall (k :: Kan). Conn k Int64 Int
i64ixx

instance Connection 'L Word8 (Maybe Integer) where conn :: Conn 'L Word8 (Maybe Integer)
conn = Conn 'L Word8 (Maybe Integer)
w08int
instance Connection 'L Word16 (Maybe Integer) where conn :: Conn 'L Word16 (Maybe Integer)
conn = Conn 'L Word16 (Maybe Integer)
w16int
instance Connection 'L Word32 (Maybe Integer) where conn :: Conn 'L Word32 (Maybe Integer)
conn = Conn 'L Word32 (Maybe Integer)
w32int
instance Connection 'L Word64 (Maybe Integer) where conn :: Conn 'L Word64 (Maybe Integer)
conn = Conn 'L Word64 (Maybe Integer)
w64int
instance Connection 'L Word (Maybe Integer) where conn :: Conn 'L Word (Maybe Integer)
conn = Conn 'L Word (Maybe Integer)
wxxint
instance Connection 'L Natural (Maybe Integer) where conn :: Conn 'L Natural (Maybe Integer)
conn = Conn 'L Natural (Maybe Integer)
natint

instance Connection 'L Int8 (Maybe Integer) where conn :: Conn 'L Int8 (Maybe Integer)
conn = Conn 'L Int8 (Maybe Integer)
i08int
instance Connection 'L Int16 (Maybe Integer) where conn :: Conn 'L Int16 (Maybe Integer)
conn = Conn 'L Int16 (Maybe Integer)
i16int
instance Connection 'L Int32 (Maybe Integer) where conn :: Conn 'L Int32 (Maybe Integer)
conn = Conn 'L Int32 (Maybe Integer)
i32int
instance Connection 'L Int64 (Maybe Integer) where conn :: Conn 'L Int64 (Maybe Integer)
conn = Conn 'L Int64 (Maybe Integer)
i64int
instance Connection 'L Int (Maybe Integer) where conn :: Conn 'L Int (Maybe Integer)
conn = Conn 'L Int (Maybe Integer)
ixxint

{-
instance Connection 'L Integer (Maybe Integer) where
  -- | Provided as a shim for /RebindableSyntax/.
  -- Note that this instance will clip negative numbers to zero.
conn = swapR $ intnat >>> natint
-}

instance Connection k Rational (Extended Int8) where conn :: Conn k Rational (Extended Int8)
conn = Conn k Rational (Extended Int8)
forall (k :: Kan). Conn k Rational (Extended Int8)
rati08
instance Connection k Rational (Extended Int16) where conn :: Conn k Rational (Extended Int16)
conn = Conn k Rational (Extended Int16)
forall (k :: Kan). Conn k Rational (Extended Int16)
rati16
instance Connection k Rational (Extended Int32) where conn :: Conn k Rational (Extended Int32)
conn = Conn k Rational (Extended Int32)
forall (k :: Kan). Conn k Rational (Extended Int32)
rati32
instance Connection k Rational (Extended Int64) where conn :: Conn k Rational (Extended Int64)
conn = Conn k Rational (Extended Int64)
forall (k :: Kan). Conn k Rational (Extended Int64)
rati64
instance Connection k Rational (Extended Int) where conn :: Conn k Rational (Extended Int)
conn = Conn k Rational (Extended Int)
forall (k :: Kan). Conn k Rational (Extended Int)
ratixx
instance Connection k Rational (Extended Integer) where conn :: Conn k Rational (Extended Integer)
conn = Conn k Rational (Extended Integer)
forall (k :: Kan). Conn k Rational (Extended Integer)
ratint

-- | All 'Data.Int.Int08' values are exactly representable in a 'Float'.
instance Connection k Float (Extended Int8) where conn :: Conn k Float (Extended Int8)
conn = Conn k Float (Extended Int8)
forall (k :: Kan). Conn k Float (Extended Int8)
f32i08

-- | All 'Data.Int.Int16' values are exactly representable in a 'Float'.
instance Connection k Float (Extended Int16) where conn :: Conn k Float (Extended Int16)
conn = Conn k Float (Extended Int16)
forall (k :: Kan). Conn k Float (Extended Int16)
f32i16

-- | All 'Data.Int.Int08' values are exactly representable in a 'Double'.
instance Connection k Double (Extended Int8) where conn :: Conn k Double (Extended Int8)
conn = Conn k Double (Extended Int8)
forall (k :: Kan). Conn k Double (Extended Int8)
f64i08

-- | All 'Data.Int.Int16' values are exactly representable in a 'Double'.
instance Connection k Double (Extended Int16) where conn :: Conn k Double (Extended Int16)
conn = Conn k Double (Extended Int16)
forall (k :: Kan). Conn k Double (Extended Int16)
f64i16

-- | All 'Data.Int.Int32' values are exactly representable in a 'Double'.
instance Connection k Double (Extended Int32) where conn :: Conn k Double (Extended Int32)
conn = Conn k Double (Extended Int32)
forall (k :: Kan). Conn k Double (Extended Int32)
f64i32

instance Connection k a b => Connection k (Identity a) b where
    conn :: Conn k (Identity a) b
conn = (Identity a -> a)
-> (a -> Identity a) -> (Identity a -> a) -> Conn k (Identity a) a
forall a b (k :: Kan).
(a -> b) -> (b -> a) -> (a -> b) -> Conn k a b
Conn Identity a -> a
forall a. Identity a -> a
runIdentity a -> Identity a
forall a. a -> Identity a
Identity Identity a -> a
forall a. Identity a -> a
runIdentity Conn k (Identity a) a -> Conn k a b -> Conn k (Identity a) b
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> Conn k a b
forall (k :: Kan) a b. Connection k a b => Conn k a b
conn

instance Connection k a b => Connection k a (Identity b) where
    conn :: Conn k a (Identity b)
conn = Conn k a b
forall (k :: Kan) a b. Connection k a b => Conn k a b
conn Conn k a b -> Conn k b (Identity b) -> Conn k a (Identity b)
forall k (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> (b -> Identity b)
-> (Identity b -> b) -> (b -> Identity b) -> Conn k b (Identity b)
forall a b (k :: Kan).
(a -> b) -> (b -> a) -> (a -> b) -> Conn k a b
Conn b -> Identity b
forall a. a -> Identity a
Identity Identity b -> b
forall a. Identity a -> a
runIdentity b -> Identity b
forall a. a -> Identity a
Identity

instance (Triple () a, Triple () b) => Connection k () (a, b) where
    conn :: Conn k () (a, b)
conn = (() -> (a, b))
-> ((a, b) -> ()) -> (() -> (a, b)) -> Conn k () (a, b)
forall a b (k :: Kan).
(a -> b) -> (b -> a) -> (a -> b) -> Conn k a b
Conn ((a, b) -> () -> (a, b)
forall a b. a -> b -> a
const (a
forall a. Left () a => a
minimal, b
forall a. Left () a => a
minimal)) (() -> (a, b) -> ()
forall a b. a -> b -> a
const ()) ((a, b) -> () -> (a, b)
forall a b. a -> b -> a
const (a
forall a. Right () a => a
maximal, b
forall a. Right () a => a
maximal))

instance Preorder a => Connection 'L () (Maybe a) where
    conn :: Conn 'L () (Maybe a)
conn = (() -> Maybe a) -> (Maybe a -> ()) -> Conn 'L () (Maybe a)
forall a b. (a -> b) -> (b -> a) -> ConnL a b
ConnL (Maybe a -> () -> Maybe a
forall a b. a -> b -> a
const Maybe a
forall a. Maybe a
Nothing) (() -> Maybe a -> ()
forall a b. a -> b -> a
const ())

instance Right () a => Connection 'R () (Maybe a) where
    conn :: Conn 'R () (Maybe a)
conn = (Maybe a -> ()) -> (() -> Maybe a) -> Conn 'R () (Maybe a)
forall b a. (b -> a) -> (a -> b) -> ConnR a b
ConnR (() -> Maybe a -> ()
forall a b. a -> b -> a
const ()) (Maybe a -> () -> Maybe a
forall a b. a -> b -> a
const (Maybe a -> () -> Maybe a) -> Maybe a -> () -> Maybe a
forall a b. (a -> b) -> a -> b
$ a -> Maybe a
forall a. a -> Maybe a
Just a
forall a. Right () a => a
maximal)

instance Preorder a => Connection k () (Extended a) where
    conn :: Conn k () (Extended a)
conn = (() -> Extended a)
-> (Extended a -> ())
-> (() -> Extended a)
-> Conn k () (Extended a)
forall a b (k :: Kan).
(a -> b) -> (b -> a) -> (a -> b) -> Conn k a b
Conn (Extended a -> () -> Extended a
forall a b. a -> b -> a
const Extended a
forall a. Extended a
Bottom) (() -> Extended a -> ()
forall a b. a -> b -> a
const ()) (Extended a -> () -> Extended a
forall a b. a -> b -> a
const Extended a
forall a. Extended a
Top)

instance (Left () a, Preorder b) => Connection 'L () (Either a b) where
    conn :: Conn 'L () (Either a b)
conn = (() -> Either a b) -> (Either a b -> ()) -> Conn 'L () (Either a b)
forall a b. (a -> b) -> (b -> a) -> ConnL a b
ConnL (Either a b -> () -> Either a b
forall a b. a -> b -> a
const (Either a b -> () -> Either a b) -> Either a b -> () -> Either a b
forall a b. (a -> b) -> a -> b
$ a -> Either a b
forall a b. a -> Either a b
Left a
forall a. Left () a => a
minimal) (() -> Either a b -> ()
forall a b. a -> b -> a
const ())

instance (Preorder a, Right () b) => Connection 'R () (Either a b) where
    conn :: Conn 'R () (Either a b)
conn = (Either a b -> ()) -> (() -> Either a b) -> Conn 'R () (Either a b)
forall b a. (b -> a) -> (a -> b) -> ConnR a b
ConnR (() -> Either a b -> ()
forall a b. a -> b -> a
const ()) (Either a b -> () -> Either a b
forall a b. a -> b -> a
const (Either a b -> () -> Either a b) -> Either a b -> () -> Either a b
forall a b. (a -> b) -> a -> b
$ b -> Either a b
forall a b. b -> Either a b
Right b
forall a. Right () a => a
maximal)

instance (Preorder a, Triple () b) => Connection k (Maybe a) (Either a b) where
    conn :: Conn k (Maybe a) (Either a b)
conn = Conn k (Maybe a) (Either a b)
forall b (k :: Kan) a. Triple () b => Conn k (Maybe a) (Either a b)
maybeL

instance (Triple () a, Preorder b) => Connection k (Maybe b) (Either a b) where
    conn :: Conn k (Maybe b) (Either a b)
conn = Conn k (Maybe b) (Either a b)
forall a (k :: Kan) b. Triple () a => Conn k (Maybe b) (Either a b)
maybeR

instance (Total a) => Connection 'L () (Set.Set a) where
    conn :: Conn 'L () (Set a)
conn = (() -> Set a) -> (Set a -> ()) -> Conn 'L () (Set a)
forall a b. (a -> b) -> (b -> a) -> ConnL a b
ConnL (Set a -> () -> Set a
forall a b. a -> b -> a
const Set a
forall a. Set a
Set.empty) (() -> Set a -> ()
forall a b. a -> b -> a
const ())

instance Total a => Connection k (Set.Set a, Set.Set a) (Set.Set a) where
    conn :: Conn k (Set a, Set a) (Set a)
conn = ((Set a, Set a) -> Set a)
-> (Set a -> (Set a, Set a))
-> ((Set a, Set a) -> Set a)
-> Conn k (Set a, Set a) (Set a)
forall a b (k :: Kan).
(a -> b) -> (b -> a) -> (a -> b) -> Conn k a b
Conn ((Set a -> Set a -> Set a) -> (Set a, Set a) -> Set a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
Set.union) Set a -> (Set a, Set a)
forall a. a -> (a, a)
fork ((Set a -> Set a -> Set a) -> (Set a, Set a) -> Set a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection)

instance Connection 'L () IntSet.IntSet where
    conn :: Conn 'L () IntSet
conn = (() -> IntSet) -> (IntSet -> ()) -> Conn 'L () IntSet
forall a b. (a -> b) -> (b -> a) -> ConnL a b
ConnL (IntSet -> () -> IntSet
forall a b. a -> b -> a
const IntSet
IntSet.empty) (() -> IntSet -> ()
forall a b. a -> b -> a
const ())

instance Connection k (IntSet.IntSet, IntSet.IntSet) IntSet.IntSet where
    conn :: Conn k (IntSet, IntSet) IntSet
conn = ((IntSet, IntSet) -> IntSet)
-> (IntSet -> (IntSet, IntSet))
-> ((IntSet, IntSet) -> IntSet)
-> Conn k (IntSet, IntSet) IntSet
forall a b (k :: Kan).
(a -> b) -> (b -> a) -> (a -> b) -> Conn k a b
Conn ((IntSet -> IntSet -> IntSet) -> (IntSet, IntSet) -> IntSet
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry IntSet -> IntSet -> IntSet
IntSet.union) IntSet -> (IntSet, IntSet)
forall a. a -> (a, a)
fork ((IntSet -> IntSet -> IntSet) -> (IntSet, IntSet) -> IntSet
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry IntSet -> IntSet -> IntSet
IntSet.intersection)

instance (Total a, Preorder b) => Connection 'L () (Map.Map a b) where
    conn :: Conn 'L () (Map a b)
conn = (() -> Map a b) -> (Map a b -> ()) -> Conn 'L () (Map a b)
forall a b. (a -> b) -> (b -> a) -> ConnL a b
ConnL (Map a b -> () -> Map a b
forall a b. a -> b -> a
const Map a b
forall k a. Map k a
Map.empty) (() -> Map a b -> ()
forall a b. a -> b -> a
const ())

instance (Total a, Left (b, b) b) => Connection 'L (Map.Map a b, Map.Map a b) (Map.Map a b) where
    conn :: Conn 'L (Map a b, Map a b) (Map a b)
conn = ((Map a b, Map a b) -> Map a b)
-> (Map a b -> (Map a b, Map a b))
-> Conn 'L (Map a b, Map a b) (Map a b)
forall a b. (a -> b) -> (b -> a) -> ConnL a b
ConnL ((Map a b -> Map a b -> Map a b) -> (Map a b, Map a b) -> Map a b
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((Map a b -> Map a b -> Map a b) -> (Map a b, Map a b) -> Map a b)
-> (Map a b -> Map a b -> Map a b) -> (Map a b, Map a b) -> Map a b
forall a b. (a -> b) -> a -> b
$ (b -> b -> b) -> Map a b -> Map a b -> Map a b
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith b -> b -> b
forall a. Left (a, a) a => a -> a -> a
join) Map a b -> (Map a b, Map a b)
forall a. a -> (a, a)
fork

instance (Total a, Right (b, b) b) => Connection 'R (Map.Map a b, Map.Map a b) (Map.Map a b) where
    conn :: Conn 'R (Map a b, Map a b) (Map a b)
conn = (Map a b -> (Map a b, Map a b))
-> ((Map a b, Map a b) -> Map a b)
-> Conn 'R (Map a b, Map a b) (Map a b)
forall b a. (b -> a) -> (a -> b) -> ConnR a b
ConnR Map a b -> (Map a b, Map a b)
forall a. a -> (a, a)
fork ((Map a b -> Map a b -> Map a b) -> (Map a b, Map a b) -> Map a b
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((Map a b -> Map a b -> Map a b) -> (Map a b, Map a b) -> Map a b)
-> (Map a b -> Map a b -> Map a b) -> (Map a b, Map a b) -> Map a b
forall a b. (a -> b) -> a -> b
$ (b -> b -> b) -> Map a b -> Map a b -> Map a b
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
Map.intersectionWith b -> b -> b
forall a. Right (a, a) a => a -> a -> a
meet)

instance Preorder a => Connection 'L () (IntMap.IntMap a) where
    conn :: Conn 'L () (IntMap a)
conn = (() -> IntMap a) -> (IntMap a -> ()) -> Conn 'L () (IntMap a)
forall a b. (a -> b) -> (b -> a) -> ConnL a b
ConnL (IntMap a -> () -> IntMap a
forall a b. a -> b -> a
const IntMap a
forall a. IntMap a
IntMap.empty) (() -> IntMap a -> ()
forall a b. a -> b -> a
const ())

instance Left (a, a) a => Connection 'L (IntMap.IntMap a, IntMap.IntMap a) (IntMap.IntMap a) where
    conn :: Conn 'L (IntMap a, IntMap a) (IntMap a)
conn = ((IntMap a, IntMap a) -> IntMap a)
-> (IntMap a -> (IntMap a, IntMap a))
-> Conn 'L (IntMap a, IntMap a) (IntMap a)
forall a b. (a -> b) -> (b -> a) -> ConnL a b
ConnL ((IntMap a -> IntMap a -> IntMap a)
-> (IntMap a, IntMap a) -> IntMap a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((IntMap a -> IntMap a -> IntMap a)
 -> (IntMap a, IntMap a) -> IntMap a)
-> (IntMap a -> IntMap a -> IntMap a)
-> (IntMap a, IntMap a)
-> IntMap a
forall a b. (a -> b) -> a -> b
$ (a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
forall a. (a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
IntMap.unionWith a -> a -> a
forall a. Left (a, a) a => a -> a -> a
join) IntMap a -> (IntMap a, IntMap a)
forall a. a -> (a, a)
fork

instance Right (a, a) a => Connection 'R (IntMap.IntMap a, IntMap.IntMap a) (IntMap.IntMap a) where
    conn :: Conn 'R (IntMap a, IntMap a) (IntMap a)
conn = (IntMap a -> (IntMap a, IntMap a))
-> ((IntMap a, IntMap a) -> IntMap a)
-> Conn 'R (IntMap a, IntMap a) (IntMap a)
forall b a. (b -> a) -> (a -> b) -> ConnR a b
ConnR IntMap a -> (IntMap a, IntMap a)
forall a. a -> (a, a)
fork ((IntMap a -> IntMap a -> IntMap a)
-> (IntMap a, IntMap a) -> IntMap a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((IntMap a -> IntMap a -> IntMap a)
 -> (IntMap a, IntMap a) -> IntMap a)
-> (IntMap a -> IntMap a -> IntMap a)
-> (IntMap a, IntMap a)
-> IntMap a
forall a b. (a -> b) -> a -> b
$ (a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
forall a b c. (a -> b -> c) -> IntMap a -> IntMap b -> IntMap c
IntMap.intersectionWith a -> a -> a
forall a. Right (a, a) a => a -> a -> a
meet)

-- Internal

-------------------------

fork :: a -> (a, a)
fork :: a -> (a, a)
fork a
x = (a
x, a
x)

bounded :: Bounded a => Conn k () a
bounded :: Conn k () a
bounded = (() -> a) -> (a -> ()) -> (() -> a) -> Conn k () a
forall a b (k :: Kan).
(a -> b) -> (b -> a) -> (a -> b) -> Conn k a b
Conn (a -> () -> a
forall a b. a -> b -> a
const a
forall a. Bounded a => a
minBound) (() -> a -> ()
forall a b. a -> b -> a
const ()) (a -> () -> a
forall a b. a -> b -> a
const a
forall a. Bounded a => a
maxBound)

latticeN5 :: (Total a, Fractional a) => Conn k (a, a) a
latticeN5 :: Conn k (a, a) a
latticeN5 = ((a, a) -> a) -> (a -> (a, a)) -> ((a, a) -> a) -> Conn k (a, a) a
forall a b (k :: Kan).
(a -> b) -> (b -> a) -> (a -> b) -> Conn k a b
Conn ((a -> a -> a) -> (a, a) -> a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry a -> a -> a
forall a. (Fractional a, Preorder a) => a -> a -> a
joinN5) a -> (a, a)
forall a. a -> (a, a)
fork ((a -> a -> a) -> (a, a) -> a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry a -> a -> a
forall a. (Fractional a, Preorder a) => a -> a -> a
meetN5)
  where
    joinN5 :: a -> a -> a
joinN5 a
x a
y = a -> (Ordering -> a) -> Maybe Ordering -> a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (a
1 a -> a -> a
forall a. Fractional a => a -> a -> a
/ a
0) (a -> a -> Bool -> a
forall a. a -> a -> Bool -> a
bool a
y a
x (Bool -> a) -> (Ordering -> Bool) -> Ordering -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Ordering -> Ordering -> Bool
forall a. Ord a => a -> a -> Bool
>= Ordering
EQ)) (a -> a -> Maybe Ordering
forall a. Preorder a => a -> a -> Maybe Ordering
pcompare a
x a
y)

    meetN5 :: a -> a -> a
meetN5 a
x a
y = a -> (Ordering -> a) -> Maybe Ordering -> a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (-a
1 a -> a -> a
forall a. Fractional a => a -> a -> a
/ a
0) (a -> a -> Bool -> a
forall a. a -> a -> Bool -> a
bool a
y a
x (Bool -> a) -> (Ordering -> Bool) -> Ordering -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Ordering -> Ordering -> Bool
forall a. Ord a => a -> a -> Bool
<= Ordering
EQ)) (a -> a -> Maybe Ordering
forall a. Preorder a => a -> a -> Maybe Ordering
pcompare a
x a
y)

extremalN5 :: (Total a, Fractional a) => Conn k () a
extremalN5 :: Conn k () a
extremalN5 = (() -> a) -> (a -> ()) -> (() -> a) -> Conn k () a
forall a b (k :: Kan).
(a -> b) -> (b -> a) -> (a -> b) -> Conn k a b
Conn (a -> () -> a
forall a b. a -> b -> a
const (a -> () -> a) -> a -> () -> a
forall a b. (a -> b) -> a -> b
$ -a
1 a -> a -> a
forall a. Fractional a => a -> a -> a
/ a
0) (() -> a -> ()
forall a b. a -> b -> a
const ()) (a -> () -> a
forall a b. a -> b -> a
const (a -> () -> a) -> a -> () -> a
forall a b. (a -> b) -> a -> b
$ a
1 a -> a -> a
forall a. Fractional a => a -> a -> a
/ a
0)

latticeOrd :: (Total a) => Conn k (a, a) a
latticeOrd :: Conn k (a, a) a
latticeOrd = ((a, a) -> a) -> (a -> (a, a)) -> ((a, a) -> a) -> Conn k (a, a) a
forall a b (k :: Kan).
(a -> b) -> (b -> a) -> (a -> b) -> Conn k a b
Conn ((a -> a -> a) -> (a, a) -> a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry a -> a -> a
forall a. Ord a => a -> a -> a
max) a -> (a, a)
forall a. a -> (a, a)
fork ((a -> a -> a) -> (a, a) -> a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry a -> a -> a
forall a. Ord a => a -> a -> a
min)

maybeL :: Triple () b => Conn k (Maybe a) (Either a b)
maybeL :: Conn k (Maybe a) (Either a b)
maybeL = (Maybe a -> Either a b)
-> (Either a b -> Maybe a)
-> (Maybe a -> Either a b)
-> Conn k (Maybe a) (Either a b)
forall a b (k :: Kan).
(a -> b) -> (b -> a) -> (a -> b) -> Conn k a b
Conn Maybe a -> Either a b
forall a. Maybe a -> Either a b
f Either a b -> Maybe a
forall a b. Either a b -> Maybe a
g Maybe a -> Either a b
forall a. Maybe a -> Either a b
h
  where
    f :: Maybe a -> Either a b
f = Either a b -> (a -> Either a b) -> Maybe a -> Either a b
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (b -> Either a b
forall a b. b -> Either a b
Right b
forall a. Left () a => a
minimal) a -> Either a b
forall a b. a -> Either a b
Left
    g :: Either a b -> Maybe a
g = (a -> Maybe a) -> (b -> Maybe a) -> Either a b -> Maybe a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either a -> Maybe a
forall a. a -> Maybe a
Just (Maybe a -> b -> Maybe a
forall a b. a -> b -> a
const Maybe a
forall a. Maybe a
Nothing)
    h :: Maybe a -> Either a b
h = Either a b -> (a -> Either a b) -> Maybe a -> Either a b
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (b -> Either a b
forall a b. b -> Either a b
Right b
forall a. Right () a => a
maximal) a -> Either a b
forall a b. a -> Either a b
Left

maybeR :: Triple () a => Conn k (Maybe b) (Either a b)
maybeR :: Conn k (Maybe b) (Either a b)
maybeR = (Maybe b -> Either a b)
-> (Either a b -> Maybe b)
-> (Maybe b -> Either a b)
-> Conn k (Maybe b) (Either a b)
forall a b (k :: Kan).
(a -> b) -> (b -> a) -> (a -> b) -> Conn k a b
Conn Maybe b -> Either a b
forall b. Maybe b -> Either a b
f Either a b -> Maybe b
forall b a. Either b a -> Maybe a
g Maybe b -> Either a b
forall b. Maybe b -> Either a b
h
  where
    f :: Maybe b -> Either a b
f = Either a b -> (b -> Either a b) -> Maybe b -> Either a b
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (a -> Either a b
forall a b. a -> Either a b
Left a
forall a. Left () a => a
minimal) b -> Either a b
forall a b. b -> Either a b
Right
    g :: Either b a -> Maybe a
g = (b -> Maybe a) -> (a -> Maybe a) -> Either b a -> Maybe a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Maybe a -> b -> Maybe a
forall a b. a -> b -> a
const Maybe a
forall a. Maybe a
Nothing) a -> Maybe a
forall a. a -> Maybe a
Just
    h :: Maybe b -> Either a b
h = Either a b -> (b -> Either a b) -> Maybe b -> Either a b
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (a -> Either a b
forall a b. a -> Either a b
Left a
forall a. Right () a => a
maximal) b -> Either a b
forall a b. b -> Either a b
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 :: Connection 'R (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 :: Connection 'R (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 :: (Connection 'R (a, a) a, Connection 'R (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)

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)

meetTuple :: (Connection 'R (a, a) a, Connection 'R (b, b) b) => (a, b) -> (a, b) -> (a, b)
meetTuple (x1, y1) (x2, y2) = (x1 `meet` x2, y1 `meet` y2)
-}