Copyright | (c) Justin Le 2018 |
---|---|
License | BSD3 |
Maintainer | justin@jle.im |
Stability | experimental |
Portability | non-portable |
Safe Haskell | None |
Language | Haskell2010 |
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)
- type Evident = (TyPred Sing :: 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 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)
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 theApply
instance, 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 :: 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.
Construct Predicates
type Impossible = (Not Evident :: Predicate k) Source #
The always-false predicate
Could also be defined as
, but this defintion gives
us a free ConstSym1
VoidDecidable
instance.
Impossible
::Predicate
k
Manipulate predicates
data Not :: Predicate k -> Predicate k Source #
is the predicate that Not
pp
is not true.
Instances
Provable (Not (Impossible :: Predicate k1) :: TyFun k1 Type -> *) Source # | |
Defined in Data.Type.Predicate | |
Provable (Not (TyPred (IProxy (Proxy :: Proxy k1))) :: TyFun k1 Type -> *) Source # | |
Decidable p => Decidable (Not p :: TyFun k1 Type -> *) Source # | |
SingI a => Auto (Not (Impossible :: Predicate k) :: TyFun k Type -> *) (a :: k) Source # | Since: decidable-0.1.2.0 |
Defined in Data.Type.Predicate.Auto | |
AutoNot p (f @@ a) => Auto (Not (PMap f p) :: TyFun k Type -> *) (a :: k) Source # | Since: decidable-0.1.2.0 |
Provable ((p &&& Not p) ==> (Impossible :: Predicate k1) :: TyFun k1 Type -> *) Source # | Since: decidable-0.1.3.0 |
Defined in Data.Type.Predicate.Logic | |
Provable (p ==> q) => Provable (Not q ==> Not p :: TyFun k1 Type -> *) Source # | |
Provable ((Impossible :: Predicate k1) ==> p :: TyFun k1 Type -> *) Source # | |
Defined in Data.Type.Predicate.Logic | |
(Decidable (p ==> q), Decidable q) => Decidable (Not q ==> Not p :: TyFun k1 Type -> *) Source # | |
Decidable ((Impossible :: Predicate k1) ==> p :: TyFun k1 Type -> *) Source # | |
Defined in Data.Type.Predicate.Logic | |
Auto (NotFound p) (f @@ a) => Auto (NotFound (PPMap f p) :: Predicate k) (a :: k) Source # | Since: decidable-0.1.2.0 |
Auto (IsNothing :: Predicate (Maybe k)) (Nothing :: Maybe k) Source # | Since: decidable-0.1.3.0 |
(SingI as, AutoAll f (Not (Found p)) as) => Auto (Not (Found (AnyMatch f p)) :: TyFun (f k) Type -> *) (as :: f k) Source # | Since: decidable-0.1.2.0 |
(SingI as, AutoAll f (Not p) as) => Auto (Not (Any f p) :: TyFun (f k) Type -> *) (as :: f k) Source # | Since: decidable-0.1.2.0 |
Auto (Null (Proxy :: * -> *) :: Predicate (Proxy k)) (Proxy :: Proxy k) Source # | |
Auto (IsLeft :: Predicate (Either j k)) (Left a :: Either j k) Source # | Since: decidable-0.1.3.0 |
type Apply (Not p :: TyFun k1 Type -> *) (a :: k1) Source # | |
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
. 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).
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".
This typeclass associates a canonical proof function for every provable predicate.
It confers two main advatnages:
Instances
type Disprovable p = Provable (Not p) Source #
is a constraint that 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 Type
is
a constraint that ProvableTC
TT
is "decidable", in that you have a canonical
function:
proveTC :: Sing a -> T a
Is essentially Provable
, except with type constructors k ->
instead of matchable type-level functions (that are Type
k ~>
).Type
Mostly is in this library for compatiblity with "traditional" predicates that are GADT type constructors.
Since: decidable-0.1.1.0
proveTC :: forall t a. ProvableTC t => Sing a -> t a Source #
The canonical proving function for
.DecidableTC
t
Since: decidable-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
is a data type
that has a branch 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:
Instances
type DecidableTC p = Decidable (TyPred p) Source #
If T :: k ->
is a type constructor, then Type
is
a constraint that DecidableTC
TT
is "decidable", in that you have a canonical
function:
decideTC :: Sing a -> Decision
(T a)
Is essentially Decidable
, except with type constructors k ->
instead of matchable type-level functions (that are Type
k ~>
).Type
Mostly is in this library for compatiblity with "traditional" predicates that are GADT type constructors.
Since: decidable-0.1.1.0
decideTC :: forall t a. DecidableTC t => Sing a -> Decision (t a) Source #
The canonical deciding function for
.DecidableTC
t
Since: decidable-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 Haskell. See
doubleNegation
for a situation where it is.
Since: decidable-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: decidable-0.1.2.0
forgetDisproof :: Decision a -> Maybe a Source #
isDisproved :: Decision a -> Bool Source #