Data.IntSet.Refined

This module implements a way of tracking the contents of an IntSet 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.

Set type

type KnownIntSet s = Reifies s IntSet

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 IntSet being passed around at runtime.

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

type IntSet s = Dict (KnownIntSet s)

A IntSet 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 (IntSet) and the constraint (KnownIntSet). 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

Int

IntSet and IntMap

type Element s = Refined (InSet 'Int s) Int

Element s is an Int that has been verified to be an element of s.

Thus, Element s is a "refinement" type of Int, 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 Int can be obtained with unrefine. An Int can be validated into an Element s with member.

revealPredicate :: forall s. KnownIntSet s => Dict (Predicate (InSet 'Int s) Int)

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 TypeableTypeable s, but at the cost of using the slow implementation of reflection.

Existentials and common proofs

data SomeIntSet 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 fromIntSet ... of
  SomeIntSet @s _ -> doSomethingWith @s

case fromIntSet ... of
  SomeIntSet (_ :: Proxy# s) -> doSomethingWith @s

Constructors

SomeIntSet :: forall s. KnownIntSet s => Proxy# s -> SomeIntSet

withIntSet :: forall r. SomeIntSet -> (forall s. KnownIntSet s => 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.:

withIntSet (fromIntSet ...) $ (_ :: Proxy s) -> doSomethingWith @s

data SomeIntSetWith p 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

SomeIntSetWith :: forall s p. KnownIntSet s => !(p s) -> SomeIntSetWith p

withIntSetWith :: forall r p. SomeIntSetWith p -> (forall s. KnownIntSet s => 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 Some2IntSetWith p where

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

Constructors

Some2IntSetWith :: forall s t p. (KnownIntSet s, KnownIntSet t) => !(p s t) -> Some2IntSetWith p

with2IntSetWith :: forall r p. Some2IntSetWith p -> (forall s t. (KnownIntSet s, KnownIntSet t) => 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 :: SomeIntSetWith (EmptyProof 'Int)

An empty set.

singleton :: Int -> SomeIntSetWith (SingletonProof 'Int Int)

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

fromIntSet :: IntSet -> SomeIntSet

Construct a set from a regular IntSet.

fromTraversable :: forall t. Traversable t => t Int -> SomeIntSetWith (FromTraversableProof 'Int t Int)

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. KnownIntSet s => Int -> SomeIntSetWith (InsertProof 'Int Int s)

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. KnownIntSet s => Int -> SomeIntSetWith (SupersetProof 'Int s)

Delete an element from a set.

Query

member :: forall s. KnownIntSet s => Int -> Maybe (Element s)

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

lookupLT :: forall s. KnownIntSet s => Int -> Maybe (Element s)

Find the largest element smaller than the given one.

lookupGT :: forall s. KnownIntSet s => Int -> Maybe (Element s)

Find the smallest element greater than the given one.

lookupLE :: forall s. KnownIntSet s => Int -> Maybe (Element s)

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

lookupGE :: forall s. KnownIntSet s => Int -> Maybe (Element s)

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

null :: forall s. KnownIntSet s => Maybe (EmptyProof 'Int s)

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

isSubsetOf :: forall s t. (KnownIntSet s, KnownIntSet t) => Maybe (SubsetProof 'Int 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. (KnownIntSet s, KnownIntSet t) => Maybe (DisjointProof 'Int 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. (KnownIntSet s, KnownIntSet t) => SomeIntSetWith (UnionProof 'Int s t)

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. (KnownIntSet s, KnownIntSet t) => SomeIntSetWith (DifferenceProof 'Int s t)

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. (KnownIntSet s, KnownIntSet t) => SomeIntSetWith (IntersectionProof 'Int s t)

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. KnownIntSet s => (Element s -> Bool) -> SomeIntSetWith (SupersetProof 'Int s)

Return a subset of elements that satisfy the given predicate.

partition :: forall s. KnownIntSet s => (Element s -> Bool) -> Some2IntSetWith (PartitionProof 'Int s Int)

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. KnownIntSet s => (Element s -> Bool) -> Some2IntSetWith (PartialPartitionProof 'Int s)

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. KnownIntSet s => Int -> Some2IntSetWith (SplitProof 'Int s (Element s))

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. KnownIntSet s => (Element s -> Int) -> SomeIntSetWith (MapProof 'Int s Int Int)

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 m. (KnownIntSet s, Monoid m) => (Element s -> 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. KnownIntSet s => (Element s -> a -> a) -> a -> a

Right associative fold with a lazy accumulator.

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

Left associative fold with a lazy accumulator.

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

Right associative fold with a strict accumulator.

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

Left associative fold with a strict accumulator.

Min/Max

minView :: forall s. KnownIntSet s => Either (EmptyProof 'Int s) (Element s, SomeIntSetWith (SupersetProof 'Int s))

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. KnownIntSet s => Either (EmptyProof 'Int s) (Element s, SomeIntSetWith (SupersetProof 'Int s))

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. KnownIntSet s => [Element s]

List of elements in the set in ascending order.

toDescList :: forall s. KnownIntSet s => [Element s]

List of elements in the set in descending order.

asSet :: forall s. KnownIntSet s => Set s Int

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

asHashSet :: forall s. KnownIntSet s => HashSet s Int

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. 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) a) (Refined (InSet 'Int 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. (forall x. Coercion (Refined (InSet 'Int s) x) (Refined (InSet 'Int t) x)) -> Coercion (IntSet s) (IntSet t)

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 'Int s s r
  -> Coercion (IntSet r) (IntSet s)
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.