Data.Type.Predicate

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

Predicates

type Predicate k = k ~> Type

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)

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.

newtype Wit p a

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.

Constructors

Wit

Fields

• getWit :: p @@ a

Construct Predicates

type TyPred = (TyCon1 :: (k -> Type) -> Predicate k)

Convert a normal '->' type constructor into a Predicate.

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

type Evident = (TyPred Sing :: Predicate k)

The always-true predicate.

Evident :: Predicate k

type EqualTo (a :: k) = (TyPred ((:~:) a) :: Predicate k)

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

type BoolPred (p :: k ~> Bool) = (EqualTo True .@#@$$$ p :: Predicate k)

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

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

type Impossible = (Not Evident :: Predicate k)

The always-false predicate

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

Manipulate predicates

type PMap (f :: k ~> j) (p :: Predicate j) = (p .@#@$$$ f :: Predicate k)

Pre-compose a function to a predicate

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

data Not :: Predicate k -> Predicate k

Not p is the predicate that p is not true.

Instances

Provable (Not (Impossible :: Predicate k1) :: TyFun k1 Type -> *)

Defined in Data.Type.Predicate

Methods

prove :: Prove (Not Impossible)

Decidable p => Decidable (Not p :: TyFun k1 Type -> *)

Defined in Data.Type.Predicate

Methods

decide :: Decide (Not p)

SingI a => Auto (Not (Impossible :: Predicate k) :: TyFun k Type -> *) (a :: k)

Since: decidable-0.1.2.0

Defined in Data.Type.Predicate.Auto

Methods

auto :: Not Impossible @@ a

AutoNot p (f @@ a) => Auto (Not (PMap f p) :: TyFun k Type -> *) (a :: k)

Since: decidable-0.1.2.0

Defined in Data.Type.Predicate.Auto

Methods

auto :: Not (PMap f p) @@ a

Provable (p ==> q) => Provable (Not q ==> Not p :: TyFun k1 Type -> *)

Defined in Data.Type.Predicate.Logic

Methods

prove :: Prove (Not q ==> Not p)

Provable ((Impossible :: Predicate k1) ==> p :: TyFun k1 Type -> *)

Defined in Data.Type.Predicate.Logic

Methods

prove :: Prove (Impossible ==> p)

(Decidable (p ==> q), Decidable q) => Decidable (Not q ==> Not p :: TyFun k1 Type -> *)

Defined in Data.Type.Predicate.Logic

Methods

decide :: Decide (Not q ==> Not p)

Decidable ((Impossible :: Predicate k1) ==> p :: TyFun k1 Type -> *)

Defined in Data.Type.Predicate.Logic

Methods

decide :: Decide (Impossible ==> p)

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

Since: decidable-0.1.2.0

Defined in Data.Type.Predicate.Auto

Methods

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

(SingI as, AutoAll f (Not (Found p)) as) => Auto (Not (Found (AnyMatch f p)) :: TyFun (f k) Type -> *) (as :: f k)

Since: decidable-0.1.2.0

Defined in Data.Type.Predicate.Auto

Methods

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

(SingI as, AutoAll f (Not p) as) => Auto (Not (Any f p) :: TyFun (f k) Type -> *) (as :: f k)

Since: decidable-0.1.2.0

Defined in Data.Type.Predicate.Auto

Methods

auto :: Not (Any f p) @@ as

type Apply (Not p :: TyFun k1 Type -> *) (a :: k1)

Defined in Data.Type.Predicate

type Apply (Not p :: TyFun k1 Type -> *) (a :: k1) = Refuted (p @@ a)

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

Decide Not p based on decisions of p.

Provable Predicates

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

A proving function for predicate p. See Provable for more information.

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

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

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

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

class Provable p where

A typeclass for provable predicates (constructivist tautologies).

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".

This typeclass associates a canonical proof function for every provable predicate.

It confers two main advatnages:

1. The proof function for every predicate 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.

Minimal complete definition

prove

Methods

prove :: Prove p

The canonical proving function for predicate 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

Instances

Provable (Evident :: Predicate k1)

Defined in Data.Type.Predicate

Methods

prove :: Prove Evident

Provable (Not (Impossible :: Predicate k1) :: TyFun k1 Type -> *)

Defined in Data.Type.Predicate

Methods

prove :: Prove (Not Impossible)

(Provable p, Provable q) => Provable (p &&& q :: TyFun k1 Type -> *)

Defined in Data.Type.Predicate.Logic

Methods

prove :: Prove (p &&& q)

Provable (p ==> (p ||| p) :: TyFun k1 Type -> *)

Since: decidable-0.1.1.0

Defined in Data.Type.Predicate.Logic

Methods

prove :: Prove (p ==> (p ||| p))

Provable (q ==> (p ||| q) :: TyFun k1 Type -> *)

Since: decidable-0.1.1.0

Defined in Data.Type.Predicate.Logic

Methods

prove :: Prove (q ==> (p ||| q))

Provable (p ==> (p ||| q) :: TyFun k1 Type -> *)

Since: decidable-0.1.1.0

Defined in Data.Type.Predicate.Logic

Methods

prove :: Prove (p ==> (p ||| q))

Provable ((p &&& p) ==> p :: TyFun k1 Type -> *)

Since: decidable-0.1.1.0

Defined in Data.Type.Predicate.Logic

Methods

prove :: Prove ((p &&& p) ==> p)

Provable ((p &&& q) ==> q :: TyFun k1 Type -> *)

Since: decidable-0.1.1.0

Defined in Data.Type.Predicate.Logic

Methods

prove :: Prove ((p &&& q) ==> q)

Provable ((p &&& q) ==> p :: TyFun k1 Type -> *)

Since: decidable-0.1.1.0

Defined in Data.Type.Predicate.Logic

Methods

prove :: Prove ((p &&& q) ==> p)

Provable (p ==> q) => Provable (Not q ==> Not p :: TyFun k1 Type -> *)

Defined in Data.Type.Predicate.Logic

Methods

prove :: Prove (Not q ==> Not p)

Provable ((Impossible :: Predicate k1) ==> p :: TyFun k1 Type -> *)

Defined in Data.Type.Predicate.Logic

Methods

prove :: Prove (Impossible ==> p)

(Provable (Found p), SingI f) => Provable (Found (PPMap f p) :: TyFun k Type -> *)

Defined in Data.Type.Predicate.Param

Methods

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

(Provable p, SingI f) => Provable (PMap f p :: Predicate k1)

Defined in Data.Type.Predicate

Methods

prove :: Prove (PMap f p)

(Universe f, Provable p) => Provable (All f p :: TyFun (f k) Type -> *)

Defined in Data.Type.Universe

Methods

prove :: Prove (All f p)

Provable p => Provable ((NotNull f :: Predicate (f k)) ==> Any f p :: TyFun (f k) Type -> *)

Defined in Data.Type.Universe

Methods

prove :: Prove (NotNull f ==> Any f p)

Provable (Found (InP f :: ParamPred (f v) v) ==> (NotNull f :: Predicate (f v)) :: TyFun (f v) Type -> *)

Defined in Data.Type.Predicate.Param

Methods

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

Provable ((NotNull f :: Predicate (f k)) ==> Found (InP f :: ParamPred (f k) k) :: TyFun (f k) Type -> *)

Defined in Data.Type.Predicate.Param

Methods

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

(Universe f, Decidable p) => Provable (Subset f p :: TyFun (f k) Type -> *)

Defined in Data.Type.Universe.Subset

Methods

prove :: Prove (Subset f p)

type Disprovable p = Provable (Not p)

Disprovable p is a constraint that p can be disproven.

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

The deciding/disproving function for Disprovable p.

Must be called by applying the Predicate to disprove:

disprove @p

type ProvableTC p = Provable (TyPred 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).

Since: decidable-0.1.1.0

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

The canonical proving function for DecidableTC t.

Since: decidable-0.1.1.0

class TFunctor f where

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

Minimal complete definition

tmap

Methods

tmap :: forall p q. (p --> q) -> f p --> f q

Instances

Universe f => TFunctor (All f :: (k1 ~> Type) -> TyFun (f k1) Type -> *)

Defined in Data.Type.Universe

Methods

tmap :: (p --> q) -> All f p --> All f q

Universe f => TFunctor (Any f :: (k1 ~> Type) -> TyFun (f k1) Type -> *)

Defined in Data.Type.Universe

Methods

tmap :: (p --> q) -> Any f p --> Any f q

compImpl :: forall p q r. (p --> q) -> (q --> r) -> p --> r

Compose two implications.

Decidable Predicates

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

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

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

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

class Decidable p where

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.

Methods

decide :: Decide p

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

decide :: Provable p => Decide p

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

Instances

Decidable (Evident :: Predicate k1)

Defined in Data.Type.Predicate

Methods

decide :: Decide Evident

(SDecide k, SingI a) => Decidable (EqualTo a :: Predicate k)

Defined in Data.Type.Predicate

Methods

decide :: Decide (EqualTo a)

Decidable p => Decidable (Not p :: TyFun k1 Type -> *)

Defined in Data.Type.Predicate

Methods

decide :: Decide (Not p)

(SingI as, SDecide k) => Decidable (TyPred (ISnd as) :: Predicate k)

Defined in Data.Type.Universe

Methods

decide :: Decide (TyPred (ISnd as))

(SingI as, SDecide k) => Decidable (TyPred (NEIndex as) :: Predicate k)

Defined in Data.Type.Universe

Methods

decide :: Decide (TyPred (NEIndex as))

(SingI as, SDecide k) => Decidable (TyPred (IRight as) :: Predicate k)

Defined in Data.Type.Universe

Methods

decide :: Decide (TyPred (IRight as))

(SingI as, SDecide k) => Decidable (TyPred (IJust as) :: Predicate k)

Defined in Data.Type.Universe

Methods

decide :: Decide (TyPred (IJust as))

(SingI as, SDecide k) => Decidable (TyPred (Index as) :: Predicate k)

Defined in Data.Type.Universe

Methods

decide :: Decide (TyPred (Index as))

(Decidable p, Decidable q) => Decidable (p &&& q :: TyFun k1 Type -> *)

Defined in Data.Type.Predicate.Logic

Methods

decide :: Decide (p &&& q)

(Decidable p, Decidable q) => Decidable (p ||| q :: TyFun k1 Type -> *)

Defined in Data.Type.Predicate.Logic

Methods

decide :: Decide (p ||| q)

Decidable (p ==> (p ||| p) :: TyFun k1 Type -> *)

Since: decidable-0.1.1.0

Defined in Data.Type.Predicate.Logic

Methods

decide :: Decide (p ==> (p ||| p))

Decidable (q ==> (p ||| q) :: TyFun k1 Type -> *)

Since: decidable-0.1.1.0

Defined in Data.Type.Predicate.Logic

Methods

decide :: Decide (q ==> (p ||| q))

Decidable (p ==> (p ||| q) :: TyFun k1 Type -> *)

Since: decidable-0.1.1.0

Defined in Data.Type.Predicate.Logic

Methods

decide :: Decide (p ==> (p ||| q))

Decidable ((p &&& p) ==> p :: TyFun k1 Type -> *)

Since: decidable-0.1.1.0

Defined in Data.Type.Predicate.Logic

Methods

decide :: Decide ((p &&& p) ==> p)

Decidable ((p &&& q) ==> q :: TyFun k1 Type -> *)

Since: decidable-0.1.1.0

Defined in Data.Type.Predicate.Logic

Methods

decide :: Decide ((p &&& q) ==> q)

Decidable ((p &&& q) ==> p :: TyFun k1 Type -> *)

Since: decidable-0.1.1.0

Defined in Data.Type.Predicate.Logic

Methods

decide :: Decide ((p &&& q) ==> p)

(Decidable (p ==> q), Decidable q) => Decidable (Not q ==> Not p :: TyFun k1 Type -> *)

Defined in Data.Type.Predicate.Logic

Methods

decide :: Decide (Not q ==> Not p)

Decidable ((Impossible :: Predicate k1) ==> p :: TyFun k1 Type -> *)

Defined in Data.Type.Predicate.Logic

Methods

decide :: Decide (Impossible ==> p)

(Decidable (Found p), SingI f) => Decidable (Found (PPMap f p) :: TyFun k Type -> *)

Defined in Data.Type.Predicate.Param

Methods

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

(Decidable p, SingI f) => Decidable (PMap f p :: Predicate k1)

Defined in Data.Type.Predicate

Methods

decide :: Decide (PMap f p)

(Universe f, Provable p) => Decidable ((NotNull f :: Predicate (f k)) ==> Any f p :: TyFun (f k) Type -> *)

Defined in Data.Type.Universe

Methods

decide :: Decide (NotNull f ==> Any f p)

(Universe f, Decidable p) => Decidable (All f p :: TyFun (f k) Type -> *)

Defined in Data.Type.Universe

Methods

decide :: Decide (All f p)

(Universe f, Decidable p) => Decidable (Any f p :: TyFun (f k) Type -> *)

Defined in Data.Type.Universe

Methods

decide :: Decide (Any f p)

(Universe f, Decidable (Found p)) => Decidable (Found (AnyMatch f p) :: TyFun (f k) Type -> *)

Defined in Data.Type.Predicate.Param

Methods

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

Decidable (Found (InP f :: ParamPred (f v) v) ==> (NotNull f :: Predicate (f v)) :: TyFun (f v) Type -> *)

Defined in Data.Type.Predicate.Param

Methods

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

Decidable ((NotNull f :: Predicate (f k)) ==> Found (InP f :: ParamPred (f k) k) :: TyFun (f k) Type -> *)

Defined in Data.Type.Predicate.Param

Methods

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

Universe f => Decidable (Found (InP f :: ParamPred (f v) v) :: TyFun (f v) Type -> *)

Defined in Data.Type.Predicate.Param

Methods

decide :: Decide (Found (InP f))

(Universe f, Decidable p) => Decidable (Subset f p :: TyFun (f k) Type -> *)

Defined in Data.Type.Universe.Subset

Methods

decide :: Decide (Subset f p)

type DecidableTC p = Decidable (TyPred p)

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

Since: decidable-0.1.1.0

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

The canonical deciding function for DecidableTC t.

Since: decidable-0.1.1.0

class DFunctor f where

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

Minimal complete definition

dmap

Methods

dmap :: forall p q. (p -?> q) -> f p -?> f q

Instances

Universe f => DFunctor (All f :: (k1 ~> Type) -> TyFun (f k1) Type -> *)

Defined in Data.Type.Universe

Methods

dmap :: (p -?> q) -> All f p -?> All f q

Manipulate Decisions

data Decision a

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

Constructors

Proved a

Witness for a

Disproved (Refuted a)

Proof that no a exists

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

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 Haskell. See doubleNegation for a situation where it is.

Since: decidable-0.1.1.0

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

Map over the value inside a Decision.

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

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

Since: decidable-0.1.2.0

forgetDisproof :: Decision a -> Maybe a

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: decidable-0.1.1.0

forgetProof :: Decision a -> Maybe (Refuted a)

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

Since: decidable-0.1.1.0

isProved :: Decision a -> Bool

Boolean test if a Decision is Proved.

Since: decidable-0.1.1.0

isDisproved :: Decision a -> Bool

Boolean test if a Decision is Disproved.

Since: decidable-0.1.1.0

mapRefuted :: (a -> b) -> Refuted b -> Refuted a

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

Since: decidable-0.1.2.0