| Copyright | (c) Justin Le 2018 |
|---|---|
| License | BSD3 |
| Maintainer | justin@jle.im |
| Stability | experimental |
| Portability | non-portable |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Data.Type.Predicate
Description
Combinators for working with type-level predicates, along with typeclasses for canonical proofs and deciding functions.
Synopsis
- type Predicate k = k ~> Type
- newtype Wit p a = Wit {}
- type TyPred = TyCon1 :: (k -> Type) -> Predicate k
- data Evident :: Predicate k
- type EqualTo (a :: k) = TyPred ((:~:) a) :: Predicate k
- type BoolPred (p :: k ~> Bool) = PMap p (EqualTo 'True) :: Predicate k
- type Impossible = Not Evident :: Predicate k
- type In (f :: Type -> Type) (as :: f k) = ElemSym1 f as
- type PMap (f :: k ~> j) (p :: Predicate j) = p .@#@$$$ f :: Predicate k
- data Not :: Predicate k -> Predicate k
- decideNot :: forall p a. Decision (p @@ a) -> Decision (Not p @@ a)
- type Prove p = forall a. Sing a -> p @@ a
- type (-->) p q = forall a. Sing a -> (p @@ a) -> q @@ a
- type (-->#) p q h = forall a. Sing a -> (p @@ a) -> h (q @@ a)
- class Provable p where
- type Disprovable p = Provable (Not p)
- disprove :: forall p. Disprovable p => Prove (Not p)
- type ProvableTC p = Provable (TyPred p)
- proveTC :: forall t a. ProvableTC t => Sing a -> t a
- class TFunctor f where
- compImpl :: forall p q r. (p --> q) -> (q --> r) -> p --> r
- type Decide p = forall a. Sing a -> Decision (p @@ a)
- type (-?>) p q = forall a. Sing a -> (p @@ a) -> Decision (q @@ a)
- type (-?>#) p q h = forall a. Sing a -> (p @@ a) -> h (Decision (q @@ a))
- class Decidable p where
- type DecidableTC p = Decidable (TyPred p)
- decideTC :: forall t a. DecidableTC t => Sing a -> Decision (t a)
- class DFunctor f where
- data Decision a
- flipDecision :: Decision a -> Decision (Refuted a)
- mapDecision :: (a -> b) -> (b -> a) -> Decision a -> Decision b
- elimDisproof :: Decision a -> Refuted (Refuted a) -> a
- forgetDisproof :: Decision a -> Maybe a
- forgetProof :: Decision a -> Maybe (Refuted a)
- isProved :: Decision a -> Bool
- isDisproved :: Decision a -> Bool
- mapRefuted :: (a -> b) -> Refuted b -> Refuted a
Predicates
type Predicate k = k ~> Type Source #
A type-level predicate in Haskell. We say that the predicate P ::
is true/satisfied by input Predicate kx :: 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 ~> 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.Type
There are two ways to define your own predicates:
- 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.
- 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 theApplyinstance, to specify the type of the -- witnesses of that predicate instanceApply(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 ::Predicatek instance Apply Evident a =Singa
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.
A Wit p ap @@ a --- that is, it is a proof
or witness that p is satisfied for a.
It essentially turns a k ~> ("matchable" TypePredicate kk -> predicate.Type
Instances
Construct Predicates
data Evident :: Predicate k Source #
Instances
type Impossible = Not Evident :: Predicate k Source #
The always-false predicate
Could also be defined as ConstSym1 VoidDecidable instance.
Impossible::Predicatek
type In (f :: Type -> Type) (as :: f k) = ElemSym1 f as Source #
In f asa is a member of
collection as.
Manipulate predicates
data Not :: Predicate k -> Predicate k Source #
Not pp is not true.
Instances
decideNot :: forall p a. Decision (p @@ a) -> Decision (Not p @@ a) Source #
Decide Not pp.
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 ) if, given --> qp 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:
Methods
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
type Disprovable p = Provable (Not p) Source #
Disprovable pp 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 -> is a type constructor, then TypeProvableTC TT is "decidable", in that you have a canonical
function:
proveTC::Singa -> T a
Is essentially Provable, except with type constructors k ->
instead of matchable type-level functions (that are Typek ~> ).
Useful because TypeproveTC 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
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)p @@ a and Refuted (p @@ a)
This typeclass associates a canonical decision function for every decidable predicate.
It confers two main advatnages:
Minimal complete definition
Nothing
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
See decideTC and DecidableTC for a version that isn't ambiguously
typed, but only works when p is a type constructor.
Instances
type DecidableTC p = Decidable (TyPred p) Source #
If T :: k -> is a type constructor, then TypeDecidableTC TT is "decidable", in that you have a canonical
function:
decideTC::Singa ->Decision(T a)
Is essentially Decidable, except with type constructors k ->
instead of matchable type-level functions (that are Typek ~>
). Useful because TypedecideTC 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
Manipulate Decisions
A Decision about a type a is either a proof of existence or a proof that a
cannot exist.
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 #