Safe Haskell | Safe |
---|---|
Language | Haskell2010 |
Synopsis
- data Kan
- data Conn (k :: Kan) a b
- embed :: Conn k a b -> b -> a
- range :: Conn k a b -> a -> (b, b)
- identity :: Conn k a a
- (>>>) :: Category cat => cat a b -> cat b c -> cat a c
- (<<<) :: Category cat => cat b c -> cat a b -> cat a c
- mapped :: Functor f => Conn k a b -> Conn k (f a) (f 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)
- type ConnL = Conn L
- pattern ConnL :: (a -> b) -> (b -> a) -> ConnL a b
- connL :: ConnR a b -> ConnL b a
- upper :: ConnL a b -> b -> a
- upper1 :: ConnL a b -> (b -> b) -> a -> a
- upper2 :: ConnL a b -> (b -> b -> b) -> a -> a -> a
- join :: ConnL (a, a) b -> a -> a -> b
- ceiling :: ConnL a b -> a -> b
- ceiling1 :: ConnL a b -> (a -> a) -> b -> b
- ceiling2 :: ConnL a b -> (a -> a -> a) -> b -> b -> b
- type ConnR = Conn R
- pattern ConnR :: (b -> a) -> (a -> b) -> ConnR a b
- connR :: ConnL a b -> ConnR b a
- lower :: ConnR a b -> b -> a
- lower1 :: ConnR a b -> (b -> b) -> a -> a
- lower2 :: ConnR a b -> (b -> b -> b) -> a -> a -> a
- meet :: ConnR (a, a) b -> a -> a -> b
- floor :: ConnR a b -> a -> b
- floor1 :: ConnR a b -> (a -> a) -> b -> b
- floor2 :: ConnR a b -> (a -> a -> a) -> b -> b -> b
- pattern Conn :: (a -> b) -> (b -> a) -> (a -> b) -> Conn k a b
- half :: (Num a, Preorder a) => (forall k. Conn k a b) -> a -> Maybe Ordering
- midpoint :: Fractional a => (forall k. Conn k a b) -> a -> a
- round :: (Num a, Preorder a) => (forall k. Conn k a b) -> a -> b
- round1 :: (Num a, Preorder a) => (forall k. Conn k a b) -> (a -> a) -> b -> b
- round2 :: (Num a, Preorder a) => (forall k. Conn k a b) -> (a -> a -> a) -> b -> b -> b
- truncate :: (Num a, Preorder a) => (forall k. Conn k a b) -> a -> b
- truncate1 :: (Num a, Preorder a) => (forall k. Conn k a b) -> (a -> a) -> b -> b
- truncate2 :: (Num a, Preorder a) => (forall k. Conn k a b) -> (a -> a -> a) -> b -> b -> b
- upL :: ConnL (Down a) (Down b) -> ConnL b a
- upR :: ConnR (Down a) (Down b) -> ConnR b a
- downL :: ConnL a b -> ConnL (Down b) (Down a)
- downR :: ConnR a b -> ConnR (Down b) (Down a)
- filterL :: Preorder b => ConnL a b -> a -> b -> Bool
- filterR :: Preorder b => ConnR a b -> a -> b -> Bool
- newtype Down a = Down a
Conn
A data kind distinguishing the directionality of a Galois connection:
data Conn (k :: Kan) a b Source #
A (chain of) Galois connections.
A Galois connection between preorders P and Q is a pair of monotone maps `f :: p -> q` and `g :: q -> p` such that:
f x <= y iff x <= g y
We say that f
is the left or right adjoint, and g
is the right or left adjoint of the connection.
Connections have many nice properties wrt numerical conversion:
>>>
range (conn @_ @Rational @Float) (1 :% 8) -- eighths are exactly representable in a float
(0.125,0.125)>>>
range (conn @_ @Rational @Float) (1 :% 7) -- sevenths are not
(0.14285713,0.14285715)
See the README file for a slightly more in-depth introduction.
range :: Conn k a b -> a -> (b, b) Source #
Retrieve the left and/or right adjoints of a connection.
range c = floor c &&& ceiling c
>>>
range f64f32 pi
(3.1415925,3.1415927)>>>
range f64f32 (0/0)
(NaN,NaN)
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 L
pattern ConnL :: (a -> b) -> (b -> a) -> ConnL a b Source #
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 \} \)
Caution: ConnL f g must obey \(f \dashv g \). This condition is not checked.
For further information see Property
.
upper1 :: ConnL a b -> (b -> b) -> a -> a Source #
Map over a ConnL
from the right.
This is the unit of the resulting monad:
x <~ upper1 c id x
>>>
compare pi $ upper1 f64f32 id pi
LT
ceiling :: ConnL a b -> a -> b Source #
Extract the lower half of a ConnL
.
ceiling identity = id ceiling c (x \/ y) = ceiling c x \/ ceiling c y
The latter law is the adjoint functor theorem for preorders.
>>>
Data.Connection.ceiling ratf32 (0 :% 0)
NaN>>>
Data.Connection.ceiling ratf32 (1 :% 0)
Infinity>>>
Data.Connection.ceiling ratf32 (13 :% 10)
1.3000001>>>
Data.Connection.ceiling f64f32 pi
3.1415927
ceiling1 :: ConnL a b -> (a -> a) -> b -> b Source #
Map over a ConnL
from the left.
This is the counit of the resulting comonad:
x >~ ceiling1 c id x
>>>
ceiling1 (conn @_ @() @Ordering) id LT
LT>>>
ceiling1 (conn @_ @() @Ordering) id GT
LT
Connection R
pattern ConnR :: (b -> a) -> (a -> b) -> ConnR a b Source #
A Galois connection between two monotone functions.
ConnR
is the mirror image of ConnL
:
connR :: 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 that can lower into a standard connection in either of two ways.
Caution: ConnR f g must obey \(f \dashv g \). This condition is not checked.
For further information see Property
.
lower1 :: ConnR a b -> (b -> b) -> a -> a Source #
Map over a ConnR
from the left.
This is the counit of the resulting comonad:
x >~ lower1 c id x
>>>
compare pi $ lower1 f64f32 id pi
GT
floor :: ConnR a b -> a -> b Source #
Extract the upper half of a ConnR
floor identity = id floor c (x /\ y) = floor c x /\ floor c y
The latter law is the adjoint functor theorem for preorders.
>>>
Data.Connection.floor ratf32 (0 :% 0)
NaN>>>
Data.Connection.floor ratf32 (1 :% 0)
Infinity>>>
Data.Connection.floor ratf32 (13 :% 10)
1.3>>>
Data.Connection.floor f64f32 pi
3.1415925
floor1 :: ConnR a b -> (a -> a) -> b -> b Source #
Map over a ConnR
from the right.
This is the unit of the resulting monad:
x <~ floor1 c id x
>>>
floor1 (conn @_ @() @Ordering) id LT
GT>>>
floor1 (conn @_ @() @Ordering) id GT
GT
Connection k
pattern Conn :: (a -> b) -> (b -> a) -> (a -> b) -> 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 \)
When applied to a ConnL
or ConnR
, the two functions of type a -> b
returned will be identical.
Caution: Conn f g h must obey \(f \dashv g \dashv h\). This condition is not checked.
For detailed properties see Property
.
midpoint :: Fractional a => (forall k. Conn k a b) -> a -> a Source #
Return the midpoint of the interval containing x.
>>>
pi - midpoint f64f32 pi
3.1786509424591713e-8
round :: (Num a, Preorder a) => (forall k. Conn k a b) -> a -> b Source #
Return the nearest value to x.
round identity = id
If x lies halfway between two finite values, then return the value with the larger absolute value (i.e. round away from zero).
round1 :: (Num a, Preorder a) => (forall k. Conn k a b) -> (a -> a) -> b -> b Source #
Lift a unary function over a Trip
.
Results are rounded to the nearest value with ties away from 0.
round2 :: (Num a, Preorder a) => (forall k. Conn k a b) -> (a -> a -> a) -> b -> b -> b Source #
Lift a binary function over a Trip
.
Results are rounded to the nearest value with ties away from 0.
Example avoiding loss-of-precision:
>>>
f x y = (x + y) - x
>>>
maxOdd32 = 1.6777215e7
>>>
f maxOdd32 2.0 :: Float
1.0>>>
round2 ratf32 f maxOdd32 2.0
2.0
truncate :: (Num a, Preorder a) => (forall k. Conn k a b) -> a -> b Source #
Truncate towards zero.
truncate identity = id
truncate1 :: (Num a, Preorder a) => (forall k. Conn k a b) -> (a -> a) -> b -> b Source #
Lift a unary function over a Trip
.
Results are truncated towards zero.
truncate1 identity = id
Down
filterL :: Preorder b => ConnL 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 meet c x y
is also in b.
filterL and filterR commute with Down:
filterL c a b <=> ideal c (Down a) (Down b)
filterL c (Down a) (Down b) <=> ideal c a b
filterL c a is upward-closed for all a:
a <= b1 && b1 <= b2 => a <= b2 a1 <= b && a2 <= b => meet c (ceiling c a1) (ceiling c a2) <= b
filterR :: Preorder b => ConnR 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 join c x y is also in B.
filterR c a is downward-closed for all a:
a >= b1 && b1 >= b2 => a >= b2
a1 >= b && a2 >= b => join c (floor c a1) (floor c a2) >= b
The Down
type allows you to reverse sort order conveniently. A value of type
contains a value of type Down
aa
(represented as
).
If Down
aa
has an
instance associated with it then comparing two
values thus wrapped will give you the opposite of their normal sort order.
This is particularly useful when sorting in generalised list comprehensions,
as in: Ord
then sortWith by
Down
x
Since: base-4.6.0.0
Down a |
Instances
Monad Down | Since: base-4.11.0.0 |
Functor Down | Since: base-4.11.0.0 |
Applicative Down | Since: base-4.11.0.0 |
Foldable Down | Since: base-4.12.0.0 |
Defined in Data.Foldable fold :: Monoid m => Down m -> m # foldMap :: Monoid m => (a -> m) -> Down a -> m # foldr :: (a -> b -> b) -> b -> Down a -> b # foldr' :: (a -> b -> b) -> b -> Down a -> b # foldl :: (b -> a -> b) -> b -> Down a -> b # foldl' :: (b -> a -> b) -> b -> Down a -> b # foldr1 :: (a -> a -> a) -> Down a -> a # foldl1 :: (a -> a -> a) -> Down a -> a # elem :: Eq a => a -> Down a -> Bool # maximum :: Ord a => Down a -> a # | |
Traversable Down | Since: base-4.12.0.0 |
Eq1 Down | Since: base-4.12.0.0 |
Ord1 Down | Since: base-4.12.0.0 |
Defined in Data.Functor.Classes | |
Read1 Down | Since: base-4.12.0.0 |
Defined in Data.Functor.Classes | |
Show1 Down | Since: base-4.12.0.0 |
Eq a => Eq (Down a) | Since: base-4.6.0.0 |
Num a => Num (Down a) | Since: base-4.11.0.0 |
Ord a => Ord (Down a) | Since: base-4.6.0.0 |
Read a => Read (Down a) | Since: base-4.7.0.0 |
Show a => Show (Down a) | Since: base-4.7.0.0 |
Generic (Down a) | |
Semigroup a => Semigroup (Down a) | Since: base-4.11.0.0 |
Monoid a => Monoid (Down a) | Since: base-4.11.0.0 |
Preorder a => Preorder (Down a) Source # | |
Defined in Data.Order (<~) :: Down a -> Down a -> Bool Source # (>~) :: Down a -> Down a -> Bool Source # (?~) :: Down a -> Down a -> Bool Source # (~~) :: Down a -> Down a -> Bool Source # (/~) :: Down a -> Down a -> Bool Source # plt :: Down a -> Down a -> Bool Source # pgt :: Down a -> Down a -> Bool Source # similar :: Down a -> Down a -> Bool Source # pmax :: Down a -> Down a -> Maybe (Down a) Source # | |
Generic1 Down | |
type Rep (Down a) | Since: base-4.12.0.0 |
Defined in GHC.Generics | |
type Rep1 Down | Since: base-4.12.0.0 |
Defined in GHC.Generics |