Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
This module defines a way to prove that a key exists in a map, so that the
key can be used to index into the map without using a Maybe
, or manually
handling the "impossible" case with error
or other partial functions.
To do this,
has a type parameter IntMap
s vs
that identifies its set
ofvkeys, so that if another map has the same type parameter, you know that
map has the same set of keys. There is
, a type of keys that have
been validated to belong to the set identified by Key
ss
, and for which the
operation of indexing into a
(only for the same IntMap
s vs
) can
proceed without failure (see !
). The type s
itself has no internal
structure, rather it is merely a skolem type variable (rank-2 polymorphism
runST
trick) introduced by Data.Reflection.
Like Data.IntMap, functions in this module are strict in the keys but lazy
in the values. The Data.IntMap.Strict.Refined module reuses the same
IntMap
type but provides functions that operate strictly on the values.
Synopsis
- data IntMap s a
- type Key s = Refined (InSet 'Int s) Int
- data SomeIntMap a where
- SomeIntMap :: forall s a. !(IntMap s a) -> SomeIntMap a
- withIntMap :: forall a r. SomeIntMap a -> (forall s. IntMap s a -> r) -> r
- data SomeIntMapWith p a where
- SomeIntMapWith :: forall s a p. !(IntMap s a) -> !(p s) -> SomeIntMapWith p a
- withIntMapWith :: forall a r p. SomeIntMapWith p a -> (forall s. IntMap s a -> p s -> r) -> r
- data Some2IntMapWith p a b where
- Some2IntMapWith :: forall s t a b p. !(IntMap s a) -> !(IntMap t b) -> !(p s t) -> Some2IntMapWith p a b
- with2IntMapWith :: forall a b r p. Some2IntMapWith p a b -> (forall s t. IntMap s a -> IntMap t b -> p s t -> r) -> r
- newtype SupersetProof f s r = SupersetProof (InSet f r :-> InSet f s)
- newtype EmptyProof f r = EmptyProof (forall s. InSet f r :-> InSet f s)
- empty :: forall a. SomeIntMapWith (EmptyProof 'Int) a
- singleton :: forall a. Int -> a -> SomeIntMapWith (SingletonProof 'Int Int) a
- newtype SingletonProof f a r = SingletonProof (Refined (InSet f r) a)
- fromSet :: forall s a. KnownIntSet s => (Key s -> a) -> IntMap s a
- fromIntMap :: forall a. IntMap a -> SomeIntMap a
- fromTraversableWithKey :: forall t a. Traversable t => (Int -> a -> a -> a) -> t (Int, a) -> SomeIntMapWith (FromTraversableProof 'Int t Int) a
- newtype FromTraversableProof f (t :: Type -> Type) a r = FromTraversableProof (t (Refined (InSet f r) a))
- insert :: forall s a. Int -> a -> IntMap s a -> SomeIntMapWith (InsertProof 'Int Int s) a
- data InsertProof f a s r = InsertProof (Refined (InSet f r) a) (InSet f s :-> InSet f r)
- reinsert :: forall s a. Key s -> a -> IntMap s a -> IntMap s a
- insertLookupWithKey :: forall s a. (Key s -> a -> a -> a) -> Int -> a -> IntMap s a -> (Maybe (Key s, a), SomeIntMapWith (InsertProof 'Int Int s) a)
- delete :: forall s a. Int -> IntMap s a -> SomeIntMapWith (SupersetProof 'Int s) a
- adjust :: forall s a. (a -> a) -> Key s -> IntMap s a -> IntMap s a
- adjustWithKey :: forall s a. (Key s -> a -> a) -> Int -> IntMap s a -> IntMap s a
- update :: forall s a. (a -> Maybe a) -> Key s -> IntMap s a -> SomeIntMapWith (SupersetProof 'Int s) a
- updateLookupWithKey :: forall s a. (Key s -> a -> Maybe a) -> Int -> IntMap s a -> (Maybe (Key s, a), SomeIntMapWith (SupersetProof 'Int s) a)
- lookup :: forall s a. Int -> IntMap s a -> Maybe (Key s, a)
- (!) :: forall s a. IntMap s a -> Key s -> a
- member :: forall s a. Int -> IntMap s a -> Maybe (Key s)
- lookupLT :: forall s a. Int -> IntMap s a -> Maybe (Key s, a)
- lookupGT :: forall s a. Int -> IntMap s a -> Maybe (Key s, a)
- lookupLE :: forall s a. Int -> IntMap s a -> Maybe (Key s, a)
- lookupGE :: forall s a. Int -> IntMap s a -> Maybe (Key s, a)
- null :: forall s a. IntMap s a -> Maybe (EmptyProof 'Int s)
- isSubmapOfBy :: forall s t a b. (a -> b -> Bool) -> IntMap s a -> IntMap t b -> Maybe (SubsetProof 'Int s t)
- newtype SubsetProof f s r = SubsetProof (InSet f s :-> InSet f r)
- disjoint :: forall s t a b. IntMap s a -> IntMap t b -> Maybe (DisjointProof 'Int s t)
- newtype DisjointProof f s r = DisjointProof (forall t. (InSet f t :-> InSet f s) -> (InSet f t :-> InSet f r) -> forall u. InSet f t :-> InSet f u)
- zipWithKey :: forall s a b c. (Key s -> a -> b -> c) -> IntMap s a -> IntMap s b -> IntMap s c
- bind :: forall s a b. IntMap s a -> (a -> IntMap s b) -> IntMap s b
- unionWithKey :: forall s t a. (Refined (InSet 'Int s && InSet 'Int t) Int -> a -> a -> a) -> IntMap s a -> IntMap t a -> SomeIntMapWith (UnionProof 'Int s t) a
- data UnionProof f s t r = UnionProof ((InSet f s || InSet f t) :-> InSet f r) (forall u. (InSet f s :-> InSet f u) -> (InSet f t :-> InSet f u) -> InSet f r :-> InSet f u)
- difference :: forall s t a b. IntMap s a -> IntMap t b -> SomeIntMapWith (DifferenceProof 'Int s t) a
- data DifferenceProof f s t r = DifferenceProof (InSet f r :-> InSet f s) (forall u. (InSet f u :-> InSet f r) -> (InSet f u :-> InSet f t) -> forall v. InSet f u :-> InSet f v) (InSet f s :-> (InSet f t || InSet f r))
- differenceWithKey :: forall s t a b. (Refined (InSet 'Int s && InSet 'Int t) Int -> a -> b -> Maybe a) -> IntMap s a -> IntMap t b -> SomeIntMapWith (PartialDifferenceProof 'Int s t) a
- data PartialDifferenceProof f s t r = PartialDifferenceProof (InSet f r :-> InSet f s) (InSet f s :-> (InSet f t || InSet f r))
- intersectionWithKey :: forall s t a b c. (Refined (InSet 'Int s && InSet 'Int t) Int -> a -> b -> c) -> IntMap s a -> IntMap t b -> SomeIntMapWith (IntersectionProof 'Int s t) c
- data IntersectionProof f s t r = IntersectionProof (InSet f r :-> (InSet f s && InSet f t)) (forall u. (InSet f u :-> InSet f s) -> (InSet f u :-> InSet f t) -> InSet f u :-> InSet f r)
- mapWithKey :: forall s a b. (Key s -> a -> b) -> IntMap s a -> IntMap s b
- traverseWithKey :: forall s f a b. Applicative f => (Key s -> a -> f b) -> IntMap s a -> f (IntMap s b)
- mapAccumLWithKey :: forall s a b c. (a -> Key s -> b -> (a, c)) -> a -> IntMap s b -> (a, IntMap s c)
- mapAccumRWithKey :: forall s a b c. (a -> Key s -> b -> (a, c)) -> a -> IntMap s b -> (a, IntMap s c)
- mapKeysWith :: forall s a. (a -> a -> a) -> (Key s -> Int) -> IntMap s a -> SomeIntMapWith (MapProof 'Int s Int Int) a
- data MapProof f s a b r = MapProof (Refined (InSet f s) a -> Refined (InSet f r) b) (Refined (InSet f r) b -> Refined (InSet f s) a)
- backpermuteKeys :: forall s1 s2 a. KnownIntSet s2 => (Key s2 -> Key s1) -> IntMap s1 a -> IntMap s2 a
- foldMapWithKey :: forall s a m. Monoid m => (Key s -> a -> m) -> IntMap s a -> m
- foldrWithKey :: forall s a b. (Key s -> a -> b -> b) -> b -> IntMap s a -> b
- foldlWithKey :: forall s a b. (b -> Key s -> a -> b) -> b -> IntMap s a -> b
- foldrWithKey' :: forall s a b. (Key s -> a -> b -> b) -> b -> IntMap s a -> b
- foldlWithKey' :: forall s a b. (b -> Key s -> a -> b) -> b -> IntMap s a -> b
- toIntMap :: forall s a. IntMap s a -> IntMap a
- keysSet :: forall s a. IntMap s a -> IntSet s
- toList :: forall s a. IntMap s a -> [(Key s, a)]
- toDescList :: forall s a. IntMap s a -> [(Key s, a)]
- restrictKeys :: forall s t a. KnownIntSet t => IntMap s a -> SomeIntMapWith (IntersectionProof 'Int s t) a
- withoutKeys :: forall s t a. KnownIntSet t => IntMap s a -> SomeIntMapWith (DifferenceProof 'Int s t) a
- filterWithKey :: forall s a. (Key s -> a -> Bool) -> IntMap s a -> SomeIntMapWith (SupersetProof 'Int s) a
- partitionWithKey :: forall s a. (Key s -> a -> Bool) -> IntMap s a -> Some2IntMapWith (PartitionProof 'Int s Int) a a
- data PartitionProof f s a r q = PartitionProof (Refined (InSet f s) a -> Either (Refined (InSet f r) a) (Refined (InSet f q) a)) ((InSet f r || InSet f q) :-> InSet f s) (forall t. (InSet f r :-> InSet f t) -> (InSet f q :-> InSet f t) -> InSet f s :-> InSet f t) (forall t. (InSet f t :-> InSet f r) -> (InSet f t :-> InSet f q) -> forall u. InSet f t :-> InSet f u)
- spanAntitone :: forall s a. (Key s -> Bool) -> IntMap s a -> Some2IntMapWith (PartialPartitionProof 'Int s) a a
- data PartialPartitionProof f s r q = PartialPartitionProof ((InSet f r || InSet f q) :-> InSet f s) (forall t. (InSet f r :-> InSet f t) -> (InSet f q :-> InSet f t) -> InSet f s :-> InSet f t) (forall t. (InSet f t :-> InSet f r) -> (InSet f t :-> InSet f q) -> forall u. InSet f t :-> InSet f u)
- mapMaybeWithKey :: forall s a b. (Key s -> a -> Maybe b) -> IntMap s a -> SomeIntMapWith (SupersetProof 'Int s) b
- mapEitherWithKey :: forall s a b c. (Key s -> a -> Either b c) -> IntMap s a -> Some2IntMapWith (PartitionProof 'Int s Int) b c
- splitLookup :: forall s a. Int -> IntMap s a -> Some2IntMapWith (SplitProof 'Int s (Key s, a)) a a
- data SplitProof f s e r q = SplitProof !(Maybe e) ((InSet f r || InSet f q) :-> InSet f s) (forall t. (InSet f t :-> InSet f r) -> (InSet f t :-> InSet f q) -> forall u. InSet f t :-> InSet f u)
- updateMinWithKey :: forall s a. (Key s -> a -> Maybe a) -> IntMap s a -> SomeIntMapWith (SupersetProof 'Int s) a
- updateMaxWithKey :: forall s a. (Key s -> a -> Maybe a) -> IntMap s a -> SomeIntMapWith (SupersetProof 'Int s) a
- adjustMinWithKey :: forall s a. (Key s -> a -> a) -> IntMap s a -> IntMap s a
- adjustMaxWithKey :: forall s a. (Key s -> a -> a) -> IntMap s a -> IntMap s a
- minViewWithKey :: forall s a. IntMap s a -> Either (EmptyProof 'Int s) ((Key s, a), SomeIntMapWith (SupersetProof 'Int s) a)
- maxViewWithKey :: forall s a. IntMap s a -> Either (EmptyProof 'Int s) ((Key s, a), SomeIntMapWith (SupersetProof 'Int s) a)
- castKey :: forall s t k. (forall x. Refined (InSet 'Int s) x -> Refined (InSet 'Int t) x) -> (forall x. Refined (InSet 'Int t) x -> Refined (InSet 'Int s) x) -> Coercion (Refined (InSet 'Int s) k) (Refined (InSet 'Int t) k)
- cast :: forall s t k. (forall x. Coercion (Refined (InSet 'Int s) x) (Refined (InSet 'Int t) x)) -> Coercion (IntMap s k) (IntMap t k)
- castFlavor :: forall (f :: Flavor) (g :: Flavor) s a. Coercion (Refined (InSet f s) a) (Refined (InSet g s) a)
Map type
A wrapper around a regular IntMap
with a type parameter s
identifying the set of keys present in the map.
An Int
key may not be present in the map, but a
is guaranteed to
be present (if the Key
ss
parameters match). Thus the map is isomorphic to a
(total) function
, which motivates many of the instances below.Key
s -> a
An IntMap
always knows its set of keys, so given
we can
always derive IntMap
s a
by pattern matching on the KnownIntSet
sDict
returned by
keysSet
.
Instances
KnownIntSet s => Representable (IntMap s) Source # | Witness isomorphism with functions from |
Foldable (IntMap s) Source # | |
Defined in Data.IntMap.Common.Refined fold :: Monoid m => IntMap s m -> m # foldMap :: Monoid m => (a -> m) -> IntMap s a -> m # foldMap' :: Monoid m => (a -> m) -> IntMap s a -> m # foldr :: (a -> b -> b) -> b -> IntMap s a -> b # foldr' :: (a -> b -> b) -> b -> IntMap s a -> b # foldl :: (b -> a -> b) -> b -> IntMap s a -> b # foldl' :: (b -> a -> b) -> b -> IntMap s a -> b # foldr1 :: (a -> a -> a) -> IntMap s a -> a # foldl1 :: (a -> a -> a) -> IntMap s a -> a # elem :: Eq a => a -> IntMap s a -> Bool # maximum :: Ord a => IntMap s a -> a # minimum :: Ord a => IntMap s a -> a # | |
Traversable (IntMap s) Source # | |
KnownIntSet s => Applicative (IntMap s) Source # | Similar to the instance for functions -- zip corresponding keys. To use
|
Functor (IntMap s) Source # | |
KnownIntSet s => Monad (IntMap s) Source # | Similar to the instance for functions. To use |
KnownIntSet s => Distributive (IntMap s) Source # | Similar to the instance for functions |
FoldableWithIndex (Key s) (IntMap s) Source # | |
Defined in Data.IntMap.Common.Refined ifoldMap :: Monoid m => (Key s -> a -> m) -> IntMap s a -> m # ifoldMap' :: Monoid m => (Key s -> a -> m) -> IntMap s a -> m # ifoldr :: (Key s -> a -> b -> b) -> b -> IntMap s a -> b # ifoldl :: (Key s -> b -> a -> b) -> b -> IntMap s a -> b # | |
FunctorWithIndex (Key s) (IntMap s) Source # | |
TraversableWithIndex (Key s) (IntMap s) Source # | |
Defined in Data.IntMap.Common.Refined | |
KnownIntSet s => MonadReader (Key s) (IntMap s) Source # | Similar to the instance for functions. See also
|
(KnownIntSet s, Monoid a) => Monoid (IntMap s a) Source # | |
Semigroup a => Semigroup (IntMap s a) Source # | Append the values at the corresponding keys |
Show a => Show (IntMap s a) Source # | |
NFData a => NFData (IntMap s a) Source # | |
Defined in Data.IntMap.Common.Refined | |
Eq a => Eq (IntMap s a) Source # | |
Ord a => Ord (IntMap s a) Source # | |
Defined in Data.IntMap.Common.Refined | |
Hashable a => Hashable (IntMap s a) Source # | |
Defined in Data.IntMap.Common.Refined | |
type Rep (IntMap s) Source # | |
Defined in Data.IntMap.Common.Refined |
type Key s = Refined (InSet 'Int s) Int Source #
is a key of type Key
sInt
that has been verified to be an element
of the set s
, and thus verified to be present in all
maps.IntMap
s k
Thus,
is a "refinement" type of Key
sInt
, and this library
integrates with an implementation of refimenement types in Refined, so
the machinery from there can be used to manipulate Key
s (however see
revealPredicate
).
The underlying Int
value can be obtained with unrefine
. An Int
can be
validated into an
with Key
smember
.
Existentials and common proofs
data SomeIntMap a where Source #
An existential wrapper for an IntMap
with an as-yet-unknown set of keys.
Pattern maching on it gives you a way to refer to the set (the parameter
s
), e.g.
casefromIntMap
... ofSomeIntMap
@s m -> doSomethingWith @s casefromIntMap
... ofSomeIntMap
(m ::IntMap
s a) -> doSomethingWith @s
SomeIntMap :: forall s a. !(IntMap s a) -> SomeIntMap a |
withIntMap :: forall a r. SomeIntMap a -> (forall s. IntMap s a -> r) -> r Source #
Apply a map with an unknown set of keys to a continuation that can accept
a map with any set of keys. This gives you a way to refer to the set (the
parameter s
), e.g.:
withIntMap
(fromIntMap
...) $ (m ::IntMap
s a) -> doSomethingWith @s
data SomeIntMapWith p a where Source #
An existential wrapper for an IntMap
with an as-yet-unknown set of keys,
together with a proof of some fact p
about the set. Pattern matching on it
gives you a way to refer to the set (the parameter s
). Functions that
change the set of keys in a map will return the map in this way, together
with a proof that somehow relates the keys set to the function's inputs.
SomeIntMapWith :: forall s a p. !(IntMap s a) -> !(p s) -> SomeIntMapWith p a |
withIntMapWith :: forall a r p. SomeIntMapWith p a -> (forall s. IntMap s a -> p s -> r) -> r Source #
Apply a map with proof for an unknown set of keys to a continuation that
can accept a map with any set of keys satisfying the proof. This gives you a
way to refer to the set (the parameter s
).
data Some2IntMapWith p a b where Source #
An existential wrapper for a pair of maps with as-yet-unknown sets of keys,
together with a proof of some fact p
relating them.
Some2IntMapWith :: forall s t a b p. !(IntMap s a) -> !(IntMap t b) -> !(p s t) -> Some2IntMapWith p a b |
with2IntMapWith :: forall a b r p. Some2IntMapWith p a b -> (forall s t. IntMap s a -> IntMap t b -> p s t -> r) -> r Source #
Apply a pair of maps with proof for unknown sets of keys to a continuation
that can accept any pair of maps with any sets of keys satisfying the proof.
This gives you a way to refer to the sets (the parameters s
and t
).
newtype SupersetProof f s r Source #
Proof that s
is a superset of the set r
.
SupersetProof (InSet f r :-> InSet f s) | \(r \subseteq s\) |
newtype EmptyProof f r Source #
Proof that the set r
is empty.
EmptyProof (forall s. InSet f r :-> InSet f s) | \(\forall s, r \subseteq s\), which is equivalent to \(r \subseteq \varnothing\) |
Construction
empty :: forall a. SomeIntMapWith (EmptyProof 'Int) a Source #
An empty map.
singleton :: forall a. Int -> a -> SomeIntMapWith (SingletonProof 'Int Int) a Source #
Create a map with a single key-value pair, and return a proof that the key is in the resulting map.
newtype SingletonProof f a r Source #
Proof that r
contains an element of type a
.
SingletonProof (Refined (InSet f r) a) | The element that is guaranteed to be in |
fromSet :: forall s a. KnownIntSet s => (Key s -> a) -> IntMap s a Source #
Create a map from a set of keys, and a function that for each key computes the corresponding value.
fromIntMap :: forall a. IntMap a -> SomeIntMap a Source #
Construct a map from a regular IntMap
.
fromTraversableWithKey :: forall t a. Traversable t => (Int -> a -> a -> a) -> t (Int, a) -> SomeIntMapWith (FromTraversableProof 'Int t Int) a Source #
Create a map from an arbitrary traversable of key-value pairs.
newtype FromTraversableProof f (t :: Type -> Type) a r Source #
Proof that elements of t a
are contained in r
.
FromTraversableProof (t (Refined (InSet f r) a)) | The original traversable, with all elements refined with a guarantee of
being in |
Insertion
insert :: forall s a. Int -> a -> IntMap s a -> SomeIntMapWith (InsertProof 'Int Int s) a Source #
Insert a key-value pair into the map to obtain a potentially larger map, guaranteed to contain the given key. If the key was already present, the associated value is replaced with the supplied value.
data InsertProof f a s r Source #
Proof that r
is s
with a
inserted.
reinsert :: forall s a. Key s -> a -> IntMap s a -> IntMap s a Source #
Overwrite a key-value pair that is known to already be in the map. The set of keys remains the same.
insertLookupWithKey :: forall s a. (Key s -> a -> a -> a) -> Int -> a -> IntMap s a -> (Maybe (Key s, a), SomeIntMapWith (InsertProof 'Int Int s) a) Source #
Insert a key-value pair into the map using a combining function, and if the key was already present, the old value is returned along with the proof that the key was present.
Deletion/Update
delete :: forall s a. Int -> IntMap s a -> SomeIntMapWith (SupersetProof 'Int s) a Source #
Delete a key and its value from the map if present, returning a potentially smaller map.
adjust :: forall s a. (a -> a) -> Key s -> IntMap s a -> IntMap s a Source #
Update the value at a specific key known the be in the map using the given function. The set of keys remains the same.
adjustWithKey :: forall s a. (Key s -> a -> a) -> Int -> IntMap s a -> IntMap s a Source #
If the given key is in the map, update the associated value using the given function with a proof that the key was in the map; otherwise return the map unchanged. In any case the set of keys remains the same.
update :: forall s a. (a -> Maybe a) -> Key s -> IntMap s a -> SomeIntMapWith (SupersetProof 'Int s) a Source #
Update or delete a key known to be in the map using the given function, returning a potentially smaller map.
updateLookupWithKey :: forall s a. (Key s -> a -> Maybe a) -> Int -> IntMap s a -> (Maybe (Key s, a), SomeIntMapWith (SupersetProof 'Int s) a) Source #
If the given key is in the map, update or delete it using the given function with a proof that the key was in the map; otherwise the map is unchanged. Alongside return the new value if it was updated, or the old value if it was deleted, and a proof that the key was in the map.
Query
lookup :: forall s a. Int -> IntMap s a -> Maybe (Key s, a) Source #
If the key is in the map, return the proof of this, and the associated
value; otherwise return Nothing
.
(!) :: forall s a. IntMap s a -> Key s -> a Source #
Given a key that is proven to be in the map, return the associated value.
Unlike !
from Data.IntMap, this function is total, as it is
impossible to obtain a
for a key that is not in the map
Key
s
.IntMap
s a
member :: forall s a. Int -> IntMap s a -> Maybe (Key s) Source #
If a key is in the map, return the proof that it is.
lookupLT :: forall s a. Int -> IntMap s a -> Maybe (Key s, a) Source #
Find the largest key smaller than the given one, and return the associated key-value pair.
lookupGT :: forall s a. Int -> IntMap s a -> Maybe (Key s, a) Source #
Find the smallest key greater than the given one, and return the associated key-value pair.
lookupLE :: forall s a. Int -> IntMap s a -> Maybe (Key s, a) Source #
Find the largest key smaller or equal to the given one, and return the associated key-value pair.
lookupGE :: forall s a. Int -> IntMap s a -> Maybe (Key s, a) Source #
Find the smallest key greater or equal to the given one, and return the associated key-value pair.
null :: forall s a. IntMap s a -> Maybe (EmptyProof 'Int s) Source #
If a map is empty, return a proof that it is.
isSubmapOfBy :: forall s t a b. (a -> b -> Bool) -> IntMap s a -> IntMap t b -> Maybe (SubsetProof 'Int s t) Source #
If all keys of the first map are also present in the second map, and the
given function returns True
for their associated values, return a proof
that the keys form a subset.
newtype SubsetProof f s r Source #
Proof that s
is a subset of the set r
.
SubsetProof (InSet f s :-> InSet f r) | \(s \subseteq r\) |
disjoint :: forall s t a b. IntMap s a -> IntMap t b -> Maybe (DisjointProof 'Int s t) Source #
If two maps are disjoint (i.e. their intersection is empty), return a proof of that.
newtype DisjointProof f s r Source #
Proof that s
and r
are disjoint.
Combine
zipWithKey :: forall s a b c. (Key s -> a -> b -> c) -> IntMap s a -> IntMap s b -> IntMap s c Source #
Given two maps proven to have the same keys, for each key apply the function to the associated values, to obtain a new map with the same keys.
unionWithKey :: forall s t a. (Refined (InSet 'Int s && InSet 'Int t) Int -> a -> a -> a) -> IntMap s a -> IntMap t a -> SomeIntMapWith (UnionProof 'Int s t) a Source #
data UnionProof f s t r Source #
Proof that unioning s
and t
gives r
.
difference :: forall s t a b. IntMap s a -> IntMap t b -> SomeIntMapWith (DifferenceProof 'Int s t) a Source #
Remove the keys that appear in the second map from the first map.
data DifferenceProof f s t r Source #
Proof that if from s
you subtract t
, then you get r
.
DifferenceProof | |
|
differenceWithKey :: forall s t a b. (Refined (InSet 'Int s && InSet 'Int t) Int -> a -> b -> Maybe a) -> IntMap s a -> IntMap t b -> SomeIntMapWith (PartialDifferenceProof 'Int s t) a Source #
data PartialDifferenceProof f s t r Source #
Proof that r
is obtained by removing some of t
's elements from s
.
intersectionWithKey :: forall s t a b c. (Refined (InSet 'Int s && InSet 'Int t) Int -> a -> b -> c) -> IntMap s a -> IntMap t b -> SomeIntMapWith (IntersectionProof 'Int s t) c Source #
data IntersectionProof f s t r Source #
Proof that intersecting s
and t
gives r
.
Traversal
mapWithKey :: forall s a b. (Key s -> a -> b) -> IntMap s a -> IntMap s b Source #
Apply a function to all values in a map, together with their corresponding keys, that are proven to be in the map. The set of keys remains the same.
traverseWithKey :: forall s f a b. Applicative f => (Key s -> a -> f b) -> IntMap s a -> f (IntMap s b) Source #
Map an Applicative
transformation in ascending order of keys, with access
to each value's corresponding key and a proof that it is in the map. The set
of keys remains unchanged.
mapAccumLWithKey :: forall s a b c. (a -> Key s -> b -> (a, c)) -> a -> IntMap s b -> (a, IntMap s c) Source #
Thread an accumularing argument through the map in ascending order of keys.
mapAccumRWithKey :: forall s a b c. (a -> Key s -> b -> (a, c)) -> a -> IntMap s b -> (a, IntMap s c) Source #
Thread an accumularing argument through the map in descending order of keys.
mapKeysWith :: forall s a. (a -> a -> a) -> (Key s -> Int) -> IntMap s a -> SomeIntMapWith (MapProof 'Int s Int Int) a Source #
applies mapKeysWith
c f mf
to each key of m
and collects the
results into a new map. For keys that were mapped to the same new key, c
acts as the combining function for corresponding values.
data MapProof f s a b r Source #
Proof that r
is the direct image of s
under some mapping f :: a -> b
.
backpermuteKeys :: forall s1 s2 a. KnownIntSet s2 => (Key s2 -> Key s1) -> IntMap s1 a -> IntMap s2 a Source #
Apply the inverse image of the given function to the keys of the given map,
so that for all k ::
,
Key
s2
.backpermuteKeys
f m !
k = m !
f k
If maps are identified with functions, this computes the composition.
Folds
foldMapWithKey :: forall s a m. Monoid m => (Key s -> a -> m) -> IntMap s a -> m Source #
Map each key-value pair of a map into a monoid (with proof that the key was
in the map), and combine the results using <>
.
foldrWithKey :: forall s a b. (Key s -> a -> b -> b) -> b -> IntMap s a -> b Source #
Right associative fold with a lazy accumulator.
foldlWithKey :: forall s a b. (b -> Key s -> a -> b) -> b -> IntMap s a -> b Source #
Left associative fold with a lazy accumulator.
foldrWithKey' :: forall s a b. (Key s -> a -> b -> b) -> b -> IntMap s a -> b Source #
Right associative fold with a strict accumulator.
foldlWithKey' :: forall s a b. (b -> Key s -> a -> b) -> b -> IntMap s a -> b Source #
Left associative fold with a strict accumulator.
Conversion
toIntMap :: forall s a. IntMap s a -> IntMap a Source #
Convert to a regular IntMap
, forgetting its set of keys.
keysSet :: forall s a. IntMap s a -> IntSet s Source #
Return the set of keys in the map, with the contents of the set still
tracked by the s
parameter. See Data.IntSet.Refined.
toList :: forall s a. IntMap s a -> [(Key s, a)] Source #
Convert to a list of key-value pairs in ascending order of keys.
toDescList :: forall s a. IntMap s a -> [(Key s, a)] Source #
Convert to a list of key-value pairs in descending order of keys.
Filter
restrictKeys :: forall s t a. KnownIntSet t => IntMap s a -> SomeIntMapWith (IntersectionProof 'Int s t) a Source #
Restrict a map to only those keys that are elements of t
.
withoutKeys :: forall s t a. KnownIntSet t => IntMap s a -> SomeIntMapWith (DifferenceProof 'Int s t) a Source #
Remove all keys that are elements of t
from the map.
filterWithKey :: forall s a. (Key s -> a -> Bool) -> IntMap s a -> SomeIntMapWith (SupersetProof 'Int s) a Source #
Retain only the key-value pairs that satisfy the predicate, returning a potentially smaller map.
partitionWithKey :: forall s a. (Key s -> a -> Bool) -> IntMap s a -> Some2IntMapWith (PartitionProof 'Int s Int) a a Source #
Partition a map into two disjoint submaps: those whose key-value pairs satisfy the predicate, and those whose don't.
data PartitionProof f s a r q Source #
Proof that s
is the union of disjoint subsets r
and q
, together with
a procedure that decides which of the two an element belongs to.
PartitionProof | |
|
spanAntitone :: forall s a. (Key s -> Bool) -> IntMap s a -> Some2IntMapWith (PartialPartitionProof 'Int s) a a Source #
Divide a map into two disjoint submaps at a point where the predicate on the keys stops holding.
If p
is antitone ( \(\forall x y, x < y \implies p(x) \ge p(y)\) ), then
this point is uniquely defined. If p
is not antitone, a splitting point is
chosen in an unspecified way.
data PartialPartitionProof f s r q Source #
Proof that s
is the union of disjoint subsets r
and q
, but without a
deciding procedure.
PartialPartitionProof | |
|
mapMaybeWithKey :: forall s a b. (Key s -> a -> Maybe b) -> IntMap s a -> SomeIntMapWith (SupersetProof 'Int s) b Source #
Apply a function to all values in a map, together with their corresponding
keys, and collect only the Just
results, returning a potentially smaller
map.
mapEitherWithKey :: forall s a b c. (Key s -> a -> Either b c) -> IntMap s a -> Some2IntMapWith (PartitionProof 'Int s Int) b c Source #
splitLookup :: forall s a. Int -> IntMap s a -> Some2IntMapWith (SplitProof 'Int s (Key s, a)) a a Source #
Return two disjoint submaps: those whose keys are less than the given key, and those whose keys are greater than the given key. If the key was in the map, also return the associated value and the proof that it was in the map.
data SplitProof f s e r q Source #
Proof that s
contains disjoint subsets r
and q
, along with an
optional element between them.
SplitProof | |
|
Min/Max
updateMinWithKey :: forall s a. (Key s -> a -> Maybe a) -> IntMap s a -> SomeIntMapWith (SupersetProof 'Int s) a Source #
Update or delete the value at the smallest key, returning a potentially smaller map.
updateMaxWithKey :: forall s a. (Key s -> a -> Maybe a) -> IntMap s a -> SomeIntMapWith (SupersetProof 'Int s) a Source #
Update or delete the value at the largest key, returning a potentially smaller map.
adjustMinWithKey :: forall s a. (Key s -> a -> a) -> IntMap s a -> IntMap s a Source #
Adjust the value at the smallest key. The set of keys remains unchanged.
adjustMaxWithKey :: forall s a. (Key s -> a -> a) -> IntMap s a -> IntMap s a Source #
Adjust the value at the greatest key. The set of keys remains unchanged.
minViewWithKey :: forall s a. IntMap s a -> Either (EmptyProof 'Int s) ((Key s, a), SomeIntMapWith (SupersetProof 'Int s) a) Source #
Retrieves the key-value pair corresponding to the smallest key of the map, and the map with that pair removed; or a proof that the map was empty.
maxViewWithKey :: forall s a. IntMap s a -> Either (EmptyProof 'Int s) ((Key s, a), SomeIntMapWith (SupersetProof 'Int s) a) Source #
Retrieves the key-value pair corresponding to the greatest key of the map, and the map with that pair removed; or a proof that the map was empty.
Casts
castKey :: forall s t k. (forall x. Refined (InSet 'Int s) x -> Refined (InSet 'Int t) x) -> (forall x. Refined (InSet 'Int t) x -> Refined (InSet 'Int s) x) -> Coercion (Refined (InSet 'Int s) k) (Refined (InSet 'Int t) k) Source #
If elements of s
can be weakened to elements of t
and vice versa, then
s
and t
actually stand for the same set and
can be safely
interconverted with Key
s
.Key
t
The requirement that the weakenings are natural transformations ensures that
they don't actually alter the keys. To build these you can compose :->
's
from proofs returned by functions in this module, or Refined functions like
andLeft
or leftOr
.
cast :: forall s t k. (forall x. Coercion (Refined (InSet 'Int s) x) (Refined (InSet 'Int t) x)) -> Coercion (IntMap s k) (IntMap t k) Source #
If keys can be interconverted (e.g. as proved by castKey
), then the maps
can be interconverted too. For example, zipWithKey
can be implemented via
intersectionWithKey
by proving that the set of keys
remains unchanged:
zipWithKey
:: forall s a b c. (Key
s -> a -> b -> c) ->IntMap
s a ->IntMap
s b ->IntMap
s czipWithKey
f m1 m2 |SomeIntMapWith
@r m proof <-intersectionWithKey
(f .andLeft
) m1 m2 ,IntersectionProof
p1 p2 <- proof , (Coercion
::Coercion
(IntMap
r c) (IntMap
s c)) <- app $cast
$castKey
(andLeft
. p1) (p2id
id
) =coerce
m where app ::Coercion
f g ->Coercion
(f x) (g x) appCoercion
=Coercion