search package:decidable

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.

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.

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.

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.