connections-0.0.1: Partial orders, Galois connections, ordered semirings, & residuated lattices.

Safe HaskellSafe
LanguageHaskell2010

Data.Connection

Contents

Synopsis

Connection

data Conn a b Source #

A Galois connection between two monotone functions: \(connl \dashv connr \)

Each side of the adjunction may be defined in terms of the other:

\( connr(x) = \sup \{y \in E \mid connl(y) \leq x \} \)

\( connl(x) = \inf \{y \in E \mid connr(y) \geq x \} \)

Galois connections have the same properties as adjunctions defined over other categories:

\( \forall x, y : connl \dashv connr \Rightarrow connl (x) \leq b \Leftrightarrow x \leq connr (y) \)

\( \forall x, y : x \leq y \Rightarrow connl (x) \leq connl (y) \)

\( \forall x, y : x \leq y \Rightarrow connr (x) \leq connr (y) \)

\( \forall x : connl \dashv connr \Rightarrow x \leq connr \circ connl (x) \)

\( \forall x : connl \dashv connr \Rightarrow connl \circ connr (x) \leq x \)

\( \forall x : unit \circ unit (x) \sim unit (x) \)

\( \forall x : counit \circ counit (x) \sim counit (x) \)

\( \forall x : counit \circ connl (x) \sim connl (x) \)

\( \forall x : unit \circ connr (x) \sim connr (x) \)

See also Property and https://en.wikipedia.org/wiki/Galois_connection.

Constructors

Conn (a -> b) (b -> a) 
Instances
Category Conn Source # 
Instance details

Defined in Data.Connection

Methods

id :: Conn a a #

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

connl :: Prd a => Prd b => Conn a b -> a -> b Source #

connr :: Prd a => Prd b => Conn a b -> b -> a Source #

unit :: Prd a => Prd b => Conn a b -> a -> a Source #

counit :: Prd a => Prd b => Conn a b -> b -> b Source #

pcomparing :: Eq b => Prd a => Prd b => Conn a b -> a -> a -> Maybe Ordering Source #

Partial version of comparing.

Helpful in conjunction with the xxxBy functions from List.

dual :: Prd a => Prd b => Conn a b -> Conn (Down b) (Down a) Source #

(***) :: Prd a => Prd b => Prd c => Prd d => Conn a b -> Conn c d -> Conn (a, c) (b, d) infixr 3 Source #

(+++) :: Prd a => Prd b => Prd c => Prd d => Conn a b -> Conn c d -> Conn (Either a c) (Either b d) infixr 2 Source #

(&&&) :: Prd a => Prd b => Lattice c => Conn c a -> Conn c b -> Conn c (a, b) infixr 3 Source #

(|||) :: Prd a => Prd b => Prd c => Conn a c -> Conn b c -> Conn (Either a b) c infixr 2 Source #

_1 :: Prd a => Prd b => Prd c => Conn a b -> Conn (a, c) (b, c) Source #

Lens into first part of a product.

_1 (ab >>> cd) = _1 ab >>> _1 cd

_2 :: Prd a => Prd b => Prd c => Conn a b -> Conn (c, a) (c, b) Source #

_L :: Prd a => Prd b => Prd c => Conn a b -> Conn (Either a c) (Either b c) Source #

Prism into left part of a sum.

_L (ab >>> cd) = _L ab >>> _L cd

_R :: Prd a => Prd b => Prd c => Conn a b -> Conn (Either c a) (Either c b) Source #

just :: Prd a => Prd b => Conn a b -> Conn (Maybe a) (Maybe b) Source #

list :: Prd a => Prd b => Conn a b -> Conn [a] [b] Source #

Triple

data Trip a b Source #

An adjoint triple.

Trip f g h satisfies:

f ⊣ g ⊥ ⊥ g ⊣ h

See https://ncatlab.org/nlab/show/adjoint+triple

Constructors

Trip (a -> b) (b -> a) (a -> b) 
Instances
Category Trip Source # 
Instance details

Defined in Data.Connection

Methods

id :: Trip a a #

(.) :: Trip b c -> Trip a b -> Trip a c #

tripl :: Prd a => Prd b => Trip a b -> Conn a b Source #

tripr :: Prd a => Prd b => Trip a b -> Conn b a Source #

unitl :: Prd a => Prd b => Trip a b -> a -> a Source #

unitr :: Prd a => Prd b => Trip a b -> b -> b Source #

counitl :: Prd a => Prd b => Trip a b -> b -> b Source #

counitr :: Prd a => Prd b => Trip a b -> a -> a Source #

ceiling' :: Prd a => Prd b => Trip a b -> a -> b Source #

floor' :: Prd a => Prd b => Trip a b -> a -> b Source #

(****) :: Prd a => Prd b => Prd c => Prd d => Trip a b -> Trip c d -> Trip (a, c) (b, d) infixr 3 Source #

(++++) :: Prd a => Prd b => Prd c => Prd d => Trip a b -> Trip c d -> Trip (Either a c) (Either b d) infixr 2 Source #

(&&&&) :: Prd a => Prd b => Lattice c => Trip a c -> Trip b c -> Trip (a, b) c infixr 3 Source #

(||||) :: Prd a => Prd b => Prd c => Trip c a -> Trip c b -> Trip c (Either a b) infixr 2 Source #

_1' :: Prd a => Prd b => Prd c => Trip a b -> Trip (a, c) (b, c) Source #

_2' :: Prd a => Prd b => Prd c => Trip a b -> Trip (c, a) (c, b) Source #

_L' :: Prd a => Prd b => Prd c => Trip a b -> Trip (Either a c) (Either b c) Source #

_R' :: Prd a => Prd b => Prd c => Trip a b -> Trip (Either c a) (Either c b) Source #

diag :: Lattice a => Trip (a, a) a Source #

codiag :: Prd a => Trip a (Either a a) Source #

bound :: Prd a => Bound a => Trip () a Source #

maybel :: Prd a => Bound b => Trip (Maybe a) (Either a b) Source #

mayber :: Prd b => Bound a => Trip (Maybe b) (Either a b) Source #