decidable-0.1.4.0: Combinators for manipulating dependently-typed predicates.

Data.Type.Universe.Subset

Description

Represent a decidable subset of a type-level collection.

Synopsis

# Subset

data Subset f :: (k ~> Type) -> f k ~> Type Source #

A Subset f p is a predicate that some decidable subset of an input as is true.

Instances
 (Universe f, Decidable p) => Provable (Subset f p :: TyFun (f k) Type -> Type) Source # Instance detailsDefined in Data.Type.Universe.Subset Methodsprove :: Prove (Subset f p) Source # (Universe f, Decidable p) => Decidable (Subset f p :: TyFun (f k) Type -> Type) Source # Instance detailsDefined in Data.Type.Universe.Subset Methodsdecide :: Decide (Subset f p) Source # type Apply (Subset f p :: TyFun (f k) Type -> Type) (as :: f k) Source # Instance detailsDefined in Data.Type.Universe.Subset type Apply (Subset f p :: TyFun (f k) Type -> Type) (as :: f k) = WitSubset f p as

newtype WitSubset f p (as :: f k) Source #

A WitSubset f p  as describes a decidable subset of type-level collection as.

Constructors

 WitSubset FieldsrunWitSubset :: 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 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 (left-biased)

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 #

mapSubset, but providing an Elem.

## 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.

fullSubset :: forall f as. (Universe f, SingI as) => Subset f Evident @@ as Source #

Construct a full subset