Copyright	(c) Justin Le 2018
License	BSD3
Maintainer	justin@jle.im
Stability	experimental
Portability	non-portable
Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.Type.Universe.Subset

Contents

Subset

Description

Represent a decidable subset of a type-level 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 Subset f p is a predicate that some decidable subset of an input as is true.

Instances

Instances details

(Universe f, Decidable p) => Decidable (Subset f p :: TyFun (f k) Type -> Type) Source #
Instance details Defined in Data.Type.Universe.Subset Methods decide :: Decide (Subset f p) Source #
(Universe f, Decidable p) => Provable (Subset f p :: TyFun (f k) Type -> Type) Source #
Instance details Defined in Data.Type.Universe.Subset Methods prove :: Prove (Subset f p) Source #
type Apply (Subset f p :: TyFun (f k) Type -> Type) (as :: f k) Source #
Instance details Defined 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
Fields 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 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