{-# 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 (
Kan (..),
Conn (),
pattern Conn,
embed,
range,
identity,
ConnK,
half,
midpoint,
roundWith,
roundWith1,
roundWith2,
truncateWith,
truncateWith1,
truncateWith2,
ConnL,
pattern ConnL,
upL,
downL,
swapL,
counit,
upper,
upper1,
upper2,
filterWith,
ceilingWith,
ceilingWith1,
ceilingWith2,
ConnR,
pattern ConnR,
upR,
downR,
swapR,
unit,
lower,
lower1,
lower2,
idealWith,
floorWith,
floorWith1,
floorWith2,
(>>>),
(<<<),
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 (..))
data Kan = L | R
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 (.) #-}
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 #-}
_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 #-}
_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 #-}
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 #-}
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 #-}
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 #-}
type ConnK a b = forall k. Conn k a b
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 #-}
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 #-}
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 #-}
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 #-}
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 #-}
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 #-}
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 #-}
type ConnL = Conn 'L
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 #-}
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 #-}
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 #-}
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 #-}
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 #-}
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 #-}
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 #-}
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 #-}
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 #-}
ceilingWith :: ConnL a b -> a -> b
ceilingWith :: ConnL a b -> a -> b
ceilingWith (ConnL a -> b
f b -> a
_) = a -> b
f
{-# INLINE ceilingWith #-}
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 #-}
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 #-}
type ConnR = Conn 'R
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 #-}
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 #-}
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 #-}
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 #-}
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 #-}
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 #-}
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 #-}
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 #-}
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 #-}
floorWith :: ConnR a b -> a -> b
floorWith :: ConnR a b -> a -> b
floorWith (ConnR b -> a
_ a -> b
g) = a -> b
g
{-# INLINE floorWith #-}
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 #-}
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 #-}
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 #-}
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 #-}