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.

Impossible :: Predicate k

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

Defined in Data.Type.Predicate

Methods

prove :: Prove (Not Impossible)

Provable (Not (TyPred (IProxy (Proxy :: Proxy k1))) :: TyFun k1 Type -> Type)

Defined in Data.Type.Universe

Methods

prove :: Prove (Not (TyPred (IProxy Proxy0)))

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

Defined in Data.Type.Predicate

Methods

decide :: Decide (Not p)

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

Since: 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 -> Type) (a :: k)

Since: 0.1.2.0

Defined in Data.Type.Predicate.Auto

Methods

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

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

Since: 0.1.3.0

Defined in Data.Type.Predicate.Logic

Methods

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

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

Defined in Data.Type.Predicate.Logic

Methods

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

Provable ((Impossible :: Predicate k1) ==> p :: TyFun k1 Type -> 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 -> Type)

Defined in Data.Type.Predicate.Logic

Methods

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

Decidable ((Impossible :: Predicate k1) ==> p :: TyFun k1 Type -> 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: 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 -> Type) (as :: f k)

Since: 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 -> Type) (as :: f k)

Since: 0.1.2.0

Defined in Data.Type.Predicate.Auto

Methods

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

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

Defined in Data.Type.Predicate

type Apply (Not p :: TyFun k1 Type -> 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 -> Type)

Defined in Data.Type.Predicate.Logic

Methods

prove :: Prove (p &&& q)

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

Since: 0.1.3.0

Defined in Data.Type.Predicate.Logic

Methods

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

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

Since: 0.1.1.0

Defined in Data.Type.Predicate.Logic

Methods

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

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

Since: 0.1.1.0

Defined in Data.Type.Predicate.Logic

Methods

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

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

Since: 0.1.1.0

Defined in Data.Type.Predicate.Logic

Methods

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

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

Defined in Data.Type.Predicate.Logic

Methods

decide :: Decide (p &&& q)

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

Since: 0.1.1.0

Defined in Data.Type.Predicate.Logic

Methods

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

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

Since: 0.1.1.0

Defined in Data.Type.Predicate.Logic

Methods

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

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

Since: 0.1.1.0

Defined in Data.Type.Predicate.Logic

Methods

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

(Auto p a, Auto q a) => Auto (p &&& q :: TyFun k Type -> Type) (a :: k)

Defined in Data.Type.Predicate.Auto

Methods

auto :: (p &&& q) @@ a

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

Defined in Data.Type.Predicate.Logic

type Apply (p &&& q :: TyFun k1 Type -> 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 ==> (p ||| p) :: TyFun k1 Type -> Type)

Since: 0.1.1.0

Defined in Data.Type.Predicate.Logic

Methods

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

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

Since: 0.1.1.0

Defined in Data.Type.Predicate.Logic

Methods

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

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

Since: 0.1.1.0

Defined in Data.Type.Predicate.Logic

Methods

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

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

Prefers p over q.

Defined in Data.Type.Predicate.Logic

Methods

decide :: Decide (p ||| q)

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

Since: 0.1.1.0

Defined in Data.Type.Predicate.Logic

Methods

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

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

Since: 0.1.1.0

Defined in Data.Type.Predicate.Logic

Methods

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

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

Since: 0.1.1.0

Defined in Data.Type.Predicate.Logic

Methods

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

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

Defined in Data.Type.Predicate.Logic

type Apply (p ||| q :: TyFun k1 Type -> 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.

Prefers p over 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.

Since: 0.1.2.0

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.

Since: 0.1.2.0

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 &&& Not p) ==> (Impossible :: Predicate k1) :: TyFun k1 Type -> Type)

Since: 0.1.3.0

Defined in Data.Type.Predicate.Logic

Methods

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

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

Since: 0.1.1.0

Defined in Data.Type.Predicate.Logic

Methods

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

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

Since: 0.1.1.0

Defined in Data.Type.Predicate.Logic

Methods

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

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

Since: 0.1.1.0

Defined in Data.Type.Predicate.Logic

Methods

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

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

Since: 0.1.1.0

Defined in Data.Type.Predicate.Logic

Methods

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

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

Since: 0.1.1.0

Defined in Data.Type.Predicate.Logic

Methods

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

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

Since: 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 -> Type)

Defined in Data.Type.Predicate.Logic

Methods

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

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

Defined in Data.Type.Predicate.Logic

Methods

prove :: Prove (Impossible ==> p)

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

Since: 0.1.1.0

Defined in Data.Type.Predicate.Logic

Methods

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

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

Since: 0.1.1.0

Defined in Data.Type.Predicate.Logic

Methods

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

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

Since: 0.1.1.0

Defined in Data.Type.Predicate.Logic

Methods

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

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

Since: 0.1.1.0

Defined in Data.Type.Predicate.Logic

Methods

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

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

Since: 0.1.1.0

Defined in Data.Type.Predicate.Logic

Methods

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

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

Since: 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 -> Type)

Defined in Data.Type.Predicate.Logic

Methods

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

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

Defined in Data.Type.Predicate.Logic

Methods

decide :: Decide (Impossible ==> p)

Auto q a => Auto (p ==> q :: TyFun k Type -> Type) (a :: k)

Defined in Data.Type.Predicate.Auto

Methods

auto :: (p ==> q) @@ a

Provable p => Provable ((NotNull f :: Predicate (f k)) ==> Any f p :: TyFun (f k) Type -> 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 -> 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 -> 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 -> 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 -> 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 -> Type)

Defined in Data.Type.Predicate.Param

Methods

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

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

Defined in Data.Type.Predicate.Logic

type Apply (p ==> q :: TyFun k1 Type -> 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.

complementation :: forall p. (p &&& Not p) --> Impossible

We cannot have both p and Not p.

(Renamed in v0.1.4.0; used to be excludedMiddle)

Since: 0.1.4.0

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

Logical double negation. Only possible if p is Decidable.

This is because in constructivist logic, not (not p) does not imply p. However, p implies not (not p) (see negateTwice), and not (not (not p)) implies not p (see tripleNegation)

tripleNegation :: forall p. Not (Not (Not p)) --> Not p

In constructivist logic, not (not (not p)) implies not p.

Since: 0.1.4.0

negateTwice :: p --> Not (Not p)

In constructivist logic, p implies not (not p).

Since: 0.1.4.0

contrapositive :: (p --> q) -> Not q --> Not 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.