Two main assumptions (and constraints) of this module:

- Cardinality can't be negative.
- For

construction it is always refined by growing. F.e., if`refinableC`

refines to`refinableC`

(7, ref_f_1)

, then`refinableC`

(x, ref_f_2)`x`

SHOULD NEVER be less then`7`

. On this assumption relies heavily functions

,`lazyIsZeroLC`

,`lazyCompare2LCs`

and also almost every refinement routine.`addLCToLC`

- type PreciseCardinality = Integer
- type CurrentNotFinalPreciseCardinality = PreciseCardinality
- type BoundaryPreciseCardinality = CurrentNotFinalPreciseCardinality
- type ContinueCounting_DoWe = Bool
- type ContinueRefiningCardinalityUntil = CurrentNotFinalPreciseCardinality -> (CurrentNotFinalPreciseCardinality -> ContinueCounting_DoWe) -> LazyCardinality
- type CardinalityRefinementState = (CurrentNotFinalPreciseCardinality, ContinueRefiningCardinalityUntil)
- data LazyCardinality
- infiniteC :: LazyCardinality
- preciseC :: PreciseCardinality -> LazyCardinality
- refinableC :: CardinalityRefinementState -> LazyCardinality
- lazyIsZeroLC :: LazyCardinality -> Maybe Bool
- refinementState :: LazyCardinality -> Maybe CardinalityRefinementState
- addPCToLC :: PreciseCardinality -> LazyCardinality -> LazyCardinality
- addLCToLC :: LazyCardinality -> LazyCardinality -> LazyCardinality
- sumLCs :: [LazyCardinality] -> LazyCardinality
- refineCRS_Till :: CardinalityRefinementState -> BoundaryPreciseCardinality -> LazyCardinality
- refineCRS_TillOneAbove :: CardinalityRefinementState -> BoundaryPreciseCardinality -> LazyCardinality
- refineCRS_TillOneBelow :: CardinalityRefinementState -> BoundaryPreciseCardinality -> LazyCardinality
- crsRefinementStep :: CardinalityRefinementState -> LazyCardinality
- refineCRS_TillEnd :: CardinalityRefinementState -> LazyCardinality
- refineTill :: LazyCardinality -> BoundaryPreciseCardinality -> LazyCardinality
- refineTillOneAbove :: LazyCardinality -> BoundaryPreciseCardinality -> LazyCardinality
- refineTillOneBelow :: LazyCardinality -> BoundaryPreciseCardinality -> LazyCardinality
- refinementStep :: LazyCardinality -> LazyCardinality
- refineTillEnd :: LazyCardinality -> LazyCardinality
- equalize2Refinements :: CardinalityRefinementState -> CardinalityRefinementState -> (LazyCardinality, LazyCardinality)
- compare2Refinements :: CardinalityRefinementState -> CardinalityRefinementState -> (Ordering, LazyCardinality, LazyCardinality)
- almostStrictCompare2LCs :: LazyCardinality -> LazyCardinality -> (Ordering, LazyCardinality, LazyCardinality)
- lazyCompare2LCs :: LazyCardinality -> LazyCardinality -> Maybe Ordering
- showLazy :: LazyCardinality -> String
- showStrict :: LazyCardinality -> String
- class HasCard a where
- cardOf :: a -> LazyCardinality

- class HasCardT t where
- cardOfT :: t elem -> LazyCardinality

- cardOf_Unity :: () -> LazyCardinality
- cardOf_EmptySet :: EmptySet a -> LazyCardinality
- cardOf_Identity1 :: Identity a -> LazyCardinality
- cardOf_Maybe :: Maybe a -> LazyCardinality
- cardOf_List :: [a] -> LazyCardinality
- cardOf_Map :: Map k e -> LazyCardinality
- cardOf_NeverEmptyList :: NeverEmptyList k -> LazyCardinality
- length2 :: [a] -> ContinueRefiningCardinalityUntil

# Core

type PreciseCardinality = IntegerSource

Count of elements in container. It's always positive or zero.

It would be best here to use

instead, however, with `Word32`

`Integer`

it's easier to catch the error of going down below zero (in case
of

).
`Word32`

0-1==4294967295

However it is decided not to allow the direct use of

data
constructor, but to wrap it into function `PreciseC`

