Data.HashMap.Refined

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, HashMap s k v has a type parameter s that identifies its set of keys, so that if another map has the same type parameter, you know that map has the same set of keys. There is Key s k, a type of keys that have been validated to belong to the set identified by s, and for which the operation of indexing into a HashMap s k v (only for the same s) 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.HashMap.Lazy, functions in this module are strict in the keys but lazy in the values. The Data.HashMap.Strict.Refined module reuses the same HashMap type but provides functions that operate strictly on the values.

Warning

This module together with Data.HashMap.Lazy rely on Eq and Hashable instances being lawful: that == is an equivalence relation, and that hashWithSalt is defined on the quotient by this equivalence relation; at least for the subset of values that are actually encountered at runtime. If this assumption is violated, this module may not be able to uphold its invariants and may throw errors. In particular beware of NaN in Float and Double, and, if using hashable < 1.3, beware of 0 and -0.

Map type

data HashMap s k a

A wrapper around a regular HashMap with a type parameter s identifying the set of keys present in the map.

A key of type k may not be present in the map, but a Key s k is guaranteed to be present (if the s parameters match). Thus the map is isomorphic to a (total) function Key s k -> a, which motivates many of the instances below.

A HashMap always knows its set of keys, so given HashMap s k a we can always derive KnownHashSet s k by pattern matching on the Dict returned by keysSet.

Instances

(Hashable k, KnownHashSet s k) => Representable (HashMap s k)

Witness isomorphism with functions from Key s k

Defined in Data.HashMap.Common.Refined

Associated Types

type Rep (HashMap s k)

Methods

tabulate :: (Rep (HashMap s k) -> a) -> HashMap s k a

index :: HashMap s k a -> Rep (HashMap s k) -> a

Foldable (HashMap s k)

Defined in Data.HashMap.Common.Refined

Methods

fold :: Monoid m => HashMap s k m -> m

foldMap :: Monoid m => (a -> m) -> HashMap s k a -> m

foldMap' :: Monoid m => (a -> m) -> HashMap s k a -> m

foldr :: (a -> b -> b) -> b -> HashMap s k a -> b

foldr' :: (a -> b -> b) -> b -> HashMap s k a -> b

foldl :: (b -> a -> b) -> b -> HashMap s k a -> b

foldl' :: (b -> a -> b) -> b -> HashMap s k a -> b

foldr1 :: (a -> a -> a) -> HashMap s k a -> a

foldl1 :: (a -> a -> a) -> HashMap s k a -> a

toList :: HashMap s k a -> [a]

null :: HashMap s k a -> Bool

length :: HashMap s k a -> Int

elem :: Eq a => a -> HashMap s k a -> Bool

maximum :: Ord a => HashMap s k a -> a

minimum :: Ord a => HashMap s k a -> a

sum :: Num a => HashMap s k a -> a

product :: Num a => HashMap s k a -> a

Traversable (HashMap s k)

Defined in Data.HashMap.Common.Refined

Methods

traverse :: Applicative f => (a -> f b) -> HashMap s k a -> f (HashMap s k b)

sequenceA :: Applicative f => HashMap s k (f a) -> f (HashMap s k a)

mapM :: Monad m => (a -> m b) -> HashMap s k a -> m (HashMap s k b)

sequence :: Monad m => HashMap s k (m a) -> m (HashMap s k a)

(Hashable k, KnownHashSet s k) => Applicative (HashMap s k)

Similar to the instance for functions -- zip corresponding keys. To use <*>/liftA2 without KnownSet see zipWithKey.

Defined in Data.HashMap.Common.Refined

Methods

pure :: a -> HashMap s k a

(<*>) :: HashMap s k (a -> b) -> HashMap s k a -> HashMap s k b

liftA2 :: (a -> b -> c) -> HashMap s k a -> HashMap s k b -> HashMap s k c

(*>) :: HashMap s k a -> HashMap s k b -> HashMap s k b

(<*) :: HashMap s k a -> HashMap s k b -> HashMap s k a

Functor (HashMap s k)

Defined in Data.HashMap.Common.Refined

Methods

fmap :: (a -> b) -> HashMap s k a -> HashMap s k b

(<$) :: a -> HashMap s k b -> HashMap s k a

(Hashable k, KnownHashSet s k) => Monad (HashMap s k)

Similar to the instance for functions. To use >>= without KnownSet see bind.

