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 TyPP :: (k -> v -> Type) -> ParamPred 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)
- type SelectableTC t = Provable (Found (TyPP t))
- selectTC :: forall t. SelectableTC t => Prove (Found (TyPP t))
- type SearchableTC t = Decidable (Found (TyPP t))
- searchTC :: forall t. SearchableTC t => Decide (Found (TyPP t))
- 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
, 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 -> Type) Source # | |
(Decidable (Found p), SingI f) => Decidable (Found (PPMap f p) :: TyFun k Type -> Type) Source # | |
Auto (NotFound p) (f @@ a) => Auto (NotFound (PPMap f p) :: Predicate k) (a :: k) Source # | Since: 0.1.2.0 |
Auto (Found p) (f @@ a) => Auto (Found (PPMap f p) :: TyFun k Type -> Type) (a :: k) Source # | Since: 0.1.2.0 |
type Apply (PPMap f p x :: TyFun k2 Type -> 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 -> Type) (as :: f k) Source # | Since: 0.1.2.0 |
(Universe f, Decidable (Found p)) => Decidable (Found (AnyMatch f p) :: TyFun (f k) Type -> Type) Source # | |
type Apply (AnyMatch f p as :: TyFun k2 Type -> 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
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: 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.
Type Constructors
type SelectableTC t = Provable (Found (TyPP t)) Source #
If T :: k -> v ->
is a type constructor, then Type
is a constraint that Selectable
TT
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 ->
instead of matchable type-level functions (that are Type
k ~>
). Useful because Type
selectTC
doesn't require anything fancy like
TypeApplications to use.
Since: 0.1.4.0
selectTC :: forall t. SelectableTC t => Prove (Found (TyPP t)) Source #
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
type SearchableTC t = Decidable (Found (TyPP t)) Source #
If T :: k -> v ->
is a type constructor, then Type
is a constraint that SearchableTC
TT
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 ->
instead of matchable type-level functions (that are Type
k ~>
). Useful because Type
searchTC
doesn't require anything fancy like
TypeApplications to use.
Since: 0.1.4.0
searchTC :: forall t. SearchableTC t => Decide (Found (TyPP t)) Source #
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
Combining
data OrP :: ParamPred k v -> ParamPred k v -> ParamPred k v Source #
Disjunction on two ParamPred
s, with appropriate Searchable
instance. Priority is given to the left predicate.
Since: 0.1.3.0
data AndP :: ParamPred k v -> ParamPred k u -> ParamPred k (v, u) Source #
Conjunction on two ParamPred
s, with appropriate Searchable
and
Selectable
instances.
Since: 0.1.3.0