, which guards from
the attemts to conctruct negative cardinality (by throwing an error).
`preciseC`

type ContinueCounting_DoWe = BoolSource

type ContinueRefiningCardinalityUntil = CurrentNotFinalPreciseCardinality -> (CurrentNotFinalPreciseCardinality -> ContinueCounting_DoWe) -> LazyCardinalitySource

An example of this is

function.
`length2`

type CardinalityRefinementState = (CurrentNotFinalPreciseCardinality, ContinueRefiningCardinalityUntil)Source

data LazyCardinality Source

In other words: count of elements in a container, with an opportunity not to refine the whole content of the container (and the container's structure).

Constructors:

infiniteC :: LazyCardinalitySource

constructor.
`LazyCardinality`

F.e., `[1..]`

list has such cardinality.

preciseC :: PreciseCardinality -> LazyCardinalitySource

constructor. If given negative value, raises error.
`LazyCardinality`

F.e., the tuple `(5,6)`

has a precise cardinality 2.

refinableC :: CardinalityRefinementState -> LazyCardinalitySource

constructor.
`LazyCardinality`

For lists it happens, that we do not want to count all the elements
of a container,
but want to count them until some lower boundary. For example,
I do not want to know the length of the list (which involves taking
each element of it, and counting it in) to reason about whether
it's content fit into the `(,,)`

data constructor. For this
case I only need to count till 3rd element and check, if list is
continued. It's actual especially, when dealing with infinite lists
or with lists, whose reading may block.

For `(refinableC (x0, refine_f))`

important rules:

- If
`(refine_f x0 (<= 5))`

evaluates to another`refinableC`

, then it is not fully refined, but (at least)`5`

is achieved (the precise cardinality is`>= 5`

). - If
`x0`

is`10`

and`(refine_f 10 (<= 15))`

returned`(refinableC (17, refine_f_2))`

, then it is known, that precise cardinality is already >=`10 + 7`

. In sight of`refine_f`

there SHOULD be everything except for what's already counted in`x0`

(which is`10`

), and in sight of`refine_f_2`

there should be even less by`7`

elements comparing to`refine_f`

. So if total cardinality was`25`

, then`(refine_f_2 17 (<= 30))`

MUST return`preciseC 25`

, to make`10 + 7 + 8 = 25`

. - The theatment of the first argument of refinement function
`refine_f`

must be relative. For example, given total count of elements`= 25`

, and`x0 = 20`

- these 20 elements are already counted, and in sight of`refine_f`

there are only 5 last elements. Then`refine_f 20 (<= 26)`

will result in`preciseC 25`

, but(!)`refine_f 10 (<= 16)`

MUST result in`preciseC 15`

.

Recomendations:

- If subject has infinite cardinality, it's best to determine
it's cardinality as

at early stages and avoid using`infiniteC`

`refinableC`

for it.

lazyIsZeroLC :: LazyCardinality -> Maybe BoolSource

Returns `Nothing`

, ONLY if LC is

(according to 2nd assumption of the module). Returns `refinableC`

(0, _)`Just True`

only for

.
`preciseC`

0

addLCToLC :: LazyCardinality -> LazyCardinality -> LazyCardinalitySource

For case when adding up 2 refinables, if both of them sooner or later
refines to

, then one that returns infinity earlier is
recommended to put as a first term. Infinity + any LazyCardinality
= infinity. Another recommendation would be to put
refinable that's easier to compute as a first term.
`infiniteC`

refineCRS_TillOneAbove :: CardinalityRefinementState -> BoundaryPreciseCardinality -> LazyCardinalitySource

refineCRS_TillOneBelow :: CardinalityRefinementState -> BoundaryPreciseCardinality -> LazyCardinalitySource

refineCRS_TillEnd :: CardinalityRefinementState -> LazyCardinalitySource

Don't use it on infinite refinables not measured with `infiniteC`

.

refineTill :: LazyCardinality -> BoundaryPreciseCardinality -> LazyCardinalitySource

Wrapper around

.
`refineCRS_Till`

refineTillOneAbove :: LazyCardinality -> BoundaryPreciseCardinality -> LazyCardinalitySource

Wrapper around

.
`refineTillOneAbove`

refineTillOneBelow :: LazyCardinality -> BoundaryPreciseCardinality -> LazyCardinalitySource

Wrapper around

.
`refineTillOneBelow`

refinementStep :: LazyCardinality -> LazyCardinalitySource

Wrapper around

.
`crsRefinementStep`

refineTillEnd :: LazyCardinality -> LazyCardinalitySource

Wrapper around

.
`refineCRS_TillEnd`

equalize2Refinements :: CardinalityRefinementState -> CardinalityRefinementState -> (LazyCardinality, LazyCardinality)Source

For `equalize2Refinements (m, ref_f_1) (n, ref_f_2)`

finishes when m == n.
Else refines them. Another termination condition is when in result of
refinement one of cardinalities becomes final (not

).
`refinableC`

compare2Refinements :: CardinalityRefinementState -> CardinalityRefinementState -> (Ordering, LazyCardinality, LazyCardinality)Source

almostStrictCompare2LCs :: LazyCardinality -> LazyCardinality -> (Ordering, LazyCardinality, LazyCardinality)Source

Used for instance of Ord typeclass.

Together with

returns also probably refined cardinalities
for reuse.
`Ordering`

WARNING!!! When comparing

with `refinableC`

, it results in `infiniteC`

(less than)!
While comparing `LT`

.
That's the reason for an `infiniteC`

`almostStrictCompare2LCs` `infiniteC`

==
`EQ`

*almost-* prefix in function name.
If there is a probability that refinement of

may evaluate to `refinableC`

, and it's important to you,
that infinities are equal, then before comparing this refinable,
use `infiniteC`

`refineCRS_TillEnd`

on it. That's laziness.

Trying to compare 2

s that are actually infinite, but don't
use `refinableC`

will hang
the system (the same as if you try to determine length of an infinite
list).
`infiniteC`

lazyCompare2LCs :: LazyCardinality -> LazyCardinality -> Maybe OrderingSource

Won't refine refinables. According to 2nd assumption of the module:

`refinableC`

(m, _) `lazyCompare2LCs``preciseC`

n

equals to `Just GT`

if `m > n`

, and `Nothing`

otherwise.

showLazy :: LazyCardinality -> StringSource

Used for Show typeclass instaniation. Here

isn't refined.
`refinableC`

showStrict :: LazyCardinality -> StringSource

Here ` `

is applied to `refineCRS_TillEnd`

argument.
`refinableC`

# Application

`HasCard`

= "Has cardinality". In other words, "it's possible to measure
current count of elements for this container"

cardOf :: a -> LazyCardinalitySource

HasCard () | |

HasCard [a] | |

HasCard (Maybe a) | |

HasCard (Identity a) | |

HasCard (NeverEmptyList a) | |

HasCard (EmptySet a) | |

HasCard (a, a) | |

HasCard (Map k e) | |

HasCard (a, a, a) | |

HasCard (a, a, a, a) | |

HasCard (a, a, a, a, a) | |

HasCard (a, a, a, a, a, a) | |

HasCard (a, a, a, a, a, a, a) | |

HasCard (a, a, a, a, a, a, a, a) | |

HasCard (a, a, a, a, a, a, a, a, a) | |

HasCard (a, a, a, a, a, a, a, a, a, a) | |

HasCard (a, a, a, a, a, a, a, a, a, a, a) | |

HasCard (a, a, a, a, a, a, a, a, a, a, a, a) |

`HasCardT`

= "Has cardinality (for container types of kind `(* -> *)`

)".
In other words, "it's possible to measure
current count of elements for this container (for container types of
kind `(* -> *)`

)"

cardOfT :: t elem -> LazyCardinalitySource

# Instances

## Cardinality = 0

## Cardinality = 1

## Cardinality = 0..1

cardOf_Maybe :: Maybe a -> LazyCardinalitySource

## Cardinality = 0..Inf

cardOf_List :: [a] -> LazyCardinalitySource

Refinable starting from 0, uses `length2`

cardOf_Map :: Map k e -> LazyCardinalitySource

Not refinable, since

is a strict structure.
`Map`

## Cardinality = 1..Inf

cardOf_NeverEmptyList :: NeverEmptyList k -> LazyCardinalitySource

Refinable starting from 1.

# Helpers

length2 :: [a] -> ContinueRefiningCardinalityUntilSource

List length of controlable greediness.