Defined in Data.HashMap.Common.Refined

Methods

(>>=) :: HashMap s k a -> (a -> HashMap s k b) -> HashMap s k b

(>>) :: HashMap s k a -> HashMap s k b -> HashMap s k b

return :: a -> HashMap s k a

(Hashable k, KnownHashSet s k) => Distributive (HashMap s k)

Similar to the instance for functions

Defined in Data.HashMap.Common.Refined

Methods

distribute :: Functor f => f (HashMap s k a) -> HashMap s k (f a)

collect :: Functor f => (a -> HashMap s k b) -> f a -> HashMap s k (f b)

distributeM :: Monad m => m (HashMap s k a) -> HashMap s k (m a)

collectM :: Monad m => (a -> HashMap s k b) -> m a -> HashMap s k (m b)

FoldableWithIndex (Key s k) (HashMap s k)

Defined in Data.HashMap.Common.Refined

Methods

ifoldMap :: Monoid m => (Key s k -> a -> m) -> HashMap s k a -> m

ifoldMap' :: Monoid m => (Key s k -> a -> m) -> HashMap s k a -> m

ifoldr :: (Key s k -> a -> b -> b) -> b -> HashMap s k a -> b

ifoldl :: (Key s k -> b -> a -> b) -> b -> HashMap s k a -> b

ifoldr' :: (Key s k -> a -> b -> b) -> b -> HashMap s k a -> b

ifoldl' :: (Key s k -> b -> a -> b) -> b -> HashMap s k a -> b

FunctorWithIndex (Key s k) (HashMap s k)

Defined in Data.HashMap.Common.Refined

Methods

imap :: (Key s k -> a -> b) -> HashMap s k a -> HashMap s k b

TraversableWithIndex (Key s k) (HashMap s k)

Defined in Data.HashMap.Common.Refined

Methods

itraverse :: Applicative f => (Key s k -> a -> f b) -> HashMap s k a -> f (HashMap s k b)

(Hashable k, KnownHashSet s k) => MonadReader (Key s k) (HashMap s k)

Similar to the instance for functions. See also backpermuteKeys.

Defined in Data.HashMap.Common.Refined

Methods

ask :: HashMap s k (Key s k)

local :: (Key s k -> Key s k) -> HashMap s k a -> HashMap s k a

reader :: (Key s k -> a) -> HashMap s k a

(Hashable k, KnownHashSet s k, Monoid a) => Monoid (HashMap s k a)

Defined in Data.HashMap.Common.Refined

Methods

mempty :: HashMap s k a

mappend :: HashMap s k a -> HashMap s k a -> HashMap s k a

mconcat :: [HashMap s k a] -> HashMap s k a

(Hashable k, Semigroup a) => Semigroup (HashMap s k a)

Append the values at the corresponding keys

Defined in Data.HashMap.Common.Refined

Methods

(<>) :: HashMap s k a -> HashMap s k a -> HashMap s k a

sconcat :: NonEmpty (HashMap s k a) -> HashMap s k a

stimes :: Integral b => b -> HashMap s k a -> HashMap s k a

(Show k, Show a) => Show (HashMap s k a)

Defined in Data.HashMap.Common.Refined

Methods

showsPrec :: Int -> HashMap s k a -> ShowS

show :: HashMap s k a -> String

showList :: [HashMap s k a] -> ShowS

(NFData k, NFData a) => NFData (HashMap s k a)

Defined in Data.HashMap.Common.Refined

Methods

rnf :: HashMap s k a -> ()

(Eq k, Eq a) => Eq (HashMap s k a)

Defined in Data.HashMap.Common.Refined

Methods

(==) :: HashMap s k a -> HashMap s k a -> Bool

(/=) :: HashMap s k a -> HashMap s k a -> Bool

(Ord k, Ord a) => Ord (HashMap s k a)

Defined in Data.HashMap.Common.Refined

Methods

compare :: HashMap s k a -> HashMap s k a -> Ordering

(<) :: HashMap s k a -> HashMap s k a -> Bool

(<=) :: HashMap s k a -> HashMap s k a -> Bool

(>) :: HashMap s k a -> HashMap s k a -> Bool

(>=) :: HashMap s k a -> HashMap s k a -> Bool

max :: HashMap s k a -> HashMap s k a -> HashMap s k a

min :: HashMap s k a -> HashMap s k a -> HashMap s k a

