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 :: (k ~> Type) -> f k ~> Type
- data WitAny f :: (k ~> Type) -> f k -> Type where
- type None f p = (Not (Any f p) :: Predicate (f k))
- 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)
- 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)
- data All f :: (k ~> Type) -> f k ~> Type
- 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)
- 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)

# Any

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

An

is a predicate testing a collection `Any`

f p`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 # | |

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

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

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

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

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

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

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

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

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

A

is a witness that, for at least one item `WitAny`

p as`a`

in the
type-level collection `as`

, the predicate `p a`

is true.

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

A

is a predicate on a collection `None`

f p`as`

that no `a`

in `as`

satisfies predicate `p`

.

## 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`

.

## 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 `Decision`

(q a)*no* `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`

.

# All

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

An

is a predicate testing a collection `All`

f p`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 # | |

Universe f => DFunctor (All f :: (k1 ~> Type) -> TyFun (f k1) Type -> *) Source # | |

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

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

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

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

A

is a witness that the predicate `WitAll`

p as`p 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.

## 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`

.