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⊣connr
Each side of the adjunction may be defined in terms of the other:
connr(x)=sup{y∈E∣connl(y)≤x}
connl(x)=inf{y∈E∣connr(y)≥x}
Galois connections have the same properties as adjunctions defined over other categories:
∀x,y:connl⊣connr⇒connl(x)≤b⇔x≤connr(y)
∀x,y:x≤y⇒connl(x)≤connl(y)
∀x,y:x≤y⇒connr(x)≤connr(y)
∀x:connl⊣connr⇒x≤connr∘connl(x)
∀x:connl⊣connr⇒connl∘connr(x)≤x
∀x:unit∘unit(x)∼unit(x)
∀x:counit∘counit(x)∼counit(x)
∀x:counit∘connl(x)∼connl(x)
∀x:unit∘connr(x)∼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 #