Safe Haskell | Safe |
---|---|
Language | Haskell2010 |
Synopsis
- data Kan
- data Conn (k :: Kan) a b
- type Semilattice k a = Connection k (a, a) a
- type Extremal k = Connection k ()
- type ConnFloat k = Connection k Float
- type ConnDouble k = Connection k Double
- type ConnInteger k = Connection k (Maybe Integer)
- type ConnRational k = Connection k Rational
- type ConnExtended k a b = Connection k a (Extended b)
- type ConnL = Conn L
- pattern ConnL :: (a -> b) -> (b -> a) -> ConnL a b
- connL :: Connection L a b => ConnL a b
- swapL :: ConnR a b -> ConnL b a
- embedL :: Connection L a b => b -> a
- ceiling :: Connection L a b => a -> b
- ceiling1 :: Connection L a b => (a -> a) -> b -> b
- ceiling2 :: Connection L a b => (a -> a -> a) -> b -> b -> b
- filterL :: Connection L a b => a -> b -> Bool
- minimal :: Extremal L a => a
- (\/) :: Semilattice L a => a -> a -> a
- glb :: Triple (a, a) a => a -> a -> a -> a
- type ConnR = Conn R
- pattern ConnR :: (b -> a) -> (a -> b) -> ConnR a b
- connR :: Connection R a b => ConnR a b
- swapR :: ConnL a b -> ConnR b a
- floor :: Connection R a b => a -> b
- floor1 :: Connection R a b => (a -> a) -> b -> b
- floor2 :: Connection R a b => (a -> a -> a) -> b -> b -> b
- embedR :: Connection R a b => b -> a
- filterR :: Connection R a b => a -> b -> Bool
- maximal :: Extremal R a => a
- (/\) :: Semilattice R a => a -> a -> a
- lub :: Triple (a, a) a => a -> a -> a -> a
- type Trip a b = forall k. Conn k a b
- pattern Conn :: (a -> b) -> (b -> a) -> (a -> b) -> Conn k a b
- maybeL :: Triple () b => Trip (Maybe a) (Either a b)
- maybeR :: Triple () a => Trip (Maybe b) (Either a b)
- choice :: Conn k a b -> Conn k c d -> Conn k (Either a c) (Either b d)
- strong :: Conn k a b -> Conn k c d -> Conn k (a, c) (b, d)
- fmapped :: Functor f => Conn k a b -> Conn k (f a) (f b)
- class (Preorder a, Preorder b) => Connection k a b where
- type Triple a b = (Connection L a b, Connection R a b)
Types
A data kind distinguishing the chirality of a Kan extension.
Here it serves to distinguish the directionality of a preorder:
- L-tagged types are 'upwards-directed'
- R-tagged types are 'downwards-directed'
data Conn (k :: Kan) a b Source #
An adjoint string of Galois connections of length 2 or 3.
type Semilattice k a = Connection k (a, a) a Source #
Semilattices.
A complete is a partially ordered set in which every two elements have a unique join (least upper bound or supremum) and a unique meet (greatest lower bound or infimum).
These operations may in turn be defined by the lower and upper adjoints to the unique function a -> (a, a).
Associativity
x\/
(y\/
z) = (x\/
y)\/
z x/\
(y/\
z) = (x/\
y)/\
z
Commutativity
x\/
y = y\/
x x/\
y = y/\
x
Idempotency
x\/
x = x x/\
x = x
Absorption
(x\/
y)/\
y = y (x/\
y)\/
y = y
See Absorption.
Note that distributivity is _not_ a requirement for a complete. However when a is distributive we have;
glb
x y z =lub
x y z
type Extremal k = Connection k () Source #
type ConnFloat k = Connection k Float Source #
type ConnDouble k = Connection k Double Source #
type ConnInteger k = Connection k (Maybe Integer) Source #
type ConnRational k = Connection k Rational Source #
type ConnExtended k a b = Connection k a (Extended b) Source #
Connection L
A Galois connection between two monotone functions.
A Galois connection between f and g, written \(f \dashv g \) is an adjunction in the category of preorders.
Each side of the connection may be defined in terms of the other:
\( g(x) = \sup \{y \in E \mid f(y) \leq x \} \)
\( f(x) = \inf \{y \in E \mid g(y) \geq x \} \)
For further information see Property
.
Caution: Monotonicity is not checked.
pattern ConnL :: (a -> b) -> (b -> a) -> ConnL a b Source #
A view pattern for a ConnL
.
Caution: ConnL f g must obey \(f \dashv g \). This condition is not checked.
connL :: Connection L a b => ConnL a b Source #
A specialization of conn to left-side connections.
This is a convenience function provided primarily to avoid needing to enable DataKinds.
ceiling :: Connection L a b => a -> b Source #
ceiling2 :: Connection L a b => (a -> a -> a) -> b -> b -> b Source #
Lift a binary function over a ConnL
.
filterL :: Connection L a b => a -> b -> Bool Source #
Obtain the principal filter in B generated by an element of A.
A subset B of a lattice is an filter if and only if it is an upper set
that is closed under finite meets, i.e., it is nonempty and for all
x, y in B, the element x / y
is also in b.
filterL and filterR commute with Down:
filterL a b <=> filterR (Down a) (Down b)
filterL (Down a) (Down b) <=> filterR a b
filterL a is upward-closed for all a:
a <= b1 && b1 <= b2 => a <= b2
a1 <= b && inf a2 <= b => ceiling a1 /\ ceiling a2 <= b
minimal :: Extremal L a => a Source #
A minimal element of a preorder defined by a connection with '()'.
minimal
needn't be unique, but we must have:
x <~ minimal => x ~~ minimal
(\/) :: Semilattice L a => a -> a -> a infixr 5 Source #
Semigroup operation on a join-semilattice.
(\/) = curry $ lowerL forked
glb :: Triple (a, a) a => a -> a -> a -> a Source #
Greatest lower bound operator.
glb x x y = x glb x y z = glb z x y glb x x y = x glb x y z = glb x z y glb (glb x w y) w z = glb x w (glb y w z)
>>>
glb 1.0 9.0 7.0
7.0>>>
glb 1.0 9.0 (0.0 / 0.0)
9.0>>>
glb (fromList [1..3]) (fromList [3..5]) (fromList [5..7]) :: Set Int
fromList [3,5]
Connection R
A Galois connection between two monotone functions.
ConnR
is the mirror image of ConnL
:
swapR :: ConnL a b -> ConnR b a
If you only require one connection there is no particular reason to use one version over the other.
However some use cases (e.g. rounding) require an adjoint triple
of connections (i.e. a Trip
) that can lower into a standard
connection in either of two ways.
pattern ConnR :: (b -> a) -> (a -> b) -> ConnR a b Source #
A view pattern for a ConnR
.
Caution: ConnR f g must obey \(f \dashv g \). This condition is not checked.
connR :: Connection R a b => ConnR a b Source #
A specialization of conn to right-side connections.
This is a convenience function provided primarily to avoid needing to enable DataKinds.
floor :: Connection R a b => a -> b Source #
floor2 :: Connection R a b => (a -> a -> a) -> b -> b -> b Source #
Lift a binary function over a ConnR
.
filterR :: Connection R a b => a -> b -> Bool Source #
Obtain the principal ideal in B generated by an element of A.
A subset B of a lattice is an ideal if and only if it is a lower set that is closed under finite joins, i.e., it is nonempty and for all x, y in B, the element x / y is also in B.
filterR a is downward-closed for all a:
a >= b1 && b1 >= b2 => a >= b2
a1 >= b && a2 >= b => floor a1 \/ floor a2 >= b
maximal :: Extremal R a => a Source #
A maximal element of a preorder defined by a connection with '()'.
maximal
needn't be unique, but we must have:
x >~ maximal => x ~~ maximal
(/\) :: Semilattice R a => a -> a -> a infixr 6 Source #
Semigroup operation on a meet-semilattice.
(/\) = curry $ upperR forked
lub :: Triple (a, a) a => a -> a -> a -> a Source #
Least upper bound operator.
The order dual of glb
.
>>>
lub 1.0 9.0 7.0
7.0>>>
lub 1.0 9.0 (0.0 / 0.0)
1.0
Connection k
type Trip a b = forall k. Conn k a b Source #
An adjoint triple of Galois connections.
An adjoint triple is a chain of connections of length 3:
\(f \dashv g \dashv h \)
For detailed properties see Property
.
choice :: Conn k a b -> Conn k c d -> Conn k (Either a c) (Either b d) Source #
Lift two Conn
s into a Conn
on the coproduct order
(choice id) (ab >>> cd) = (choice id) ab >>> (choice id) cd (flip choice id) (ab >>> cd) = (flip choice id) ab >>> (flip choice id) cd
strong :: Conn k a b -> Conn k c d -> Conn k (a, c) (b, d) Source #
Lift two Conn
s into a Conn
on the product order
(strong id) (ab >>> cd) = (strong id) ab >>> (strong id) cd (flip strong id) (ab >>> cd) = (flip strong id) ab >>> (flip strong id) cd
Connection
class (Preorder a, Preorder b) => Connection k a b where Source #
An adjoint string of Galois connections of length 2 or 3.
>>>
range (conn @_ @Double @Float) pi
(3.1415925,3.1415927)>>>
range (conn @_ @Rational @Float) (1 :% 7)
(0.14285713,0.14285715)>>>
range (conn @_ @Rational @Float) (1 :% 8)
(0.125,0.125)
Instances
type Triple a b = (Connection L a b, Connection R a b) Source #
A constraint kind representing an adjoint triple of Galois connections.