Safe Haskell | Safe |
---|---|
Language | Haskell2010 |
Synopsis
- data Side
- data Cast (k :: Side) a b
- (>>>) :: 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 => Cast k a b -> Cast k (f a) (f b)
- choice :: Cast k a b -> Cast k c d -> Cast k (Either a c) (Either b d)
- select :: Cast k c a -> Cast k c b -> Cast k c (Either a b)
- strong :: Cast k a b -> Cast k c d -> Cast k (a, c) (b, d)
- divide :: Ord c => Cast k a c -> Cast k b c -> Cast k (a, b) c
- bounded :: Bounded a => Cast k () a
- ordered :: Ord a => Cast k (a, a) a
- identity :: Cast k a a
- pattern CastL :: (a -> b) -> (b -> a) -> Cast L a b
- swapL :: Cast R a b -> Cast L b a
- upper :: Cast L a b -> b -> a
- upper1 :: Cast L a b -> (b -> b) -> a -> a
- upper2 :: Cast L a b -> (b -> b -> b) -> a -> a -> a
- ceiling :: Cast L a b -> a -> b
- ceiling1 :: Cast L a b -> (a -> a) -> b -> b
- ceiling2 :: Cast L a b -> (a -> a -> a) -> b -> b -> b
- maximize :: Cast L (a, b) c -> a -> b -> c
- pattern CastR :: (b -> a) -> (a -> b) -> Cast R a b
- swapR :: Cast L a b -> Cast R b a
- lower :: Cast R a b -> b -> a
- lower1 :: Cast R a b -> (b -> b) -> a -> a
- lower2 :: Cast R a b -> (b -> b -> b) -> a -> a -> a
- floor :: Cast R a b -> a -> b
- floor1 :: Cast R a b -> (a -> a) -> b -> b
- floor2 :: Cast R a b -> (a -> a -> a) -> b -> b -> b
- minimize :: Cast R (a, b) c -> a -> b -> c
- pattern Cast :: (a -> b) -> (b -> a) -> (a -> b) -> Cast k a b
- midpoint :: Fractional a => (forall k. Cast k a b) -> a -> a
- interval :: (Num a, Preorder a) => (forall k. Cast k a b) -> a -> Maybe Ordering
- round :: (Num a, Preorder a) => (forall k. Cast k a b) -> a -> b
- round1 :: (Num a, Preorder a) => (forall k. Cast k a b) -> (a -> a) -> b -> b
- round2 :: (Num a, Preorder a) => (forall k. Cast k a b) -> (a -> a -> a) -> b -> b -> b
- truncate :: (Num a, Preorder a) => (forall k. Cast k a b) -> a -> b
- truncate1 :: (Num a, Preorder a) => (forall k. Cast k a b) -> (a -> a) -> b -> b
- truncate2 :: (Num a, Preorder a) => (forall k. Cast k a b) -> (a -> a -> a) -> b -> b -> b
- median :: (forall k. Cast k (a, a) a) -> a -> a -> a -> a
- upL :: Cast L (Down a) (Down b) -> Cast L b a
- upR :: Cast R (Down a) (Down b) -> Cast R b a
- downL :: Cast L a b -> Cast L (Down b) (Down a)
- downR :: Cast R a b -> Cast R (Down b) (Down a)
- filterL :: Preorder b => Cast L a b -> a -> b -> Bool
- filterR :: Preorder b => Cast R a b -> a -> b -> Bool
- extend :: (a -> Bool) -> (a -> Bool) -> (a -> b) -> a -> Extended b
- extended :: b -> b -> (a -> b) -> Extended a -> b
- data Extended r
Cast
A data kind distinguishing links in a chain of Galois connections of length 2 or 3.
- L-tagged types are increasing (e.g.
ceiling
,maximize
) - R-tagged types are decreasing (e.g.
floor
,minimize
)
If a connection is existentialized over this value (i.e. has type forall k. Cast k a b) then it can provide either of two functions f, h :: a -> b.
This is useful because it enables rounding, truncation, medians, etc.
data Cast (k :: Side) a b Source #
A chain of Galois connections of length 2 or 3.
Connections have many nice properties wrt numerical conversion:
>>>
upper ratf32 (1 / 8) -- eighths are exactly representable in a float
1 % 8>>>
upper ratf32 (1 / 7) -- sevenths are not
9586981 % 67108864>>>
floor ratf32 &&& ceiling ratf32 $ 1 % 8
(0.125,0.125)>>>
floor ratf32 &&& ceiling ratf32 $ 1 % 7
(0.14285713,0.14285715)
Another example avoiding loss-of-precision:
>>>
f x y = (x + y) - x
>>>
maxOdd32 = 1.6777215e7
>>>
f maxOdd32 2.0 :: Float
1.0>>>
round2 f64f32 f maxOdd32 2.0
2.0
choice :: Cast k a b -> Cast k c d -> Cast k (Either a c) (Either b d) Source #
Lift two connections into a connection 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
select :: Cast k c a -> Cast k c b -> Cast k c (Either a b) infixr 3 Source #
Lift two connections into a connection on the coproduct order
strong :: Cast k a b -> Cast k c d -> Cast k (a, c) (b, d) Source #
Lift two connections into a connection 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
divide :: Ord c => Cast k a c -> Cast k b c -> Cast k (a, b) c infixr 4 Source #
Lift two connections into a connection on the product order
ordered :: Ord a => Cast k (a, a) a Source #
The defining connections of a total order.
>>>
floor ordered &&& ceiling ordered $ (True, False)
(False,True)
Cast 'L
pattern CastL :: (a -> b) -> (b -> a) -> Cast L 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: CastL f g must obey \(f \dashv g \). This condition is not checked.
For further information see Property
.
upper :: Cast L a b -> b -> a Source #
Extract the upper half of a CastL
.
>>>
upper ratf32 (1 / 8) -- eighths are exactly representable in a float
1 % 8>>>
upper ratf32 (1 / 7) -- sevenths are not
9586981 % 67108864
upper1 :: Cast L a b -> (b -> b) -> a -> a Source #
Map over a CastL
from the right.
This is the unit of the resulting monad:
x <~ upper1 c id x
>>>
compare pi $ upper1 f64f32 id pi
LT
ceiling :: Cast L a b -> a -> b Source #
Extract the lower half of a CastL
.
ceiling identity = id ceiling c (x \/ y) = ceiling c x \/ ceiling c y
The latter law is the adjoint functor theorem for preorders.
>>>
ceiling ratf32 (0 :% 0)
NaN>>>
ceiling ratf32 (13 :% 10)
1.3000001>>>
ceiling f64f32 pi
3.1415927
ceiling1 :: Cast L a b -> (a -> a) -> b -> b Source #
Map over a CastL
from the left.
ceiling1 identity = id
This is the counit of the resulting comonad:
x >~ ceiling1 c id x
Cast 'R
pattern CastR :: (b -> a) -> (a -> b) -> Cast R a b Source #
A Galois connection between two monotone functions.
CastR
is the mirror image of CastL
.
If you only require one connection there is no particular reason to use one version over the other. However many use cases (e.g. rounding) require an adjoint triple of connections that can lower into a standard connection in either of two ways.
Caution: CastR f g must obey \(f \dashv g \). This condition is not checked.
For further information see Property
.
lower1 :: Cast R a b -> (b -> b) -> a -> a Source #
Map over a CastR
from the left.
This is the counit of the resulting comonad:
x >~ lower1 c id x
>>>
compare pi $ lower1 f64f32 id pi
GT
floor :: Cast R a b -> a -> b Source #
Extract the upper half of a CastR
floor identity = id floor c (x /\ y) = floor c x /\ floor c y
The latter law is the adjoint functor theorem for preorders.
>>>
floor ratf32 (0 :% 0)
NaN>>>
floor ratf32 (13 :% 10)
1.3>>>
floor f64f32 pi
3.1415925
floor1 :: Cast R a b -> (a -> a) -> b -> b Source #
Map over a CastR
from the right.
floor1 identity = id
This is the unit of the resulting monad:
x <~ floor1 c id x
Cast k
pattern Cast :: (a -> b) -> (b -> a) -> (a -> b) -> Cast 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 CastL
or CastR
, the two functions of type a -> b
returned will be identical.
Caution: Cast 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. Cast k a b) -> a -> a Source #
Return the midpoint of the interval containing x.
For example, the (double-precision) error of the single-precision floating point approximation of pi is:
>>>
pi - midpoint f64f32 pi
3.1786509424591713e-8
round :: (Num a, Preorder a) => (forall k. Cast 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 smaller absolute value (i.e. round towards from zero).
round1 :: (Num a, Preorder a) => (forall k. Cast k a b) -> (a -> a) -> b -> b Source #
Lift a unary function over an adjoint triple.
round1 identity = id
Results are rounded to the nearest value with ties away from 0.
round2 :: (Num a, Preorder a) => (forall k. Cast k a b) -> (a -> a -> a) -> b -> b -> b Source #
Lift a binary function over an adjoint triple.
round2 identity = id
Results are rounded to the nearest value with ties away from 0.
For example, to avoid a 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. Cast k a b) -> a -> b Source #
Truncate towards zero.
truncate identity = id
truncate1 :: (Num a, Preorder a) => (forall k. Cast k a b) -> (a -> a) -> b -> b Source #
Lift a unary function over an adjoint triple.
truncate1 identity = id
Results are truncated towards zero.
truncate2 :: (Num a, Preorder a) => (forall k. Cast k a b) -> (a -> a -> a) -> b -> b -> b Source #
Lift a binary function over an adjoint triple.
truncate2 identity = id
Results are truncated towards zero.
median :: (forall k. Cast k (a, a) a) -> a -> a -> a -> a Source #
Birkoff's median operator.
median x x y = x median x y z = median z x y median x y z = median x z y median (median x w y) w z = median x w (median y w z)
>>>
median f32f32 1.0 9.0 7.0
7.0>>>
median f32f32 1.0 9.0 (0.0 / 0.0)
9.0
Down
downL :: Cast L a b -> Cast L (Down b) (Down a) Source #
Invert a Cast
.
>>>
let counit = upper1 (downL $ bounded @Ordering) id
>>>
counit (Down LT)
Down LT>>>
counit (Down GT)
Down LT
downR :: Cast R a b -> Cast R (Down b) (Down a) Source #
Invert a Cast
.
>>>
let unit = lower1 (downR $ bounded @Ordering) id
>>>
unit (Down LT)
Down GT>>>
unit (Down GT)
Down GT
filterL :: Preorder b => Cast 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 meet c x y
is also in b.
filterL and filterR commute with Down:
filterL c a b <=> filterR c (Down a) (Down b)
filterL c (Down a) (Down b) <=> filterR c a b
filterL c a is upward-closed for all a:
a <= b1 && b1 <= b2 => a <= b2 a1 <= b && a2 <= b => minimize c (ceiling c a1) (ceiling c a2) <= b
filterR :: Preorder b => Cast 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 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 => maximize c (floor c a1) (floor c a2) >= b
Extended
Extended r
is an extension of r with positive/negative infinity (±∞).