Data.Connection.Conn

Conn

data Kan

A data kind distinguishing the directionality of a Galois connection:

• L-tagged types are low / increasing (e.g. minimal, upper, ceiling, join)
• R-tagged types are high / decreasing (e.g. maximal, lower, floor, meet)

Constructors

L

R

data Conn (k :: Kan) a b

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

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)

Instances

Category (Conn k :: Type -> Type -> Type)

Defined in Data.Connection.Conn

Methods

id :: forall (a :: k0). Conn k a a

(.) :: forall (b :: k0) (c :: k0) (a :: k0). Conn k b c -> Conn k a b -> Conn k a c

pattern Conn :: (a -> b) -> (b -> a) -> (a -> b) -> Conn k a b

Obtain a Conn from an adjoint triple of monotone functions.

This is a view pattern for an arbitrary Conn. 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.

embed :: Conn k a b -> b -> a

Obtain the center of a ConnK, upper adjoint of a ConnL, or lower adjoint of a ConnR.

range :: Conn k a b -> a -> (b, b)

Obtain the upper and/or lower adjoints of a connection.

range c = floorWith c &&& ceilingWith c

>>> range f64f32 pi
(3.1415925,3.1415927)
>>> range f64f32 (0/0)
(NaN,NaN)

identity :: Conn k a a

The identity Conn.

Connection k

type ConnK a b = forall k. Conn k a b

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.

half :: (Num a, Preorder a) => ConnK a b -> a -> Maybe Ordering

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

 half t x = pcompare (x - lower t x) (upper t x - x)

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

midpoint :: Fractional a => ConnK a b -> a -> a

Return the midpoint of the interval containing x.

>>> pi - midpoint f64f32 pi
3.1786509424591713e-8

roundWith :: forall a b. (Num a, Preorder a) => ConnK a b -> a -> b

Return the nearest value to x.

roundWith 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).

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

roundWith1 :: (Num a, Preorder a) => ConnK a b -> (a -> a) -> b -> b

Lift a unary function over a ConnK.

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

roundWith2 :: (Num a, Preorder a) => ConnK a b -> (a -> a -> a) -> b -> b -> b

Lift a binary function over a ConnK.

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
>>> roundWith2 ratf32 f maxOdd32 2.0
2.0

truncateWith :: (Num a, Preorder a) => ConnK a b -> a -> b

Truncate towards zero.

truncateWith identity = id

truncateWith1 :: (Num a, Preorder a) => ConnK a b -> (a -> a) -> b -> b

Lift a unary function over a ConnK.

Results are truncated towards zero.

truncateWith1 identity = id

truncateWith2 :: (Num a, Preorder a) => ConnK a b -> (a -> a -> a) -> b -> b -> b

Connection L

type ConnL = Conn '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

A view pattern for a ConnL.

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

upL :: ConnL (Down a) (Down b) -> ConnL b a

Convert an inverted ConnL to a ConnL.

upL . downL = downL . upL = id

downL :: ConnL a b -> ConnL (Down b) (Down a)

Convert a ConnL to an inverted ConnL.

>>> upper (downL $ conn @_ @() @Ordering) (Down LT)
Down LT
>>> upper (downL $ conn @_ @() @Ordering) (Down GT)
Down LT

swapL :: ConnR a b -> ConnL b a

Witness to the symmetry between ConnL and ConnR.

swapL . swapR = id
swapR . swapL = id

counit :: ConnL a b -> b -> b

Reverse round trip through a ConnK or ConnL.

This is the counit of the resulting comonad:

x >~ counit c x

>>> counit (conn @_ @() @Ordering) LT
LT
>>> counit (conn @_ @() @Ordering) GT
LT

upper :: ConnL a b -> a -> a

Round trip through a ConnK or ConnL.

upper c = upper1 c id = embed c . ceilingWith c
x <= upper c x

>>> compare pi $ upper f64f32 pi
LT

upper1 :: ConnL a b -> (b -> b) -> a -> a

