| Copyright | (c) Justin Le 2018 |
|---|---|
| License | BSD3 |
| Maintainer | justin@jle.im |
| Stability | experimental |
| Portability | non-portable |
| Safe Haskell | None |
| Language | Haskell2010 |
Data.Type.Predicate.Param
Synopsis
- type ParamPred k v = k -> Predicate v
- data FlipPP :: ParamPred v k -> ParamPred k v
- data ConstPP :: Predicate v -> ParamPred k v
- data PPMap :: (k ~> j) -> ParamPred j v -> ParamPred k v
- type InP f = (ElemSym1 f :: ParamPred (f k) k)
- data AnyMatch f :: ParamPred k v -> ParamPred (f k) v
- data Found :: ParamPred k v -> Predicate k
- type NotFound (p :: ParamPred k v) = (Not (Found p) :: Predicate k)
- type Selectable p = Provable (Found p)
- select :: forall p. Selectable p => Prove (Found p)
- type Searchable p = Decidable (Found p)
- search :: forall p. Searchable p => Decide (Found p)
- inPNotNull :: Found (InP f) --> NotNull f
- notNullInP :: NotNull f --> Found (InP f)
- data OrP :: ParamPred k v -> ParamPred k v -> ParamPred k v
- data AndP :: ParamPred k v -> ParamPred k u -> ParamPred k (v, u)
Parameterized Predicates
type ParamPred k v = k -> Predicate v Source #
A parameterized predicate. See Found for more information.
data PPMap :: (k ~> j) -> ParamPred j v -> ParamPred k v Source #
Pre-compose a function to a ParamPred. Is essentially flip
(.)
Instances
| (Provable (Found p), SingI f) => Provable (Found (PPMap f p) :: TyFun k Type -> *) Source # | |
| (Decidable (Found p), SingI f) => Decidable (Found (PPMap f p) :: TyFun k Type -> *) Source # | |
| Auto (NotFound p) (f @@ a) => Auto (NotFound (PPMap f p) :: Predicate k) (a :: k) Source # | Since: decidable-0.1.2.0 |
| Auto (Found p) (f @@ a) => Auto (Found (PPMap f p) :: TyFun k Type -> *) (a :: k) Source # | Since: decidable-0.1.2.0 |
| type Apply (PPMap f p x :: TyFun k2 Type -> *) (y :: k2) Source # | |
data AnyMatch f :: ParamPred k v -> ParamPred (f k) v Source #
AnyMatch fk (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 asa and
testing if p a :: is satisfied for any item in Predicate kas ::
f k.
A ParamPred k vk can create some v. The resulting
ParamPred (f k) vk in f k can create some v.
Instances
| (SingI as, AutoAll f (Not (Found p)) as) => Auto (Not (Found (AnyMatch f p)) :: TyFun (f k) Type -> *) (as :: f k) Source # | Since: decidable-0.1.2.0 |
| (Universe f, Decidable (Found p)) => Decidable (Found (AnyMatch f p) :: TyFun (f k) Type -> *) Source # | |
| type Apply (AnyMatch f p as :: TyFun k2 Type -> *) (a :: k2) Source # | |
Deciding and Proving
data Found :: ParamPred k v -> Predicate k Source #
Convert a parameterized predicate into a predicate on the parameter.
A Found pp :: that tests a ParamPred k vk
for the fact that there exists a v where ParamPred k v
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)P ::
, means that for any input ParamPred k vx :: 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)x
:: k, we can prove or disprove the fact that there exists a y :: v
such that P x @@ y.
Instances
type NotFound (p :: ParamPred k v) = (Not (Found p) :: Predicate k) Source #
Convert a parameterized predicate into a predicate on the parameter.
A Found pp :: that tests a ParamPred k vk
for the fact that there cannot exist a v where ParamPred k vNotFound P @@ xy :: v
can exist where P x @@ y is satisfied.
For some context, an instance of Provable (NotFound P)P
:: , means that for any input ParamPred k vx :: 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)x
:: k, we can prove or disprove the fact that there does not exist a y
:: v such that P x @@ y.
Since: decidable-0.1.2.0
type Selectable p = Provable (Found p) Source #
A constraint that a ParamPred k vx :: k, we can always find a y :: v that satisfies P
x @@ y. We can "select" that y, no matter what.
type Searchable p = Decidable (Found p) Source #
A constraint that a ParamPred k vx :: 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.
Combining
data OrP :: ParamPred k v -> ParamPred k v -> ParamPred k v Source #
Disjunction on two ParamPreds, with appropriate Searchable
instance. Priority is given to the left predicate.
Since: decidable-0.1.3.0
data AndP :: ParamPred k v -> ParamPred k u -> ParamPred k (v, u) Source #
Conjunction on two ParamPreds, with appropriate Searchable and
Selectable instances.
Since: decidable-0.1.3.0