Safe Haskell	Safe
Language	Haskell2010
Extensions	PatternSynonyms

Data.Connection

Contents

Types
Combinators
Accessors
Connections
Extended

Description

This library provides connections between common types, combinators & accessors, including lawful versions of floor, ceiling, round, and truncate. There is also a separately exported Connection class, along with lawful versions of fromInteger and fromRational, suitable for use with -XRebindableSyntax. Lastly, there are Semilattice and Algebra classes based on the same construction.

connections is extensively tested, and it exports properties for use in testing your own connections. See Data.Connection.Property and Data.Lattice.Property. In addition to the property tests there are several doctests scattered around, these are runnable as a standalone executable. See the doctest stanza in the library's cabal file.

Synopsis

data Conn (k :: Side) a b
data Side
- = L
- | R
type ConnL = Conn L
connL :: Conn R a b -> Conn L b a
pattern ConnL :: (a -> b) -> (b -> a) -> Conn L a b
type ConnR = Conn R
connR :: Conn L a b -> Conn R b a
pattern ConnR :: (b -> a) -> (a -> b) -> Conn R a b
pattern Conn :: (a -> b) -> (b -> a) -> (a -> b) -> Conn k 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 => 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)
select :: Conn k c a -> Conn k c b -> Conn k c (Either a b)
strong :: Conn k a b -> Conn k c d -> Conn k (a, c) (b, d)
divide :: Total c => Conn k a c -> Conn k b c -> Conn k (a, b) c
upper :: Conn L a b -> b -> a
lower :: Conn R a b -> b -> a
inner :: Conn k a b -> b -> a
outer :: Conn k a b -> a -> (b, b)
maximize :: Conn L (a, b) c -> a -> b -> c
minimize :: Conn R (a, b) c -> a -> b -> c
median :: (forall k. Conn k (a, a) a) -> a -> a -> a -> a
ceiling :: Conn L a b -> a -> b
ceiling1 :: Conn L a b -> (a -> a) -> b -> b
ceiling2 :: Conn L a b -> (a -> a -> a) -> b -> b -> b
floor :: Conn R a b -> a -> b
floor1 :: Conn R a b -> (a -> a) -> b -> b
floor2 :: Conn R a b -> (a -> a -> a) -> b -> b -> b
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
bounded :: Bounded a => Conn k () a
ordered :: Total a => Conn k (a, a) a
identity :: Conn k a a
i08w08 :: Conn L Int8 Word8
f32w08 :: Conn k Float (Extended Word8)
f64w08 :: Conn k Double (Extended Word8)
ratw08 :: Conn k Rational (Extended Word8)
w08w16 :: Conn L Word8 Word16
i08w16 :: Conn L Int8 Word16
i16w16 :: Conn L Int16 Word16
f32w16 :: Conn k Float (Extended Word16)
f64w16 :: Conn k Double (Extended Word16)
ratw16 :: Conn k Rational (Extended Word16)
w08w32 :: Conn L Word8 Word32
w16w32 :: Conn L Word16 Word32
i08w32 :: Conn L Int8 Word32
i16w32 :: Conn L Int16 Word32
i32w32 :: Conn L Int32 Word32
f64w32 :: Conn k Double (Extended Word32)
ratw32 :: Conn k Rational (Extended Word32)
w08w64 :: Conn L Word8 Word64
w16w64 :: Conn L Word16 Word64
w32w64 :: Conn L Word32 Word64
i08w64 :: Conn L Int8 Word64
i16w64 :: Conn L Int16 Word64
i32w64 :: Conn L Int32 Word64
i64w64 :: Conn L Int64 Word64
ixxw64 :: Conn L Int Word64
ratw64 :: Conn k Rational (Extended Word64)
w08wxx :: Conn L Word8 Word
w16wxx :: Conn L Word16 Word
w32wxx :: Conn L Word32 Word
w64wxx :: Conn k Word64 Word
i08wxx :: Conn L Int8 Word
i16wxx :: Conn L Int16 Word
i32wxx :: Conn L Int32 Word
i64wxx :: Conn L Int64 Word
ixxwxx :: Conn L Int Word
ratwxx :: Conn k Rational (Extended Word)
w08nat :: Conn L Word8 Natural
w16nat :: Conn L Word16 Natural
w32nat :: Conn L Word32 Natural
w64nat :: Conn L Word64 Natural
wxxnat :: Conn L Word Natural
i08nat :: Conn L Int8 Natural
i16nat :: Conn L Int16 Natural
i32nat :: Conn L Int32 Natural
i64nat :: Conn L Int64 Natural
ixxnat :: Conn L Int Natural
intnat :: Conn L Integer Natural
ratnat :: Conn k Rational (Extended Natural)
f32i08 :: Conn k Float (Extended Int8)
f64i08 :: Conn k Double (Extended Int8)
rati08 :: Conn k Rational (Extended Int8)
w08i16 :: Conn L Word8 (Maybe Int16)
i08i16 :: Conn L Int8 (Maybe Int16)
f32i16 :: Conn k Float (Extended Int16)
f64i16 :: Conn k Double (Extended Int16)
rati16 :: Conn k Rational (Extended Int16)
w08i32 :: Conn L Word8 (Maybe Int32)
w16i32 :: Conn L Word16 (Maybe Int32)
i08i32 :: Conn L Int8 (Maybe Int32)
i16i32 :: Conn L Int16 (Maybe Int32)
f64i32 :: Conn k Double (Extended Int32)
rati32 :: Conn k Rational (Extended Int32)
w08i64 :: Conn L Word8 (Maybe Int64)
w16i64 :: Conn L Word16 (Maybe Int64)
w32i64 :: Conn L Word32 (Maybe Int64)
i08i64 :: Conn L Int8 (Maybe Int64)
i16i64 :: Conn L Int16 (Maybe Int64)
i32i64 :: Conn L Int32 (Maybe Int64)
rati64 :: Conn k Rational (Extended Int64)
w08ixx :: Conn L Word8 (Maybe Int)
w16ixx :: Conn L Word16 (Maybe Int)
w32ixx :: Conn L Word32 (Maybe Int)
i08ixx :: Conn L Int8 (Maybe Int)
i16ixx :: Conn L Int16 (Maybe Int)
i32ixx :: Conn L Int32 (Maybe Int)
i64ixx :: Conn k Int64 Int
ratixx :: Conn k Rational (Extended Int)
sysixx :: Conn k SystemTime Int
w08int :: Conn L Word8 (Maybe Integer)
w16int :: Conn L Word16 (Maybe Integer)
w32int :: Conn L Word32 (Maybe Integer)
w64int :: Conn L Word64 (Maybe Integer)
wxxint :: Conn L Word (Maybe Integer)
natint :: Conn L Natural (Maybe Integer)
i08int :: Conn L Int8 (Maybe Integer)
i16int :: Conn L Int16 (Maybe Integer)
i32int :: Conn L Int32 (Maybe Integer)
i64int :: Conn L Int64 (Maybe Integer)
ixxint :: Conn L Int (Maybe Integer)
f00int :: Conn k Uni Integer
ratint :: Conn k Rational (Extended Integer)
ratrat :: Conn k (Rational, Rational) Rational
f32f32 :: Conn k (Float, Float) Float
f64f32 :: Conn k Double Float
ratf32 :: Conn k Rational Float
f64f64 :: Conn k (Double, Double) Double
ratf64 :: Conn k Rational Double
f32fix :: HasResolution e => Conn L Float (Extended (Fixed e))
f64fix :: HasResolution e => Conn L Double (Extended (Fixed e))
ratfix :: forall e k. HasResolution e => Conn k Rational (Extended (Fixed e))
f01f00 :: Conn k Deci Uni
f02f00 :: Conn k Centi Uni
f03f00 :: Conn k Milli Uni
f06f00 :: Conn k Micro Uni
f09f00 :: Conn k Nano Uni
f12f00 :: Conn k Pico Uni
f02f01 :: Conn k Centi Deci
f03f01 :: Conn k Milli Deci
f06f01 :: Conn k Micro Deci
f09f01 :: Conn k Nano Deci
f12f01 :: Conn k Pico Deci
f03f02 :: Conn k Milli Centi
f06f02 :: Conn k Micro Centi
f09f02 :: Conn k Nano Centi
f12f02 :: Conn k Pico Centi
f06f03 :: Conn k Micro Milli
f09f03 :: Conn k Nano Milli
f12f03 :: Conn k Pico Milli
f09f06 :: Conn k Nano Micro
f12f06 :: Conn k Pico Micro
f12f09 :: Conn k Pico Nano
f32sys :: Conn L Float (Extended SystemTime)
f64sys :: Conn L Double (Extended SystemTime)
f09sys :: Conn k (Extended Nano) (Extended SystemTime)
ratsys :: Conn k Rational (Extended SystemTime)
extended :: b -> b -> (a -> b) -> Extended a -> b
data Extended r
- = NegInf
- | Finite !r
- | PosInf

