Cardinality-0.1: Data/Cardinality.hs
{-
Copyright (C) 2010 Andrejs Sisojevs <andrejs.sisojevs@nextmail.ru>
All rights reserved.
For license and copyright information, see the file COPYRIGHT
-}
--------------------------------------------------------------------------
--------------------------------------------------------------------------
{-# LANGUAGE BangPatterns, FlexibleInstances #-}
-- | 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.
module Data.Cardinality (
-- * Core
PreciseCardinality
, CurrentNotFinalPreciseCardinality
, BoundaryPreciseCardinality
, ContinueCounting_DoWe
, ContinueRefiningCardinalityUntil
, CardinalityRefinementState
, LazyCardinality
, infiniteC
, preciseC
, refinableC
, lazyIsZeroLC
, refinementState
, addPCToLC
, addLCToLC
, sumLCs
, refineCRS_Till
, refineCRS_TillOneAbove
, refineCRS_TillOneBelow
, crsRefinementStep
, refineCRS_TillEnd
, refineTill
, refineTillOneAbove
, refineTillOneBelow
, refinementStep
, refineTillEnd
, equalize2Refinements
, compare2Refinements
, almostStrictCompare2LCs
, lazyCompare2LCs
, showLazy
, showStrict
-- * Application
, HasCard(..)
, HasCardT(..)
-- * Instances
-- ** Cardinality = 0
, cardOf_Unity
, cardOf_EmptySet
-- ** Cardinality = 1
-- , cardOf_Identity0
, cardOf_Identity1
-- ** Cardinality = 0..1
, cardOf_Maybe
-- ** Cardinality = 0..Inf
, cardOf_List
, cardOf_Map
-- ** Cardinality = 1..Inf
, cardOf_NeverEmptyList
-- * Helpers
, length2
) where
import Data.EmptySet
import Data.NeverEmptyList
import qualified Data.Map as M
import Data.Map (Map, (!))
import Data.Word
import Data.Typeable
import Control.Monad.Identity
--------------------------------------------------------------
-- * Core
-- | 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).
type PreciseCardinality = Integer
type CurrentNotFinalPreciseCardinality = PreciseCardinality
type BoundaryPreciseCardinality = CurrentNotFinalPreciseCardinality
type ContinueCounting_DoWe = Bool
-- | An example of this is @'length2'@ function.
type ContinueRefiningCardinalityUntil = CurrentNotFinalPreciseCardinality -> (CurrentNotFinalPreciseCardinality -> ContinueCounting_DoWe) -> LazyCardinality
type CardinalityRefinementState = (CurrentNotFinalPreciseCardinality, ContinueRefiningCardinalityUntil)
-- | 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'@
--
-- * @'preciseC' 'PreciseCardinality'@
--
-- * @'refinableC' 'CardinalityRefinementState'@
data LazyCardinality =
InfiniteC
| PreciseC PreciseCardinality
| RefinableC CardinalityRefinementState
deriving (Typeable)
-- | @'LazyCardinality'@ constructor.
--
-- F.e., @[1..]@ list has such cardinality.
infiniteC :: LazyCardinality
infiniteC = InfiniteC
-- | @'LazyCardinality'@ constructor. If given negative value, raises error.
--
-- F.e., the tuple @(5,6)@ has a precise cardinality 2.
preciseC :: PreciseCardinality -> LazyCardinality
preciseC c = case c < 0 of { True -> error ("Can't construct negative cardinality '" ++ show c ++ "' "); False -> PreciseC c }
-- | @'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@.
--
-- Recomendations:
--
-- 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.
refinableC :: CardinalityRefinementState -> LazyCardinality
refinableC = RefinableC
lcIsInfinite :: LazyCardinality -> Bool
lcIsInfinite InfiniteC = True
lcIsInfinite _ = False
preciseOfLC :: LazyCardinality -> Maybe PreciseCardinality
preciseOfLC (PreciseC c) = Just c
preciseOfLC _ = Nothing
-- | Returns @Nothing@, ONLY if LC is @'refinableC' (0, _)@
-- (according to 2nd assumption of the module). Returns @Just True@
-- only for @'preciseC' 0@.
lazyIsZeroLC :: LazyCardinality -> Maybe Bool
lazyIsZeroLC (PreciseC c) = Just (c == 0)
lazyIsZeroLC InfiniteC = Just False
lazyIsZeroLC (RefinableC (c, _)) = case c `compare` 0 of { EQ -> Nothing; _ -> Just False }
refinementState :: LazyCardinality -> Maybe CardinalityRefinementState
refinementState (RefinableC rs) = Just rs
refinementState _ = Nothing
infixr 6 `addPCToLC`
-- Throws an error if @'preciseC'@ is attempted to construct with negative
-- resulting cardinality.
addPCToLC :: PreciseCardinality -> LazyCardinality -> LazyCardinality
addPCToLC n lc =
case lc of
InfiniteC -> lc
PreciseC m -> preciseC (m + n)
RefinableC (c, ref_while) -> refinableC (c + n, ref_while)
infixr 6 `addLCToLC`
-- | 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.
addLCToLC :: LazyCardinality -> LazyCardinality -> LazyCardinality
addLCToLC lc_1 lc_2 =
case (lc_1, lc_2) of
(InfiniteC, _) -> InfiniteC
(_, InfiniteC) -> InfiniteC
(PreciseC m, PreciseC n) -> preciseC (m + n)
(PreciseC m, RefinableC (c, ref_while)) -> refinableC (c + m, ref_while)
(RefinableC (c, ref_while), PreciseC m) -> refinableC (c + m, ref_while)
(RefinableC (c, ref_while_1), RefinableC (d, ref_while_2)) -> refinableC (c + d, refWhileSyn ref_while_1 ref_while_2)
where
refWhileSyn :: ContinueRefiningCardinalityUntil -> ContinueRefiningCardinalityUntil -> ContinueRefiningCardinalityUntil
refWhileSyn ref_while_1 ref_while_2 =
(\ sofar stop_cond ->
case ref_while_1 sofar stop_cond of
InfiniteC -> InfiniteC
RefinableC (sofar_2, ref_while_1_2) -> RefinableC (sofar_2, refWhileSyn ref_while_1_2 ref_while_2)
PreciseC c ->
case ref_while_1 (sofar + c) stop_cond of
InfiniteC -> InfiniteC
RefinableC (sofar_3, ref_while_2_2) -> RefinableC (sofar_3, ref_while_2_2)
PreciseC final_c -> PreciseC final_c
)
-- | @foldl 'addLCToLC'@
--
-- See recommendations by @'addLCToLC'@.
sumLCs :: [LazyCardinality] -> LazyCardinality
sumLCs = foldl addLCToLC (preciseC 0)
refineCRS_Till :: CardinalityRefinementState -> BoundaryPreciseCardinality -> LazyCardinality
refineCRS_Till crs@(c, ref_while) n =
case c >= n of
True -> refinableC crs
False -> ref_while c (<= n)
-- [1,2,3,4,5,6,7,8,9,10]
-- refineCRS_Till (refinableC (5, ref_while)) 8
-- ref_while sees [6,7,8,9,10]
-- ref_while (<= 8 - 5) -> ref_while (<= 3) -> refinableC (8, ref_while'))
-- ref_while' sees [9, 10]
refineCRS_TillOneAbove :: CardinalityRefinementState -> BoundaryPreciseCardinality -> LazyCardinality
refineCRS_TillOneBelow :: CardinalityRefinementState -> BoundaryPreciseCardinality -> LazyCardinality
refineCRS_TillOneAbove crs n = refineCRS_Till crs (n + 1)
refineCRS_TillOneBelow crs n = refineCRS_Till crs (n - 1)
crsRefinementStep :: CardinalityRefinementState -> LazyCardinality
crsRefinementStep crs@(c, ref_while) = ref_while c (<= (c + 1))
-- | Don't use it on infinite refinables not measured with 'infiniteC'.
refineCRS_TillEnd :: CardinalityRefinementState -> LazyCardinality
refineCRS_TillEnd crs@(c, ref_while) = ref_while c (const True)
-- | Wrapper around @'refineCRS_Till'@.
refineTill :: LazyCardinality -> BoundaryPreciseCardinality -> LazyCardinality
refineTill lc n =
case lc of
RefinableC crs -> refineCRS_Till crs n
_ -> lc
-- | Wrapper around @'refineTillOneAbove'@.
refineTillOneAbove :: LazyCardinality -> BoundaryPreciseCardinality -> LazyCardinality
-- | Wrapper around @'refineTillOneBelow'@.
refineTillOneBelow :: LazyCardinality -> BoundaryPreciseCardinality -> LazyCardinality
refineTillOneAbove lc n = case lc of { RefinableC crs -> refineCRS_Till crs (n + 1); _ -> lc }
refineTillOneBelow lc n = case lc of { RefinableC crs -> refineCRS_Till crs (n - 1); _ -> lc }
-- | Wrapper around @'crsRefinementStep'@.
refinementStep :: LazyCardinality -> LazyCardinality
refinementStep lc = case lc of { RefinableC crs -> crsRefinementStep crs ; _ -> lc }
-- | Wrapper around @'refineCRS_TillEnd'@.
refineTillEnd :: LazyCardinality -> LazyCardinality
refineTillEnd lc = case lc of { RefinableC crs -> refineCRS_TillEnd crs ; _ -> lc }
-- | 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'@).
equalize2Refinements :: CardinalityRefinementState -> CardinalityRefinementState -> (LazyCardinality, LazyCardinality)
equalize2Refinements crs1@(m, ref_f_1) crs2@(n, ref_f_2) =
case m `compare` n of
LT -> let lc_of_crs1_refined = ref_f_1 m (<= n)
in case refinementState lc_of_crs1_refined of
Nothing -> (lc_of_crs1_refined, refinableC crs2)
Just crs1_refined -> equalize2Refinements crs1_refined crs2
EQ -> (refinableC crs1, refinableC crs2)
GT -> let lc_of_crs2_refined = ref_f_2 n (<= m)
in case refinementState lc_of_crs2_refined of
Nothing -> (refinableC crs1, lc_of_crs2_refined)
Just crs2_refined -> equalize2Refinements crs1 crs2_refined
compare2Refinements :: CardinalityRefinementState -> CardinalityRefinementState -> (Ordering, LazyCardinality, LazyCardinality)
compare2Refinements crs1@(m, _) crs2@(n, _) =
let cards = equalize2Refinements crs1 crs2
in case cards of
(lc1_2@(RefinableC crs1_2), lc2_2@(RefinableC crs2_2)) -> -- m == n
let lc1_3 = crsRefinementStep crs1_2
in case lc1_3 of -- I could have made crsRefinementStep for both in tuple here, but let's keep it as lazy as possible
RefinableC crs1_3 ->
let lc2_3 = crsRefinementStep crs2_2
in case lc2_3 of
RefinableC crs2_3 -> compare2Refinements crs1_3 crs2_3
_ -> almostStrictCompare2LCs lc1_3 lc2_3
_ -> almostStrictCompare2LCs lc1_3 lc2_2
_ -> uncurry almostStrictCompare2LCs cards
infixr 9 `almostStrictCompare2LCs`
-- | 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 @'refinableC'@s 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).
almostStrictCompare2LCs :: LazyCardinality -> LazyCardinality -> (Ordering, LazyCardinality, LazyCardinality)
almostStrictCompare2LCs a b =
let reverseOrdering :: (Ordering, LazyCardinality, LazyCardinality) -> (Ordering, LazyCardinality, LazyCardinality)
reverseOrdering (GT, a, b) = (LT, b, a)
reverseOrdering (LT, a, b) = (GT, b, a)
reverseOrdering (EQ, a, b) = (EQ, b, a)
in case (a,b) of
(InfiniteC , InfiniteC) -> (EQ, a, b)
(InfiniteC , _ ) -> (GT, a, b)
(_ , InfiniteC) -> (LT, a, b) -- !!! even though 'refinableC' may return 'infiniteC' !!!
(PreciseC m, PreciseC n) -> (m `compare` n, a, b)
----------------------------
(RefinableC crs@(m, _), PreciseC n) -> case m > n of { True -> (GT, a, b); False -> almostStrictCompare2LCs (refineCRS_TillOneAbove crs n) b }
(RefinableC crs1, RefinableC crs2) -> compare2Refinements crs1 crs2
(_ , RefinableC _) -> reverseOrdering $ almostStrictCompare2LCs b a
instance Eq LazyCardinality where
lc1 == lc2 = (fst3 $ almostStrictCompare2LCs lc1 lc2) == EQ
instance Ord LazyCardinality where
lc1 `compare` lc2 = fst3 $ almostStrictCompare2LCs lc1 lc2
infixr 9 `lazyCompare2LCs`
-- | 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.
lazyCompare2LCs :: LazyCardinality -> LazyCardinality -> Maybe Ordering
lazyCompare2LCs a b =
let reverseOrdering :: Maybe Ordering -> Maybe Ordering
reverseOrdering (Just GT) = (Just LT)
reverseOrdering (Just LT) = (Just GT)
reverseOrdering (Just EQ) = (Just EQ)
reverseOrdering Nothing = Nothing
in case (a,b) of
(InfiniteC , InfiniteC) -> Just EQ
(InfiniteC , _ ) -> Just GT
(_ , InfiniteC) -> Just LT -- !!! even though 'refinableC' may return 'infiniteC' !!!
(PreciseC m, PreciseC n) -> Just (m `compare` n)
----------------------------
(RefinableC crs@(m, _), PreciseC n) -> case m > n of { True -> Just GT; False -> Nothing }
(PreciseC n, RefinableC crs@(m, _)) -> case m > n of { True -> Just LT; False -> Nothing }
_ -> Nothing
-- | Used for Show typeclass instaniation. Here @'refinableC'@ isn't refined.
showLazy :: LazyCardinality -> String
showLazy lc =
case lc of
InfiniteC -> "infiniteC"
PreciseC c -> "preciseC " ++ show c
RefinableC (c, _) -> "Refinable (" ++ show c ++ ", refine_f)"
-- | Here @ 'refineCRS_TillEnd'@ is applied to @'refinableC'@ argument.
showStrict :: LazyCardinality -> String
showStrict lc =
case lc of
InfiniteC -> "infiniteC"
PreciseC c -> "preciseC " ++ show c
RefinableC crs -> show $ refineCRS_TillEnd crs
instance Show LazyCardinality where
show = showLazy
--------------------------------------------------------------
-- * Application
-- | @HasCard@ = \"Has cardinality\". In other words, \"it's possible to measure
-- current count of elements for this container\"
class HasCard a where
cardOf :: a -> LazyCardinality
-- | @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 @(* -> *)@)\"
class HasCardT t where
cardOfT :: t elem -> LazyCardinality
--------------------------------------------------------------
--------------------------------------------------------------
-- * Instances
-- ** Cardinality = 0
cardOf_Unity :: () -> LazyCardinality
cardOf_Unity _ = preciseC 0
instance HasCard () where
cardOf = cardOf_Unity
cardOf_EmptySet :: EmptySet a -> LazyCardinality
cardOf_EmptySet _ = preciseC 0
instance HasCard (EmptySet a) where
cardOf = cardOf_EmptySet
instance HasCardT EmptySet where
cardOfT = cardOf_EmptySet
-- ** Cardinality = 1
{-
cardOf_Identity0 :: a -> LazyCardinality
cardOf_Identity0 _ = preciseC 1
instance HasCard a where
cardOf = cardOf_Identity0
-}
cardOf_Identity1 :: Identity a -> LazyCardinality
cardOf_Identity1 _ = preciseC 1
instance HasCard (Identity a) where
cardOf = cardOf_Identity1
instance HasCardT Identity where
cardOfT = cardOf_Identity1
-- ** Cardinality = 0..1
cardOf_Maybe :: Maybe a -> LazyCardinality
cardOf_Maybe Nothing = preciseC 0
cardOf_Maybe (Just _) = preciseC 1
instance HasCard (Maybe a) where
cardOf = cardOf_Maybe
instance HasCardT Maybe where
cardOfT = cardOf_Maybe
-- ** Cardinality = 0..N
-- | Refinable starting from 0, uses @'length2'@
cardOf_List :: [a] -> LazyCardinality
cardOf_List l = refinableC (0, \ sofar refine_while -> length2 l sofar refine_while)
instance HasCard [a] where
cardOf = cardOf_List
instance HasCardT ([]) where
cardOfT = cardOf_List
-- | Not refinable, since @'Data.Map.Map'@ is a strict structure.
cardOf_Map :: Map k e -> LazyCardinality
cardOf_Map = preciseC . fromIntegral . M.size
instance HasCard (Map k e) where
cardOf = cardOf_Map
instance HasCardT (Map k) where
cardOfT = cardOf_Map
-- ** Cardinality = 1..N
-- | Refinable starting from 1.
cardOf_NeverEmptyList :: NeverEmptyList k -> LazyCardinality
cardOf_NeverEmptyList (NEL _ l) = 1 `addPCToLC` cardOf l
instance HasCard (NeverEmptyList a) where
cardOf = cardOf_NeverEmptyList
instance HasCardT NeverEmptyList where
cardOfT = cardOf_NeverEmptyList
-- Other instances
instance HasCardT ((,) key) where { cardOfT _ = preciseC 1 } -- this messes up things, in the context of HasCard (a,a) instance...
instance HasCard (a,a) where { cardOf _ = preciseC 2 }
instance HasCard (a,a,a) where { cardOf _ = preciseC 3 }
instance HasCard (a,a,a,a) where { cardOf _ = preciseC 4 }
instance HasCard (a,a,a,a,a) where { cardOf _ = preciseC 5 }
instance HasCard (a,a,a,a,a,a) where { cardOf _ = preciseC 6 }
instance HasCard (a,a,a,a,a,a,a) where { cardOf _ = preciseC 7 }
instance HasCard (a,a,a,a,a,a,a,a) where { cardOf _ = preciseC 8 }
instance HasCard (a,a,a,a,a,a,a,a,a) where { cardOf _ = preciseC 9 }
instance HasCard (a,a,a,a,a,a,a,a,a,a) where { cardOf _ = preciseC 10 }
instance HasCard (a,a,a,a,a,a,a,a,a,a,a) where { cardOf _ = preciseC 11 }
instance HasCard (a,a,a,a,a,a,a,a,a,a,a,a) where { cardOf _ = preciseC 12 }
--------------------------------------------------------------
-- * Helpers
-- type ContinueRefiningCardinalityUntil =
-- CurrentNotFinalPreciseCardinality
-- -> (CurrentNotFinalPreciseCardinality -> ContinueCounting_DoWe)
-- -> LazyCardinality
-- | List length of controlable greediness.
length2 :: [a] -> ContinueRefiningCardinalityUntil
length2 l !sofar p =
case _length2 l sofar of
(i, Nothing) -> preciseC i
(i, Just new_ref_while) -> RefinableC (i, new_ref_while)
where
_length2 :: [a] -> CurrentNotFinalPreciseCardinality
-> ( BoundaryPreciseCardinality
, Maybe ContinueRefiningCardinalityUntil
)
_length2 [] !_sofar = (_sofar, Nothing)
_length2 l@(_:t) !_sofar =
let next_sofar = _sofar + 1
in case p next_sofar of
False -> (_sofar, Just (length2 l))
True -> _length2 t next_sofar
fst3 :: (a,b,c) -> a
snd3 :: (a,b,c) -> b
thrd3 :: (a,b,c) -> c
fst3 (a,_,_) = a
snd3 (_,b,_) = b
thrd3 (_,_,c) = c