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

Data.Type.Predicate.Quantification

Description

Higher-level predicates for quantifying predicates over universes and sets.

Synopsis

# Any

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

An Any f p is a predicate testing a collection as :: f a for the fact that at least one item in as satisfies p. Represents the "exists" quantifier over a given universe.

This is mostly useful for its Decidable and TFunctor instances, which lets you lift predicates on p to predicates on Any f p.

Instances
 Universe f => TFunctor (Any f :: (k1 ~> Type) -> TyFun (f k1) Type -> *) Source # Instance detailsDefined in Data.Type.Universe Methodstmap :: (p --> q) -> Any f p --> Any f q Source # Provable p => Provable ((NotNull f :: Predicate (f k)) ==> Any f p :: TyFun (f k) Type -> *) Source # Instance detailsDefined in Data.Type.Universe Methodsprove :: Prove (NotNull f ==> Any f p) Source # Provable (Found (InP f :: ParamPred (f v) v) ==> (NotNull f :: Predicate (f v)) :: TyFun (f v) Type -> *) Source # Instance detailsDefined in Data.Type.Predicate.Param Methods Provable ((NotNull f :: Predicate (f k)) ==> Found (InP f :: ParamPred (f k) k) :: TyFun (f k) Type -> *) Source # Instance detailsDefined in Data.Type.Predicate.Param Methods (Universe f, Provable p) => Decidable ((NotNull f :: Predicate (f k)) ==> Any f p :: TyFun (f k) Type -> *) Source # Instance detailsDefined in Data.Type.Universe Methodsdecide :: Decide (NotNull f ==> Any f p) Source # (Universe f, Decidable p) => Decidable (Any f p :: TyFun (f k) Type -> *) Source # Instance detailsDefined in Data.Type.Universe Methodsdecide :: Decide (Any f p) Source # Decidable (Found (InP f :: ParamPred (f v) v) ==> (NotNull f :: Predicate (f v)) :: TyFun (f v) Type -> *) Source # Instance detailsDefined in Data.Type.Predicate.Param Methods Decidable ((NotNull f :: Predicate (f k)) ==> Found (InP f :: ParamPred (f k) k) :: TyFun (f k) Type -> *) Source # Instance detailsDefined in Data.Type.Predicate.Param Methods type Apply (Any f p :: TyFun (f k) Type -> *) (as :: f k) Source # Instance detailsDefined in Data.Type.Universe type Apply (Any f p :: TyFun (f k) Type -> *) (as :: f k) = WitAny f p as

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

A WitAny p as is a witness that, for at least one item a in the type-level collection as, the predicate p a is true.

Constructors

 WitAny :: Elem f as a -> (p @@ a) -> WitAny f p as

type None f p = (Not (Any f p) :: Predicate (f k)) Source #

A None f p is a predicate on a collection as that no a in as satisfies predicate p.

## Decision

Arguments

 :: forall (p :: k ~> Type). Universe f => Decide p predicate on value -> Decide (Any f p) predicate on collection

Lifts a predicate p on an individual a into a predicate that on a collection as that is true if and only if any item in as satisfies the original predicate.

That is, it turns a predicate of kind k ~> Type into a predicate of kind f k ~> Type.

Essentially tests existential quantification.

Arguments

 :: forall (p :: k ~> Type) (as :: f k). Universe f => (forall a. Elem f as a -> Sing a -> Decision (p @@ a)) predicate on value -> Sing as -> Decision (Any f p @@ as) predicate on collection

decideAny, but providing an Elem.

Arguments

 :: forall (p :: k ~> Type). Universe f => Decide p predicate on value -> Decide (None f p) predicate on collection

Lifts a predicate p on an individual a into a predicate that on a collection as that is true if and only if no item in as satisfies the original predicate.

That is, it turns a predicate of kind k ~> Type into a predicate of kind f k ~> Type.

Arguments

 :: forall (p :: k ~> Type) (as :: f k). Universe f => (forall a. Elem f as a -> Sing a -> Decision (p @@ a)) predicate on value -> Sing as -> Decision (None f p @@ as) predicate on collection

decideNone, but providing an Elem.

## Entailment

entailAny :: forall f p q. Universe f => (p --> q) -> Any f p --> Any f q Source #

If there exists an a s.t. p a, and if p implies q, then there must exist an a s.t. q a.