Documentation

What is a Galois connection?

A Galois connection is an adjunction in the category of preorders: a pair of monotone maps f :: p -> q and g :: q -> p between preorders p and q, such that

f x <= y if and only if x <= g y

We say that f is the left or lower adjoint, and g is the right or upper adjoint of the connection.

For illustration, here is a simple example from 7 Sketches:

example

Note that the two component functions are each monotonic:

 x1 <= x2 implies f x1 <= f x2

and furthermore they are are interlocked (i.e. adjoint) in the specific way outlined above:

 f x <= y if and only if x <= g y

See the README for a more extensive overview.

Types

data Conn (k :: Side) a b Source #

A chain of Galois connections of length 2 or 3.

Connections have many nice properties wrt numerical conversion:

>>> inner ratf32 (1 / 8)    -- eighths are exactly representable in a float
1 % 8
>>> outer ratf32 (1 % 8)
(0.125,0.125)
>>> inner ratf32 (1 / 7)    -- sevenths are not
9586981 % 67108864
>>> outer 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

See the README file for a slightly more in-depth introduction.

Instances

Category (Conn k :: Type -> Type -> Type) Source #
Instance details Defined in Data.Connection.Conn Methods id :: Conn k a a # (.) :: Conn k b c -> Conn k a b -> Conn k a c #

