Two main assumptions (and constraints) of this module:
- Cardinality can't be negative.
- For
construction it is always refined by growing. F.e., ifrefinableC
refines torefinableC
(7, ref_f_1)
, thenrefinableC
(x, ref_f_2)x
SHOULD NEVER be less then7
. 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 anotherrefinableC
, then it is not fully refined, but (at least)5
is achieved (the precise cardinality is>= 5
). - If
x0
is10
and(refine_f 10 (<= 15))
returned(refinableC (17, refine_f_2))
, then it is known, that precise cardinality is already >=10 + 7
. In sight ofrefine_f
there SHOULD be everything except for what's already counted inx0
(which is10
), and in sight ofrefine_f_2
there should be even less by7
elements comparing torefine_f
. So if total cardinality was25
, then(refine_f_2 17 (<= 30))
MUST returnpreciseC 25
, to make10 + 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
, andx0 = 20
- these 20 elements are already counted, and in sight ofrefine_f
there are only 5 last elements. Thenrefine_f 20 (<= 26)
will result inpreciseC 25
, but(!)refine_f 10 (<= 16)
MUST result inpreciseC 15
.
Recomendations:
- If subject has infinite cardinality, it's best to determine
it's cardinality as
at early stages and avoid usinginfiniteC
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 almost- prefix in function name.
If there is a probability that refinement of
infiniteC
`almostStrictCompare2LCs` infiniteC
==
EQ
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.