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'

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

See https://en.wikipedia.org/wiki/Lattice_(order).

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.

A view pattern for a ConnL.

Caution: ConnL f g must obey \(f \dashv g \). This condition is not checked.

A specialization of conn to left-side connections.

This is a convenience function provided primarily to avoid needing to enable DataKinds.

Witness to the symmetry between ConnL and ConnR.

swapL . swapR = id
swapR . swapL = id

Extract the center of a Trip or upper half of a ConnL.

Extract the ceiling of a Trip or lower half of a ConnL.

ceiling @a @a = id

>>> ceiling @Rational @Float (0 :% 0)
NaN
>>> ceiling @Rational @Float (1 :% 0)
Infinity
>>> ceiling @Rational @Float (13 :% 10)
1.3000001

Lift a unary function over a ConnL.

Lift a binary function over a ConnL.

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

See https://en.wikipedia.org/wiki/Filter_(mathematics)

A minimal element of a preorder defined by a connection with '()'.

minimal needn't be unique, but we must have:

x <~ minimal => x ~~ minimal

Semigroup operation on a join-semilattice.

(\/) = curry $ lowerL forked

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]

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.

A view pattern for a ConnR.

Caution: ConnR f g must obey \(f \dashv g \). This condition is not checked.

A specialization of conn to right-side connections.

This is a convenience function provided primarily to avoid needing to enable DataKinds.

Witness to the symmetry between ConnL and ConnR.

swapL . swapR = id
swapR . swapL = id

Extract the floor of a Trip or upper half of a ConnL.

floor @a @a = id

>>> floor @Rational @Float (0 :% 0)
NaN
>>> floor @Rational @Float (1 :% 0)
Infinity
>>> floor @Rational @Float (13 :% 10)
1.3

Lift a unary function over a ConnR.

Lift a binary function over a ConnR.

Extract the center of a Trip or lower half of a ConnR.

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

See https://en.wikipedia.org/wiki/Ideal_(order_theory)

A maximal element of a preorder defined by a connection with '()'.

maximal needn't be unique, but we must have:

x >~ maximal => x ~~ maximal

Semigroup operation on a meet-semilattice.

(/\) = curry $ upperR forked

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

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.

A view pattern for an arbitrary (left or right) Conn.

Caution: Conn f g h must obey \(f \dashv g \dashv h\). This condition is not checked.

For detailed properties see Property.

Determine which half of the interval between 2 representations of a a particular value lies.

 half t x = pcompare (x - counitR t x) (unitL t x - x)

Return the midpoint of the interval containing x.

>>> midpoint f32i08 4.3
4.5
>>> midpoint f64i08 4.3
4.5
>>> pi - midpoint f64f32 pi
3.1786509424591713e-8

>>> maybe False (~~ EQ) $ half f64f32 (midpoint f64f32 pi)
True

Return the nearest value to x.

round @a @a = id

If x lies halfway between two finite values, then return the value with the larger absolute value (i.e. round away from zero).

See https://en.wikipedia.org/wiki/Rounding.

Usable in conjunction with RebindableSyntax:

>>> fromRational = round
>>> fromRational @Float 1.3
1.3
>>> fromRational @Float (1 :% 0)
Infinity
>>> fromRational @Float (0 :% 0)
NaN

Lift a unary function over a Trip.

Results are rounded to the nearest value with ties away from 0.

Lift a binary function over a Trip.

Results are rounded to the nearest value with ties away from 0.

>>> f x y = (x + y) - x
>>> maxOdd32 = 1.6777215e7
>>> maxOdd64 = 9.007199254740991e15
>>> f maxOdd32 2.0 :: Float
1.0
>>> round2 @Rational @Float f maxOdd32 2.0
2.0
>>> f maxOdd64 2.0 :: Double
1.0
>>> round2 @Rational @Double f maxOdd64 2.0
2.0

Truncate towards zero.

truncate @a @a = id

Lift a unary function over a Trip.

Results are truncated towards 0.

Lift a binary function over a Trip.

Results are truncated towards 0.

Lift two Conns 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

Lift two Conns 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

Lift a Conn into a functor.

Caution: This function will result in an invalid connection if the functor alters the internal preorder (i.e. Down).

An adjoint string of Galois connections of length 2 or 3.

A constraint kind representing an adjoint triple of Galois connections.

An adjoint string of Galois connections of length 2 or 3.