Copyright | (c) Justin Le 2018 |
---|---|
License | BSD3 |
Maintainer | justin@jle.im |
Stability | experimental |
Portability | non-portable |
Safe Haskell | None |
Language | Haskell2010 |
Higher-level predicates for quantifying predicates over universes and sets.
Synopsis
- data Any f :: Predicate k -> Predicate (f k)
- data WitAny f :: (k ~> Type) -> f k -> Type where
- anyImpossible :: Universe f => Any f Impossible --> Impossible
- decideAny :: forall f k (p :: k ~> Type). Universe f => Decide p -> Decide (Any f p)
- idecideAny :: forall k (p :: k ~> Type) (as :: f k). Universe f => (forall a. Elem f as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (Any f p @@ as)
- decideNone :: forall f k (p :: k ~> Type). Universe f => Decide p -> Decide (None f p)
- idecideNone :: forall f k (p :: k ~> Type) (as :: f k). Universe f => (forall a. Elem f as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (None f p @@ as)
- type None f p = (Not (Any f p) :: Predicate (f k))
- allNotNone :: All f (Not p) --> None f p
- noneAllNot :: forall f p. (Universe f, Decidable p) => None f p --> All f (Not p)
- entailAny :: forall f p q. Universe f => (p --> q) -> Any f p --> Any f q
- ientailAny :: forall f p q as. (Universe f, SingI as) => (forall a. Elem f as a -> Sing a -> (p @@ a) -> q @@ a) -> (Any f p @@ as) -> Any f q @@ as
- entailAnyF :: forall f p q h. (Universe f, Functor h) => (p --># q) h -> (Any f p --># Any f q) h
- ientailAnyF :: forall f p q as h. Functor h => (forall a. Elem f as a -> (p @@ a) -> h (q @@ a)) -> (Any f p @@ as) -> h (Any f q @@ as)
- allComp :: (All f (All g p) @@ as) -> All (f :.: g) p @@ Comp as
- compAll :: (All (f :.: g) p @@ Comp as) -> All f (All g p) @@ as
- data All f :: Predicate k -> Predicate (f k)
- newtype WitAll f p (as :: f k) = WitAll {}
- decideAll :: forall f k (p :: k ~> Type). Universe f => Decide p -> Decide (All f p)
- idecideAll :: forall k (p :: k ~> Type) (as :: f k). Universe f => (forall a. Elem f as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (All f p @@ as)
- type NotAll f p = (Not (All f p) :: Predicate (f k))
- anyNotNotAll :: Any f (Not p) --> NotAll f p
- notAllAnyNot :: forall f p. (Universe f, Decidable p) => NotAll f p --> Any f (Not p)
- entailAll :: forall f p q. Universe f => (p --> q) -> All f p --> All f q
- ientailAll :: forall f p q as. (Universe f, SingI as) => (forall a. Elem f as a -> Sing a -> (p @@ a) -> q @@ a) -> (All f p @@ as) -> All f q @@ as
- entailAllF :: forall f p q h. (Universe f, Applicative h) => (p --># q) h -> (All f p --># All f q) h
- ientailAllF :: forall f p q as h. (Universe f, Applicative h, SingI as) => (forall a. Elem f as a -> (p @@ a) -> h (q @@ a)) -> (All f p @@ as) -> h (All f q @@ as)
- decideEntailAll :: forall f p q. Universe f => (p -?> q) -> All f p -?> All f q
- idecideEntailAll :: forall f p q as. (Universe f, SingI as) => (forall a. Elem f as a -> (p @@ a) -> Decision (q @@ a)) -> (All f p @@ as) -> Decision (All f q @@ as)
- anyComp :: (Any f (Any g p) @@ as) -> Any (f :.: g) p @@ Comp as
- compAny :: (Any (f :.: g) p @@ Comp as) -> Any f (Any g p) @@ as
Any
data Any f :: Predicate k -> Predicate (f k) Source #
An
is a predicate testing a collection Any
f pas :: 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
data WitAny f :: (k ~> Type) -> f k -> Type where Source #
A
is a witness that, for at least one item WitAny
p asa
in the
type-level collection as
, the predicate p a
is true.
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
:: 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.
:: 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
.
:: 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
.
Negation
type None f p = (Not (Any f p) :: Predicate (f k)) Source #
A
is a predicate on a collection None
f pas
that no a
in as
satisfies predicate p
.
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
to interrogate the input disproof.Decidable
p
Since: 0.1.2.0
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
.
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 ->
.
This is if the Decision
(q a)p a ->
implication is false, there
it doesn't mean that there is no Decision
(q a)a
such that q a
, necessarily.
There could have been an a
where p
does not hold, but q
does.
:: 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
.
Composition
All
data All f :: Predicate k -> Predicate (f k) Source #
An
is a predicate testing a collection All
f pas :: 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 :: Predicate k1 -> TyFun (f k1) Type -> Type) Source # | |
Universe f => DFunctor (All f :: Predicate k1 -> TyFun (f k1) Type -> Type) Source # | |
(Universe f, Provable p) => Provable (All f p :: TyFun (f k) Type -> Type) Source # | |
(Universe f, Decidable p) => Decidable (All f p :: TyFun (f k) Type -> Type) Source # | |
AutoAll f p as => Auto (All f p :: TyFun (f k) Type -> Type) (as :: f k) Source # | Since: 0.1.2.0 |
type Apply (All f p :: TyFun (f k) Type -> Type) (as :: f k) Source # | |
newtype WitAll f p (as :: f k) Source #
A
is a witness that the predicate WitAll
p asp a
is true for all
items a
in the type-level collection as
.
Decision
:: 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.
Negation
type NotAll f p = (Not (All f p) :: Predicate (f k)) Source #
A
is a predicate on a collection NotAll
f pas
that at least one
a
in as
does not satisfy predicate p
.
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
in
order to locate that specific Decidable
pa
.
Since: 0.1.2.0
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
.
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
.
:: (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 a
s for q a
.
:: (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
.