data Side Source #

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. Conn 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.

Constructors

L
R

Conn L

type ConnL = Conn L Source #

connL :: Conn R a b -> Conn L b a Source #

Witness to the mirror symmetry between ConnL and ConnR.

connL . connR = id
connR . connL = id

pattern ConnL :: (a -> b) -> (b -> a) -> Conn 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: ConnL f g must obey $f \dashv g $. This condition is not checked.

For further information see Property.

Conn R

type ConnR = Conn R Source #

connR :: Conn L a b -> Conn R b a Source #

Witness to the mirror symmetry between ConnL and ConnR.

connL . connR = id
connR . connL = id

pattern ConnR :: (b -> a) -> (a -> b) -> Conn R 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.

Conn 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.

Combinators

(>>>) :: Category cat => cat a b -> cat b c -> cat a c infixr 1 #

Left-to-right composition

(<<<) :: Category cat => cat b c -> cat a b -> cat a c infixr 1 #

Right-to-left composition

mapped :: Functor f => Conn k a b -> Conn k (f a) (f b) Source #

Lift a Conn into a functor.

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

choice :: Conn k a b -> Conn k c d -> Conn 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 :: Conn k c a -> Conn k c b -> Conn k c (Either a b) infixr 3 Source #

Lift two connections into a connection on the coproduct order

strong :: Conn k a b -> Conn k c d -> Conn 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 :: Total c => Conn k a c -> Conn k b c -> Conn k (a, b) c infixr 4 Source #

Lift two connections into a connection on the product order

Accessors

upper :: Conn L a b -> b -> a Source #

Extract the upper adjoint of a ConnL.

lower :: Conn R a b -> b -> a Source #

Extract the lower adjoint of a ConnR.

inner :: Conn k a b -> b -> a Source #

Extract the upper adjoint of a ConnL, or lower adjoint of a ConnR.

When the connection is an adjoint triple the inner function is returned:

>>> inner ratf32 (1 / 8)    -- eighths are exactly representable in a float
1 % 8
>>> inner ratf32 (1 / 7)    -- sevenths are not
9586981 % 67108864

outer :: Conn k a b -> a -> (b, b) Source #

Extract the left and/or right adjoints of a connection.

When the connection is an adjoint triple the outer functions are returned:

outer c = floor c &&& ceiling c