(Hashable k, Hashable a) => Hashable (HashMap s k a)

Defined in Data.HashMap.Common.Refined

Methods

hashWithSalt :: Int -> HashMap s k a -> Int

hash :: HashMap s k a -> Int

type Rep (HashMap s k)

Defined in Data.HashMap.Common.Refined

type Rep (HashMap s k) = Key s k

type Key s = Refined (InSet 'Hashed s)

Key s k is a key of type k that has been verified to be an element of the set s, and thus verified to be present in all HashMap s k maps.

Thus, Key s k is a "refinement" type of k, and this library integrates with an implementation of refimenement types in Refined, so the machinery from there can be used to manipulate Keys (however see revealPredicate).

The underlying k value can be obtained with unrefine. A k can be validated into an Key s k with member.

Existentials and common proofs

data SomeHashMap k a where

An existential wrapper for a HashMap 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.

case fromHashMap ... of
  SomeHashMap @s m -> doSomethingWith @s

case fromHashMap ... of
  SomeHashMap (m :: HashMap s k a) -> doSomethingWith @s

Constructors

SomeHashMap :: forall s k a. !(HashMap s k a) -> SomeHashMap k a

withHashMap :: forall k a r. SomeHashMap k a -> (forall s. HashMap s k a -> r) -> r

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

withHashMap (fromHashMap ...
  $ (m :: HashMap s k a) -> doSomethingWith @s

data SomeHashMapWith p k a where

An existential wrapper for a HashMap 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.

Constructors

SomeHashMapWith :: forall s k a p. !(HashMap s k a) -> !(p s) -> SomeHashMapWith p k a

withHashMapWith :: forall k a r p. SomeHashMapWith p k a -> (forall s. HashMap s k a -> p s -> r) -> r

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 Some2HashMapWith p k a b where

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.

Constructors

Some2HashMapWith :: forall s t k a b p. !(HashMap s k a) -> !(HashMap t k b) -> !(p s t) -> Some2HashMapWith p k a b

with2HashMapWith :: forall k a b r p. Some2HashMapWith p k a b -> (forall s t. HashMap s k a -> HashMap t k b -> p s t -> r) -> r

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

Proof that s is a superset of the set r.

Constructors

SupersetProof (InSet f r :-> InSet f s)

\(r \subseteq s\)

newtype EmptyProof f r

Proof that the set r is empty.

Constructors

EmptyProof (forall s. InSet f r :-> InSet f s)

\(\forall s, r \subseteq s\), which is equivalent to \(r \subseteq \varnothing\)

Construction

empty :: forall k a. SomeHashMapWith (EmptyProof 'Hashed) k a

An empty map.

singleton :: forall k a. Hashable k => k -> a -> SomeHashMapWith (SingletonProof 'Hashed k) k a

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

Proof that r contains an element of type a.

Constructors

SingletonProof (Refined (InSet f r) a)

The element that is guaranteed to be in r

fromSet :: forall s k a. KnownHashSet s k => (Key s k -> a) -> HashMap s k a

Create a map from a set of keys, and a function that for each key computes the corresponding value.

fromHashMap :: forall k a. HashMap k a -> SomeHashMap k a

Construct a map from a regular HashMap.

fromTraversableWithKey :: forall t k a. (Traversable t, Hashable k) => (k -> a -> a -> a) -> t (k, a) -> SomeHashMapWith (FromTraversableProof 'Hashed t k) k a

Create a map from an arbitrary traversable of key-value pairs.

newtype FromTraversableProof f (t :: Type -> Type) a r

Proof that elements of t a are contained in r.

Constructors

FromTraversableProof (t (Refined (InSet f r) a))

The original traversable, with all elements refined with a guarantee of being in r

Insertion

insert :: forall s k a. Hashable k => k -> a -> HashMap s k a -> SomeHashMapWith (InsertProof 'Hashed k s) k a

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

Proof that r is s with a inserted.

Constructors

InsertProof

Fields

• (Refined (InSet f r) a)

  The element that was inserted and is guaranteed to be in r.

• (InSet f s :-> InSet f r)

  \(s \subseteq r \)

reinsert :: forall s k a. Hashable k => Key s k -> a -> HashMap s k a -> HashMap s k a

Overwrite a key-value pair that is known to already be in the map. The set of keys remains the same.

insertLookupWithKey :: forall s k a. Hashable k => (Key s k -> a -> a -> a) -> k -> a -> HashMap s k a -> (Maybe (Key s k, a), SomeHashMapWith (InsertProof 'Hashed k s) k a)

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 k a. Hashable k => k -> HashMap s k a -> SomeHashMapWith (SupersetProof 'Hashed s) k a

Delete a key and its value from the map if present, returning a potentially smaller map.

adjust :: forall s k a. Hashable k => (a -> a) -> Key s k -> HashMap s k a -> HashMap s k a

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 k a. Hashable k => (Key s k -> a -> a) -> k -> HashMap s k a -> HashMap s k a

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 k a. Hashable k => (a -> Maybe a) -> Key s k -> HashMap s k a -> SomeHashMapWith (SupersetProof 'Hashed s) k a

Update or delete a key known to be in the map using the given function, returning a potentially smaller map.

updateLookupWithKey :: forall s k a. Hashable k => (Key s k -> a -> Maybe a) -> k -> HashMap s k a -> (Maybe (Key s k, a), SomeHashMapWith (SupersetProof 'Hashed s) k a)

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 k a. Hashable k => k -> HashMap s k a -> Maybe (Key s k, a)

If the key is in the map, return the proof of this, and the associated value; otherwise return Nothing.

(!) :: forall s k a. Hashable k => HashMap s k a -> Key s k -> a

Given a key that is proven to be in the map, return the associated value.

Unlike ! from Data.HashMap.Lazy, this function is total, as it is impossible to obtain a Key s k for a key that is not in the map HashMap s k a.

member :: forall s k a. Hashable k => k -> HashMap s k a -> Maybe (Key s k)

If a key is in the map, return the proof that it is.

null :: forall s k a. HashMap s k a -> Maybe (EmptyProof 'Hashed s)

If a map is empty, return a proof that it is.

isSubmapOfBy :: forall s t k a b. Hashable k => (a -> b -> Bool) -> HashMap s k a -> HashMap t k b -> Maybe (SubsetProof 'Hashed s t)

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

Proof that s is a subset of the set r.

Constructors

SubsetProof (InSet f s :-> InSet f r)

\(s \subseteq r\)

disjoint :: forall s t k a b. Hashable k => HashMap s k a -> HashMap t k b -> Maybe (DisjointProof 'Hashed s t)

If two maps are disjoint (i.e. their intersection is empty), return a proof of that.

newtype DisjointProof f s r

Proof that s and r are disjoint.

Constructors

DisjointProof (forall t. (InSet f t :-> InSet f s) -> (InSet f t :-> InSet f r) -> forall u. InSet f t :-> InSet f u)

\(\forall t,(t\subseteq s)\land(t\subseteq r)\implies\forall u,t\subseteq u\), which is equivalent to \(s \cap r \subseteq \varnothing\)

Combine

zipWithKey :: forall s k a b c. Hashable k => (Key s k -> a -> b -> c) -> HashMap s k a -> HashMap s k b -> HashMap s k c

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.

bind :: forall s k a b. Hashable k => HashMap s k a -> (a -> HashMap s k b) -> HashMap s k b

bind m f is a map that for each key k :: Key s k, contains the value f (m ! k) ! k, similar to >>= for functions.

unionWithKey :: forall s t k a. Hashable k => (Refined (InSet 'Hashed s && InSet 'Hashed t) k -> a -> a -> a) -> HashMap s k a -> HashMap t k a -> SomeHashMapWith (UnionProof 'Hashed s t) k a

Return the union of two maps, with a given combining function for keys that exist in both maps simultaneously.

You can use andLeft and andRight to obtain Key s k and Key t k respectively.

data UnionProof f s t r

Proof that unioning s and t gives r.

Constructors

UnionProof

Fields

• ((InSet f s || InSet f t) :-> InSet f r)

  \(s \cup t \subseteq r\)

• (forall u. (InSet f s :-> InSet f u) -> (InSet f t :-> InSet f u) -> InSet f r :-> InSet f u)

  \(\forall u,(s\subseteq u)\land(t\subseteq u)\implies r\subseteq u\), which is equivalent to \(r \subseteq s \cup u\)

difference :: forall s t k a b. Hashable k => HashMap s k a -> HashMap t k b -> SomeHashMapWith (DifferenceProof 'Hashed s t) k a

Remove the keys that appear in the second map from the first map.

data DifferenceProof f s t r

Proof that if from s you subtract t, then you get r.

Constructors

DifferenceProof

Fields

• (InSet f r :-> InSet f s)

  \(r \subseteq s\)

• (forall u. (InSet f u :-> InSet f r) -> (InSet f u :-> InSet f t) -> forall v. InSet f u :-> InSet f v)

  \(\forall u,(u\subseteq r)\land(u\subseteq t)\implies\forall v,u\subseteq v\), which is equivalent to \(r \cap t \subseteq \varnothing\)

• (InSet f s :-> (InSet f t || InSet f r))

  \(s \subseteq t \cup r\)

differenceWithKey :: forall s t k a b. Hashable k => (Refined (InSet 'Hashed s && InSet 'Hashed t) k -> a -> b -> Maybe a) -> HashMap s k a -> HashMap t k b -> SomeHashMapWith (PartialDifferenceProof 'Hashed s t) k a

For keys that appear in both maps, the given function decides whether the key is removed from the first map.

You can use andLeft and andRight to obtain Key s k and Key t k respectively.

data PartialDifferenceProof f s t r

Proof that r is obtained by removing some of t's elements from s.

Constructors

PartialDifferenceProof

Fields

• (InSet f r :-> InSet f s)

  \(r \subseteq s\)

• (InSet f s :-> (InSet f t || InSet f r))

  \(s \subseteq t \cup r\)

intersectionWithKey :: forall s t k a b c. Hashable k => (Refined (InSet 'Hashed s && InSet 'Hashed t) k -> a -> b -> c) -> HashMap s k a -> HashMap t k b -> SomeHashMapWith (IntersectionProof 'Hashed s t) k c

Return the intersection of two maps with the given combining function.

You can use andLeft and andRight to obtain Key s k and Key t k respectively.

data IntersectionProof f s t r

Proof that intersecting s and t gives r.

Constructors

IntersectionProof

Fields

• (InSet f r :-> (InSet f s && InSet f t))

  \(r \subseteq s \cap t\)

• (forall u. (InSet f u :-> InSet f s) -> (InSet f u :-> InSet f t) -> InSet f u :-> InSet f r)

  \(\forall u,(u\subseteq s)\land(u\subseteq t)\implies u\subseteq r\), which is equivalent to \(s \cap t \subseteq r\)

Traversal

mapWithKey :: forall s k a b. (Key s k -> a -> b) -> HashMap s k a -> HashMap s k b

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 k a b. Applicative f => (Key s k -> a -> f b) -> HashMap s k a -> f (HashMap s k b)

Map an Applicative transformation 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 k a b c. (a -> Key s k -> b -> (a, c)) -> a -> HashMap s k b -> (a, HashMap s k c)

Thread an accumularing argument through the map in ascending order of hashes.

mapAccumRWithKey :: forall s k a b c. (a -> Key s k -> b -> (a, c)) -> a -> HashMap s k b -> (a, HashMap s k c)

Thread an accumularing argument through the map in descending order of hashes.

mapKeysWith :: forall s k1 k2 a. Hashable k2 => (a -> a -> a) -> (Key s k1 -> k2) -> HashMap s k1 a -> SomeHashMapWith (MapProof 'Hashed s k1 k2) k2 a

mapKeysWith c f m applies f 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

Proof that r is the direct image of s under some mapping f :: a -> b.

Constructors

MapProof

Fields

• (Refined (InSet f s) a -> Refined (InSet f r) b)

  Compute the image of an element of s (the image is then an element of r)

• (Refined (InSet f r) b -> Refined (InSet f s) a)

  For an element of r, return an arbitrary preimage from s

backpermuteKeys :: forall s1 s2 k1 k2 a. (Hashable k1, KnownHashSet s2 k2) => (Key s2 k2 -> Key s1 k1) -> HashMap s1 k1 a -> HashMap s2 k2 a

Apply the inverse image of the given function to the keys of the given map, so that for all k :: Key s2 k2,c backpermuteKeys f m ! k = m ! f k.

If maps are identified with functions, this computes the composition.

Folds

foldMapWithKey :: forall s k a m. Monoid m => (Key s k -> a -> m) -> HashMap s k a -> m

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 k a b. (Key s k -> a -> b -> b) -> b -> HashMap s k a -> b

Right associative fold with a lazy accumulator.

foldlWithKey :: forall s k a b. (b -> Key s k -> a -> b) -> b -> HashMap s k a -> b

Left associative fold with a lazy accumulator.

foldrWithKey' :: forall s k a b. (Key s k -> a -> b -> b) -> b -> HashMap s k a -> b

Right associative fold with a strict accumulator.

foldlWithKey' :: forall s k a b. (b -> Key s k -> a -> b) -> b -> HashMap s k a -> b

Left associative fold with a strict accumulator.

Conversion

toMap :: forall s k a. HashMap s k a -> HashMap k a

Convert to a regular HashMap, forgetting its set of keys.

keysSet :: forall s k a. HashMap s k a -> HashSet s k

Return the set of keys in the map, with the contents of the set still tracked by the s parameter. See Data.HashSet.Refined.

toList :: forall s k a. HashMap s k a -> [(Key s k, a)]

Convert to a list of key-value pairs.

Filter

restrictKeys :: forall s t k a. (Hashable k, KnownHashSet t k) => HashMap s k a -> SomeHashMapWith (IntersectionProof 'Hashed s t) k a

Restrict a map to only those keys that are elements of t.

withoutKeys :: forall s t k a. (Hashable k, KnownHashSet t k) => HashMap s k a -> SomeHashMapWith (DifferenceProof 'Hashed s t) k a

Remove all keys that are elements of t from the map.

filterWithKey :: forall s k a. (Key s k -> a -> Bool) -> HashMap s k a -> SomeHashMapWith (SupersetProof 'Hashed s) k a

Retain only the key-value pairs that satisfy the predicate, returning a potentially smaller map.

partitionWithKey :: forall s k a. Hashable k => (Key s k -> a -> Bool) -> HashMap s k a -> Some2HashMapWith (PartitionProof 'Hashed s k) k a a

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

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.

Constructors

PartitionProof

Fields

• (Refined (InSet f s) a -> Either (Refined (InSet f r) a) (Refined (InSet f q) a))

  Decide whether a given element of s belongs to r or to q

• ((InSet f r || InSet f q) :-> InSet f s)

  \(r \cup q \subseteq s\)

• (forall t. (InSet f r :-> InSet f t) -> (InSet f q :-> InSet f t) -> InSet f s :-> InSet f t)

  \(\forall t,(r\subseteq t)\land(q\subseteq t)\implies s\subseteq t\), which is equivalent to \(s \subseteq r \cup q\)

• (forall t. (InSet f t :-> InSet f r) -> (InSet f t :-> InSet f q) -> forall u. InSet f t :-> InSet f u)

  \(\forall t,(t\subseteq r)\land(t\subseteq q)\implies\forall u,t\subseteq u\), which is equivalent to \(r \cap q \subseteq \varnothing\)

mapMaybeWithKey :: forall s k a b. (Key s k -> a -> Maybe b) -> HashMap s k a -> SomeHashMapWith (SupersetProof 'Hashed s) k b

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 k a b c. Hashable k => (Key s k -> a -> Either b c) -> HashMap s k a -> Some2HashMapWith (PartitionProof 'Hashed s k) k b c

Apply a function to all values in a map, together with their corresponding keys, and collect the Left and Right results into separate (disjoint) maps.

Casts

castKey :: forall s t k. (forall x. Key s x -> Key t x) -> (forall x. Key t x -> Key s x) -> Coercion (Key s k) (Key t k)

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 Key s can be safely interconverted with 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 (Key s x) (Key t x)) -> Coercion (HashMap s k) (HashMap t k)

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 k a b c. Hashable k
  => (Key s k -> a -> b -> c) -> HashMap s k a -> HashMap s k b -> HashMap s k c
zipWithKey f m1 m2
  | SomeHashMapWith @r m proof <- intersectionWithKey (f . andLeft) m1 m2
  , IntersectionProof p1 p2 <- proof
  , ( Coercion :: Coercion (HashMap r k c) (HashMap s k c))
    <- app $ cast $ castKey (andLeft . p1) (p2 id id)
  = coerce m
  where
    app :: Coercion f g -> Coercion (f x) (g x)
    app Coercion = Coercion

castFlavor :: forall (f :: Flavor) (g :: Flavor) s a. Coercion (Refined (InSet f s) a) (Refined (InSet g s) a)

This function can be used to freely convert between Element and Key types of various flavors (Regular, Int, Hashed), corresponding to the different implementations of sets and maps.