A parameterized predicate. See Found for more information.

Found (IsTC t) @@ x is true if x was made using the unary type constructor t.

For example:

type IsJust = (Found (IsTC 'Just) :: Predicate (Maybe v))

makes a predicate where IsJust @@ x is true if x is Just, and false if x is Nothing.

For a more general version, see EqBy

The kind of IsTC is:

IsTC :: (v -> k) -> ParamPred k v
Found (IsTC t) :: Predicate k

Applied to specific things:

IsTC 'Just :: ParamPred (Maybe v) v
Found (IsTC 'Just') :: Predicate (Maybe v)

Since: 0.1.5.0

Found (EqBy f) @@ x is true if there exists some value when, with f applied to it, is equal to x.

See IsTC for a useful specific application.

EqBy :: (v ~> k) -> ParamPred k v
Found (EqBy f) :: Predicate k

Since: 0.1.5.0

Flip the arguments of a ParamPred.

Promote a Predicate v to a ParamPred k v, ignoring the k input.

Pre-compose a function to a ParamPred. Is essentially flip (.), but unfortunately defunctionalization doesn't work too well with that definition.

Pre-compose a function to a ParamPred, but on the "value" side.

Since: 0.1.5.0

A ParamPred (f k) k. Parameterized on an as :: f k, returns a predicate that is true if there exists any a :: k in as.

Essentially NotNull.

AnyMatch f takes a parmaeterized predicate on k (testing for a v) and turns it into a parameterized predicate on f k (testing for a v). It "lifts" the domain into f.

An AnyMatch f p as is a predicate taking an argument a and testing if p a :: Predicate k is satisfied for any item in as :: f k.

A ParamPred k v tests if a k can create some v. The resulting ParamPred (f k) v tests if any k in f k can create some v.

Convert a normal -> type constructor taking two arguments into a ParamPred.

TyPP :: (k -> v -> Type) -> ParamPred k v

Since: 0.1.4.0

Convert a parameterized predicate into a predicate on the parameter.

A Found p is a predicate on p :: ParamPred k v that tests a k for the fact that there exists a v where ParamPred k v is satisfied.

Intended as the basic interface for ParamPred, since it turns a ParamPred into a normal Predicate, which can have Decidable and Provable instances.

For some context, an instance of Provable (Found P), where P :: ParamPred k v, means that for any input x :: k, we can always find a y :: v such that we have P x @@ y.

In the language of quantifiers, it means that forall x :: k, there exists a y :: v such that P x @@ y.

For an instance of Decidable (Found P), it means that for all x :: k, we can prove or disprove the fact that there exists a y :: v such that P x @@ y.

Convert a parameterized predicate into a predicate on the parameter.

A Found p is a predicate on p :: ParamPred k v that tests a k for the fact that there cannot exist a v where ParamPred k v is satisfied. That is, NotFound P @@ x is satisfied if no y :: v can exist where P x @@ y is satisfied.

For some context, an instance of Provable (NotFound P), where P :: ParamPred k v, means that for any input x :: k, we can always reject any y :: v that claims to satisfy P x @@ y.

In the language of quantifiers, it means that forall x :: k, there does not exist a y :: v such that P x @@ y.

For an instance of Decidable (Found P), it means that for all x :: k, we can prove or disprove the fact that there does not exist a y :: v such that P x @@ y.

Since: 0.1.2.0

A constraint that a ParamPred k v s "selectable". It means that for any input x :: k, we can always find a y :: v that satisfies P x @@ y. We can "select" that y, no matter what.

The proving/selecting function for Selectable p.

Because this is ambiguously typed, it must be called by applying the ParamPred:

select @p

See selectTC and SelectableTC for a version that isn't ambiguously typed, but only works when p is a type constructor.

A constraint that a ParamPred k v is "searchable". It means that for any input x :: k, we can prove or disprove that there exists a y :: v that satisfies P x @@ y. We can "search" for that y, and prove that it can or cannot be found.

The deciding/searching function for Searchable p.

Because this is ambiguously typed, it must be called by applying the ParamPred:

search @p

See searchTC and SearchableTC for a version that isn't ambiguously typed, but only works when p is a type constructor.

NotNull f is basically Found (InP f).

Since: 0.1.2.0

NotNull f is basically Found (InP f).

Since: 0.1.2.0

If T :: k -> v -> Type is a type constructor, then Selectable T is a constraint that T is "selectable", in that you have a canonical function:

selectTC :: Sing a -> Σ v (TyPP T x)

That is, given an x :: k, we can always find a y :: k that satisfies T x y.

Is essentially Selectable, except with type constructors k -> Type instead of matchable type-level functions (that are k ~> Type). Useful because selectTC doesn't require anything fancy like TypeApplications to use.

Since: 0.1.4.0

The canonical selecting function for SelectableTC t.

Note that because t must be an injective type constructor, you can use this without explicit type applications; the instance of SelectableTC can be inferred from the result type.

Since: 0.1.4.0

If T :: k -> v -> Type is a type constructor, then SearchableTC T is a constraint that T is "searchable", in that you have a canonical function:

searchTC :: Sing x -> Decision (Σ v (TyPP T x))

That, given an x :: k, we can decide whether or not a y :: v exists that satisfies T x y.

Is essentially Searchable, except with type constructors k -> Type instead of matchable type-level functions (that are k ~> Type). Useful because searchTC doesn't require anything fancy like TypeApplications to use.

Since: 0.1.4.0

The canonical selecting function for Searchable t.

Note that because t must be an injective type constructor, you can use this without explicit type applications; the instance of SearchableTC can be inferred from the result type.

Since: 0.1.4.0

Disjunction on two ParamPreds, with appropriate Searchable instance. Priority is given to the left predicate.

Since: 0.1.3.0

Conjunction on two ParamPreds, with appropriate Searchable and Selectable instances.

Since: 0.1.3.0