Data.Type.Predicate.Param

Manipulate "parameterized predicates". See ParamPred and Found for more information.

Parameterized Predicates

type ParamPred k v = k -> Predicate v

A parameterized predicate. See Found for more information.

data FlipPP :: ParamPred v k -> ParamPred k v

Flip the arguments of a ParamPred.

Instances

type Apply (FlipPP p x :: TyFun k2 Type -> *) (y :: k2)

Defined in Data.Type.Predicate.Param

type Apply (FlipPP p x :: TyFun k2 Type -> *) (y :: k2) = p y @@ x

data ConstPP :: Predicate v -> ParamPred k v

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

Instances

type Apply (ConstPP p k3 :: TyFun k2 Type -> *) (v :: k2)

Defined in Data.Type.Predicate.Param

type Apply (ConstPP p k3 :: TyFun k2 Type -> *) (v :: k2) = p @@ v

data PPMap :: (k ~> j) -> ParamPred j v -> ParamPred k v

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

Instances

(Provable (Found p), SingI f) => Provable (Found (PPMap f p) :: TyFun k Type -> *)

Defined in Data.Type.Predicate.Param

Methods

prove :: Prove (Found (PPMap f p))

(Decidable (Found p), SingI f) => Decidable (Found (PPMap f p) :: TyFun k Type -> *)

Defined in Data.Type.Predicate.Param

Methods

decide :: Decide (Found (PPMap f p))

type Apply (PPMap f p x :: TyFun k2 Type -> *) (y :: k2)

Defined in Data.Type.Predicate.Param

type Apply (PPMap f p x :: TyFun k2 Type -> *) (y :: k2) = p (f @@ x) @@ y

type InP f = (ElemSym1 f :: ParamPred (f k) k)

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.

data AnyMatch f :: ParamPred k v -> ParamPred (f k) v

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.

Instances

(Universe f, Decidable (Found p)) => Decidable (Found (AnyMatch f p) :: TyFun (f k) Type -> *)

Defined in Data.Type.Predicate.Param

Methods

decide :: Decide (Found (AnyMatch f p))

type Apply (AnyMatch f p as :: TyFun k2 Type -> *) (a :: k2)

Defined in Data.Type.Predicate.Param

type Apply (AnyMatch f p as :: TyFun k2 Type -> *) (a :: k2) = Any f (FlipPP p a) @@ as

Deciding and Proving

data Found :: ParamPred k v -> Predicate k

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.

Instances

(Provable (Found p), SingI f) => Provable (Found (PPMap f p) :: TyFun k Type -> *)

Defined in Data.Type.Predicate.Param

Methods

prove :: Prove (Found (PPMap f p))

(Decidable (Found p), SingI f) => Decidable (Found (PPMap f p) :: TyFun k Type -> *)

Defined in Data.Type.Predicate.Param

Methods

decide :: Decide (Found (PPMap f p))

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

Defined in Data.Type.Predicate.Param

Methods

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

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

Defined in Data.Type.Predicate.Param

Methods

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

(Universe f, Decidable (Found p)) => Decidable (Found (AnyMatch f p) :: TyFun (f k) Type -> *)

Defined in Data.Type.Predicate.Param

Methods

decide :: Decide (Found (AnyMatch f p))

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

Defined in Data.Type.Predicate.Param

Methods

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

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

Defined in Data.Type.Predicate.Param

Methods

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

Universe f => Decidable (Found (InP f :: ParamPred (f v) v) :: TyFun (f v) Type -> *)

Defined in Data.Type.Predicate.Param

Methods

decide :: Decide (Found (InP f))

type Apply (Found p :: TyFun k Type -> *) (a :: k)

Defined in Data.Type.Predicate.Param

type Apply (Found p :: TyFun k Type -> *) (a :: k) = Σ v (p a)

type Selectable p = Provable (Found p)

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.

select :: forall p. Selectable p => Prove (Found p)

The proving/selecting function for Selectable p.

Must be called by applying the ParamPred:

select @p

type Searchable p = Decidable (Found p)

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.

search :: forall p. Searchable p => Decide (Found p)

The deciding/searching function for Searchable p.

Must be called by applying the ParamPred:

search @p