Copyright  (c) Justin Le 2018 

License  BSD3 
Maintainer  justin@jle.im 
Stability  experimental 
Portability  nonportable 
Safe Haskell  None 
Language  Haskell2010 
Represent a decidable subset of a typelevel collection.
Synopsis
 data Subset f :: (k ~> Type) > f k ~> Type
 newtype WitSubset f p (as :: f k) = WitSubset {
 runWitSubset :: forall a. Elem f as a > Decision (p @@ a)
 makeSubset :: forall f k p (as :: f k). Universe f => (forall a. Elem f as a > Sing a > Decision (p @@ a)) > Sing as > Subset f p @@ as
 intersection :: forall f p q. (Subset f p &&& Subset f q) > Subset f (p &&& q)
 union :: forall f p q. (Subset f p &&& Subset f q) > Subset f (p  q)
 symDiff :: forall f p q. (Subset f p &&& Subset f q) > Subset f (p ^^^ q)
 mergeSubset :: forall f k p q r (as :: f k). (forall a. Decision (p @@ a) > Decision (q @@ a) > Decision (r @@ a)) > (Subset f p @@ as) > (Subset f q @@ as) > Subset f r @@ as
 imergeSubset :: forall f k p q r (as :: f k). (forall a. Elem f as a > Decision (p @@ a) > Decision (q @@ a) > Decision (r @@ a)) > (Subset f p @@ as) > (Subset f q @@ as) > Subset f r @@ as
 mapSubset :: Universe f => (p > q) > (q > p) > Subset f p > Subset f q
 imapSubset :: (forall a. Elem f as a > (p @@ a) > q @@ a) > (forall a. Elem f as a > (q @@ a) > p @@ a) > (Subset f p @@ as) > Subset f q @@ as
 subsetToList :: forall f p t. (Universe f, Alternative t) => (Subset f p ># Any f p) t
 subsetToAny :: forall f p. Universe f => Subset f p ?> Any f p
 subsetToAll :: forall f p. Universe f => Subset f p ?> All f p
 subsetToNone :: forall f p. Universe f => Subset f p ?> None f p
 emptySubset :: forall f as. (Universe f, SingI as) => Subset f Impossible @@ as
 fullSubset :: forall f as. (Universe f, SingI as) => Subset f Evident @@ as
Subset
data Subset f :: (k ~> Type) > f k ~> Type Source #
A
is a predicate that some decidable subset of an input
Subset
f pas
is true.
newtype WitSubset f p (as :: f k) Source #
A WitSubset
f p as
describes a decidable subset of typelevel
collection as
.
WitSubset  

makeSubset :: forall f k p (as :: f k). Universe f => (forall a. Elem f as a > Sing a > Decision (p @@ a)) > Sing as > Subset f p @@ as Source #
Create a Subset
from a predicate.
Subset manipulation
intersection :: forall f p q. (Subset f p &&& Subset f q) > Subset f (p &&& q) Source #
Subset intersection
union :: forall f p q. (Subset f p &&& Subset f q) > Subset f (p  q) Source #
Subset union (leftbiased)
symDiff :: forall f p q. (Subset f p &&& Subset f q) > Subset f (p ^^^ q) Source #
Symmetric subset difference
mergeSubset :: forall f k p q r (as :: f k). (forall a. Decision (p @@ a) > Decision (q @@ a) > Decision (r @@ a)) > (Subset f p @@ as) > (Subset f q @@ as) > Subset f r @@ as Source #
Combine two subsets based on a decision function
imergeSubset :: forall f k p q r (as :: f k). (forall a. Elem f as a > Decision (p @@ a) > Decision (q @@ a) > Decision (r @@ a)) > (Subset f p @@ as) > (Subset f q @@ as) > Subset f r @@ as Source #
Combine two subsets based on a decision function
mapSubset :: Universe f => (p > q) > (q > p) > Subset f p > Subset f q Source #
Map a bidirectional implication over a subset described by that implication.
Implication needs to be bidirectional, or otherwise we can't produce a decidable subset as a result.
imapSubset :: (forall a. Elem f as a > (p @@ a) > q @@ a) > (forall a. Elem f as a > (q @@ a) > p @@ a) > (Subset f p @@ as) > Subset f q @@ as Source #
Subset extraction
subsetToList :: forall f p t. (Universe f, Alternative t) => (Subset f p ># Any f p) t Source #
Turn a Subset
into a list (or any Alternative
) of satisfied
predicates.
List is meant to include no duplicates.
Subset tests
subsetToAny :: forall f p. Universe f => Subset f p ?> Any f p Source #
Restrict a Subset
to a single (arbitrary) member, or fail if none
exists.
subsetToAll :: forall f p. Universe f => Subset f p ?> All f p Source #
Test if a subset is equal to the entire original collection
subsetToNone :: forall f p. Universe f => Subset f p ?> None f p Source #
Test if a subset is empty.
Subset construction
emptySubset :: forall f as. (Universe f, SingI as) => Subset f Impossible @@ as Source #
Construct an empty subset.