>>> outer ratf32 (1 % 8)    -- eighths are exactly representable in a float
(0.125,0.125)
>>> outer ratf32 (1 % 7)    -- sevenths are not
(0.14285713,0.14285715)

max/min

maximize :: Conn L (a, b) c -> a -> b -> c Source #

Generalized maximum.

minimize :: Conn R (a, b) c -> a -> b -> c Source #

Generalized minimum.

median :: (forall k. Conn 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

ceiling

ceiling :: Conn L 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 (13 :% 10)
1.3000001
>>> Data.Connection.ceiling f64f32 pi
3.1415927

ceiling1 :: Conn L a b -> (a -> a) -> b -> b Source #

Map over a ConnL from the left.

ceiling1 identity = id

This is the counit of the resulting comonad:

x >~ ceiling1 c id x

ceiling2 :: Conn L a b -> (a -> a -> a) -> b -> b -> b Source #

Zip over a ConnL from the left.

floor

floor :: Conn R 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 (13 :% 10)
1.3
>>> Data.Connection.floor f64f32 pi
3.1415925

floor1 :: Conn R a b -> (a -> a) -> b -> b Source #

Map over a ConnR from the right.

floor1 identity = id

This is the unit of the resulting monad:

x <~ floor1 c id x

floor2 :: Conn R a b -> (a -> a -> a) -> b -> b -> b Source #

Zip over a ConnR from the right.

round

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 smaller absolute value (i.e. round towards from zero).

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

round1 :: (Num a, Preorder a) => (forall k. Conn 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. Conn 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.

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

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 an adjoint triple.

truncate1 identity = id

Results are truncated towards zero.

truncate2 :: (Num a, Preorder a) => (forall k. Conn 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.

Connections

bounded :: Bounded a => Conn k () a Source #

The defining connections of a bounded preorder.

ordered :: Total a => Conn k (a, a) a Source #

The defining connections of a total order.

>>> outer ordered (True, False)
(False,True)

identity :: Conn k a a Source #

The identity connection.

Unsigned ints

Caution: This assumes that Word on your system is 64 bits.

i08wxx :: Conn L Int8 Word Source #

i16wxx :: Conn L Int16 Word Source #

i32wxx :: Conn L Int32 Word Source #

i64wxx :: Conn L Int64 Word Source #

ixxwxx :: Conn L Int Word Source #

ratwxx :: Conn k Rational (Extended Word) Source #

Natural

w08nat :: Conn L Word8 Natural Source #

w16nat :: Conn L Word16 Natural Source #

w32nat :: Conn L Word32 Natural Source #

w64nat :: Conn L Word64 Natural Source #

wxxnat :: Conn L Word Natural Source #

i08nat :: Conn L Int8 Natural Source #

i16nat :: Conn L Int16 Natural Source #

i32nat :: Conn L Int32 Natural Source #

i64nat :: Conn L Int64 Natural Source #

ixxnat :: Conn L Int Natural Source #

intnat :: Conn L Integer Natural Source #

ratnat :: Conn k Rational (Extended Natural) Source #

Signed ints

Int8

f32i08 :: Conn k Float (Extended Int8) Source #

f64i08 :: Conn k Double (Extended Int8) Source #

rati08 :: Conn k Rational (Extended Int8) Source #

Int16

w08i16 :: Conn L Word8 (Maybe Int16) Source #

i08i16 :: Conn L Int8 (Maybe Int16) Source #

f32i16 :: Conn k Float (Extended Int16) Source #

f64i16 :: Conn k Double (Extended Int16) Source #

rati16 :: Conn k Rational (Extended Int16) Source #

Int32

w08i32 :: Conn L Word8 (Maybe Int32) Source #

w16i32 :: Conn L Word16 (Maybe Int32) Source #

i08i32 :: Conn L Int8 (Maybe Int32) Source #

i16i32 :: Conn L Int16 (Maybe Int32) Source #

f64i32 :: Conn k Double (Extended Int32) Source #

rati32 :: Conn k Rational (Extended Int32) Source #

Int64

w08i64 :: Conn L Word8 (Maybe Int64) Source #

w16i64 :: Conn L Word16 (Maybe Int64) Source #

w32i64 :: Conn L Word32 (Maybe Int64) Source #

i08i64 :: Conn L Int8 (Maybe Int64) Source #

i16i64 :: Conn L Int16 (Maybe Int64) Source #

i32i64 :: Conn L Int32 (Maybe Int64) Source #

rati64 :: Conn k Rational (Extended Int64) Source #

Int

w08ixx :: Conn L Word8 (Maybe Int) Source #

w16ixx :: Conn L Word16 (Maybe Int) Source #

w32ixx :: Conn L Word32 (Maybe Int) Source #

i08ixx :: Conn L Int8 (Maybe Int) Source #

i16ixx :: Conn L Int16 (Maybe Int) Source #

i32ixx :: Conn L Int32 (Maybe Int) Source #

i64ixx :: Conn k Int64 Int Source #

Caution: This assumes that Int on your system is 64 bits.

ratixx :: Conn k Rational (Extended Int) Source #

sysixx :: Conn k SystemTime Int Source #

The Int is valued in seconds

Integer

w08int :: Conn L Word8 (Maybe Integer) Source #

w16int :: Conn L Word16 (Maybe Integer) Source #

w32int :: Conn L Word32 (Maybe Integer) Source #

w64int :: Conn L Word64 (Maybe Integer) Source #

wxxint :: Conn L Word (Maybe Integer) Source #

natint :: Conn L Natural (Maybe Integer) Source #

i08int :: Conn L Int8 (Maybe Integer) Source #

i16int :: Conn L Int16 (Maybe Integer) Source #

i32int :: Conn L Int32 (Maybe Integer) Source #

i64int :: Conn L Int64 (Maybe Integer) Source #

ixxint :: Conn L Int (Maybe Integer) Source #

f00int :: Conn k Uni Integer Source #

ratint :: Conn k Rational (Extended Integer) Source #

ratf32 :: Conn k Rational Float Source #

Double

f64f64 :: Conn k (Double, Double) Double Source #

ratf64 :: Conn k Rational Double Source #

Fixed point

f32fix :: HasResolution e => Conn L Float (Extended (Fixed e)) Source #

f64fix :: HasResolution e => Conn L Double (Extended (Fixed e)) Source #

ratfix :: forall e k. HasResolution e => Conn k Rational (Extended (Fixed e)) Source #

Uni

f01f00 :: Conn k Deci Uni Source #

f02f00 :: Conn k Centi Uni Source #

f03f00 :: Conn k Milli Uni Source #

f06f00 :: Conn k Micro Uni Source #

f09f00 :: Conn k Nano Uni Source #

f12f00 :: Conn k Pico Uni Source #

Deci

f02f01 :: Conn k Centi Deci Source #

f03f01 :: Conn k Milli Deci Source #

f06f01 :: Conn k Micro Deci Source #

f09f01 :: Conn k Nano Deci Source #

f12f01 :: Conn k Pico Deci Source #

Centi

f03f02 :: Conn k Milli Centi Source #

f06f02 :: Conn k Micro Centi Source #

f09f02 :: Conn k Nano Centi Source #

f12f02 :: Conn k Pico Centi Source #

Milli

f06f03 :: Conn k Micro Milli Source #

f09f03 :: Conn k Nano Milli Source #

f12f03 :: Conn k Pico Milli Source #

>>> Data.Connection.ceiling f32sys (0/0)
PosInf
>>> Data.Connection.ceiling f32sys pi
Finite (MkSystemTime {systemSeconds = 3, systemNanoseconds = 141592742})

f64sys :: Conn L Double (Extended SystemTime) Source #

The Double is valued in seconds.

>>> Data.Connection.ceiling f64sys (0/0)
PosInf
>>> Data.Connection.ceiling f64sys pi
Finite (MkSystemTime {systemSeconds = 3, systemNanoseconds = 141592654})

f09sys :: Conn k (Extended Nano) (Extended SystemTime) Source #

The Nano is valued in seconds (to nanosecond precision).

ratsys :: Conn k Rational (Extended SystemTime) Source #

The Rational is valued in seconds.

Extended

extended :: b -> b -> (a -> b) -> Extended a -> b Source #

Eliminate an Extended.

data Extended r #

Extended r is an extension of r with positive/negative infinity (±∞).