Cardinality-0.2: Measure container capacity. Use it to safely change container.




Two main assumptions (and constraints) of this module:

  1. Cardinality can't be negative.
  2. For refinableC construction it is always refined by growing. F.e., if refinableC (7, ref_f_1) refines to refinableC (x, ref_f_2), then x SHOULD NEVER be less then 7. On this assumption relies heavily functions lazyIsZeroLC, lazyCompare2LCs, addLCToLC and also almost every refinement routine.



type PreciseCardinality = IntegerSource

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

It would be best here to use Word32 instead, however, with 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 PreciseC data constructor, but to wrap it into function preciseC, which guards from the attemts to conctruct negative cardinality (by throwing an error).

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


infiniteC :: LazyCardinalitySource

LazyCardinality constructor.

F.e., [1..] list has such cardinality.

preciseC :: PreciseCardinality -> LazyCardinalitySource

LazyCardinality constructor. If given negative value, raises error.

F.e., the tuple (5,6) has a precise cardinality 2.

refinableC :: CardinalityRefinementState -> LazyCardinalitySource

LazyCardinality constructor.

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:

  1. 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).
  2. 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.
  3. 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.


  1. If subject has infinite cardinality, it's best to determine it's cardinality as infiniteC at early stages and avoid using refinableC for it.

lazyIsZeroLC :: LazyCardinality -> Maybe BoolSource

Returns Nothing, ONLY if LC is refinableC (0, _) (according to 2nd assumption of the module). Returns 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 infiniteC, 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.

sumLCs :: [LazyCardinality] -> LazyCardinalitySource

foldl addLCToLC

See recommendations by addLCToLC.

refineCRS_TillEnd :: CardinalityRefinementState -> LazyCardinalitySource

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

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

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

Used for instance of Ord typeclass.

Together with Ordering returns also probably refined cardinalities for reuse.

WARNING!!! When comparing refinableC with infiniteC , it results in LT (less than)! While comparing infiniteC `almostStrictCompare2LCs` infiniteC == EQ. That's the reason for an almost- prefix in function name. If there is a probability that refinement of refinableC may evaluate to infiniteC, and it's important to you, that infinities are equal, then before comparing this refinable, use refineCRS_TillEnd on it. That's laziness.

Trying to compare 2 refinableCs that are actually infinite, but don't use infiniteC will hang the system (the same as if you try to determine length of an infinite list).

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 refinableC isn't refined.


class HasCard a whereSource

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


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) 

class HasCardT t whereSource

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


Cardinality = 0

Cardinality = 1

Cardinality = 0..1

Cardinality = 0..Inf

cardOf_List :: [a] -> LazyCardinalitySource

Refinable starting from 0, uses length2

cardOf_Map :: Map k e -> LazyCardinalitySource

Not refinable, since Map is a strict structure.

Cardinality = 1..Inf


length2 :: [a] -> ContinueRefiningCardinalityUntilSource

List length of controlable greediness.