A type-level predicate in Haskell. We say that the predicate P :: Predicate k is true/satisfied by input 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 ~> Type 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.

There are two ways to define your own predicates:

1. 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.
2. 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 Wit p a is a value of type p @@ a --- that is, it is a proof or witness that p is satisfied for a.

It essentially turns a k ~> Type ("matchable" Predicate k) /back into/ a k -> Type predicate.

Convert a normal -> type constructor into a Predicate.

TyPred :: (k -> Type) -> Predicate k

The always-true predicate.

Evident :: Predicate k

EqualTo a is a predicate that the input is equal to a.

EqualTo :: k -> Predicate k

Convert a tradtional k ~> Bool predicate into a Predicate.

BoolPred :: (k ~> Bool) -> Predicate k

The always-false predicate

Could also be defined as ConstSym1 Void, but this defintion gives us a free Decidable instance.

Impossible :: Predicate k

In f as is a predicate that a given input a is a member of collection as.

Pre-compose a function to a predicate

PMap :: (k ~> j) -> Predicate j -> Predicate k

Not p is the predicate that p is not true.

Decide Not p based on decisions of p.

A proving function for predicate p; in some contexts, also called a "view function". See Provable for more information.

We say that p implies q (p --> q) if, given p a, we can always prove q @@ a.

This is implication -->#, but only in a specific context h.

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:

1. The proof functionview for every predicateview is available via the same name
2. We can write Provable instances for polymorphic predicate transformers (predicates parameterized on other predicates) easily, by refering to Provable instances of the transformed predicates.

Disprovable p is a constraint that p can be disproven.

The deciding/disproving function for Disprovable p.

Must be called by applying the Predicate to disprove:

disprove @p

If T :: k -> Type is a type constructor, then ProvableTC T is a constraint that T is "decidable", in that you have a canonical function:

proveTC :: Sing a -> T a

Is essentially Provable, except with type constructors k -> Type instead of matchable type-level functions (that are k ~> Type). Useful because 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

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

Implicatons p --> q can be lifted "through" a TFunctor into an f p --> f q.

Compose two implications.

A decision function for predicate p. See Decidable for more information.

Like implication -->, but knowing p @@ a can only let us decidably prove q a is true or false.

Like -?>, but only in a specific context h.

A typeclass for decidable predicates.

A predicate is decidable if, given any input a, you can either prove or disprove p @@ a. A Decision (p @@ a) is a data type that has a branch p @@ a and Refuted (p @@ a).

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

It confers two main advatnages:

1. The decision function for every predicate is available via the same name
2. We can write Decidable instances for polymorphic predicate transformers (predicates parameterized on other predicates) easily, by refering to Decidable instances of the transformed predicates.

If T :: k -> Type is a type constructor, then DecidableTC T is a constraint that T is "decidable", in that you have a canonical function:

decideTC :: Sing a -> Decision (T a)

Is essentially Decidable, except with type constructors k -> Type instead of matchable type-level functions (that are k ~> Type). Useful because 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

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

Implicatons p -?> q can be lifted "through" a DFunctor into an f p -?> f q.

A Decision about a type a is either a proof of existence or a proof that a cannot exist.

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

Map over the value inside a Decision.

Helper function for a common pattern of eliminating the disproved branch of Decision to certaintify the proof.

Since: 0.1.2.0

Converts a Decision to a Maybe. Drop the witness of disproof of a, returning Just if Proved (with the proof) and Nothing if Disproved.

Since: 0.1.1.0

Drop the witness of proof of a, returning Nothing if Proved and Just if Disproved (with the disproof).

Since: 0.1.1.0

Boolean test if a Decision is Proved.

Since: 0.1.1.0

Boolean test if a Decision is Disproved.

Since: 0.1.1.0

Change the target of a Refuted with a contravariant mapping function.

Since: 0.1.2.0