| Safe Haskell | Safe |
|---|---|
| Language | Haskell2010 |
Data.Connection
Contents
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 :: Eq b => Prd a => Prd b => Conn a b -> a -> a -> Maybe Ordering
- dual :: Prd a => Prd b => Conn a b -> Conn (Down b) (Down a)
- (***) :: Prd a => Prd b => Prd c => Prd d => Conn a b -> Conn c d -> Conn (a, c) (b, d)
- (+++) :: 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 => Lattice 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
- _1 :: Prd a => Prd b => Prd c => Conn a b -> Conn (a, c) (b, c)
- _2 :: Prd a => Prd b => Prd c => Conn a b -> Conn (c, a) (c, b)
- _L :: Prd a => Prd b => Prd c => Conn a b -> Conn (Either a c) (Either b c)
- _R :: Prd a => Prd b => Prd c => Conn a b -> Conn (Either c a) (Either c b)
- just :: Prd a => Prd b => Conn a b -> Conn (Maybe a) (Maybe b)
- list :: Prd a => Prd b => Conn a b -> Conn [a] [b]
- binord :: Conn Bool Ordering
- ordbin :: Conn Ordering Bool
- 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
- ceiling' :: Prd a => Prd b => Trip a b -> a -> b
- floor' :: Prd a => Prd b => Trip a b -> a -> b
- (****) :: Prd a => Prd b => Prd c => Prd d => Trip a b -> Trip c d -> Trip (a, c) (b, d)
- (++++) :: Prd a => Prd b => Prd c => Prd d => Trip a b -> Trip c d -> Trip (Either a c) (Either b d)
- (&&&&) :: Prd a => Prd b => Lattice c => Trip a c -> Trip b c -> Trip (a, b) c
- (||||) :: Prd a => Prd b => Prd c => Trip c a -> Trip c b -> Trip c (Either a b)
- _1' :: Prd a => Prd b => Prd c => Trip a b -> Trip (a, c) (b, c)
- _2' :: Prd a => Prd b => Prd c => Trip a b -> Trip (c, a) (c, b)
- _L' :: Prd a => Prd b => Prd c => Trip a b -> Trip (Either a c) (Either b c)
- _R' :: Prd a => Prd b => Prd c => Trip a b -> Trip (Either c a) (Either c b)
- diag :: Lattice a => Trip (a, a) a
- codiag :: Prd a => Trip a (Either a a)
- bound :: Prd a => Bound a => Trip () a
- maybel :: Prd a => Bound b => Trip (Maybe a) (Either a b)
- mayber :: Prd b => Bound a => Trip (Maybe b) (Either a b)
Connection
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) |
(***) :: 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 #
Triple
(****) :: Prd a => Prd b => Prd c => Prd d => Trip a b -> Trip c d -> Trip (a, c) (b, d) infixr 3 Source #