Data.Connection.Type

Conn

data Kan

A data kind distinguishing the chirality of a Kan extension.

Constructors

L

R

data Conn (k :: Kan) a b

An adjoint triple of Galois connections.

An adjoint triple is a chain of connections of length 2:

\(f \dashv g \dashv h \)

For further information see Property and https://ncatlab.org/nlab/show/adjoint+triple.

Instances

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

Defined in Data.Connection.Type

Methods

id :: Conn k a a

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

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

A view pattern for a 'Conn k'.

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

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

\(f \dashv g \dashv h \)

For further information see Property and https://ncatlab.org/nlab/show/adjoint+triple.

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 (bounded @Ordering) ()
(LT,GT)
>>> range f64f32 pi
(3.1415925,3.1415927)

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 and https://ncatlab.org/nlab/show/Conn+connection.

Caution: Monotonicity is not checked.

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

A view pattern for a ConnL.

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

lft :: Conn k a b -> ConnL a b

Convert an arbitrary Conn to a ConnL.

lft' :: Conn k a b -> ConnL (Down b) (Down a)

Convert an arbitrary Conn to an inverted ConnL.

>>> unitL (lft' $ bounded @Ordering) (Down LT)
Down LT
>>> unitL (lft' $ bounded @Ordering) (Down EQ)
Down LT
>>> unitL (lft' $ bounded @Ordering) (Down GT)
Down LT

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

Obtain a ConnL from an adjoint pair of monotone functions.

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

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 (bounded @Ordering) LT
GT
>>> counitL (bounded @Ordering) EQ
GT
>>> counitL (bounded @Ordering) GT
GT

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

Obtain the lower half of a Trip or ConnL.

upperR c x <~ lowerL c x

>>> upperR (bounded @Ordering) ()
LT
>>> lowerL (bounded @Ordering) ()
GT

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:

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 many use cases (e.g. rounding) require an adjoint triple of connections (i.e. a 'Conn k') that can lower into a standard connection in one of two ways.

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

A view pattern for a ConnR.

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

rgt :: Conn k a b -> ConnR a b

Convert an arbitrary Conn to a ConnR.

rgt' :: Conn k a b -> ConnR (Down b) (Down a)

Convert an arbitrary Conn to an inverted ConnR.

>>> counitR (rgt' $ bounded @Ordering) (Down LT)
Down GT
>>> counitR (rgt' $ bounded @Ordering) (Down EQ)
Down GT
>>> counitR (rgt' $ bounded @Ordering) (Down GT)
Down GT

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

Obtain a ConnR from an adjoint pair of monotone functions.

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

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 (bounded @Ordering) LT
LT
>>> unitR (bounded @Ordering) EQ
LT
>>> unitR (bounded @Ordering) GT
LT

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

Obtain the upper half of a Connection.

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

bounded :: Bounded a => Conn k () a

Every bounded preorder admits a pair of connections with a single-object preorder.

>>> upperR (bounded @Ordering) ()
LT
>>> lowerL (bounded @Ordering) ()
GT

(\|/) :: Conn k c a -> Conn k c b -> Conn k c (Either a b) infixr 3

A preorder variant of |||.

(/|\) :: Lattice c => Conn k a c -> Conn k b c -> Conn k (a, b) c infixr 4

A preorder variant of &&&.

joined :: Conn k a (Either a a)

forked :: Lattice a => Conn k (a, a) a

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.