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

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

(`.`

)

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

takes a parmaeterized predicate on `AnyMatch`

f`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

is a predicate taking an argument `AnyMatch`

f p as`a`

and
testing if `p a :: `

is satisfied for any item in `Predicate`

k```
as ::
f k
```

.

A

tests if a `ParamPred`

k v`k`

can create some `v`

. The resulting

tests if any `ParamPred`

(f k) v`k`

in `f k`

can create some `v`

.

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

p`p :: `

that tests a `ParamPred`

k v`k`

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 v`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

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

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 Selectable p = Provable (Found p) Source #

A constraint that a

s "selectable". It means that
for any input `ParamPred`

k v`x :: 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 v`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.