Copyright | (c) Justin Le 2018 |
---|---|
License | BSD3 |
Maintainer | justin@jle.im |
Stability | experimental |
Portability | non-portable |
Safe Haskell | None |
Language | Haskell2010 |
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)
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
, but unfortunately defunctionalization doesn't work too well with
that definition.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 #
takes a parmaeterized predicate on 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
is a predicate taking an argument AnyMatch
f p asa
and
testing if p a ::
is satisfied for any item in Predicate
kas ::
f k
.
A
tests if a ParamPred
k vk
can create some v
. The resulting
tests if any 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
is a predicate on Found
pp ::
that tests a ParamPred
k vk
for the fact that there exists a v
where
is satisfied.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
, where 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
, it means that for all Decidable
(Found
P)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 -> *) 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 |
(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 |
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, Decidable (Found p)) => Decidable (Found (AnyMatch 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 # | |
Universe f => Decidable (Found (InP f :: ParamPred (f v) v) :: TyFun (f v) Type -> *) Source # | |
type Apply (Found p :: TyFun k Type -> *) (a :: k) Source # | |
type NotFound (p :: ParamPred k v) = (Not (Found p) :: Predicate k) Source #
Convert a parameterized predicate into a predicate on the parameter.
A
is a predicate on Found
pp ::
that tests a ParamPred
k vk
for the fact that there cannot exist a v
where
is
satisfied. That is, ParamPred
k v
is satisfied if no NotFound
P @@ xy :: v
can exist where P x @@ y
is satisfied.
For some context, an instance of
, where 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
, it means that for all 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
s "selectable". It means that
for any input 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
is "searchable". It means that
for any input 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.