Data.Set.Refined

This module implements a way of tracking the contents of a Set 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.Set rely on Eq and Ord instances being lawful: that == is an equivalence relation, and that the Ord operations define a total order on the quotient defined 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.

Set type

type KnownSet s a = Reifies s (Set 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 Set a being passed around at runtime.

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

type Set s a = Dict (KnownSet s a)

A Set 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 (Set) and the constraint (KnownSet). 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

Regular

Set and Map

type Element s = Refined (InSet 'Regular 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, Ord a, KnownSet s a) => Dict (Predicate (InSet 'Regular 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 SomeSet 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 fromSet ... of
  SomeSet @s _ -> doSomethingWith @s

case fromSet ... of
  SomeSet (_ :: Proxy# s) -> doSomethingWith @s

Constructors

SomeSet :: forall s a. KnownSet s a => Proxy# s -> SomeSet a

withSet :: forall a r. SomeSet a -> (forall s. KnownSet 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.:

withSet (fromSet ...) $ (_ :: Proxy s) -> doSomethingWith @s

data SomeSetWith 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

SomeSetWith :: forall s a p. KnownSet s a => !(p s) -> SomeSetWith p a

withSetWith :: forall a r p. SomeSetWith p a -> (forall s. KnownSet 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 Some2SetWith 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

Some2SetWith :: forall s t a p. (KnownSet s a, KnownSet t a) => !(p s t) -> Some2SetWith p a

with2SetWith :: forall a r p. Some2SetWith p a -> (forall s t. (KnownSet s a, KnownSet 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. SomeSetWith (EmptyProof 'Regular) a

An empty set.

singleton :: forall a. a -> SomeSetWith (SingletonProof 'Regular 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

fromSet :: forall a. Set a -> SomeSet a

Construct a set from a regular Set.

fromTraversable :: forall t a. (Traversable t, Ord a) => t a -> SomeSetWith (FromTraversableProof 'Regular 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. (Ord a, KnownSet s a) => a -> SomeSetWith (InsertProof 'Regular 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. (Ord a, KnownSet s a) => a -> SomeSetWith (SupersetProof 'Regular s) a

Delete an element from a set.

Query

member :: forall s a. (Ord a, KnownSet s a) => a -> Maybe (Element s a)

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

lookupLT :: forall s a. (Ord a, KnownSet s a) => a -> Maybe (Element s a)

Find the largest element smaller than the given one.

lookupGT :: forall s a. (Ord a, KnownSet s a) => a -> Maybe (Element s a)

Find the smallest element greater than the given one.

lookupLE :: forall s a. (Ord a, KnownSet s a) => a -> Maybe (Element s a)

Find the largest element smaller or equal to the given one.

lookupGE :: forall s a. (Ord a, KnownSet s a) => a -> Maybe (Element s a)

Find the smallest element greater or equal to the given one.

null :: forall s a. KnownSet s a => Maybe (EmptyProof 'Regular s)

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

isSubsetOf :: forall s t a. (Ord a, KnownSet s a, KnownSet t a) => Maybe (SubsetProof 'Regular 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. (Ord a, KnownSet s a, KnownSet t a) => Maybe (DisjointProof 'Regular 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. (Ord a, KnownSet s a, KnownSet t a) => SomeSetWith (UnionProof 'Regular 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. (Ord a, KnownSet s a, KnownSet t a) => SomeSetWith (DifferenceProof 'Regular s t) a

Set 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. (Ord a, KnownSet s a, KnownSet t a) => SomeSetWith (IntersectionProof 'Regular 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\)

cartesianProduct :: forall s t a b. (KnownSet s a, KnownSet t b) => SomeSetWith (ProductProof 'Regular s t) (a, b)

Cartesian product of two sets. The elements are all pairs (x, y) for each x from s and for each y from t.

newtype ProductProof f s t r

Proof that the cartesian product of s and t is r.

Constructors

ProductProof (forall a b. Coercion (Refined (InSet f s) a, Refined (InSet f t) b) (Refined (InSet f r) (a, b)))

A pair of elements from s and t respectively can be converted into an element of r and back. You can use coerceWith co and coerceWith (sym co).

disjointUnion :: forall s t a b. (KnownSet s a, KnownSet t b) => SomeSetWith (CoproductProof 'Regular s t) (Either a b)

Disjoint union of two sets. Includes Left x for each x from s, and Right y for each y from t.

newtype CoproductProof f s t r

Proof that the tagged disjoint union of s and t is r.

Constructors

CoproductProof (forall a b. Coercion (Either (Refined (InSet f s) a) (Refined (InSet f t) b)) (Refined (InSet f r) (Either a b)))

Coproduct of elements of s and t can be converted into an element of r and back. You can use coerceWith co and coerceWith (sym co).

Filter

filter :: forall s a. KnownSet s a => (Element s a -> Bool) -> SomeSetWith (SupersetProof 'Regular s) a

Return a subset of elements that satisfy the given predicate.

partition :: forall s a. KnownSet s a => (Element s a -> Bool) -> Some2SetWith (PartitionProof 'Regular 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\)

spanAntitone :: forall s a. KnownSet s a => (Element s a -> Bool) -> Some2SetWith (PartialPartitionProof 'Regular s) a

Divide a set into two disjoint subsets at a point where the predicate 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

Proof that s is the union of disjoint subsets r and q, but without a deciding procedure.

Constructors

PartialPartitionProof

Fields

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

splitMember :: forall s a. (Ord a, KnownSet s a) => a -> Some2SetWith (SplitProof 'Regular s (Element s a)) a

Return two disjoint subsets: those less than the given element, and those greater than the given element; along with the proof that the given element was in the set, if it was.

data SplitProof f s e r q

Proof that s contains disjoint subsets r and q, along with an optional element between them.

Constructors

SplitProof

Fields

• !(Maybe e)

  The element between r and q

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

  \(r \cup q \subseteq s\)

• (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. (Ord b, KnownSet s a) => (Element s a -> b) -> SomeSetWith (MapProof 'Regular 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. (KnownSet 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. KnownSet s a => (Element s a -> b -> b) -> b -> b

Right associative fold with a lazy accumulator.

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

Left associative fold with a lazy accumulator.

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

Right associative fold with a strict accumulator.

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

Left associative fold with a strict accumulator.

Min/Max

minView :: forall s a. KnownSet s a => Either (EmptyProof 'Regular s) (Element s a, SomeSetWith (SupersetProof 'Regular s) a)

Retrieves the smallest element of the set, and the set with that element removed; or a proof that the set was empty.

maxView :: forall s a. KnownSet s a => Either (EmptyProof 'Regular s) (Element s a, SomeSetWith (SupersetProof 'Regular s) a)

Retrieves the greatest element of the set, and the set with that element removed; or a proof that the set was empty.

Conversion

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

List of elements in the set in ascending order.

toDescList :: forall s a. KnownSet s a => [Element s a]

List of elements in the set in descending order.

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

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

asHashSet :: forall s a. (Hashable a, KnownSet s a) => HashSet s a

Convert a Set 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 (Set s a) (Set 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 'Regular s s r
  -> Coercion (Set r a) (Set 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.