Arguments

 :: (Universe f, SingI as) => (forall a. Elem f as a -> Sing a -> (p @@ a) -> q @@ a) implication -> (Any f p @@ as) -> Any f q @@ as

entailAny, but providing an Elem.

Arguments

 :: (Universe f, Functor h) => (p --># q) h implication in context -> (Any f p --># Any f q) h

If p implies q under some context h, and if there exists some a such that p a, then there must exist some a such that p q under that context h.

h might be something like, say, Maybe, to give predicate that is either provably true or unprovably false.

Note that it is not possible to do this with p a -> Decision (q a). This is if the p a -> Decision (q a) implication is false, there it doesn't mean that there is no a such that q a, necessarily. There could have been an a where p does not hold, but q does.

Arguments

 :: Functor h => (forall a. Elem f as a -> (p @@ a) -> h (q @@ a)) implication in context -> (Any f p @@ as) -> h (Any f q @@ as)

entailAnyF, but providing an Elem.

# All

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

An All f p is a predicate testing a collection as :: f a for the fact that all items in as satisfy p. Represents the "forall" quantifier over a given universe.

This is mostly useful for its Decidable, Provable, and TFunctor instances, which lets you lift predicates on p to predicates on All f p.

Instances
 Universe f => TFunctor (All f :: (k1 ~> Type) -> TyFun (f k1) Type -> *) Source # Instance detailsDefined in Data.Type.Universe Methodstmap :: (p --> q) -> All f p --> All f q Source # Universe f => DFunctor (All f :: (k1 ~> Type) -> TyFun (f k1) Type -> *) Source # Instance detailsDefined in Data.Type.Universe Methodsdmap :: (p -?> q) -> All f p -?> All f q Source # (Universe f, Provable p) => Provable (All f p :: TyFun (f k) Type -> *) Source # Instance detailsDefined in Data.Type.Universe Methodsprove :: Prove (All f p) Source # (Universe f, Decidable p) => Decidable (All f p :: TyFun (f k) Type -> *) Source # Instance detailsDefined in Data.Type.Universe Methodsdecide :: Decide (All f p) Source # type Apply (All f p :: TyFun (f k) Type -> *) (as :: f k) Source # Instance detailsDefined in Data.Type.Universe type Apply (All f p :: TyFun (f k) Type -> *) (as :: f k) = WitAll f p as

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

A WitAll p as is a witness that the predicate p a is true for all items a in the type-level collection as.

Constructors

 WitAll FieldsrunWitAll :: forall a. Elem f as a -> p @@ a

## Decision

Arguments

 :: forall (p :: k ~> Type). Universe f => Decide p predicate on value -> Decide (All f p) predicate on collection

Lifts a predicate p on an individual a into a predicate that on a collection as that is true if and only if all items in as satisfies the original predicate.

That is, it turns a predicate of kind k ~> Type into a predicate of kind f k ~> Type.

Essentially tests universal quantification.

Arguments

 :: forall (p :: k ~> Type) (as :: f k). Universe f => (forall a. Elem f as a -> Sing a -> Decision (p @@ a)) predicate on value -> Sing as -> Decision (All f p @@ as) predicate on collection

decideAll, but providing an Elem.

## Entailment

entailAll :: forall f p q. Universe f => (p --> q) -> All f p --> All f q Source #

If for all a we have p a, and if p implies q, then for all a we must also have p a.

Arguments

 :: (Universe f, SingI as) => (forall a. Elem f as a -> Sing a -> (p @@ a) -> q @@ a) implication -> (All f p @@ as) -> All f q @@ as

entailAll, but providing an Elem.

Arguments

 :: (Universe f, Applicative h) => (p --># q) h implication in context -> (All f p --># All f q) h

If p implies q under some context h, and if we have p a for all a, then we must have q a for all a under context h.

Arguments

 :: (Universe f, Applicative h, SingI as) => (forall a. Elem f as a -> (p @@ a) -> h (q @@ a)) implication in context -> (All f p @@ as) -> h (All f q @@ as)

entailAllF, but providing an Elem.

decideEntailAll :: forall f p q. Universe f => (p -?> q) -> All f p -?> All f q Source #

If we have p a for all a, and p a can be used to test for q a, then we can test all as for q a.

Arguments

 :: (Universe f, SingI as) => (forall a. Elem f as a -> (p @@ a) -> Decision (q @@ a)) decidable implication -> (All f p @@ as) -> Decision (All f q @@ as)

entailAllF, but providing an Elem.