decidable-0.1.1.0: Combinators for manipulating dependently-typed predicates.

Data.Type.Predicate

Description

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

Synopsis

# Predicates

type Predicate k = k ~> Type Source #

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

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 FieldsgetWit :: p @@ a

## Construct Predicates

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

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

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


type Evident = (TyPred Sing :: Predicate k) Source #

The always-true predicate.

Evident :: Predicate k


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

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

type BoolPred (p :: k ~> Bool) = (EqualTo True .@#@$$p :: Predicate k) Source # Convert a tradtional k ~> Bool predicate into a Predicate. BoolPred :: (k ~> Bool) -> Predicate k  type Impossible = (Not Evident :: Predicate k) Source # 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) Source # Pre-compose a function to a predicate PMap :: (k ~> j) -> Predicate j -> Predicate k  data Not :: Predicate k -> Predicate k Source # Not p is the predicate that p is not true. Instances  Provable (Not (Impossible :: Predicate k1) :: TyFun k1 Type -> *) Source # Instance detailsDefined in Data.Type.Predicate Methods Decidable p => Decidable (Not p :: TyFun k1 Type -> *) Source # Instance detailsDefined in Data.Type.Predicate Methods Provable (p ==> q) => Provable (Not q ==> Not p :: TyFun k1 Type -> *) Source # Instance detailsDefined in Data.Type.Predicate.Logic Methods Provable ((Impossible :: Predicate k1) ==> p :: TyFun k1 Type -> *) Source # Instance detailsDefined in Data.Type.Predicate.Logic Methods (Decidable (p ==> q), Decidable q) => Decidable (Not q ==> Not p :: TyFun k1 Type -> *) Source # Instance detailsDefined in Data.Type.Predicate.Logic Methods Decidable ((Impossible :: Predicate k1) ==> p :: TyFun k1 Type -> *) Source # Instance detailsDefined in Data.Type.Predicate.Logic Methods type Apply (Not p :: TyFun k1 Type -> *) (a :: k1) Source # Instance detailsDefined 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) Source # Decide Not p based on decisions of p. # Provable Predicates type Prove p = forall a. Sing a -> p @@ a Source # A proving function for predicate p. 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 --> 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 Source # This is implication -->#, but only in a specific context h. class Provable p where Source # 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 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) Source # Instance detailsDefined in Data.Type.Predicate Methods Provable (Not (Impossible :: Predicate k1) :: TyFun k1 Type -> *) Source # Instance detailsDefined in Data.Type.Predicate Methods (Provable p, Provable q) => Provable (p &&& q :: TyFun k1 Type -> *) Source # Instance detailsDefined in Data.Type.Predicate.Logic Methodsprove :: Prove (p &&& q) Source # Provable (p ==> (p ||| p) :: TyFun k1 Type -> *) Source # Since: decidable-0.1.1.0 Instance detailsDefined in Data.Type.Predicate.Logic Methodsprove :: Prove (p ==> (p ||| p)) Source # Provable (q ==> (p ||| q) :: TyFun k1 Type -> *) Source # Since: decidable-0.1.1.0 Instance detailsDefined in Data.Type.Predicate.Logic Methodsprove :: Prove (q ==> (p ||| q)) Source # Provable (p ==> (p ||| q) :: TyFun k1 Type -> *) Source # Since: decidable-0.1.1.0 Instance detailsDefined in Data.Type.Predicate.Logic Methodsprove :: Prove (p ==> (p ||| q)) Source # Provable ((p &&& p) ==> p :: TyFun k1 Type -> *) Source # Since: decidable-0.1.1.0 Instance detailsDefined in Data.Type.Predicate.Logic Methodsprove :: Prove ((p &&& p) ==> p) Source # Provable ((p &&& q) ==> q :: TyFun k1 Type -> *) Source # Since: decidable-0.1.1.0 Instance detailsDefined in Data.Type.Predicate.Logic Methodsprove :: Prove ((p &&& q) ==> q) Source # Provable ((p &&& q) ==> p :: TyFun k1 Type -> *) Source # Since: decidable-0.1.1.0 Instance detailsDefined in Data.Type.Predicate.Logic Methodsprove :: Prove ((p &&& q) ==> p) Source # Provable (p ==> q) => Provable (Not q ==> Not p :: TyFun k1 Type -> *) Source # Instance detailsDefined in Data.Type.Predicate.Logic Methods Provable ((Impossible :: Predicate k1) ==> p :: TyFun k1 Type -> *) Source # Instance detailsDefined in Data.Type.Predicate.Logic Methods (Provable (Found p), SingI f) => Provable (Found (PPMap f p) :: TyFun k Type -> *) Source # Instance detailsDefined in Data.Type.Predicate.Param Methodsprove :: Prove (Found (PPMap f p)) Source # (Provable f, SingI g) => Provable (f .@#@$$g :: TyFun k1 * -> *) Source # Instance detailsDefined in Data.Type.Predicate Methodsprove :: Prove (f .@#@$$$ g) Source # (Universe f, Provable p) => Provable (All f p :: TyFun (f k) Type -> *) Source # Instance detailsDefined in Data.Type.Universe Methodsprove :: Prove (All f p) Source # Provable p => Provable ((NotNull f :: Predicate (f k)) ==> Any f p :: TyFun (f k) Type -> *) Source # Instance detailsDefined in Data.Type.Universe Methodsprove :: Prove (NotNull f ==> Any f p) Source # Provable (Found (InP f :: ParamPred (f v) v) ==> (NotNull f :: Predicate (f v)) :: TyFun (f v) Type -> *) Source # Instance detailsDefined in Data.Type.Predicate.Param Methods Provable ((NotNull f :: Predicate (f k)) ==> Found (InP f :: ParamPred (f k) k) :: TyFun (f k) Type -> *) Source # Instance detailsDefined in Data.Type.Predicate.Param Methods (Universe f, Decidable p) => Provable (Subset f p :: TyFun (f k) Type -> *) Source # Instance detailsDefined in Data.Type.Universe.Subset Methodsprove :: Prove (Subset f p) Source #

type Disprovable p = Provable (Not p) Source #

Disprovable p is a constraint that 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 -> 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 Source #

The canonical proving function for DecidableTC t.

Since: decidable-0.1.1.0

class TFunctor f where Source #

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

Instances
 Universe f => TFunctor (All f :: (k1 ~> Type) -> TyFun (f k1) Type -> *) Source # Instance detailsDefined in Data.Type.Universe Methodstmap :: (p --> q) -> All f p --> All f q Source # Universe f => TFunctor (Any f :: (k1 ~> Type) -> TyFun (f k1) Type -> *) Source # Instance detailsDefined in Data.Type.Universe Methodstmap :: (p --> q) -> Any f p --> Any f q Source #

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

Compose two implications.

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

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

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

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
 Source # Instance detailsDefined in Data.Type.Predicate Methods (SDecide k, SingI a) => Decidable (EqualTo a :: Predicate k) Source # Instance detailsDefined in Data.Type.Predicate Methods Decidable p => Decidable (Not p :: TyFun k1 Type -> *) Source # Instance detailsDefined in Data.Type.Predicate Methods (SingI as, SDecide k) => Decidable (TyPred (Snd as) :: Predicate k) Source # Instance detailsDefined in Data.Type.Universe Methodsdecide :: Decide (TyPred (Snd as)) Source # (SingI as, SDecide k) => Decidable (TyPred (NEIndex as) :: Predicate k) Source # Instance detailsDefined in Data.Type.Universe Methodsdecide :: Decide (TyPred (NEIndex as)) Source # (SingI as, SDecide k) => Decidable (TyPred (IsRight as) :: Predicate k) Source # Instance detailsDefined in Data.Type.Universe Methodsdecide :: Decide (TyPred (IsRight as)) Source # (SingI as, SDecide k) => Decidable (TyPred (IsJust as) :: Predicate k) Source # Instance detailsDefined in Data.Type.Universe Methodsdecide :: Decide (TyPred (IsJust as)) Source # (SingI as, SDecide k) => Decidable (TyPred (Index as) :: Predicate k) Source # Instance detailsDefined in Data.Type.Universe Methodsdecide :: Decide (TyPred (Index as)) Source # (Decidable p, Decidable q) => Decidable (p &&& q :: TyFun k1 Type -> *) Source # Instance detailsDefined in Data.Type.Predicate.Logic Methodsdecide :: Decide (p &&& q) Source # (Decidable p, Decidable q) => Decidable (p ||| q :: TyFun k1 Type -> *) Source # Instance detailsDefined in Data.Type.Predicate.Logic Methodsdecide :: Decide (p ||| q) Source # Decidable (p ==> (p ||| p) :: TyFun k1 Type -> *) Source # Since: decidable-0.1.1.0 Instance detailsDefined in Data.Type.Predicate.Logic Methodsdecide :: Decide (p ==> (p ||| p)) Source # Decidable (q ==> (p ||| q) :: TyFun k1 Type -> *) Source # Since: decidable-0.1.1.0 Instance detailsDefined in Data.Type.Predicate.Logic Methodsdecide :: Decide (q ==> (p ||| q)) Source # Decidable (p ==> (p ||| q) :: TyFun k1 Type -> *) Source # Since: decidable-0.1.1.0 Instance detailsDefined in Data.Type.Predicate.Logic Methodsdecide :: Decide (p ==> (p ||| q)) Source # Decidable ((p &&& p) ==> p :: TyFun k1 Type -> *) Source # Since: decidable-0.1.1.0 Instance detailsDefined in Data.Type.Predicate.Logic Methodsdecide :: Decide ((p &&& p) ==> p) Source # Decidable ((p &&& q) ==> q :: TyFun k1 Type -> *) Source # Since: decidable-0.1.1.0 Instance detailsDefined in Data.Type.Predicate.Logic Methodsdecide :: Decide ((p &&& q) ==> q) Source # Decidable ((p &&& q) ==> p :: TyFun k1 Type -> *) Source # Since: decidable-0.1.1.0 Instance detailsDefined in Data.Type.Predicate.Logic Methodsdecide :: Decide ((p &&& q) ==> p) Source # (Decidable (p ==> q), Decidable q) => Decidable (Not q ==> Not p :: TyFun k1 Type -> *) Source # Instance detailsDefined in Data.Type.Predicate.Logic Methods Decidable ((Impossible :: Predicate k1) ==> p :: TyFun k1 Type -> *) Source # Instance detailsDefined in Data.Type.Predicate.Logic Methods (Decidable (Found p), SingI f) => Decidable (Found (PPMap f p) :: TyFun k Type -> *) Source # Instance detailsDefined in Data.Type.Predicate.Param Methodsdecide :: Decide (Found (PPMap f p)) Source # (Decidable f, SingI g) => Decidable (f .@#@\$ g :: TyFun k1 * -> *) Source # Instance detailsDefined in Data.Type.Predicate Methods (Universe f, Provable p) => Decidable ((NotNull f :: Predicate (f k)) ==> Any f p :: TyFun (f k) Type -> *) Source # Instance detailsDefined in Data.Type.Universe Methodsdecide :: Decide (NotNull f ==> Any f p) Source # (Universe f, Decidable p) => Decidable (All f p :: TyFun (f k) Type -> *) Source # Instance detailsDefined in Data.Type.Universe Methodsdecide :: Decide (All f p) Source # (Universe f, Decidable p) => Decidable (Any f p :: TyFun (f k) Type -> *) Source # Instance detailsDefined in Data.Type.Universe Methodsdecide :: Decide (Any f p) Source # (Universe f, Decidable (Found p)) => Decidable (Found (AnyMatch f p) :: TyFun (f k) Type -> *) Source # Instance detailsDefined in Data.Type.Predicate.Param Methodsdecide :: Decide (Found (AnyMatch f p)) Source # Decidable (Found (InP f :: ParamPred (f v) v) ==> (NotNull f :: Predicate (f v)) :: TyFun (f v) Type -> *) Source # Instance detailsDefined in Data.Type.Predicate.Param Methods Decidable ((NotNull f :: Predicate (f k)) ==> Found (InP f :: ParamPred (f k) k) :: TyFun (f k) Type -> *) Source # Instance detailsDefined in Data.Type.Predicate.Param Methods Universe f => Decidable (Found (InP f :: ParamPred (f v) v) :: TyFun (f v) Type -> *) Source # Instance detailsDefined in Data.Type.Predicate.Param Methodsdecide :: Decide (Found (InP f)) Source # (Universe f, Decidable p) => Decidable (Subset f p :: TyFun (f k) Type -> *) Source # Instance detailsDefined in Data.Type.Universe.Subset Methodsdecide :: Decide (Subset f p) Source #

type DecidableTC p = Decidable (TyPred p) Source #

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

The canonical deciding function for DecidableTC t.

Since: decidable-0.1.1.0

class DFunctor f where Source #

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

Instances
 Universe f => DFunctor (All f :: (k1 ~> Type) -> TyFun (f k1) Type -> *) Source # Instance detailsDefined in Data.Type.Universe Methodsdmap :: (p -?> q) -> All f p -?> All f q Source #

# 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

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

Map over the value inside a Decision.

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

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

Since: decidable-0.1.1.0

Boolean test if a Decision is Proved.

Since: decidable-0.1.1.0

Boolean test if a Decision is Disproved.

Since: decidable-0.1.1.0