Data.Connection.Conn

Conn

data Kan

A data kind distinguishing the chirality of a Kan extension.

Here it serves to distinguish the directionality of a preorder:

• L-tagged types are 'upwards-directed'
• R-tagged types are 'downwards-directed'

Constructors

L

R

data Conn (k :: Kan) a b

An adjoint string of Galois connections of length 2 or 3.

Instances

Category (Conn k :: Type -> Type -> Type)

Defined in Data.Connection.Conn

Methods

id :: Conn k a a

(.) :: Conn k b c -> Conn k a b -> Conn k a c

embed :: Conn k a b -> b -> a

Obtain the center of a Trip, upper half of a ConnL, or the lower half of a ConnR.

Trip

type Trip a b = forall k. Conn k a b

An 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 Property.

pattern Conn :: (a -> b) -> (b -> a) -> (a -> b) -> Conn k a b

A view pattern for an arbitrary (left or right) Conn.

Caution: Conn f g h must obey \(f \dashv g \dashv h\). This condition is not checked.

For detailed properties see Property.

trip :: (a -> b) -> (b -> a) -> (a -> b) -> Trip a b

Obtain a forall k. Conn k from an adjoint triple of monotone functions.

Caution: Conn f g h must obey \(f \dashv g \dashv h\). This condition is not checked.

range :: Trip a b -> a -> (b, b)

Obtain the lower and upper functions from a Trip.

range c = upperR c &&& lowerL c

>>> range f64f32 pi
(3.1415925,3.1415927)
>>> range f64f32 (0/0)
(NaN,NaN)

ConnL

type ConnL = Conn L

A 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 Property.

Caution: Monotonicity is not checked.

pattern ConnL :: (a -> b) -> (b -> a) -> ConnL a b

A view pattern for a ConnL.

Caution: ConnL f g must obey \(f \dashv g \). This condition is not checked.

swapL :: ConnR a b -> ConnL b a

Witness to the symmetry between ConnL and ConnR.

swapL . swapR = id
swapR . swapL = id

downL :: ConnL a b -> ConnL (Down b) (Down a)

Convert an arbitrary Conn to an inverted ConnL.

>>> unitL (downL $ conn @_ @() @Ordering) (Down LT)
Down LT
>>> unitL (downL $ conn @_ @() @Ordering) (Down GT)
Down LT

unitL :: ConnL a b -> a -> a

Round trip through a connection.

unitL c = upperL1 c id = embed c . lowerL c
x <= unitL c x

>>> compare pi $ unitL f64f32 pi
LT

counitL :: ConnL a b -> b -> b

Reverse round trip through a connection.

x >= counitL c x

>>> counitL (conn @_ @() @Ordering) LT
LT
>>> counitL (conn @_ @() @Ordering) GT
LT

lowerL :: ConnL a b -> a -> b

Extract the lower half of a Trip or ConnL.

When a and b are lattices we have:

lowerL c (x1 \/ a2) = lowerL c x1 \/ lowerL c x2

This is the adjoint functor theorem for preorders.

>>> upperR f64f32 pi
3.1415925
>>> lowerL f64f32 pi
3.1415927

lowerL1 :: ConnL a b -> (a -> a) -> b -> b

Map over a connection from the left.

lowerL2 :: ConnL a b -> (a -> a -> a) -> b -> b -> b

Zip over a connection from the left.

upperL1 :: ConnL a b -> (b -> b) -> a -> a

Map over a connection from the left.

upperL2 :: ConnL a b -> (b -> b -> b) -> a -> a -> a

Zip over a connection from the left.

ConnR

type ConnR = Conn R

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 Trip) that can lower into a standard connection in either of two ways.

pattern ConnR :: (b -> a) -> (a -> b) -> ConnR a b

A view pattern for a ConnR.

Caution: ConnR f g must obey \(f \dashv g \). This condition is not checked.

swapR :: ConnL a b -> ConnR b a

Witness to the symmetry between ConnL and ConnR.

swapL . swapR = id
swapR . swapL = id

downR :: ConnR a b -> ConnR (Down b) (Down a)

Convert an arbitrary Conn to an inverted ConnR.

>>> counitR (downR $ conn @_ @() @Ordering) (Down LT)
Down GT
>>> counitR (downR $ conn @_ @() @Ordering) (Down GT)
Down GT

unitR :: ConnR a b -> b -> b

Round trip through a connection.

unitR c = upperR1 c id = upperR c . embed c
x <= unitR c x

>>> unitR (conn @_ @() @Ordering) LT
GT
>>> unitR (conn @_ @() @Ordering) GT
GT

counitR :: ConnR a b -> a -> a

Reverse round trip through a connection.

x >= counitR c x

>>> compare pi $ counitR f64f32 pi
GT

upperR :: ConnR a b -> a -> b

Extract the upper half of a connection.

When a and b are lattices we have:

upperR c (x1 /\ x2) = upperR c x1 /\ upperR c x2

This is the adjoint functor theorem for preorders.

>>> upperR f64f32 pi
3.1415925
>>> lowerL f64f32 pi
3.1415927

upperR1 :: ConnR a b -> (a -> a) -> b -> b

Map over a connection from the left.

upperR2 :: ConnR a b -> (a -> a -> a) -> b -> b -> b

Zip over a connection from the left.

lowerR1 :: ConnR a b -> (b -> b) -> a -> a

Map over a connection from the right.

lowerR2 :: ConnR a b -> (b -> b -> b) -> a -> a -> a

Zip over a connection from the right.

Connections

choice :: Conn k a b -> Conn k c d -> Conn k (Either a c) (Either b d)

Lift two Conns into a Conn on the 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

strong :: Conn k a b -> Conn k c d -> Conn k (a, c) (b, d)

Lift two Conns into a Conn on the 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

fmapped :: Functor f => Conn k a b -> Conn k (f a) (f b)

Lift a Conn into a functor.

Caution: This function will result in an invalid connection if the functor alters the internal preorder (i.e. Down).