HashSet package:refined-containers
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.
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.
An existential wrapper for an as-yet-unknown pair of sets, together
with a proof of some fact p relating them.
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
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.
Construct a set from a regular
HashSet.
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).
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
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).
Convert a
Set into a
HashSet, retaining its set of
elements, which can be converted with
castFlavor.