decidable-0.3.1.0: Combinators for manipulating dependently-typed predicates.
Copyright(c) Justin Le 2018
LicenseBSD3
Maintainerjustin@jle.im
Stabilityexperimental
Portabilitynon-portable
Safe HaskellSafe-Inferred
LanguageHaskell2010

Data.Type.Predicate.Param

Description

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

Synopsis

Parameterized Predicates

type ParamPred k v = k -> Predicate v Source #

A parameterized predicate. See Found for more information.

type IsTC t = EqBy (TyCon1 t) Source #

Found (IsTC t) @@ x is true if x was made using the unary type constructor t.

For example:

type IsJust = (Found (IsTC 'Just) :: Predicate (Maybe v))

makes a predicate where IsJust @@ x is true if x is Just, and false if x is Nothing.

For a more general version, see EqBy

The kind of IsTC is:

IsTC :: (v -> k) -> ParamPred k v
Found (IsTC t) :: Predicate k

Applied to specific things:

IsTC 'Just :: ParamPred (Maybe v) v
Found (IsTC 'Just') :: Predicate (Maybe v)

Since: 0.1.5.0

data EqBy :: (v ~> k) -> ParamPred k v Source #

Found (EqBy f) @@ x is true if there exists some value when, with f applied to it, is equal to x.

See IsTC for a useful specific application.

EqBy :: (v ~> k) -> ParamPred k v
Found (EqBy f) :: Predicate k

Since: 0.1.5.0

Instances

Instances details
type Apply (EqBy f x :: TyFun k1 Type -> Type) (y :: k1) Source # 
Instance details

Defined in Data.Type.Predicate.Param

type Apply (EqBy f x :: TyFun k1 Type -> Type) (y :: k1) = x :~: (f @@ y)

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

Flip the arguments of a ParamPred.

Instances

Instances details
type Apply (FlipPP p x :: TyFun k2 Type -> Type) (y :: k2) Source # 
Instance details

Defined in Data.Type.Predicate.Param

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

data ConstPP :: Predicate v -> ParamPred k v Source #

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

Instances

Instances details
type Apply (ConstPP p k3 :: TyFun k1 Type -> Type) (v :: k1) Source # 
Instance details

Defined in Data.Type.Predicate.Param

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

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

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

Instances

Instances details
(Decidable (Found p), SingI f) => Decidable (Found (PPMap f p) :: TyFun k Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate.Param

Methods

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

(Provable (Found p), SingI f) => Provable (Found (PPMap f p) :: TyFun k Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate.Param

Methods

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

Auto (Found p) (f @@ a) => Auto (Found (PPMap f p) :: TyFun k Type -> Type) (a :: k) Source #

Since: 0.1.2.0

Instance details

Defined in Data.Type.Predicate.Auto

Methods

auto :: Found (PPMap f p) @@ a Source #

Auto (NotFound p) (f @@ a) => Auto (NotFound (PPMap f p) :: Predicate k) (a :: k) Source #

Since: 0.1.2.0

Instance details

Defined in Data.Type.Predicate.Auto

Methods

auto :: NotFound (PPMap f p) @@ a Source #

type Apply (PPMap f p x :: TyFun k2 Type -> Type) (y :: k2) Source # 
Instance details

Defined in Data.Type.Predicate.Param

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

data PPMapV :: (u ~> v) -> ParamPred k u -> ParamPred k v Source #

Pre-compose a function to a ParamPred, but on the "value" side.

Since: 0.1.5.0

Instances

Instances details
type Apply (PPMapV f p x :: TyFun k1 Type -> Type) (y :: k1) Source # 
Instance details

Defined in Data.Type.Predicate.Param

type Apply (PPMapV f p x :: TyFun k1 Type -> Type) (y :: k1) = p x @@ (f @@ y)

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

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 Source #

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

Instances details
(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

Instance details

Defined in Data.Type.Predicate.Auto

Methods

auto :: Not (Found (AnyMatch f p)) @@ as Source #

(Universe f, Decidable (Found p)) => Decidable (Found (AnyMatch f p) :: TyFun (f k) Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate.Param

Methods

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

type Apply (AnyMatch f p as :: TyFun k1 Type -> Type) (a :: k1) Source # 
Instance details

Defined in Data.Type.Predicate.Param

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

data TyPP :: (k -> v -> Type) -> ParamPred k v Source #

Convert a normal -> type constructor taking two arguments into a ParamPred.

TyPP :: (k -> v -> Type) -> ParamPred k v

Since: 0.1.4.0

Instances

Instances details
type Apply (TyPP t k3 :: TyFun k1 Type -> Type) (v :: k1) Source # 
Instance details

Defined in Data.Type.Predicate.Param

type Apply (TyPP t k3 :: TyFun k1 Type -> Type) (v :: k1) = t k3 v

Deciding and Proving

data Found :: ParamPred k v -> Predicate k Source #

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

Instances details
(Decidable (Found p), SingI f) => Decidable (Found (PPMap f p) :: TyFun k Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate.Param

Methods

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

(Searchable p, Searchable q) => Decidable (Found (AndP p q) :: TyFun k1 Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate.Param

Methods

decide :: Decide (Found (AndP p q)) Source #

(Searchable p, Searchable q) => Decidable (Found (OrP p q) :: TyFun k1 Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate.Param

Methods

decide :: Decide (Found (OrP p q)) Source #

(Provable (Found p), SingI f) => Provable (Found (PPMap f p) :: TyFun k Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate.Param

Methods

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

(Selectable p, Selectable q) => Provable (Found (AndP p q) :: TyFun k1 Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate.Param

Methods

prove :: Prove (Found (AndP p q)) Source #

Auto (Found p) (f @@ a) => Auto (Found (PPMap f p) :: TyFun k Type -> Type) (a :: k) Source #

Since: 0.1.2.0

Instance details

Defined in Data.Type.Predicate.Auto

Methods

auto :: Found (PPMap f p) @@ a Source #

Auto (NotFound p) (f @@ a) => Auto (NotFound (PPMap f p) :: Predicate k) (a :: k) Source #

Since: 0.1.2.0

Instance details

Defined in Data.Type.Predicate.Auto

Methods

auto :: NotFound (PPMap f p) @@ a Source #

(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

Instance details

Defined in Data.Type.Predicate.Auto

Methods

auto :: Not (Found (AnyMatch f p)) @@ as Source #

Decidable ((NotNull f :: Predicate (f k)) ==> Found (InP f :: ParamPred (f k) k) :: TyFun (f k) Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate.Param

Methods

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

(Universe f, Decidable (Found p)) => Decidable (Found (AnyMatch f p) :: TyFun (f k) Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate.Param

Methods

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

Decidable (Found (InP f :: ParamPred (f v) v) ==> (NotNull f :: Predicate (f v)) :: TyFun (f v) Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate.Param

Methods

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

Universe f => Decidable (Found (InP f :: ParamPred (f v) v) :: TyFun (f v) Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate.Param

Methods

decide :: Decide (Found (InP f)) Source #

Provable ((NotNull f :: Predicate (f k)) ==> Found (InP f :: ParamPred (f k) k) :: TyFun (f k) Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate.Param

Methods

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

Provable (Found (InP f :: ParamPred (f v) v) ==> (NotNull f :: Predicate (f v)) :: TyFun (f v) Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate.Param

Methods

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

type Apply (Found p :: TyFun k Type -> Type) (a :: k) Source # 
Instance details

Defined in Data.Type.Predicate.Param

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

type NotFound (p :: ParamPred k v) = Not (Found p) :: Predicate k Source #

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 cannot exist a v where ParamPred k v is satisfied. That is, NotFound P @@ x is satisfied if no y :: v can exist where P x @@ y is satisfied.

For some context, an instance of Provable (NotFound P), where P :: ParamPred k v, means that for any input x :: 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), it means that for all 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 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) Source #

The proving/selecting function for Selectable p.

Because this is ambiguously typed, it must be called by applying the ParamPred:

select @p

See selectTC and SelectableTC for a version that isn't ambiguously typed, but only works when p is a type constructor.

type Searchable p = Decidable (Found p) Source #

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) Source #

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.

inPNotNull :: Found (InP f) --> NotNull f Source #

NotNull f is basically Found (InP f).

Since: 0.1.2.0

notNullInP :: NotNull f --> Found (InP f) Source #

NotNull f is basically Found (InP f).

Since: 0.1.2.0

Type Constructors

type SelectableTC t = Provable (Found (TyPP t)) Source #

If T :: k -> v -> Type is a type constructor, then Selectable T is a constraint that T 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 -> Type instead of matchable type-level functions (that are k ~> Type). Useful because 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 -> 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.

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 ParamPreds, with appropriate Searchable instance. Priority is given to the left predicate.

Since: 0.1.3.0

Instances

Instances details
(Searchable p, Searchable q) => Decidable (Found (OrP p q) :: TyFun k1 Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate.Param

Methods

decide :: Decide (Found (OrP p q)) Source #

type Apply (OrP p q x :: TyFun k1 Type -> Type) (y :: k1) Source # 
Instance details

Defined in Data.Type.Predicate.Param

type Apply (OrP p q x :: TyFun k1 Type -> Type) (y :: k1) = (p x ||| q x) @@ y

data AndP :: ParamPred k v -> ParamPred k u -> ParamPred k (v, u) Source #

Conjunction on two ParamPreds, with appropriate Searchable and Selectable instances.

Since: 0.1.3.0

Instances

Instances details
(Searchable p, Searchable q) => Decidable (Found (AndP p q) :: TyFun k1 Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate.Param

Methods

decide :: Decide (Found (AndP p q)) Source #

(Selectable p, Selectable q) => Provable (Found (AndP p q) :: TyFun k1 Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate.Param

Methods

prove :: Prove (Found (AndP p q)) Source #

type Apply (AndP p q x :: TyFun (k2, k3) Type -> Type) ('(y, z) :: (k2, k3)) Source # 
Instance details

Defined in Data.Type.Predicate.Param

type Apply (AndP p q x :: TyFun (k2, k3) Type -> Type) ('(y, z) :: (k2, k3)) = (p x @@ y, q x @@ z)