Data.Type.Predicate.Logic

Logical and algebraic connectives for predicates, as well as common logical combinators.

Top and bottom

type Evident = (TyPred Sing :: Predicate k)

The always-true predicate.

Evident :: 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.

Logical connectives

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)

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)

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.

data (&&&) :: Predicate k -> Predicate k -> Predicate k infixr 3

p &&& q is a predicate that both p and q are true.

Instances

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

Defined in Data.Type.Predicate.Logic

Methods

prove :: Prove (p &&& q)

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

Defined in Data.Type.Predicate.Logic

Methods

decide :: Decide (p &&& q)

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

Defined in Data.Type.Predicate.Logic

type Apply (p &&& q :: TyFun k1 Type -> *) (a :: k1) = (p @@ a, q @@ a)

decideAnd :: forall p q a. Decision (p @@ a) -> Decision (q @@ a) -> Decision ((p &&& q) @@ a)

Decide p &&& q based on decisions of p and q.

data (|||) :: Predicate k -> Predicate k -> Predicate k infixr 2

p ||| q is a predicate that either p and q are true.

Instances

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

Picks the proof of p. Note that this is instance has stronger constraints than is strictly necessary; we should really only have to require that either p or q is true.

Defined in Data.Type.Predicate.Logic

Methods

prove :: Prove (p ||| q)

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

Defined in Data.Type.Predicate.Logic

Methods

decide :: Decide (p ||| q)

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

Defined in Data.Type.Predicate.Logic

type Apply (p ||| q :: TyFun k1 Type -> *) (a :: k1) = Either (p @@ a) (q @@ a)

decideOr :: forall p q a. Decision (p @@ a) -> Decision (q @@ a) -> Decision ((p ||| q) @@ a)

Decide p ||| q based on decisions of p and q.

type (^||) p q = p ||| (Not p &&& q)

Left-biased "or". In proofs, prioritize a proof of the left side over a proof of the right side.

type (||^) p q = (p &&& Not q) ||| q

Right-biased "or". In proofs, prioritize a proof of the right side over a proof of the left side.

type (^^^) p q = (p &&& Not q) ||| (Not p &&& q)

p ^^^ q is a predicate that either p and q are true, but not both.

decideXor :: forall p q a. Decision (p @@ a) -> Decision (q @@ a) -> Decision ((p ^^^ q) @@ a)

Decide p ^^^ q based on decisions of p and q.

data (==>) :: Predicate k -> Predicate k -> Predicate k infixr 1

p ==> q is true if q is provably true under the condition that p is true.

Instances

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)

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

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

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

Defined in Data.Type.Predicate.Logic

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

proveImplies :: Prove q -> Prove (p ==> q)

If q is provable, then so is p ==> q.

This can be used as an easy plug-in Provable instance for p ==> q if q is Provable:

instance Provable (p ==> MyPred) where
    prove = proveImplies @MyPred

This instance isn't provided polymorphically because of overlapping instance issues.

type Implies p q = Provable (p ==> q)

Implies p q is a constraint that p ==> q is Provable; that is, you can prove that p implies q.

type (<==>) p q = p ==> ((q &&& q) ==> p) infixr 1

Two-way implication, or logical equivalence

type Equiv p q = Provable (p <==> q)

Equiv p q is a constraint that p <==> q is Provable; that is, you can prove that p is logically equivalent to q.

Logical deductions

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

Compose two implications.

explosion :: Impossible --> p

From Impossible a, you can prove anything. Essentially a lifted version of absurd.

atom :: p --> Evident

Evident can be proven from all predicates.

excludedMiddle :: (p &&& Not p) --> Impossible

We cannot have both p and Not p.

doubleNegation :: forall p. Decidable p => Not (Not p) --> p

Logical double negation. Only possible if p is Decidable.

contrapositive :: (p --> q) -> Not q --> Not p

If only this worked, but darn overlapping instances. Same for p ==> p ||| q and p &&& q ==> p :( q) ==> instance Provable (p &&& Not p ==> Impossible) where prove = excludedMiddle @p

If p implies q, then not q implies not p.

contrapositive' :: forall p q. Decidable q => (Not q --> Not p) -> p --> q

Reverse direction of contrapositive. Only possible if q is Decidable on its own, without the help of p, which makes this much less useful.

Lattice

projAndFst :: (p &&& q) --> p

If p &&& q is true, then so is p.

projAndSnd :: (p &&& q) --> q

If p &&& q is true, then so is q.

injOrLeft :: forall p q. p --> (p ||| q)

If p is true, then so is p ||| q.

injOrRight :: forall p q. q --> (p ||| q)

If q is true, then so is p ||| q.