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

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). In some contexts, this is also known as a dependently typed "view".

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 

Fields

Instances

Instances details
Decidable p => Decidable (TyPred (PIdentity (Wit p)) :: Predicate (Identity k)) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate

Decidable p => Decidable (TyPred (NERec (Wit p)) :: Predicate (NonEmpty k)) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate

Methods

decide :: Decide (TyPred (NERec (Wit p))) Source #

Decidable p => Decidable (TyPred (PMaybe (Wit p)) :: Predicate (Maybe k)) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate

Methods

decide :: Decide (TyPred (PMaybe (Wit p))) Source #

Decidable p => Decidable (TyPred (Rec (Wit p)) :: Predicate [u]) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate

Methods

decide :: Decide (TyPred (Rec (Wit p))) Source #

Provable p => Provable (TyPred (PIdentity (Wit p)) :: Predicate (Identity k)) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate

Methods

prove :: Prove (TyPred (PIdentity (Wit p))) Source #

Provable p => Provable (TyPred (NERec (Wit p)) :: Predicate (NonEmpty k)) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate

Methods

prove :: Prove (TyPred (NERec (Wit p))) Source #

Provable p => Provable (TyPred (PMaybe (Wit p)) :: Predicate (Maybe k)) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate

Methods

prove :: Prove (TyPred (PMaybe (Wit p))) Source #

Provable p => Provable (TyPred (Rec (Wit p)) :: Predicate [u]) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate

Methods

prove :: Prove (TyPred (Rec (Wit p))) Source #

(SingI as, Provable p) => Auto (TyPred (PIdentity (Wit p)) :: Predicate (Identity k)) (as :: Identity k) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate.Auto

Methods

auto :: TyPred (PIdentity (Wit p)) @@ as Source #

(SingI as, Provable p) => Auto (TyPred (NERec (Wit p)) :: Predicate (NonEmpty k)) (as :: NonEmpty k) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate.Auto

Methods

auto :: TyPred (NERec (Wit p)) @@ as Source #

(SingI as, Provable p) => Auto (TyPred (PMaybe (Wit p)) :: Predicate (Maybe k)) (as :: Maybe k) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate.Auto

Methods

auto :: TyPred (PMaybe (Wit p)) @@ as Source #

(SingI as, Provable p) => Auto (TyPred (Rec (Wit p)) :: Predicate [u]) (as :: [u]) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate.Auto

Methods

auto :: TyPred (Rec (Wit p)) @@ as Source #

Decidable p => Decidable (TyPred (PEither (Wit p) :: Either j k -> Type) :: Predicate (Either j k)) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate

Methods

decide :: Decide (TyPred (PEither (Wit p))) Source #

Decidable p => Decidable (TyPred (PTup (Wit p) :: (j, k) -> Type) :: Predicate (j, k)) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate

Methods

decide :: Decide (TyPred (PTup (Wit p))) Source #

Provable p => Provable (TyPred (PEither (Wit p) :: Either j k -> Type) :: Predicate (Either j k)) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate

Methods

prove :: Prove (TyPred (PEither (Wit p))) Source #

Provable p => Provable (TyPred (PTup (Wit p) :: (j, k) -> Type) :: Predicate (j, k)) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate

Methods

prove :: Prove (TyPred (PTup (Wit p))) Source #

(SingI as, Provable p) => Auto (TyPred (PEither (Wit p) :: Either j k -> Type) :: Predicate (Either j k)) (as :: Either j k) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate.Auto

Methods

auto :: TyPred (PEither (Wit p)) @@ as Source #

(SingI as, Provable p) => Auto (TyPred (PTup (Wit p) :: (j, k) -> Type) :: Predicate (j, k)) (as :: (j, k)) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate.Auto

Methods

auto :: TyPred (PTup (Wit p)) @@ as Source #

Construct Predicates

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

Convert a normal -> type constructor into a Predicate.

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

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 EqualTo (a :: k) = TyPred ((:~:) a) :: Predicate k Source #

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

EqualTo :: k -> Predicate k

type BoolPred (p :: k ~> Bool) = PMap p (EqualTo 'True) :: 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.

Impossible :: Predicate k

type In (f :: Type -> Type) (as :: f k) = ElemSym1 f as Source #

In f as is a predicate that a given input a is a member of collection as.

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

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.

Provable Predicates

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

A proving function for predicate p; in some contexts, also called a "view function". 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). In some context, these are also known as "views".

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

We can call a type a view if, for any input a, there is some constructor of p @@ a that can we can use to "categorize" a.

This typeclass associates a canonical proof function for every provable predicate, or a canonical view function for any view.

It confers two main advatnages:

  1. The proof functionview for every predicateview 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.

Methods

prove :: Prove p Source #

