decidable-0.3.1.0: Combinators for manipulating dependently-typed predicates.
Copyright(c) Justin Le 2018
LicenseBSD3
Maintainerjustin@jle.im
Stabilityexperimental
Portabilitynon-portable
Safe HaskellSafe-Inferred
LanguageHaskell2010

Data.Type.Predicate.Quantification

Description

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

Synopsis

Any

data Any f :: Predicate k -> Predicate (f k) 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

Instances details
Universe f => TFunctor (Any f :: Predicate k1 -> TyFun (f k1) Type -> Type) Source # 
Instance details

Defined in Data.Type.Universe

Methods

tmap :: forall (p :: k10 ~> Type) (q :: k10 ~> Type). (p --> q) -> Any f p --> Any f q Source #

SingI a => Auto (IsJust :: Predicate (Maybe k)) ('Just a :: Maybe k) Source #

Since: 0.1.2.0

Instance details

Defined in Data.Type.Predicate.Auto

Methods

auto :: IsJust @@ 'Just a Source #

(SingI as, AutoAll f (Not p) as) => Auto (Not (Any f p) :: TyFun (f k) Type -> Type) (as :: f k) Source #

Since: 0.1.2.0

Instance details

Defined in Data.Type.Predicate.Auto

Methods

auto :: Not (Any f p) @@ as Source #

SingI a => Auto (NotNull Identity :: Predicate (Identity k)) ('Identity a :: Identity k) Source # 
Instance details

Defined in Data.Type.Predicate.Auto

SingI a => Auto (NotNull NonEmpty :: Predicate (NonEmpty k)) (a :| as :: NonEmpty k) Source #

Since: 0.1.2.0

Instance details

Defined in Data.Type.Predicate.Auto

Methods

auto :: NotNull NonEmpty @@ (a :| as) Source #

SingI a => Auto (NotNull [] :: Predicate [k]) (a ': as :: [k]) Source #

Since: 0.1.2.0

Instance details

Defined in Data.Type.Predicate.Auto

Methods

auto :: NotNull [] @@ (a ': as) Source #

Decidable ((NotNull f :: Predicate (f k)) ==> Found (InP f :: ParamPred (f k) k) :: TyFun (f k) Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate.Param

Methods

decide :: Decide (NotNull f ==> Found (InP f)) Source #

(Universe f, Provable p) => Decidable ((NotNull f :: Predicate (f k)) ==> Any f p :: TyFun (f k) Type -> Type) Source # 
Instance details

Defined in Data.Type.Universe

Methods

decide :: Decide (NotNull f ==> Any f p) Source #

(Universe f, Decidable p) => Decidable (Any f p :: TyFun (f k) Type -> Type) Source # 
Instance details

Defined in Data.Type.Universe

Methods

decide :: Decide (Any f p) Source #

Decidable (Found (InP f :: ParamPred (f v) v) ==> (NotNull f :: Predicate (f v)) :: TyFun (f v) Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate.Param

Methods

decide :: Decide (Found (InP f) ==> NotNull f) Source #

Provable ((NotNull f :: Predicate (f k)) ==> Found (InP f :: ParamPred (f k) k) :: TyFun (f k) Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate.Param

Methods

prove :: Prove (NotNull f ==> Found (InP f)) Source #

Provable p => Provable ((NotNull f :: Predicate (f k)) ==> Any f p :: TyFun (f k) Type -> Type) Source # 
Instance details

Defined in Data.Type.Universe

Methods

prove :: Prove (NotNull f ==> Any f p) Source #

Provable (Found (InP f :: ParamPred (f v) v) ==> (NotNull f :: Predicate (f v)) :: TyFun (f v) Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate.Param

Methods

prove :: Prove (Found (InP f) ==> NotNull f) Source #

SingI a => Auto (IsRight :: Predicate (Either j k)) ('Right a :: Either j k) Source #

Since: 0.1.2.0

Instance details

Defined in Data.Type.Predicate.Auto

Methods

auto :: IsRight @@ 'Right a Source #

SingI a => Auto (NotNull ((,) j) :: Predicate (j, k)) ('(w, a) :: (j, k)) Source #

Since: 0.1.2.0

Instance details

Defined in Data.Type.Predicate.Auto

Methods

auto :: NotNull ((,) j) @@ '(w, a) Source #

type Apply (Any f p :: TyFun (f k) Type -> Type) (as :: f k) Source # 
Instance details

Defined in Data.Type.Universe

type Apply (Any f p :: TyFun (f k) Type -> 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.

anyImpossible :: Universe f => Any f Impossible --> Impossible Source #

It is impossible for any value in a collection to be Impossible.

Since: 0.1.2.0

Decision

decideAny Source #

Arguments

:: forall f k (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.

idecideAny Source #

Arguments

:: forall k (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.

decideNone Source #

Arguments

:: forall f k (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.

idecideNone Source #

Arguments

:: forall f k (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.

ientailAny Source #

Arguments

:: forall f p q as. (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.

entailAnyF Source #

Arguments

:: forall f p q h. (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.

ientailAnyF Source #

Arguments

:: forall f p q as h. 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 :: Predicate k -> Predicate (f k) 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

Instances details
Universe f => DFunctor (All f :: Predicate k1 -> TyFun (f k1) Type -> Type) Source # 
Instance details

Defined in Data.Type.Universe

Methods

dmap :: forall (p :: k10 ~> Type) (q :: k10 ~> Type). (p -?> q) -> All f p -?> All f q Source #

Universe f => TFunctor (All f :: Predicate k1 -> TyFun (f k1) Type -> Type) Source # 
Instance details

Defined in Data.Type.Universe

Methods

tmap :: forall (p :: k10 ~> Type) (q :: k10 ~> Type). (p --> q) -> All f p --> All f q Source #

(Universe f, Decidable p) => Decidable (All f p :: TyFun (f k) Type -> Type) Source # 
Instance details

Defined in Data.Type.Universe

Methods

decide :: Decide (All f p) Source #

(Universe f, Provable p) => Provable (All f p :: TyFun (f k) Type -> Type) Source # 
Instance details

Defined in Data.Type.Universe

Methods

prove :: Prove (All f p) Source #

AutoAll f p as => Auto (All f p :: TyFun (f k) Type -> Type) (as :: f k) Source #

Since: 0.1.2.0

Instance details

Defined in Data.Type.Predicate.Auto

Methods

auto :: All f p @@ as Source #

type Apply (All f p :: TyFun (f k) Type -> Type) (as :: f k) Source # 
Instance details

Defined in Data.Type.Universe

type Apply (All f p :: TyFun (f k) Type -> 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 

Fields

type NotAll f p = Not (All f p) :: Predicate (f k) Source #

A NotAll f p is a predicate on a collection as that at least one a in as does not satisfy predicate p.

Decision

decideAll Source #

Arguments

:: forall f k (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.

idecideAll Source #

Arguments

:: forall k (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.

ientailAll Source #

Arguments

:: forall f p q as. (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.

entailAllF Source #

Arguments

:: forall f p q h. (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.

ientailAllF Source #

Arguments

:: forall f p q as h. (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.

idecideEntailAll Source #

Arguments

:: forall f p q as. (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.

Logical interplay

allToAny :: (All f p &&& NotNull f) --> Any f p Source #

If something is true for all xs, then it must be true for at least one x in xs, provided that xs is not empty.

Since: 0.1.5.0

allNotNone :: All f (Not p) --> None f p Source #

If p is false for all a in as, then no a in as satisfies p.

Since: 0.1.2.0

noneAllNot :: forall f p. (Universe f, Decidable p) => None f p --> All f (Not p) Source #

If no a in as satisfies p, then p is false for all a in as. Requires Decidable p to interrogate the input disproof.

Since: 0.1.2.0

anyNotNotAll :: Any f (Not p) --> NotAll f p Source #

If any a in as does not satisfy p, then not all a in as satisfy p.

Since: 0.1.2.0

notAllAnyNot :: forall f p. (Universe f, Decidable p) => NotAll f p --> Any f (Not p) Source #

If not all a in as satisfy p, then there must be at least one a in as that does not satisfy p. Requires Decidable p in order to locate that specific a.

Since: 0.1.2.0