Loading [MathJax]/jax/output/HTML-CSS/jax.js

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

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

connr(x)=sup{yEconnl(y)x}

connl(x)=inf{yEconnr(y)x}

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

x,y:connlconnrconnl(x)bxconnr(y)

x,y:xyconnl(x)connl(y)

x,y:xyconnr(x)connr(y)

x:connlconnrxconnrconnl(x)

x:connlconnrconnlconnr(x)x

x:unitunit(x)unit(x)

x:counitcounit(x)counit(x)

x:counitconnl(x)connl(x)

x:unitconnr(x)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 #