decidable-0.3.1.0: Combinators for manipulating dependently-typed predicates.
Copyright(c) Justin Le 2018
LicenseBSD3
Maintainerjustin@jle.im
Stabilityexperimental
Portabilitynon-portable
Safe HaskellSafe-Inferred
LanguageHaskell2010

Data.Type.Predicate.Logic

Description

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

Synopsis

Top and bottom

data Evident :: Predicate k Source #

The always-true predicate.

Evident :: Predicate k

Instances

Instances details
Decidable (Evident :: TyFun k1 Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate

Provable (Evident :: TyFun k1 Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate

SingI a => Auto (Evident :: TyFun k Type -> Type) (a :: k) Source # 
Instance details

Defined in Data.Type.Predicate.Auto

Methods

auto :: Evident @@ a Source #

Provable (Not (Impossible :: Predicate k1) :: TyFun k1 Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate

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

Since: 0.1.2.0

Instance details

Defined in Data.Type.Predicate.Auto

Decidable ((Impossible :: Predicate k1) ==> p :: TyFun k1 Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate.Logic

Provable ((Impossible :: Predicate k1) ==> p :: TyFun k1 Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate.Logic

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

Since: 0.1.3.0

Instance details

Defined in Data.Type.Predicate.Logic

Methods

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

SingI a => Auto (IsJust :: Predicate (Maybe k)) ('Just a :: Maybe k) Source #

Since: 0.1.2.0

Instance details

Defined in Data.Type.Predicate.Auto

Methods

auto :: IsJust @@ 'Just a Source #

SingI a => Auto (NotNull Identity :: Predicate (Identity k)) ('Identity a :: Identity k) Source # 
Instance details

Defined in Data.Type.Predicate.Auto

SingI a => Auto (NotNull NonEmpty :: Predicate (NonEmpty k)) (a :| as :: NonEmpty k) Source #

Since: 0.1.2.0

Instance details

Defined in Data.Type.Predicate.Auto

Methods

auto :: NotNull NonEmpty @@ (a :| as) Source #

SingI a => Auto (NotNull [] :: Predicate [k]) (a ': as :: [k]) Source #

Since: 0.1.2.0

Instance details

Defined in Data.Type.Predicate.Auto

Methods

auto :: NotNull [] @@ (a ': as) Source #

Decidable ((NotNull f :: Predicate (f k)) ==> Found (InP f :: ParamPred (f k) k) :: TyFun (f k) Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate.Param

Methods

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

(Universe f, Provable p) => Decidable ((NotNull f :: Predicate (f k)) ==> Any f p :: TyFun (f k) Type -> Type) Source # 
Instance details

Defined in Data.Type.Universe

Methods

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

Decidable (Found (InP f :: ParamPred (f v) v) ==> (NotNull f :: Predicate (f v)) :: TyFun (f v) Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate.Param

Methods

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

Provable ((NotNull f :: Predicate (f k)) ==> Found (InP f :: ParamPred (f k) k) :: TyFun (f k) Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate.Param

Methods

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

Provable p => Provable ((NotNull f :: Predicate (f k)) ==> Any f p :: TyFun (f k) Type -> Type) Source # 
Instance details

Defined in Data.Type.Universe

Methods

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

Provable (Found (InP f :: ParamPred (f v) v) ==> (NotNull f :: Predicate (f v)) :: TyFun (f v) Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate.Param

Methods

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

SingI a => Auto (IsRight :: Predicate (Either j k)) ('Right a :: Either j k) Source #

Since: 0.1.2.0

Instance details

Defined in Data.Type.Predicate.Auto

Methods

auto :: IsRight @@ 'Right a Source #

SingI a => Auto (NotNull ((,) j) :: Predicate (j, k)) ('(w, a) :: (j, k)) Source #

Since: 0.1.2.0

Instance details

Defined in Data.Type.Predicate.Auto

Methods

auto :: NotNull ((,) j) @@ '(w, a) Source #

type Apply (Evident :: TyFun k Type -> Type) (a :: k) Source # 
Instance details

Defined in Data.Type.Predicate

type Apply (Evident :: TyFun k Type -> Type) (a :: k) = Sing a

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.

Impossible :: Predicate k

Logical connectives

data Not :: Predicate k -> Predicate k Source #

Not p is the predicate that p is not true.

Instances

Instances details
Decidable p => Decidable (Not p :: TyFun k1 Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate

Methods

decide :: Decide (Not p) Source #

Provable (Not (Impossible :: Predicate k1) :: TyFun k1 Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate

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

Since: 0.1.2.0

Instance details

Defined in Data.Type.Predicate.Auto

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

Since: 0.1.2.0

Instance details

Defined in Data.Type.Predicate.Auto

Methods

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

Decidable ((Impossible :: Predicate k1) ==> p :: TyFun k1 Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate.Logic

(Decidable (p ==> q), Decidable q) => Decidable (Not q ==> Not p :: TyFun k1 Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate.Logic

Methods

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

Provable ((Impossible :: Predicate k1) ==> p :: TyFun k1 Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate.Logic

Provable (p ==> q) => Provable (Not q ==> Not p :: TyFun k1 Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate.Logic

Methods

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

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

Since: 0.1.3.0

Instance details

Defined in Data.Type.Predicate.Logic

Methods

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

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

Since: 0.1.2.0

Instance details

Defined in Data.Type.Predicate.Auto

Methods

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

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

Since: 0.1.2.0

Instance details

Defined in Data.Type.Predicate.Auto

Methods

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

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

Since: 0.1.2.0

Instance details

Defined in Data.Type.Predicate.Auto

Methods

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

type Apply (Not p :: TyFun k1 Type -> Type) (a :: k1) Source # 
Instance details

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

Decide Not p based on decisions of p.

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

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

Instances

Instances details
(Decidable p, Decidable q) => Decidable (p &&& q :: TyFun k1 Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate.Logic

Methods

decide :: Decide (p &&& q) Source #

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

Since: 0.1.1.0

Instance details

Defined in Data.Type.Predicate.Logic

Methods

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

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

Since: 0.1.1.0

Instance details

Defined in Data.Type.Predicate.Logic

Methods

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

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

Since: 0.1.1.0

Instance details

Defined in Data.Type.Predicate.Logic

Methods

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

(Provable p, Provable q) => Provable (p &&& q :: TyFun k1 Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate.Logic

Methods

prove :: Prove (p &&& q) Source #

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

Since: 0.1.3.0

Instance details

Defined in Data.Type.Predicate.Logic

Methods

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

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

Since: 0.1.1.0

Instance details

Defined in Data.Type.Predicate.Logic

Methods

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

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

Since: 0.1.1.0

Instance details

Defined in Data.Type.Predicate.Logic

Methods

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

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

Since: 0.1.1.0

Instance details

Defined in Data.Type.Predicate.Logic

Methods

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

(Auto p a, Auto q a) => Auto (p &&& q :: TyFun k Type -> Type) (a :: k) Source # 
Instance details

Defined in Data.Type.Predicate.Auto

Methods

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

type Apply (p &&& q :: TyFun k1 Type -> Type) (a :: k1) Source # 
Instance details

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

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

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

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

Instances

Instances details
Decidable (p ==> (p ||| p) :: TyFun k1 Type -> Type) Source #

Since: 0.1.1.0

Instance details

Defined in Data.Type.Predicate.Logic

Methods

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

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

Since: 0.1.1.0

Instance details

Defined in Data.Type.Predicate.Logic

Methods

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

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

Since: 0.1.1.0

Instance details

Defined in Data.Type.Predicate.Logic

Methods

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

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

Prefers p over q.

Instance details

Defined in Data.Type.Predicate.Logic

Methods

decide :: Decide (p ||| q) Source #

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

Since: 0.1.1.0

Instance details

Defined in Data.Type.Predicate.Logic

Methods

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

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

Since: 0.1.1.0

Instance details

Defined in Data.Type.Predicate.Logic

Methods

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

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

Since: 0.1.1.0

Instance details

Defined in Data.Type.Predicate.Logic

Methods

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

type Apply (p ||| q :: TyFun k1 Type -> Type) (a :: k1) Source # 
Instance details

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

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

Prefers p over q.

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

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

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

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

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

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

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

Instances

Instances details
Decidable ((Impossible :: Predicate k1) ==> p :: TyFun k1 Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate.Logic

(Decidable (p ==> q), Decidable q) => Decidable (Not q ==> Not p :: TyFun k1 Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate.Logic

Methods

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

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

Since: 0.1.1.0

Instance details

Defined in Data.Type.Predicate.Logic

Methods

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

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

Since: 0.1.1.0

Instance details

Defined in Data.Type.Predicate.Logic

Methods

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

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

Since: 0.1.1.0

Instance details

Defined in Data.Type.Predicate.Logic

Methods

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

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

Since: 0.1.1.0

Instance details

Defined in Data.Type.Predicate.Logic

Methods

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

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

Since: 0.1.1.0

Instance details

Defined in Data.Type.Predicate.Logic

Methods

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

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

Since: 0.1.1.0

Instance details

Defined in Data.Type.Predicate.Logic

Methods

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

Provable ((Impossible :: Predicate k1) ==> p :: TyFun k1 Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate.Logic

Provable (p ==> q) => Provable (Not q ==> Not p :: TyFun k1 Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate.Logic

Methods

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

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

Since: 0.1.3.0

Instance details

Defined in Data.Type.Predicate.Logic

Methods

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

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

Since: 0.1.1.0

Instance details

Defined in Data.Type.Predicate.Logic

Methods

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

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

Since: 0.1.1.0

Instance details

Defined in Data.Type.Predicate.Logic

Methods

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

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

Since: 0.1.1.0

Instance details

Defined in Data.Type.Predicate.Logic

Methods

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

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

Since: 0.1.1.0

Instance details

Defined in Data.Type.Predicate.Logic

Methods

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

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

Since: 0.1.1.0

Instance details

Defined in Data.Type.Predicate.Logic

Methods

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

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

Since: 0.1.1.0

Instance details

Defined in Data.Type.Predicate.Logic

Methods

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

Auto q a => Auto (p ==> q :: TyFun k Type -> Type) (a :: k) Source # 
Instance details

Defined in Data.Type.Predicate.Auto

Methods

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

Decidable ((NotNull f :: Predicate (f k)) ==> Found (InP f :: ParamPred (f k) k) :: TyFun (f k) Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate.Param

Methods

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

(Universe f, Provable p) => Decidable ((NotNull f :: Predicate (f k)) ==> Any f p :: TyFun (f k) Type -> Type) Source # 
Instance details

Defined in Data.Type.Universe

Methods

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

Decidable (Found (InP f :: ParamPred (f v) v) ==> (NotNull f :: Predicate (f v)) :: TyFun (f v) Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate.Param

Methods

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

Provable ((NotNull f :: Predicate (f k)) ==> Found (InP f :: ParamPred (f k) k) :: TyFun (f k) Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate.Param

Methods

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

Provable p => Provable ((NotNull f :: Predicate (f k)) ==> Any f p :: TyFun (f k) Type -> Type) Source # 
Instance details

Defined in Data.Type.Universe

Methods

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

Provable (Found (InP f :: ParamPred (f v) v) ==> (NotNull f :: Predicate (f v)) :: TyFun (f v) Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate.Param

Methods

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

type Apply (p ==> q :: TyFun k1 Type -> Type) (a :: k1) Source # 
Instance details

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

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

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

Two-way implication, or logical equivalence

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

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

Compose two implications.

explosion :: Impossible --> p Source #

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

atom :: p --> Evident Source #

Evident can be proven from all predicates.

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

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

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

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

Since: 0.1.4.0

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

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

Since: 0.1.4.0

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

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

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

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

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

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

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

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

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

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

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