Data.HashSet.Refined

This module implements a way of tracking the contents of a HashSet at the type level, and provides utilities for manipulating such sets.

The contents of a set are associated with a type parameter, e.g. s, so that whenever you see the same type parameter, you know you are working with the same set. 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.

Warning

This module together with Data.HashSet 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.

Set type

type KnownHashSet s a = Reifies s (HashSet a)

A constraint evidencing that we know the contents of the set s at runtime. Whenever you see this constraint on a function, there is an actual HashSet a being passed around at runtime.

Given this constraint, to obtain a regular HashSet a you can use reflect.

type HashSet s a = Dict (KnownHashSet s a)

A HashSet whose contents are tracked by the type parameter s. This is a "singleton": for a given s there's only one value of this type.

Since this is just a Dict, you can freely convert between the value (HashSet) and the constraint (KnownHashSet). This library prefers to use the constraint.

Refinement type

data InSet (f :: Flavor) (s :: Type)

A predicate for use with Refined, verifying that a value is an element of the set s.

Constructors

InSet

Instances

(Hashable a, Typeable s, KnownHashSet s a) => Predicate (InSet 'Hashed s :: Type) a

See revealPredicate.

Defined in Data.Container.Refined.Proofs

Methods

validate :: Proxy (InSet 'Hashed s) -> a -> Maybe RefineException

(a ~ Int, Typeable s, KnownIntSet s) => Predicate (InSet 'Int s :: Type) a

See revealPredicate.

Defined in Data.Container.Refined.Proofs

Methods

validate :: Proxy (InSet 'Int s) -> a -> Maybe RefineException

(Ord a, Typeable s, KnownSet s a) => Predicate (InSet 'Regular s :: Type) a

See revealPredicate.

Defined in Data.Container.Refined.Proofs

Methods

validate :: Proxy (InSet 'Regular s) -> a -> Maybe RefineException

FoldableWithIndex (Key s) (IntMap s)

Defined in Data.IntMap.Common.Refined

Methods

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

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)

Defined in Data.IntMap.Common.Refined

Methods

imap :: (Key s -> a -> b) -> IntMap s a -> IntMap s b

TraversableWithIndex (Key s) (IntMap s)

Defined in Data.IntMap.Common.Refined

Methods

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

KnownIntSet s => MonadReader (Key s) (IntMap s)

Similar to the instance for functions. See also backpermuteKeys.

Defined in Data.IntMap.Common.Refined

Methods

ask :: IntMap s (Key s)

local :: (Key s -> Key s) -> IntMap s a -> IntMap s a

reader :: (Key s -> a) -> IntMap s a

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

FoldableWithIndex (Key s k) (Map s k)

Defined in Data.Map.Common.Refined

Methods

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

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

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

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

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

ifoldl' :: (Key s k -> b -> a -> b) -> b -> Map 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

FunctorWithIndex (Key s k) (Map s k)

Defined in Data.Map.Common.Refined

Methods

imap :: (Key s k -> a -> b) -> Map s k a -> Map 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)

TraversableWithIndex (Key s k) (Map s k)

Defined in Data.Map.Common.Refined

Methods

itraverse :: Applicative f => (Key s k -> a -> f b) -> Map s k a -> f (Map 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

(Ord k, KnownSet s k) => MonadReader (Key s k) (Map s k)

Similar to the instance for functions. See also backpermuteKeys.

Defined in Data.Map.Common.Refined

Methods

ask :: Map s k (Key s k)

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

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

data Flavor

Disambiguate the choice of implementation for sets and maps.

Constructors

Hashed

HashSet and HashMap

type Element s = Refined (InSet 'Hashed s)

Element s a is a value of type a that has been verified to be an element of s.

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

The underlying a value can be obtained with unrefine. An a can be validated into an Element s a with member.

revealPredicate :: forall s a. (Typeable a, Hashable a, KnownHashSet s a) => Dict (Predicate (InSet 'Hashed s) a)

To use Refined machinery that uses the Predicate typeclass you will need to pattern match on this Dict.

The reason is that in the default fast implementation of reflection, we don't have Typeable s, which Refined wants for pretty-printing exceptions. We can provide Typeable s, but at the cost of using the slow implementation of reflection.

Existentials and common proofs

data SomeHashSet a where

An existential wrapper for an as-yet-unknown set. Pattern maching on it gives you a way to refer to the set, e.g.

case fromHashSet ... of
  SomeHashSet @s _ -> doSomethingWith @s

case fromHashSet ... of
  SomeHashSet (_ :: Proxy# s) -> doSomethingWith @s

Constructors

SomeHashSet :: forall s a. KnownHashSet s a => Proxy# s -> SomeHashSet a

withHashSet :: forall a r. SomeHashSet a -> (forall s. KnownHashSet s a => Proxy s -> r) -> r

Apply an unknown set to a continuation that can accept any set. This gives you a way to refer to the set (the parameter s), e.g.:

withHashSet (fromHashSet ...) $ (_ :: Proxy s) -> doSomethingWith @s

data SomeHashSetWith p a where

An existential wrapper for an as-yet-unknown set, 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). Most functions will return a set in this way, together with a proof that somehow relates the set to the function's inputs.

Constructors

SomeHashSetWith :: forall s a p. KnownHashSet s a => !(p s) -> SomeHashSetWith p a

withHashSetWith :: forall a r p. SomeHashSetWith p a -> (forall s. KnownHashSet s a => p s -> r) -> r

Apply an unknown set with proof to a continuation that can accept any set satisfying the proof. This gives you a way to refer to the set (the parameter s).

data Some2HashSetWith p a where

An existential wrapper for an as-yet-unknown pair of sets, together with a proof of some fact p relating them.

Constructors

Some2HashSetWith :: forall s t a p. (KnownHashSet s a, KnownHashSet t a) => !(p s t) -> Some2HashSetWith p a

with2HashSetWith :: forall a r p. Some2HashSetWith p a -> (forall s t. (KnownHashSet s a, KnownHashSet t a) => p s t -> r) -> r

Apply a pair of unknown sets with proof to a continuation that can accept any pair of sets satisfying the proof. This gives you a way to refer to the sets (the parameters s and t).

type (:->) p q = forall x. Refined p x -> Refined q x infix 1

A proof that values satisfying p can be cast into values satisfying q.

For example, InSet s :-> InSet r proves that \(s \subseteq r\).

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 a. SomeHashSetWith (EmptyProof 'Hashed) a

An empty set.

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

Create a set with a single element.

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

fromHashSet :: forall a. HashSet a -> SomeHashSet a

Construct a set from a regular HashSet.

fromTraversable :: forall t a. (Traversable t, Hashable a) => t a -> SomeHashSetWith (FromTraversableProof 'Hashed t a) a

Create a set from the elements of an arbitrary traversable.

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 a. (Hashable a, KnownHashSet s a) => a -> SomeHashSetWith (InsertProof 'Hashed a s) a

Insert an element in a set.

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

Deletion

delete :: forall s a. (Hashable a, KnownHashSet s a) => a -> SomeHashSetWith (SupersetProof 'Hashed s) a

Delete an element from a set.

Query

member :: forall s a. (Hashable a, KnownHashSet s a) => a -> Maybe (Element s a)

If an element is in the set, return the proof that it is.

null :: forall s a. KnownHashSet s a => Maybe (EmptyProof 'Hashed s)

If the set is empty, return the proof that it is.

isSubsetOf :: forall s t a. (Hashable a, KnownHashSet s a, KnownHashSet t a) => Maybe (SubsetProof 'Hashed s t)

If s is a subset of t (or is equal to), return a proof of that.

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 a. (Hashable a, KnownHashSet s a, KnownHashSet t a) => Maybe (DisjointProof 'Hashed s t)

If s and t 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

union :: forall s t a. (Hashable a, KnownHashSet s a, KnownHashSet t a) => SomeHashSetWith (UnionProof 'Hashed s t) a

The union of two sets.

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 a. (Hashable a, KnownHashSet s a, KnownHashSet t a) => SomeHashSetWith (DifferenceProof 'Hashed s t) a

HashSet with elements of s that are not in t.

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

intersection :: forall s t a. (Hashable a, KnownHashSet s a, KnownHashSet t a) => SomeHashSetWith (IntersectionProof 'Hashed s t) a

Intersection of two sets.

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

Filter

filter :: forall s a. KnownHashSet s a => (Element s a -> Bool) -> SomeHashSetWith (SupersetProof 'Hashed s) a

Return a subset of elements that satisfy the given predicate.

partition :: forall s a. KnownHashSet s a => (Element s a -> Bool) -> Some2HashSetWith (PartitionProof 'Hashed s a) a

Partition a set into two disjoint subsets: those that satisfy the predicate, and those that 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\)

Map

map :: forall s a b. (Hashable b, KnownHashSet s a) => (Element s a -> b) -> SomeHashSetWith (MapProof 'Hashed s a b) b

Apply the given function to each element of the set and collect the results. Note that the resulting set can be smaller.

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

Folds

foldMap :: forall s a m. (KnownHashSet s a, Monoid m) => (Element s a -> m) -> m

Map each element of s into a monoid (with proof that it was an element), and combine the results using <>.

foldr :: forall s a b. KnownHashSet s a => (Element s a -> b -> b) -> b -> b

Right associative fold with a lazy accumulator.

foldl :: forall s a b. KnownHashSet s a => (b -> Element s a -> b) -> b -> b

Left associative fold with a lazy accumulator.

foldr' :: forall s a b. KnownHashSet s a => (Element s a -> b -> b) -> b -> b

Right associative fold with a strict accumulator.

foldl' :: forall s a b. KnownHashSet s a => (b -> Element s a -> b) -> b -> b

Left associative fold with a strict accumulator.

Conversion

toList :: forall s a. KnownHashSet s a => [Element s a]

List of elements in the set.

asSet :: forall s a. (Ord a, KnownHashSet s a) => Set s a

Convert an IntSet into a Set, retaining its set of elements, which can be converted with castFlavor.

asIntSet :: forall s. KnownHashSet s Int => IntSet s

Convert an IntSet into a HashSet, retaining its set of elements, which can be converted with castFlavor.

Casts

castElement :: forall s t a. (forall x. Element s x -> Element t x) -> (forall x. Element t x -> Element s x) -> Coercion (Element s a) (Element t a)

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 Element s can be safely interconverted with Element t.

The requirement that the weakenings are natural transformations ensures that they don't actually alter the elements. 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 a. (forall x. Coercion (Element s x) (Element t x)) -> Coercion (HashSet s a) (HashSet t a)

If elements can be interconverted (e.g. as proved by castElement), then the sets can be interconverted too. For example we can establish that the intersection of a set with itself is interconvertible with that set:

castIntersection
  :: IntersectionProof 'Hashed s s r
  -> Coercion (HashSet r a) (HashSet s a)
castIntersection ( IntersectionProof p1 p2)
  = cast $ castElement (andLeft . p1) (p2 id id)

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.