Map over a ConnK or ConnL from the right.

upper2 :: ConnL a b -> (b -> b -> b) -> a -> a -> a

Zip over a ConnK or ConnL from the right.

filterWith :: Preorder b => ConnL a b -> a -> b -> Bool

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 meet y is also in b.

filterWith and idealWith commute with Down:

filterWith c a b <=> idealWith c (Down a) (Down b)

filterWith c (Down a) (Down b) <=> idealWith c a b

filterWith c a is upward-closed for all a:

a <= b1 && b1 <= b2 => a <= b2

a1 <= b && inf a2 <= b => ceiling a1 `meet` ceiling a2 <= b

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

ceilingWith :: ConnL a b -> a -> b

Extract the left half of a ConnK or ConnL.

>>> floorWith f64f32 pi
3.1415925
>>> ceilingWith f64f32 pi
3.1415927

ceilingWith1 :: ConnL a b -> (a -> a) -> b -> b

Map over a ConnK or ConnL from the left.

ceilingWith2 :: ConnL a b -> (a -> a -> a) -> b -> b -> b

Zip over a ConnK or ConnL from the left.

Connection R

type ConnR = Conn '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 ConnK) that can lower into a standard connection in either of two ways.

pattern ConnR :: (b -> a) -> (a -> b) -> ConnR a b

A view pattern for a ConnR.

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

upR :: ConnR (Down a) (Down b) -> ConnR b a

Convert an inverted ConnR to a ConnR.

upR . downR = downR . upR = id

downR :: ConnR a b -> ConnR (Down b) (Down a)

Convert a ConnR to an inverted ConnR.

>>> lower (downR $ conn @_ @() @Ordering) (Down LT)
Down GT
>>> lower (downR $ conn @_ @() @Ordering) (Down GT)
Down GT

swapR :: ConnL a b -> ConnR b a

Witness to the symmetry between ConnL and ConnR.

swapL . swapR = id
swapR . swapL = id

unit :: ConnR a b -> b -> b

Round trip through a ConnK or ConnR.

This is the unit of the resulting monad:

x <~ unit c x
unit c = floorWith1 c id = floorWith c . embed c

>>> unit (conn @_ @() @Ordering) LT
GT
>>> unit (conn @_ @() @Ordering) GT
GT

lower :: ConnR a b -> a -> a

Reverse round trip through a ConnK or ConnR.

x >~ lower c x

>>> compare pi $ lower f64f32 pi
GT

lower1 :: ConnR a b -> (b -> b) -> a -> a

Map over a ConnK or ConnR from the left.

lower2 :: ConnR a b -> (b -> b -> b) -> a -> a -> a

Zip over a ConnK or ConnR from the left.

idealWith :: Preorder b => ConnR a b -> a -> b -> Bool

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 join y is also in B.

idealWith c a is downward-closed for all a:

a >= b1 && b1 >= b2 => a >= b2

a1 >= b && a2 >= b => floor a1 `join` floor a2 >= b

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

floorWith :: ConnR a b -> a -> b

Extract the right half of a ConnK or ConnR

This is the adjoint functor theorem for preorders.

>>> floorWith f64f32 pi
3.1415925
>>> ceilingWith f64f32 pi
3.1415927

floorWith1 :: ConnR a b -> (a -> a) -> b -> b

Map over a ConnK or ConnR from the right.

floorWith2 :: ConnR a b -> (a -> a -> a) -> b -> b -> b

Zip over a ConnK or ConnR from the right.

Combinators

(>>>) :: forall k cat (a :: k) (b :: k) (c :: k). Category cat => cat a b -> cat b c -> cat a c infixr 1

Left-to-right composition

(<<<) :: forall k cat (b :: k) (c :: k) (a :: k). Category cat => cat b c -> cat a b -> cat a c infixr 1

Right-to-left composition

choice :: Conn k a b -> Conn k c d -> Conn k (Either a c) (Either b d)

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

strong :: Conn k a b -> Conn k c d -> Conn k (a, c) (b, d)

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