Safe Haskell	Safe
Language	Haskell2010

Data.Connection

Contents

Connection
Triple

Synopsis

data Conn a b = Conn (a -> b) (b -> a)
connl :: Prd a => Prd b => Conn a b -> a -> b
connr :: Prd a => Prd b => Conn a b -> b -> a
unit :: Prd a => Prd b => Conn a b -> a -> a
counit :: Prd a => Prd b => Conn a b -> b -> b
pcomparing :: Prd a => Prd b => Conn a b -> a -> a -> Maybe Ordering
dual :: Prd a => Prd b => Conn a b -> Conn (Down b) (Down a)
first :: Prd a => Prd b => Prd c => Conn a b -> Conn (a, c) (b, c)
second :: Prd a => Prd b => Prd c => Conn a b -> Conn (c, a) (c, b)
left :: Prd a => Prd b => Prd c => Conn a b -> Conn (Either a c) (Either b c)
right :: Prd a => Prd b => Prd c => Conn a b -> Conn (Either c a) (Either c b)
strong :: Prd a => Prd b => Prd c => Prd d => Conn a b -> Conn c d -> Conn (a, c) (b, d)
choice :: Prd a => Prd b => Prd c => Prd d => Conn a b -> Conn c d -> Conn (Either a c) (Either b d)
(&&&) :: Prd a => Prd b => JoinSemilattice c => MeetSemilattice c => Conn c a -> Conn c b -> Conn c (a, b)
(|||) :: Prd a => Prd b => Prd c => Conn a c -> Conn b c -> Conn (Either a b) c
just :: Prd a => Prd b => Conn a b -> Conn (Maybe a) (Maybe b)
list :: Prd a => Prd b => Conn a b -> Conn [a] [b]
ordbin :: Conn Ordering Bool
binord :: Conn Bool Ordering
data Trip a b = Trip (a -> b) (b -> a) (a -> b)
tripl :: Prd a => Prd b => Trip a b -> Conn a b
tripr :: Prd a => Prd b => Trip a b -> Conn b a
unitl :: Prd a => Prd b => Trip a b -> a -> a
unitr :: Prd a => Prd b => Trip a b -> b -> b
counitl :: Prd a => Prd b => Trip a b -> b -> b
counitr :: Prd a => Prd b => Trip a b -> a -> a
bound :: Prd a => Bound a => Trip () a
first' :: Prd a => Prd b => Prd c => Trip a b -> Trip (a, c) (b, c)
second' :: Prd a => Prd b => Prd c => Trip a b -> Trip (c, a) (c, b)
left' :: Prd a => Prd b => Prd c => Trip a b -> Trip (Either a c) (Either b c)
right' :: Prd a => Prd b => Prd c => Trip a b -> Trip (Either c a) (Either c b)
strong' :: Prd a => Prd b => Prd c => Prd d => Trip a b -> Trip c d -> Trip (a, c) (b, d)
choice' :: Prd a => Prd b => Prd c => Prd d => Trip a b -> Trip c d -> Trip (Either a c) (Either b d)
forked :: JoinSemilattice a => MeetSemilattice a => Trip (a, a) a
joined :: Prd a => Trip a (Either a a)
maybel :: Prd a => Bound b => Trip (Maybe a) (Either a b)
mayber :: Prd b => Bound a => Trip (Maybe b) (Either a b)

Connection

data Conn a b Source #

A Galois connection between two monotone functions.

Each side of the connection 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) \)

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 #

Extract the left side of a connection.

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

Extract the right side of a connection.

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

Round trip through a connection.

x <= unit x

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

Reverse round trip through a connection.

counit x <= x

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

Partial version of comparing.

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

Reverse a connection using the dual partial order on each side.

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

first (ab >>> cd) = first ab >>> first cd

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

second (ab >>> cd) = second ab >>> second cd

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

left (ab >>> cd) = left ab >>> left cd

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

right (ab >>> cd) = right ab >>> right cd

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

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

(&&&) :: Prd a => Prd b => JoinSemilattice c => MeetSemilattice 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 #

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 #

ordbin :: Conn Ordering Bool Source #

binord :: Conn Bool Ordering 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 #

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

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

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

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

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

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

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

forked :: JoinSemilattice a => MeetSemilattice a => Trip (a, a) a Source #

joined :: Prd a => Trip a (Either a 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 #