Copyright	(c) Justin Le 2018
License	BSD3
Maintainer	[email protected]
Stability	experimental
Portability	non-portable
Safe Haskell	None
Language	Haskell2010

Data.Type.Universe.Subset

Contents

Subset

Description

Represent a decidable subset of a type-level collection.

Synopsis

data Subset (f :: Type -> Type) (a :: k ~> Type) (b :: TyFun (f k) Type)
newtype WitSubset (f :: Type -> Type) (p :: k ~> Type) (as :: f k) = WitSubset {
- runWitSubset :: forall (a :: k). Elem f as a -> Decision (p @@ a)
}
makeSubset :: forall (f :: Type -> Type) k (p :: k ~> Type) (as :: f k). Universe f => (forall (a :: k). Elem f as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Subset f p @@ as
intersection :: forall {k} (f :: Type -> Type) (p :: k ~> Type) (q :: k ~> Type) (a :: f k). Sing a -> ((Subset f p &&& Subset f q) @@ a) -> Subset f (p &&& q) @@ a
union :: forall {k} (f :: Type -> Type) (p :: k ~> Type) (q :: k ~> Type) (a :: f k). Sing a -> ((Subset f p &&& Subset f q) @@ a) -> Subset f (p ||| q) @@ a
symDiff :: forall {k} (f :: Type -> Type) (p :: k ~> Type) (q :: k ~> Type) (a :: f k). Sing a -> ((Subset f p &&& Subset f q) @@ a) -> Subset f (p ^^^ q) @@ a
mergeSubset :: forall (f :: Type -> Type) k (p :: k ~> Type) (q :: k ~> Type) (r :: k ~> Type) (as :: f k). (forall (a :: k). Decision (p @@ a) -> Decision (q @@ a) -> Decision (r @@ a)) -> (Subset f p @@ as) -> (Subset f q @@ as) -> Subset f r @@ as
imergeSubset :: forall (f :: Type -> Type) k (p :: k ~> Type) (q :: k ~> Type) (r :: k ~> Type) (as :: f k). (forall (a :: k). 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 :: forall {k} (f :: Type -> Type) (p :: k ~> Type) (q :: k ~> Type). Universe f => (p --> q) -> (q --> p) -> Subset f p --> Subset f q
imapSubset :: forall {k} (f :: Type -> Type) (as :: f k) (p :: k ~> Type) (q :: k ~> Type). (forall (a :: k). Elem f as a -> (p @@ a) -> q @@ a) -> (forall (a :: k). Elem f as a -> (q @@ a) -> p @@ a) -> (Subset f p @@ as) -> Subset f q @@ as
subsetToList :: forall {k} (f :: Type -> Type) (p :: k ~> Type) (t :: Type -> Type). (Universe f, Alternative t) => (Subset f p --># Any f p) t
subsetToAny :: forall {k} (f :: Type -> Type) (p :: k ~> Type). Universe f => Subset f p -?> Any f p
subsetToAll :: forall {k} (f :: Type -> Type) (p :: k ~> Type). Universe f => Subset f p -?> All f p
subsetToNone :: forall {k} (f :: Type -> Type) (p :: k ~> Type). Universe f => Subset f p -?> None f p
emptySubset :: forall {k} (f :: Type -> Type) (as :: f k). (Universe f, SingI as) => Subset f (Impossible :: Predicate k) @@ as
fullSubset :: forall {k} (f :: Type -> Type) (as :: f k). (Universe f, SingI as) => Subset f (Evident :: TyFun k Type -> Type) @@ as

Subset

data Subset (f :: Type -> Type) (a :: k ~> Type) (b :: TyFun (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 :: Type -> Type) (p :: k ~> Type) (as :: f k) Source #

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

Constructors

WitSubset
Fields runWitSubset :: forall (a :: k). Elem f as a -> Decision (p @@ a)

makeSubset :: forall (f :: Type -> Type) k (p :: k ~> Type) (as :: f k). Universe f => (forall (a :: k). 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 {k} (f :: Type -> Type) (p :: k ~> Type) (q :: k ~> Type) (a :: f k). Sing a -> ((Subset f p &&& Subset f q) @@ a) -> Subset f (p &&& q) @@ a Source #

Subset intersection

union :: forall {k} (f :: Type -> Type) (p :: k ~> Type) (q :: k ~> Type) (a :: f k). Sing a -> ((Subset f p &&& Subset f q) @@ a) -> Subset f (p ||| q) @@ a Source #

Subset union (left-biased)

symDiff :: forall {k} (f :: Type -> Type) (p :: k ~> Type) (q :: k ~> Type) (a :: f k). Sing a -> ((Subset f p &&& Subset f q) @@ a) -> Subset f (p ^^^ q) @@ a Source #

Symmetric subset difference

mergeSubset :: forall (f :: Type -> Type) k (p :: k ~> Type) (q :: k ~> Type) (r :: k ~> Type) (as :: f k). (forall (a :: k). 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 :: Type -> Type) k (p :: k ~> Type) (q :: k ~> Type) (r :: k ~> Type) (as :: f k). (forall (a :: k). 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 :: forall {k} (f :: Type -> Type) (p :: k ~> Type) (q :: k ~> Type). 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 {k} (f :: Type -> Type) (as :: f k) (p :: k ~> Type) (q :: k ~> Type). (forall (a :: k). Elem f as a -> (p @@ a) -> q @@ a) -> (forall (a :: k). 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 {k} (f :: Type -> Type) (p :: k ~> Type) (t :: Type -> Type). (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 {k} (f :: Type -> Type) (p :: k ~> Type). Universe f => Subset f p -?> Any f p Source #

Restrict a Subset to a single (arbitrary) member, or fail if none exists.

subsetToAll :: forall {k} (f :: Type -> Type) (p :: k ~> Type). Universe f => Subset f p -?> All f p Source #

Test if a subset is equal to the entire original collection

subsetToNone :: forall {k} (f :: Type -> Type) (p :: k ~> Type). Universe f => Subset f p -?> None f p Source #

Test if a subset is empty.

Subset construction

emptySubset :: forall {k} (f :: Type -> Type) (as :: f k). (Universe f, SingI as) => Subset f (Impossible :: Predicate k) @@ as Source #

Construct an empty subset.

fullSubset :: forall {k} (f :: Type -> Type) (as :: f k). (Universe f, SingI as) => Subset f (Evident :: TyFun k Type -> Type) @@ as Source #

Construct a full subset