Copyright | (c) Justin Le 2018 |
---|---|

License | BSD3 |

Maintainer | justin@jle.im |

Stability | experimental |

Portability | non-portable |

Safe Haskell | None |

Language | Haskell2010 |

Combinators for working with type-level predicates, along with typeclasses for canonical proofs and deciding functions.

## Synopsis

- type Predicate k = k ~> Type
- newtype Wit p a = Wit {}
- type TyPred = TyCon1 :: (k -> Type) -> Predicate k
- data Evident :: Predicate k
- type EqualTo (a :: k) = TyPred ((:~:) a) :: Predicate k
- type BoolPred (p :: k ~> Bool) = PMap p (EqualTo 'True) :: Predicate k
- type Impossible = Not Evident :: Predicate k
- type In (f :: Type -> Type) (as :: f k) = ElemSym1 f as
- type PMap (f :: k ~> j) (p :: Predicate j) = p .@#@$$$ f :: Predicate k
- data Not :: Predicate k -> Predicate k
- decideNot :: forall p a. Decision (p @@ a) -> Decision (Not p @@ a)
- type Prove p = forall a. Sing a -> p @@ a
- type (-->) p q = forall a. Sing a -> (p @@ a) -> q @@ a
- type (-->#) p q h = forall a. Sing a -> (p @@ a) -> h (q @@ a)
- class Provable p where
- type Disprovable p = Provable (Not p)
- disprove :: forall p. Disprovable p => Prove (Not p)
- type ProvableTC p = Provable (TyPred p)
- proveTC :: forall t a. ProvableTC t => Sing a -> t a
- class TFunctor f where
- compImpl :: forall p q r. (p --> q) -> (q --> r) -> p --> r
- type Decide p = forall a. Sing a -> Decision (p @@ a)
- type (-?>) p q = forall a. Sing a -> (p @@ a) -> Decision (q @@ a)
- type (-?>#) p q h = forall a. Sing a -> (p @@ a) -> h (Decision (q @@ a))
- class Decidable p where
- type DecidableTC p = Decidable (TyPred p)
- decideTC :: forall t a. DecidableTC t => Sing a -> Decision (t a)
- class DFunctor f where
- data Decision a
- flipDecision :: Decision a -> Decision (Refuted a)
- mapDecision :: (a -> b) -> (b -> a) -> Decision a -> Decision b
- elimDisproof :: Decision a -> Refuted (Refuted a) -> a
- forgetDisproof :: Decision a -> Maybe a
- forgetProof :: Decision a -> Maybe (Refuted a)
- isProved :: Decision a -> Bool
- isDisproved :: Decision a -> Bool
- mapRefuted :: (a -> b) -> Refuted b -> Refuted a

# Predicates

type Predicate k = k ~> Type Source #

A type-level predicate in Haskell. We say that the predicate ```
P ::
```

is true/satisfied by input `Predicate`

k`x :: k`

if there exists
a value of type `P @@ x`

, and that it false/disproved if such a value
cannot exist. (Where `@@`

is `Apply`

, the singleton library's type-level
function application for mathcable functions). In some contexts, this
is also known as a dependently typed "view".

See `Provable`

and `Decidable`

for more information on how to use, prove
and decide these predicates.

The kind `k ~> `

is the kind of "matchable" type-level functions
in Haskell. They are type-level functions that are encoded as dummy
type constructors ("defunctionalization symbols") that can be decidedly
"matched" on for things like typeclass instances.`Type`

There are two ways to define your own predicates:

- Using the predicate combinators and predicate transformers in
this library and the
*singletons*library, which let you construct pre-made predicates and sometimes create predicates from other predicates. - Manually creating a data type that acts as a matchable predicate.

For an example of the latter, we can create the "not p" predicate, which
takes a predicate `p`

as input and returns the negation of the
predicate:

-- First, create the data type with the kind signature you want data Not :: Predicate k -> Predicate k -- Then, write the`Apply`

instance, to specify the type of the -- witnesses of that predicate instance`Apply`

(Not p) a = (p`@@`

a) ->`Void`

See the source of Data.Type.Predicate and Data.Type.Predicate.Logic
for simple examples of hand-made predicates. For example, we have the
always-true predicate `Evident`

:

data Evident ::`Predicate`

k instance Apply Evident a =`Sing`

a

And the "and" predicate combinator:

data (&&&) :: Predicate k -> Predicate k -> Predicate k instance Apply (p &&& q) a = (p`@@`

a, q`@@`

a)

Typically it is recommended to create predicates from the supplied
predicate combinators (`TyPred`

can be used for any type constructor to
turn it into a predicate, for instance) whenever possible.

A

is a value of type `Wit`

p a`p @@ a`

--- that is, it is a proof
or witness that `p`

is satisfied for `a`

.

It essentially turns a `k ~> `

("matchable" `Type`

) /back
into/ a `Predicate`

k`k -> `

predicate.`Type`

#### Instances

## Construct Predicates

data Evident :: Predicate k Source #

#### Instances

type Impossible = Not Evident :: Predicate k Source #

The always-false predicate

Could also be defined as

, but this defintion gives
us a free `ConstSym1`

Void`Decidable`

instance.

`Impossible`

::`Predicate`

k

type In (f :: Type -> Type) (as :: f k) = ElemSym1 f as Source #

is a predicate that a given input `In`

f as`a`

is a member of
collection `as`

.

## Manipulate predicates

data Not :: Predicate k -> Predicate k Source #

is the predicate that `Not`

p`p`

is not true.

#### Instances

decideNot :: forall p a. Decision (p @@ a) -> Decision (Not p @@ a) Source #

Decide

based on decisions of `Not`

p`p`

.

# Provable Predicates

type Prove p = forall a. Sing a -> p @@ a Source #

A proving function for predicate `p`

; in some contexts, also called
a "view function". See `Provable`

for more information.

type (-->) p q = forall a. Sing a -> (p @@ a) -> q @@ a infixr 1 Source #

We say that `p`

implies `q`

(`p `

) if, given `-->`

q`p `

` a`

, we can
always prove `q @@ a`

.

type (-->#) p q h = forall a. Sing a -> (p @@ a) -> h (q @@ a) infixr 1 Source #

This is implication `-->#`

, but only in a specific context `h`

.

class Provable p where Source #

A typeclass for provable predicates (constructivist tautologies). In some context, these are also known as "views".

A predicate is provable if, given any input `a`

, you can generate
a proof of `p @@ a`

. Essentially, it means that a predicate is "always
true".

We can call a type a view if, for any input `a`

, there is *some*
constructor of `p @@ a`

that can we can use to "categorize" `a`

.

This typeclass associates a canonical proof function for every provable predicate, or a canonical view function for any view.

It confers two main advatnages:

The canonical proving function for predicate `p`

(or a canonical
view function for view `p`

).

Note that `prove`

is ambiguously typed, so you *always* need to call
by specifying the predicate you want to prove using TypeApplications
syntax:

`prove`

@MyPredicate

See `proveTC`

and `ProvableTC`

for a version that isn't ambiguously
typed, but only works when `p`

is a type constructor.

#### Instances

type Disprovable p = Provable (Not p) Source #

is a constraint that `Disprovable`

p`p`

can be disproven.

disprove :: forall p. Disprovable p => Prove (Not p) Source #

The deciding/disproving function for

.`Disprovable`

p

Must be called by applying the `Predicate`

to disprove:

`disprove`

@p

type ProvableTC p = Provable (TyPred p) Source #

If `T :: k -> `

is a type constructor, then `Type`

is
a constraint that `ProvableTC`

T`T`

is "decidable", in that you have a canonical
function:

`proveTC`

::`Sing`

a -> T a

Is essentially `Provable`

, except with *type constructors* `k -> `

instead of matchable type-level functions (that are `Type`

`k ~> `

).
Useful because `Type`

`proveTC`

doesn't require anything fancy like
TypeApplications to use.

Also is in this library for compatiblity with "traditional" predicates that are GADT type constructors.

*Since: 0.1.1.0*

proveTC :: forall t a. ProvableTC t => Sing a -> t a Source #

The canonical proving function for

.`DecidableTC`

t

Note that because `t`

must be an injective type constructor, you can use
this without explicit type applications; the instance of `ProvableTC`

can be inferred from the result type.

*Since: 0.1.1.0*

# Decidable Predicates

type Decide p = forall a. Sing a -> Decision (p @@ a) Source #

A decision function for predicate `p`

. See `Decidable`

for more
information.

type (-?>) p q = forall a. Sing a -> (p @@ a) -> Decision (q @@ a) infixr 1 Source #

Like implication `-->`

, but knowing `p @@ a`

can only let us decidably
prove `q `

` a`

is true or false.

type (-?>#) p q h = forall a. Sing a -> (p @@ a) -> h (Decision (q @@ a)) infixr 1 Source #

Like `-?>`

, but only in a specific context `h`

.

class Decidable p where Source #

A typeclass for decidable predicates.

A predicate is decidable if, given any input `a`

, you can either prove
or disprove `p @@ a`

. A

is a data type
that has a branch `Decision`

(p @@ a)`p @@ a`

and

.`Refuted`

(p @@ a)

This typeclass associates a canonical decision function for every decidable predicate.

It confers two main advatnages:

Nothing

The canonical decision function for predicate `p`

.

Note that `decide`

is ambiguously typed, so you *always* need to call by
specifying the predicate you want to prove using TypeApplications
syntax:

`decide`

@MyPredicate

See `decideTC`

and `DecidableTC`

for a version that isn't ambiguously
typed, but only works when `p`

is a type constructor.

#### Instances

type DecidableTC p = Decidable (TyPred p) Source #

If `T :: k -> `

is a type constructor, then `Type`

is
a constraint that `DecidableTC`

T`T`

is "decidable", in that you have a canonical
function:

`decideTC`

::`Sing`

a ->`Decision`

(T a)

Is essentially `Decidable`

, except with *type constructors* ```
k ->
```

instead of matchable type-level functions (that are `Type`

```
k ~>
```

). Useful because `Type`

`decideTC`

doesn't require anything fancy like
TypeApplications to use.

Also is in this library for compatiblity with "traditional" predicates that are GADT type constructors.

*Since: 0.1.1.0*

decideTC :: forall t a. DecidableTC t => Sing a -> Decision (t a) Source #

The canonical deciding function for

.`DecidableTC`

t

Note that because `t`

must be an injective type constructor, you can use
this without explicit type applications; the instance of `DecidableTC`

can be inferred from the result type.

*Since: 0.1.1.0*

# Manipulate Decisions

A `Decision`

about a type `a`

is either a proof of existence or a proof that `a`

cannot exist.

flipDecision :: Decision a -> Decision (Refuted a) Source #

Flip the contents of a decision. Turn a proof of `a`

into a disproof
of not-`a`

.

Note that this is not reversible in general in constructivist logic See
`doubleNegation`

for a situation where it is.

*Since: 0.1.1.0*

mapDecision :: (a -> b) -> (b -> a) -> Decision a -> Decision b Source #

Map over the value inside a `Decision`

.

elimDisproof :: Decision a -> Refuted (Refuted a) -> a Source #

Helper function for a common pattern of eliminating the disproved
branch of `Decision`

to certaintify the proof.

*Since: 0.1.2.0*

forgetDisproof :: Decision a -> Maybe a Source #