The canonical proving function for predicate p (or a canonical view function for view 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

See proveTC and ProvableTC for a version that isn't ambiguously typed, but only works when p is a type constructor.

Instances

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

Defined in Data.Type.Predicate

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

Defined in Data.Type.Predicate

Provable (TyPred (WrappedSing :: k1 -> Type) :: Predicate k1) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate

(Provable (Found p), SingI f) => Provable (Found (PPMap f p) :: TyFun k Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate.Param

Methods

prove :: Prove (Found (PPMap f p)) 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 ((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 #

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

Defined in Data.Type.Predicate.Param

Methods

prove :: Prove (Found (AndP p q)) Source #

(Provable p, SingI f) => Provable (PMap f p :: Predicate k1) Source # 
Instance details

Defined in Data.Type.Predicate

Methods

prove :: Prove (PMap f p) Source #

Provable p => Provable (TyPred (PIdentity (Wit p)) :: Predicate (Identity k)) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate

Methods

prove :: Prove (TyPred (PIdentity (Wit p))) Source #

Provable (TyPred (PIdentity (WrappedSing :: k -> Type)) :: Predicate (Identity k)) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate

Provable p => Provable (TyPred (NERec (Wit p)) :: Predicate (NonEmpty k)) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate

Methods

prove :: Prove (TyPred (NERec (Wit p))) Source #

Provable (TyPred (NERec (WrappedSing :: k -> Type)) :: Predicate (NonEmpty k)) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate

Provable p => Provable (TyPred (PMaybe (Wit p)) :: Predicate (Maybe k)) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate

Methods

prove :: Prove (TyPred (PMaybe (Wit p))) Source #

Provable (TyPred (PMaybe (WrappedSing :: k -> Type)) :: Predicate (Maybe k)) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate

Provable p => Provable (TyPred (Rec (Wit p)) :: Predicate [u]) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate

Methods

prove :: Prove (TyPred (Rec (Wit p))) Source #

Provable (TyPred (Rec (WrappedSing :: u -> Type)) :: Predicate [u]) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate

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 #

(Universe f, Provable p) => Provable (All f p :: TyFun (f k) Type -> Type) Source # 
Instance details

Defined in Data.Type.Universe

Methods

prove :: Prove (All f p) Source #

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

Defined in Data.Type.Universe.Subset

Methods

prove :: Prove (Subset 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 #

Provable p => Provable (TyPred (PEither (Wit p) :: Either j k -> Type) :: Predicate (Either j k)) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate

Methods

prove :: Prove (TyPred (PEither (Wit p))) Source #

Provable (TyPred (PEither (WrappedSing :: k -> Type) :: Either j k -> Type) :: Predicate (Either j k)) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate

Provable p => Provable (TyPred (PTup (Wit p) :: (j, k) -> Type) :: Predicate (j, k)) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate

Methods

prove :: Prove (TyPred (PTup (Wit p))) Source #

Provable (TyPred (PTup (WrappedSing :: k -> Type) :: (j, k) -> Type) :: Predicate (j, k)) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate

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). Useful because proveTC doesn't require anything fancy like TypeApplications to use.

Also is in this library for compatiblity with "traditional" predicates that are GADT type constructors.

Since: 0.1.1.0

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

The canonical proving function for DecidableTC t.

Note that because t must be an injective type constructor, you can use this without explicit type applications; the instance of ProvableTC can be inferred from the result type.

Since: 0.1.1.0

class TFunctor f where Source #

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

Methods

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

Instances

Instances details
Universe f => TFunctor (All f :: Predicate k1 -> TyFun (f k1) Type -> Type) Source # 
Instance details

Defined in Data.Type.Universe

Methods

tmap :: forall (p :: k10 ~> Type) (q :: k10 ~> Type). (p --> q) -> All f p --> All f q Source #

Universe f => TFunctor (Any f :: Predicate k1 -> TyFun (f k1) Type -> Type) Source # 
Instance details

Defined in Data.Type.Universe

Methods

tmap :: forall (p :: k10 ~> Type) (q :: k10 ~> Type). (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.

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.

Minimal complete definition

Nothing

Methods

decide :: 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

See decideTC and DecidableTC for a version that isn't ambiguously typed, but only works when p is a type constructor.

default decide :: Provable p => Decide p Source #

Instances

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

Defined in Data.Type.Predicate

(SDecide k, SingI a) => Decidable (EqualTo a :: Predicate k) Source # 
Instance details

Defined in Data.Type.Predicate

Methods

decide :: Decide (EqualTo a) Source #

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

Defined in Data.Type.Predicate

Methods

decide :: Decide (Not p) Source #

Decidable (TyPred (WrappedSing :: k1 -> Type) :: Predicate k1) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate

(SDecide k, SingI as) => Decidable (In (Either j) as :: TyFun k Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate

Methods

decide :: Decide (In (Either j) as) Source #

(SDecide k, SingI as) => Decidable (In Identity as :: TyFun k Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate

Methods

decide :: Decide (In Identity as) Source #

(SDecide k, SingI as) => Decidable (In NonEmpty as :: TyFun k Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate

Methods

decide :: Decide (In NonEmpty as) Source #

(SDecide k, SingI as) => Decidable (In Maybe as :: TyFun k Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate

Methods

decide :: Decide (In Maybe as) Source #

(SDecide k, SingI as) => Decidable (In ((,) j) as :: TyFun k Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate

Methods

decide :: Decide (In ((,) j) as) Source #

(SDecide k, SingI as) => Decidable (In [] as :: TyFun k Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate

Methods

decide :: Decide (In [] as) Source #

(Decidable (Found p), SingI f) => Decidable (Found (PPMap f p) :: TyFun k Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate.Param

Methods

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

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

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

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

Defined in Data.Type.Predicate.Param

Methods

decide :: Decide (Found (AndP p q)) Source #

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

Defined in Data.Type.Predicate.Param

Methods

decide :: Decide (Found (OrP p q)) Source #

(Decidable p, SingI f) => Decidable (PMap f p :: Predicate k1) Source # 
Instance details

Defined in Data.Type.Predicate

Methods

decide :: Decide (PMap f p) Source #

Decidable p => Decidable (TyPred (PIdentity (Wit p)) :: Predicate (Identity k)) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate

Decidable (TyPred (PIdentity (WrappedSing :: k -> Type)) :: Predicate (Identity k)) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate

Decidable p => Decidable (TyPred (NERec (Wit p)) :: Predicate (NonEmpty k)) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate

Methods

decide :: Decide (TyPred (NERec (Wit p))) Source #

Decidable (TyPred (NERec (WrappedSing :: k -> Type)) :: Predicate (NonEmpty k)) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate

Decidable p => Decidable (TyPred (PMaybe (Wit p)) :: Predicate (Maybe k)) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate

Methods

decide :: Decide (TyPred (PMaybe (Wit p))) Source #

Decidable (TyPred (PMaybe (WrappedSing :: k -> Type)) :: Predicate (Maybe k)) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate

Decidable p => Decidable (TyPred (Rec (Wit p)) :: Predicate [u]) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate

Methods

decide :: Decide (TyPred (Rec (Wit p))) Source #

Decidable (TyPred (Rec (WrappedSing :: u -> Type)) :: Predicate [u]) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate

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 #

(Universe f, Decidable (Found p)) => Decidable (Found (AnyMatch f p) :: TyFun (f k) Type -> Type) Source # 
Instance details

Defined in Data.Type.Predicate.Param

Methods

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

(Universe f, Decidable p) => Decidable (All f p :: TyFun (f k) Type -> Type) Source # 
Instance details

Defined in Data.Type.Universe

Methods

decide :: Decide (All f p) Source #

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

Defined in Data.Type.Universe

Methods

decide :: Decide (Any f p) Source #

(Universe f, Decidable p) => Decidable (Subset f p :: TyFun (f k) Type -> Type) Source # 
Instance details

Defined in Data.Type.Universe.Subset

Methods

decide :: Decide (Subset 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 #

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

Defined in Data.Type.Predicate.Param

Methods

decide :: Decide (Found (InP f)) Source #

Decidable p => Decidable (TyPred (PEither (Wit p) :: Either j k -> Type) :: Predicate (Either j k)) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate

Methods

decide :: Decide (TyPred (PEither (Wit p))) Source #

Decidable (TyPred (PEither (WrappedSing :: k -> Type) :: Either j k -> Type) :: Predicate (Either j k)) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate

Decidable p => Decidable (TyPred (PTup (Wit p) :: (j, k) -> Type) :: Predicate (j, k)) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate

Methods

decide :: Decide (TyPred (PTup (Wit p))) Source #

Decidable (TyPred (PTup (WrappedSing :: k -> Type) :: (j, k) -> Type) :: Predicate (j, k)) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate

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). Useful because decideTC doesn't require anything fancy like TypeApplications to use.

Also is in this library for compatiblity with "traditional" predicates that are GADT type constructors.

Since: 0.1.1.0

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

The canonical deciding function for DecidableTC t.

Note that because t must be an injective type constructor, you can use this without explicit type applications; the instance of DecidableTC can be inferred from the result type.

Since: 0.1.1.0

class DFunctor f where Source #

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

Methods

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

Instances

Instances details
Universe f => DFunctor (All f :: Predicate k1 -> TyFun (f k1) Type -> Type) Source # 
Instance details

Defined in Data.Type.Universe

Methods

dmap :: forall (p :: k10 ~> Type) (q :: k10 ~> Type). (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

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

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

Since: 0.1.1.0

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

Map over the value inside a Decision.

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

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

Since: 0.1.2.0

forgetDisproof :: Decision a -> Maybe a Source #

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

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

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

Since: 0.1.1.0

isProved :: Decision a -> Bool Source #

Boolean test if a Decision is Proved.

Since: 0.1.1.0

isDisproved :: Decision a -> Bool Source #

Boolean test if a Decision is Disproved.

Since: 0.1.1.0

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

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

Since: 0.1.2.0