-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | Combinators for manipulating dependently-typed predicates.
--
-- This library provides combinators and typeclasses for working and
-- manipulating type-level predicates in Haskell, which are represented
-- as matchable type-level functions k ~> Type from the
-- singletons library. See Data.Type.Predicate for a good
-- starting point, and the documentation for Predicate on how to
-- define predicates.
@package decidable
@version 0.1.2.0
-- | Combinators for working with type-level predicates, along with
-- typeclasses for canonical proofs and deciding functions.
module Data.Type.Predicate
-- | 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)
--
-- 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:
--
--
-- - 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 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.
type Predicate k = k ~> Type
-- | 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.
newtype Wit p a
Wit :: p @@ a -> Wit p a
[getWit] :: Wit p a -> p @@ a
-- | Convert a normal '->' type constructor into a Predicate.
--
--
-- TyPred :: (k -> Type) -> Predicate k
--
type TyPred = (TyCon1 :: (k -> Type) -> Predicate k)
-- | The always-true predicate.
--
--
-- Evident :: Predicate k
--
type Evident = (TyPred Sing :: Predicate k)
-- | EqualTo a is a predicate that the input is equal to
-- a.
type EqualTo (a :: k) = (TyPred ((:~:) a) :: Predicate k)
-- | Convert a tradtional k ~> Bool predicate into a
-- Predicate.
--
--
-- BoolPred :: (k ~> Bool) -> Predicate k
--
type BoolPred (p :: k ~> Bool) = (EqualTo 'True .@#@$$$ p :: Predicate k)
-- | The always-false predicate
--
-- Could also be defined as ConstSym1 Void, but this
-- defintion gives us a free Decidable instance.
type Impossible = (Not Evident :: Predicate k)
-- | Pre-compose a function to a predicate
--
--
-- PMap :: (k ~> j) -> Predicate j -> Predicate k
--
type PMap (f :: k ~> j) (p :: Predicate j) = (p .@#@$$$ f :: Predicate k)
-- | Not p is the predicate that p is not true.
data Not :: Predicate k -> Predicate k
-- | Decide Not p based on decisions of p.
decideNot :: forall p a. () => Decision (p @@ a) -> Decision (Not p @@ a)
-- | A proving function for predicate p. See Provable for
-- more information.
type Prove p = forall a. Sing a -> p @@ a
-- | We say that p implies q (p --> q)
-- if, given p a, we can always prove q @@ a.
type p --> q = forall a. Sing a -> p @@ a -> q @@ a
-- | This is implication -->#, but only in a specific context
-- h.
type ( p --># q ) h = forall a. Sing a -> p @@ a -> h (q @@ a)
-- | 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:
--
--
-- - The proof function for every predicate is available via the same
-- name
-- - We can write Provable instances for polymorphic predicate
-- transformers (predicates parameterized on other predicates) easily, by
-- refering to Provable instances of the transformed
-- predicates.
--
class Provable p
-- | The canonical proving function for predicate 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
--
prove :: Provable p => Prove p
-- | Disprovable p is a constraint that p can be
-- disproven.
type Disprovable p = Provable (Not p)
-- | The deciding/disproving function for Disprovable p.
--
-- Must be called by applying the Predicate to disprove:
--
--
-- disprove @p
--
disprove :: forall p. Disprovable p => Prove (Not p)
-- | 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).
type ProvableTC p = Provable (TyPred p)
-- | The canonical proving function for DecidableTC t.
proveTC :: forall t a. ProvableTC t => Sing a -> t a
-- | Implicatons p --> q can be lifted "through" a
-- TFunctor into an f p --> f q.
class TFunctor f
tmap :: forall p q. TFunctor f => (p --> q) -> (f p --> f q)
-- | Compose two implications.
compImpl :: forall p q r. () => p --> q -> q --> r -> p --> r
-- | A decision function for predicate p. See Decidable for
-- more information.
type Decide p = forall a. Sing a -> Decision (p @@ a)
-- | Like implication -->, but knowing p @@ a can only
-- let us decidably prove q a is true or false.
type p -?> q = forall a. Sing a -> p @@ a -> Decision (q @@ a)
-- | Like -?>, but only in a specific context h.
type ( p -?># q ) h = forall a. Sing a -> p @@ a -> h (Decision (q @@ a))
-- | 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:
--
--
-- - The decision function for every predicate is available via the
-- same name
-- - We can write Decidable instances for polymorphic predicate
-- transformers (predicates parameterized on other predicates) easily, by
-- refering to Decidable instances of the transformed
-- predicates.
--
class Decidable p
-- | 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
--
decide :: Decidable p => Decide p
-- | 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
--
decide :: (Decidable p, Provable p) => Decide p
-- | 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).
type DecidableTC p = Decidable (TyPred p)
-- | The canonical deciding function for DecidableTC t.
decideTC :: forall t a. DecidableTC t => Sing a -> Decision (t a)
-- | Implicatons p -?> q can be lifted "through" a
-- DFunctor into an f p -?> f q.
class DFunctor f
dmap :: forall p q. DFunctor f => (p -?> q) -> (f p -?> f q)
-- | A Decision about a type a is either a proof of
-- existence or a proof that a cannot exist.
data Decision a
-- | Witness for a
Proved :: a -> Decision a
-- | Proof that no a exists
Disproved :: Refuted a -> Decision a
-- | 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.
flipDecision :: Decision a -> Decision (Refuted a)
-- | Map over the value inside a Decision.
mapDecision :: (a -> b) -> (b -> a) -> Decision a -> Decision b
-- | Helper function for a common pattern of eliminating the disproved
-- branch of Decision to certaintify the proof.
elimDisproof :: Decision a -> Refuted (Refuted a) -> a
-- | Converts a Decision to a Maybe. Drop the witness of
-- disproof of a, returning Just if Proved (with
-- the proof) and Nothing if Disproved.
forgetDisproof :: Decision a -> Maybe a
-- | Drop the witness of proof of a, returning Nothing if
-- Proved and Just if Disproved (with the disproof).
forgetProof :: Decision a -> Maybe (Refuted a)
-- | Boolean test if a Decision is Proved.
isProved :: Decision a -> Bool
-- | Boolean test if a Decision is Disproved.
isDisproved :: Decision a -> Bool
-- | Change the target of a Refuted with a contravariant mapping
-- function.
mapRefuted :: (a -> b) -> Refuted b -> Refuted a
instance Data.Type.Predicate.Provable (Data.Type.Predicate.Not Data.Type.Predicate.Impossible)
instance forall k1 (p :: k1 Data.Singletons.Internal.~> *). Data.Type.Predicate.Decidable p => Data.Type.Predicate.Decidable (Data.Type.Predicate.Not p)
instance forall k (a :: k). (Data.Singletons.Decide.SDecide k, Data.Singletons.Internal.SingI a) => Data.Type.Predicate.Decidable (Data.Type.Predicate.EqualTo a)
instance Data.Type.Predicate.Decidable Data.Type.Predicate.Evident
instance forall k1 j (p :: j Data.Singletons.Internal.~> *) (f :: k1 Data.Singletons.Internal.~> j). (Data.Type.Predicate.Decidable p, Data.Singletons.Internal.SingI f) => Data.Type.Predicate.Decidable (Data.Type.Predicate.PMap f p)
instance Data.Type.Predicate.Provable Data.Type.Predicate.Evident
instance forall k1 j (p :: j Data.Singletons.Internal.~> *) (f :: k1 Data.Singletons.Internal.~> j). (Data.Type.Predicate.Provable p, Data.Singletons.Internal.SingI f) => Data.Type.Predicate.Provable (Data.Type.Predicate.PMap f p)
-- | Logical and algebraic connectives for predicates, as well as common
-- logical combinators.
module Data.Type.Predicate.Logic
-- | The always-true predicate.
--
--
-- Evident :: Predicate k
--
type Evident = (TyPred Sing :: Predicate k)
-- | The always-false predicate
--
-- Could also be defined as ConstSym1 Void, but this
-- defintion gives us a free Decidable instance.
type Impossible = (Not Evident :: Predicate k)
-- | Not p is the predicate that p is not true.
data Not :: Predicate k -> Predicate k
-- | Decide Not p based on decisions of p.
decideNot :: forall p a. () => Decision (p @@ a) -> Decision (Not p @@ a)
-- | p &&& q is a predicate that both
-- p and q are true.
data (&&&) :: Predicate k -> Predicate k -> Predicate k
-- | Decide p &&& q based on decisions of
-- p and q.
decideAnd :: forall p q a. () => Decision (p @@ a) -> Decision (q @@ a) -> Decision ((p &&& q) @@ a)
-- | p ||| q is a predicate that either p and
-- q are true.
data (|||) :: Predicate k -> Predicate k -> Predicate k
-- | Decide p ||| q based on decisions of p and
-- q.
decideOr :: forall p q a. () => Decision (p @@ a) -> Decision (q @@ a) -> Decision ((p ||| q) @@ a)
-- | Left-biased "or". In proofs, prioritize a proof of the left side over
-- a proof of the right side.
type p ^|| q = p ||| Not p &&& q
-- | Right-biased "or". In proofs, prioritize a proof of the right side
-- over a proof of the left side.
type p ||^ q = p &&& Not q ||| q
-- | p ^^^ q is a predicate that either p and
-- q are true, but not both.
type p ^^^ q = (p &&& Not q) ||| (Not p &&& q)
-- | Decide p ^^^ q based on decisions of p and
-- q.
decideXor :: forall p q a. () => Decision (p @@ a) -> Decision (q @@ a) -> Decision ((p ^^^ q) @@ a)
-- | p ==> q is true if q is provably true under the
-- condition that p is true.
data (==>) :: Predicate k -> Predicate k -> Predicate k
-- | 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.
proveImplies :: Prove q -> Prove (p ==> q)
-- | Implies p q is a constraint that p ==>
-- q is Provable; that is, you can prove that p
-- implies q.
type Implies p q = Provable (p ==> q)
-- | Two-way implication, or logical equivalence
type p <==> q = p ==> q &&& q ==> p
-- | Equiv p q is a constraint that p <==>
-- q is Provable; that is, you can prove that p is
-- logically equivalent to q.
type Equiv p q = Provable (p <==> q)
-- | Compose two implications.
compImpl :: forall p q r. () => p --> q -> q --> r -> p --> r
-- | From Impossible a, you can prove anything.
-- Essentially a lifted version of absurd.
explosion :: Impossible --> p
-- | Evident can be proven from all predicates.
atom :: p --> Evident
-- | We cannot have both p and Not p.
excludedMiddle :: (p &&& Not p) --> Impossible
-- | Logical double negation. Only possible if p is
-- Decidable.
doubleNegation :: forall p. Decidable p => Not (Not p) --> p
-- | If only this worked, but darn overlapping instances. Same for p ==>
-- p ||| q and p &&& q ==> p :( q) ==> instance
-- Provable (p &&& Not p ==> Impossible) where prove =
-- excludedMiddle @p
--
-- If p implies q, then not q implies not p.
contrapositive :: (p --> q) -> (Not q --> Not p)
-- | Reverse direction of contrapositive. Only possible if
-- q is Decidable on its own, without the help of
-- p, which makes this much less useful.
contrapositive' :: forall p q. Decidable q => (Not q --> Not p) -> (p --> q)
-- | If p &&& q is true, then so is p.
projAndFst :: (p &&& q) --> p
-- | If p &&& q is true, then so is q.
projAndSnd :: (p &&& q) --> q
-- | If p is true, then so is p ||| q.
injOrLeft :: forall p q. p --> (p ||| q)
-- | If q is true, then so is p ||| q.
injOrRight :: forall p q. q --> (p ||| q)
instance forall k1 (p :: Data.Type.Predicate.Predicate k1). Data.Type.Predicate.Decidable (Data.Type.Predicate.Impossible Data.Type.Predicate.Logic.==> p)
instance forall k1 (p :: Data.Type.Predicate.Predicate k1). Data.Type.Predicate.Provable (Data.Type.Predicate.Impossible Data.Type.Predicate.Logic.==> p)
instance forall k1 (p :: Data.Type.Predicate.Predicate k1) (q :: Data.Type.Predicate.Predicate k1). (Data.Type.Predicate.Decidable (p Data.Type.Predicate.Logic.==> q), Data.Type.Predicate.Decidable q) => Data.Type.Predicate.Decidable (Data.Type.Predicate.Not q Data.Type.Predicate.Logic.==> Data.Type.Predicate.Not p)
instance forall k1 (p :: Data.Type.Predicate.Predicate k1) (q :: Data.Type.Predicate.Predicate k1). Data.Type.Predicate.Provable (p Data.Type.Predicate.Logic.==> q) => Data.Type.Predicate.Provable (Data.Type.Predicate.Not q Data.Type.Predicate.Logic.==> Data.Type.Predicate.Not p)
instance forall k1 (p :: Data.Type.Predicate.Predicate k1) (q :: Data.Type.Predicate.Predicate k1). Data.Type.Predicate.Decidable ((p Data.Type.Predicate.Logic.&&& q) Data.Type.Predicate.Logic.==> p)
instance forall k1 (p :: Data.Type.Predicate.Predicate k1) (q :: Data.Type.Predicate.Predicate k1). Data.Type.Predicate.Provable ((p Data.Type.Predicate.Logic.&&& q) Data.Type.Predicate.Logic.==> p)
instance forall k1 (p :: Data.Type.Predicate.Predicate k1) (q :: Data.Type.Predicate.Predicate k1). Data.Type.Predicate.Decidable ((p Data.Type.Predicate.Logic.&&& q) Data.Type.Predicate.Logic.==> q)
instance forall k1 (p :: Data.Type.Predicate.Predicate k1) (q :: Data.Type.Predicate.Predicate k1). Data.Type.Predicate.Provable ((p Data.Type.Predicate.Logic.&&& q) Data.Type.Predicate.Logic.==> q)
instance forall k1 (p :: Data.Type.Predicate.Predicate k1). Data.Type.Predicate.Decidable ((p Data.Type.Predicate.Logic.&&& p) Data.Type.Predicate.Logic.==> p)
instance forall k1 (p :: Data.Type.Predicate.Predicate k1). Data.Type.Predicate.Provable ((p Data.Type.Predicate.Logic.&&& p) Data.Type.Predicate.Logic.==> p)
instance forall k1 (p :: Data.Type.Predicate.Predicate k1) (q :: Data.Type.Predicate.Predicate k1). Data.Type.Predicate.Decidable (p Data.Type.Predicate.Logic.==> (p Data.Type.Predicate.Logic.||| q))
instance forall k1 (p :: Data.Type.Predicate.Predicate k1) (q :: Data.Type.Predicate.Predicate k1). Data.Type.Predicate.Provable (p Data.Type.Predicate.Logic.==> (p Data.Type.Predicate.Logic.||| q))
instance forall k1 (q :: Data.Type.Predicate.Predicate k1) (p :: Data.Type.Predicate.Predicate k1). Data.Type.Predicate.Decidable (q Data.Type.Predicate.Logic.==> (p Data.Type.Predicate.Logic.||| q))
instance forall k1 (q :: Data.Type.Predicate.Predicate k1) (p :: Data.Type.Predicate.Predicate k1). Data.Type.Predicate.Provable (q Data.Type.Predicate.Logic.==> (p Data.Type.Predicate.Logic.||| q))
instance forall k1 (p :: Data.Type.Predicate.Predicate k1). Data.Type.Predicate.Decidable (p Data.Type.Predicate.Logic.==> (p Data.Type.Predicate.Logic.||| p))
instance forall k1 (p :: Data.Type.Predicate.Predicate k1). Data.Type.Predicate.Provable (p Data.Type.Predicate.Logic.==> (p Data.Type.Predicate.Logic.||| p))
instance forall k1 (p :: k1 Data.Singletons.Internal.~> *) (q :: k1 Data.Singletons.Internal.~> *). (Data.Type.Predicate.Decidable p, Data.Type.Predicate.Decidable q) => Data.Type.Predicate.Decidable (p Data.Type.Predicate.Logic.||| q)
instance forall k1 (p :: k1 Data.Singletons.Internal.~> *) (q :: k1 Data.Singletons.Internal.~> *). (Data.Type.Predicate.Decidable p, Data.Type.Predicate.Decidable q) => Data.Type.Predicate.Decidable (p Data.Type.Predicate.Logic.&&& q)
instance forall k1 (p :: k1 Data.Singletons.Internal.~> *) (q :: k1 Data.Singletons.Internal.~> *). (Data.Type.Predicate.Provable p, Data.Type.Predicate.Provable q) => Data.Type.Predicate.Provable (p Data.Type.Predicate.Logic.&&& q)
-- | Combinators for working with type-level predicates, along with
-- typeclasses for canonical proofs and deciding functions.
module Data.Type.Universe
-- | A witness for membership of a given item in a type-level collection
-- | In f as is a predicate that a given input a
-- is a member of collection as.
type In (f :: Type -> Type) (as :: f k) = ElemSym1 f as
-- | Typeclass for a type-level container that you can quantify or lift
-- type-level predicates over.
class Universe (f :: Type -> Type)
-- | decideAny, but providing an Elem.
idecideAny :: forall k (p :: k ~> Type) (as :: f k). Universe f => (forall a. Elem f as a -> Sing a -> Decision (p @@ a)) -> (Sing as -> Decision (Any f p @@ as))
-- | decideAll, but providing an Elem.
idecideAll :: forall k (p :: k ~> Type) (as :: f k). Universe f => (forall a. Elem f as a -> Sing a -> Decision (p @@ a)) -> (Sing as -> Decision (All f p @@ as))
-- | genAllA, but providing an Elem.
igenAllA :: forall k (p :: k ~> Type) (as :: f k) h. (Universe f, Applicative h) => (forall a. Elem f as a -> Sing a -> h (p @@ a)) -> (Sing as -> h (All f p @@ as))
-- | Witness an item in a type-level list by providing its index.
data Index :: [k] -> k -> Type
[IZ] :: Index (a : as) a
[IS] :: Index bs a -> Index (b : bs) a
-- | Witness an item in a type-level Maybe by proving the
-- Maybe is Just.
data IJust :: Maybe k -> k -> Type
[IJust] :: IJust ( 'Just a) a
-- | Witness an item in a type-level Either j by proving
-- the Either is Right.
data IRight :: Either j k -> k -> Type
[IRight] :: IRight ( 'Right a) a
-- | Witness an item in a type-level NonEmpty by either indicating
-- that it is the "head", or by providing an index in the "tail".
data NEIndex :: NonEmpty k -> k -> Type
[NEHead] :: NEIndex (a :| as) a
[NETail] :: Index as a -> NEIndex (b :| as) a
-- | Trivially witness an item in the second field of a type-level tuple.
data ISnd :: (j, k) -> k -> Type
[ISnd] :: ISnd '(a, b) b
-- | A pair of indices allows you to index into a nested structure.
data CompElem :: (f :.: g) k -> k -> Type
[:?] :: Elem f ass as -> Elem g as a -> CompElem ( 'Comp ass) a
-- | An All f p is a predicate testing a collection as
-- :: f a for the fact that all items in as satisfy
-- p. Represents the "forall" quantifier over a given universe.
--
-- This is mostly useful for its Decidable, Provable, and
-- TFunctor instances, which lets you lift predicates on
-- p to predicates on All f p.
data All f :: (k ~> Type) -> (f k ~> Type)
-- | A WitAll p as is a witness that the predicate p
-- a is true for all items a in the type-level collection
-- as.
newtype WitAll f p (as :: f k)
WitAll :: forall a. Elem f as a -> p @@ a -> WitAll f p
[runWitAll] :: WitAll f p -> forall a. Elem f as a -> p @@ a
-- | A NotAll f p is a predicate on a collection
-- as that at least one a in as does not
-- satisfy predicate p.
type NotAll f p = (Not (All f p) :: Predicate (f k))
-- | An Any f p is a predicate testing a collection as
-- :: f a for the fact that at least one item in as
-- satisfies p. Represents the "exists" quantifier over a given
-- universe.
--
-- This is mostly useful for its Decidable and TFunctor
-- instances, which lets you lift predicates on p to predicates
-- on Any f p.
data Any f :: (k ~> Type) -> (f k ~> Type)
-- | A WitAny p as is a witness that, for at least one item
-- a in the type-level collection as, the predicate
-- p a is true.
data WitAny f :: (k ~> Type) -> f k -> Type
[WitAny] :: Elem f as a -> p @@ a -> WitAny f p as
-- | A None f p is a predicate on a collection as
-- that no a in as satisfies predicate p.
type None f p = (Not (Any f p) :: Predicate (f k))
-- | Predicate that a given as :: f k is empty and has no items in
-- it.
type Null f = (None f Evident :: Predicate (f k))
-- | Predicate that a given as :: f k is not empty, and has at
-- least one item in it.
type NotNull f = (Any f Evident :: Predicate (f k))
-- | Test that a Maybe is Just.
type IsJust = (NotNull Maybe :: Predicate (Maybe k))
-- | Test that a Maybe is Nothing.
type IsNothing = (Null Maybe :: Predicate (Maybe k))
-- | Test that an Either is Right
type IsRight = (NotNull (Either j) :: Predicate (Either j k))
-- | Test that an Either is Left
type IsLeft = (Null (Either j) :: Predicate (Either j k))
-- | Lifts a predicate p on an individual a into a
-- predicate that on a collection as that is true if and only if
-- any item in as satisfies the original predicate.
--
-- That is, it turns a predicate of kind k ~> Type into a
-- predicate of kind f k ~> Type.
--
-- Essentially tests existential quantification.
decideAny :: forall f k (p :: k ~> Type). Universe f => Decide p -> Decide (Any f p)
-- | Lifts a predicate p on an individual a into a
-- predicate that on a collection as that is true if and only if
-- all items in as satisfies the original predicate.
--
-- That is, it turns a predicate of kind k ~> Type into a
-- predicate of kind f k ~> Type.
--
-- Essentially tests universal quantification.
decideAll :: forall f k (p :: k ~> Type). Universe f => Decide p -> Decide (All f p)
-- | If p a is true for all values a in as under
-- some (Applicative) context h, then you can create an
-- All p as under that Applicative context h.
--
-- Can be useful with Identity (which is basically unwrapping and
-- wrapping All), or with Maybe (which can express
-- predicates that are either provably true or not provably false).
--
-- In practice, this can be used to iterate and traverse and sequence
-- actions over all "items" in as.
genAllA :: forall f k (p :: k ~> Type) (as :: f k) h. (Universe f, Applicative h) => (forall a. Sing a -> h (p @@ a)) -> (Sing as -> h (All f p @@ as))
-- | If p a is true for all values a in as, then
-- we have All p as. Basically witnesses the definition
-- of All.
genAll :: forall f k (p :: k ~> Type). Universe f => Prove p -> Prove (All f p)
-- | genAll, but providing an Elem.
igenAll :: forall f k (p :: k ~> Type) (as :: f k). Universe f => (forall a. Elem f as a -> Sing a -> p @@ a) -> (Sing as -> All f p @@ as)
-- | A foldMap over all items in a collection.
foldMapUni :: forall f k (as :: f k) m. (Universe f, Monoid m) => (forall (a :: k). Sing a -> m) -> Sing as -> m
-- | foldMapUni but with access to the index.
ifoldMapUni :: forall f k (as :: f k) m. (Universe f, Monoid m) => (forall a. Elem f as a -> Sing a -> m) -> Sing as -> m
-- | Extract the item from the container witnessed by the Elem
index :: forall f as a. Universe f => Elem f as a -> Sing as -> Sing a
-- | Automatically generate a witness for a member, if possible
pickElem :: forall f k (as :: f k) a. (Universe f, SingI as, SingI a, SDecide k) => Decision (Elem f as a)
-- | Compose two Functors. Is the same as Compose and :.:,
-- except with a singleton and meant to be used at the type level. Will
-- be redundant if either of the above gets brought into the singletons
-- library.
--
-- Note that because this is a higher-kinded data constructor, there is
-- no SingKind instance; if you need fromSing and
-- toSing, try going through Comp and getComp and
-- SComp and sGetComp.
data ( f (:.:) g ) a
Comp :: f (g a) -> (:.:) f g a
[getComp] :: (:.:) f g a -> f (g a)
-- | The singleton kind-indexed data family.
-- | Singletonized witness for GetComp
sGetComp :: Sing a -> Sing (GetComp a)
-- | getComp lifted to the type level
-- | Turn a composition of All into an All of a composition.
allComp :: All f (All g p) @@ as -> All (f :.: g) p @@ 'Comp as
-- | Turn an All of a composition into a composition of All.
compAll :: All (f :.: g) p @@ 'Comp as -> All f (All g p) @@ as
-- | Turn a composition of Any into an Any of a composition.
anyComp :: Any f (Any g p) @@ as -> Any (f :.: g) p @@ 'Comp as
-- | Turn an Any of a composition into a composition of Any.
compAny :: Any (f :.: g) p @@ 'Comp as -> Any f (Any g p) @@ as
data ElemSym0 (f :: Type -> Type) :: f k ~> k ~> Type
data ElemSym1 (f :: Type -> Type) :: f k -> k ~> Type
type ElemSym2 (f :: Type -> Type) (as :: f k) (a :: k) = Elem f as a
data GetCompSym0 :: (f :.: g) k ~> f (g k)
type GetCompSym1 a = GetComp a
instance forall k1 (f :: k1 -> *) k2 (g :: k2 -> k1) (a :: k2). GHC.Generics.Generic ((Data.Type.Universe.:.:) f g a)
instance (Data.Foldable.Foldable f, Data.Foldable.Foldable g) => Data.Foldable.Foldable (f Data.Type.Universe.:.: g)
instance (GHC.Base.Functor f, GHC.Base.Functor g) => GHC.Base.Functor (f Data.Type.Universe.:.: g)
instance forall k1 (f :: k1 -> *) k2 (g :: k2 -> k1) (a :: k2). GHC.Classes.Ord (f (g a)) => GHC.Classes.Ord ((Data.Type.Universe.:.:) f g a)
instance forall k1 (f :: k1 -> *) k2 (g :: k2 -> k1) (a :: k2). GHC.Classes.Eq (f (g a)) => GHC.Classes.Eq ((Data.Type.Universe.:.:) f g a)
instance forall k1 (f :: k1 -> *) k2 (g :: k2 -> k1) (a :: k2). GHC.Show.Show (f (g a)) => GHC.Show.Show ((Data.Type.Universe.:.:) f g a)
instance forall k (as :: [k]) (a :: k). GHC.Show.Show (Data.Type.Universe.Index as a)
instance forall k (as :: GHC.Base.Maybe k) (a :: k). GHC.Show.Show (Data.Type.Universe.IJust as a)
instance forall j k (as :: Data.Either.Either j k) (a :: k). GHC.Show.Show (Data.Type.Universe.IRight as a)
instance forall k (as :: GHC.Base.NonEmpty k) (a :: k). GHC.Show.Show (Data.Type.Universe.NEIndex as a)
instance forall j k (as :: (j, k)) (a :: k). GHC.Show.Show (Data.Type.Universe.ISnd as a)
instance (Data.Traversable.Traversable f, Data.Traversable.Traversable g) => Data.Traversable.Traversable (f Data.Type.Universe.:.: g)
instance (Data.Type.Universe.Universe f, Data.Type.Universe.Universe g) => Data.Type.Universe.Universe (f Data.Type.Universe.:.: g)
instance forall k1 (f :: k1 -> *) k2 (g :: k2 -> k1) (a :: k2) (ass :: f (g a)). Data.Singletons.Internal.SingI ass => Data.Singletons.Internal.SingI ('Data.Type.Universe.Comp ass)
instance forall j k (as :: (j, k)). (Data.Singletons.Internal.SingI as, Data.Singletons.Decide.SDecide k) => Data.Type.Predicate.Decidable (Data.Type.Predicate.TyPred (Data.Type.Universe.ISnd as))
instance Data.Type.Universe.Universe ((,) j)
instance forall k (as :: GHC.Base.NonEmpty k). (Data.Singletons.Internal.SingI as, Data.Singletons.Decide.SDecide k) => Data.Type.Predicate.Decidable (Data.Type.Predicate.TyPred (Data.Type.Universe.NEIndex as))
instance Data.Type.Universe.Universe GHC.Base.NonEmpty
instance forall j k (as :: Data.Either.Either j k). (Data.Singletons.Internal.SingI as, Data.Singletons.Decide.SDecide k) => Data.Type.Predicate.Decidable (Data.Type.Predicate.TyPred (Data.Type.Universe.IRight as))
instance Data.Type.Universe.Universe (Data.Either.Either j)
instance forall k (as :: GHC.Base.Maybe k). (Data.Singletons.Internal.SingI as, Data.Singletons.Decide.SDecide k) => Data.Type.Predicate.Decidable (Data.Type.Predicate.TyPred (Data.Type.Universe.IJust as))
instance Data.Type.Universe.Universe GHC.Base.Maybe
instance forall k (as :: [k]). (Data.Singletons.Internal.SingI as, Data.Singletons.Decide.SDecide k) => Data.Type.Predicate.Decidable (Data.Type.Predicate.TyPred (Data.Type.Universe.Index as))
instance Data.Type.Universe.Universe []
instance forall k (f :: * -> *) (p :: k Data.Singletons.Internal.~> *). (Data.Type.Universe.Universe f, Data.Type.Predicate.Provable p) => Data.Type.Predicate.Decidable (Data.Type.Universe.NotNull f Data.Type.Predicate.Logic.==> Data.Type.Universe.Any f p)
instance forall k (p :: k Data.Singletons.Internal.~> *) (f :: * -> *). Data.Type.Predicate.Provable p => Data.Type.Predicate.Provable (Data.Type.Universe.NotNull f Data.Type.Predicate.Logic.==> Data.Type.Universe.Any f p)
instance forall k (f :: * -> *) (p :: k Data.Singletons.Internal.~> *). (Data.Type.Universe.Universe f, Data.Type.Predicate.Decidable p) => Data.Type.Predicate.Decidable (Data.Type.Universe.Any f p)
instance forall k (f :: * -> *) (p :: k Data.Singletons.Internal.~> *). (Data.Type.Universe.Universe f, Data.Type.Predicate.Decidable p) => Data.Type.Predicate.Decidable (Data.Type.Universe.All f p)
instance forall k (f :: * -> *) (p :: k Data.Singletons.Internal.~> *). (Data.Type.Universe.Universe f, Data.Type.Predicate.Provable p) => Data.Type.Predicate.Provable (Data.Type.Universe.All f p)
instance Data.Type.Universe.Universe f => Data.Type.Predicate.TFunctor (Data.Type.Universe.Any f)
instance Data.Type.Universe.Universe f => Data.Type.Predicate.TFunctor (Data.Type.Universe.All f)
instance Data.Type.Universe.Universe f => Data.Type.Predicate.DFunctor (Data.Type.Universe.All f)
-- | Higher-level predicates for quantifying predicates over universes and
-- sets.
module Data.Type.Predicate.Quantification
-- | An Any f p is a predicate testing a collection as
-- :: f a for the fact that at least one item in as
-- satisfies p. Represents the "exists" quantifier over a given
-- universe.
--
-- This is mostly useful for its Decidable and TFunctor
-- instances, which lets you lift predicates on p to predicates
-- on Any f p.
data Any f :: (k ~> Type) -> (f k ~> Type)
-- | A WitAny p as is a witness that, for at least one item
-- a in the type-level collection as, the predicate
-- p a is true.
data WitAny f :: (k ~> Type) -> f k -> Type
[WitAny] :: Elem f as a -> p @@ a -> WitAny f p as
-- | It is impossible for any value in a collection to be
-- Impossible.
anyImpossible :: Universe f => Any f Impossible --> Impossible
-- | Lifts a predicate p on an individual a into a
-- predicate that on a collection as that is true if and only if
-- any item in as satisfies the original predicate.
--
-- That is, it turns a predicate of kind k ~> Type into a
-- predicate of kind f k ~> Type.
--
-- Essentially tests existential quantification.
decideAny :: forall f k (p :: k ~> Type). Universe f => Decide p -> Decide (Any f p)
-- | decideAny, but providing an Elem.
idecideAny :: forall k (p :: k ~> Type) (as :: f k). Universe f => (forall a. Elem f as a -> Sing a -> Decision (p @@ a)) -> (Sing as -> Decision (Any f p @@ as))
-- | Lifts a predicate p on an individual a into a
-- predicate that on a collection as that is true if and only if
-- no item in as satisfies the original predicate.
--
-- That is, it turns a predicate of kind k ~> Type into a
-- predicate of kind f k ~> Type.
decideNone :: forall f k (p :: k ~> Type). Universe f => Decide p -> Decide (None f p)
-- | decideNone, but providing an Elem.
idecideNone :: forall f k (p :: k ~> Type) (as :: f k). Universe f => (forall a. Elem f as a -> Sing a -> Decision (p @@ a)) -> (Sing as -> Decision (None f p @@ as))
-- | A None f p is a predicate on a collection as
-- that no a in as satisfies predicate p.
type None f p = (Not (Any f p) :: Predicate (f k))
-- | If p is false for all a in as, then no
-- a in as satisfies p.
allNotNone :: All f (Not p) --> None f p
-- | If no a in as satisfies p, then p
-- is false for all a in as. Requires
-- Decidable p to interrogate the input disproof.
noneAllNot :: forall f p. (Universe f, Decidable p) => None f p --> All f (Not p)
-- | If there exists an a s.t. p a, and if p
-- implies q, then there must exist an a s.t. q
-- a.
entailAny :: forall f p q. Universe f => (p --> q) -> (Any f p --> Any f q)
-- | entailAny, but providing an Elem.
ientailAny :: forall f p q as. (Universe f, SingI as) => (forall a. Elem f as a -> Sing a -> p @@ a -> q @@ a) -> Any f p @@ as -> Any f q @@ as
-- | If p implies q under some context h, and if
-- there exists some a such that p a, then there must
-- exist some a such that p q under that context
-- h.
--
-- h might be something like, say, Maybe, to give
-- predicate that is either provably true or unprovably false.
--
-- Note that it is not possible to do this with p a ->
-- Decision (q a). This is if the p a ->
-- Decision (q a) implication is false, there it doesn't mean
-- that there is no a such that q a,
-- necessarily. There could have been an a where p does
-- not hold, but q does.
entailAnyF :: forall f p q h. (Universe f, Functor h) => (p --># q) h -> (Any f p --># Any f q) h
-- | entailAnyF, but providing an Elem.
ientailAnyF :: forall f p q as h. Functor h => (forall a. Elem f as a -> p @@ a -> h (q @@ a)) -> Any f p @@ as -> h (Any f q @@ as)
-- | Turn a composition of All into an All of a composition.
allComp :: All f (All g p) @@ as -> All (f :.: g) p @@ 'Comp as
-- | Turn an All of a composition into a composition of All.
compAll :: All (f :.: g) p @@ 'Comp as -> All f (All g p) @@ as
-- | An All f p is a predicate testing a collection as
-- :: f a for the fact that all items in as satisfy
-- p. Represents the "forall" quantifier over a given universe.
--
-- This is mostly useful for its Decidable, Provable, and
-- TFunctor instances, which lets you lift predicates on
-- p to predicates on All f p.
data All f :: (k ~> Type) -> (f k ~> Type)
-- | A WitAll p as is a witness that the predicate p
-- a is true for all items a in the type-level collection
-- as.
newtype WitAll f p (as :: f k)
WitAll :: forall a. Elem f as a -> p @@ a -> WitAll f p
[runWitAll] :: WitAll f p -> forall a. Elem f as a -> p @@ a
-- | Lifts a predicate p on an individual a into a
-- predicate that on a collection as that is true if and only if
-- all items in as satisfies the original predicate.
--
-- That is, it turns a predicate of kind k ~> Type into a
-- predicate of kind f k ~> Type.
--
-- Essentially tests universal quantification.
decideAll :: forall f k (p :: k ~> Type). Universe f => Decide p -> Decide (All f p)
-- | decideAll, but providing an Elem.
idecideAll :: forall k (p :: k ~> Type) (as :: f k). Universe f => (forall a. Elem f as a -> Sing a -> Decision (p @@ a)) -> (Sing as -> Decision (All f p @@ as))
-- | A NotAll f p is a predicate on a collection
-- as that at least one a in as does not
-- satisfy predicate p.
type NotAll f p = (Not (All f p) :: Predicate (f k))
-- | If any a in as does not satisfy p, then not
-- all a in as satisfy p.
anyNotNotAll :: Any f (Not p) --> NotAll f p
-- | If not all a in as satisfy p, then there
-- must be at least one a in as that does not satisfy
-- p. Requires Decidable p in order to locate
-- that specific a.
notAllAnyNot :: forall f p. (Universe f, Decidable p) => NotAll f p --> Any f (Not p)
-- | If for all a we have p a, and if p implies
-- q, then for all a we must also have p a.
entailAll :: forall f p q. Universe f => (p --> q) -> (All f p --> All f q)
-- | entailAll, but providing an Elem.
ientailAll :: forall f p q as. (Universe f, SingI as) => (forall a. Elem f as a -> Sing a -> p @@ a -> q @@ a) -> All f p @@ as -> All f q @@ as
-- | If p implies q under some context h, and if
-- we have p a for all a, then we must have q
-- a for all a under context h.
entailAllF :: forall f p q h. (Universe f, Applicative h) => (p --># q) h -> (All f p --># All f q) h
-- | entailAllF, but providing an Elem.
ientailAllF :: forall f p q as h. (Universe f, Applicative h, SingI as) => (forall a. Elem f as a -> p @@ a -> h (q @@ a)) -> All f p @@ as -> h (All f q @@ as)
-- | If we have p a for all a, and p a can be
-- used to test for q a, then we can test all as for
-- q a.
decideEntailAll :: forall f p q. Universe f => p -?> q -> All f p -?> All f q
-- | entailAllF, but providing an Elem.
idecideEntailAll :: forall f p q as. (Universe f, SingI as) => (forall a. Elem f as a -> p @@ a -> Decision (q @@ a)) -> All f p @@ as -> Decision (All f q @@ as)
-- | Turn a composition of Any into an Any of a composition.
anyComp :: Any f (Any g p) @@ as -> Any (f :.: g) p @@ 'Comp as
-- | Turn an Any of a composition into a composition of Any.
compAny :: Any (f :.: g) p @@ 'Comp as -> Any f (Any g p) @@ as
-- | Manipulate "parameterized predicates". See ParamPred and
-- Found for more information.
module Data.Type.Predicate.Param
-- | A parameterized predicate. See Found for more information.
type ParamPred k v = k -> Predicate v
-- | Flip the arguments of a ParamPred.
data FlipPP :: ParamPred v k -> ParamPred k v
-- | Promote a Predicate v to a ParamPred k
-- v, ignoring the k input.
data ConstPP :: Predicate v -> ParamPred k v
-- | Pre-compose a function to a ParamPred. Is essentially
-- flip (.), but unfortunately defunctionalization
-- doesn't work too well with that definition.
data PPMap :: (k ~> j) -> ParamPred j v -> ParamPred k v
-- | A ParamPred (f k) k. Parameterized on an as :: f
-- k, returns a predicate that is true if there exists any a ::
-- k in as.
--
-- Essentially NotNull.
type InP f = (ElemSym1 f :: ParamPred (f k) k)
-- | AnyMatch f takes a parmaeterized predicate on
-- k (testing for a v) and turns it into a
-- parameterized predicate on f k (testing for a v). It
-- "lifts" the domain into f.
--
-- An AnyMatch f p as is a predicate taking an argument
-- a and testing if p a :: Predicate k is
-- satisfied for any item in as :: f k.
--
-- A ParamPred k v tests if a k can create some
-- v. The resulting ParamPred (f k) v tests if
-- any k in f k can create some v.
data AnyMatch f :: ParamPred k v -> ParamPred (f k) v
-- | Convert a parameterized predicate into a predicate on the parameter.
--
-- A Found p is a predicate on p :: ParamPred
-- k v that tests a k for the fact that there exists a
-- v where ParamPred k v is satisfied.
--
-- Intended as the basic interface for ParamPred, since it turns a
-- ParamPred into a normal Predicate, which can have
-- Decidable and Provable instances.
--
-- For some context, an instance of Provable (Found
-- P), where P :: ParamPred k v, means that for any
-- input x :: k, we can always find a y :: v such that
-- we have P x @@ y.
--
-- In the language of quantifiers, it means that forall x :: k,
-- there exists a y :: v such that P x @@ y.
--
-- For an instance of Decidable (Found P), it
-- means that for all x :: k, we can prove or disprove the fact
-- that there exists a y :: v such that P x @@ y.
data Found :: ParamPred k v -> Predicate k
-- | Convert a parameterized predicate into a predicate on the parameter.
--
-- A Found p is a predicate on p :: ParamPred
-- k v that tests a k for the fact that there cannot
-- exist a v where ParamPred k v is
-- satisfied. That is, NotFound P @@ x is satisfied if no
-- y :: v can exist where P x @@ y is satisfied.
--
-- For some context, an instance of Provable (NotFound
-- P), where P :: ParamPred k v, means that for any
-- input x :: k, we can always reject any y :: v that
-- claims to satisfy P x @@ y.
--
-- In the language of quantifiers, it means that forall x :: k,
-- there does not exist a y :: v such that P x @@ y.
--
-- For an instance of Decidable (Found P), it
-- means that for all x :: k, we can prove or disprove the fact
-- that there does not exist a y :: v such that P x @@
-- y.
type NotFound (p :: ParamPred k v) = (Not (Found p) :: Predicate k)
-- | A constraint that a ParamPred k v s "selectable". It
-- means that for any input x :: k, we can always find a y
-- :: v that satisfies P x @@ y. We can "select" that
-- y, no matter what.
type Selectable p = Provable (Found p)
-- | The proving/selecting function for Selectable p.
--
-- Must be called by applying the ParamPred:
--
--
-- select @p
--
select :: forall p. Selectable p => Prove (Found p)
-- | A constraint that a ParamPred k v is "searchable". It
-- means that for any input x :: k, we can prove or disprove
-- that there exists a y :: v that satisfies P x @@ y.
-- We can "search" for that y, and prove that it can or cannot
-- be found.
type Searchable p = Decidable (Found p)
-- | The deciding/searching function for Searchable p.
--
-- Must be called by applying the ParamPred:
--
--
-- search @p
--
search :: forall p. Searchable p => Decide (Found p)
-- | NotNull f is basically Found (InP
-- f).
inPNotNull :: Found (InP f) --> NotNull f
-- | NotNull f is basically Found (InP
-- f).
notNullInP :: NotNull f --> Found (InP f)
instance forall k v (f :: * -> *) (p :: Data.Type.Predicate.Param.ParamPred k v). (Data.Type.Universe.Universe f, Data.Type.Predicate.Decidable (Data.Type.Predicate.Param.Found p)) => Data.Type.Predicate.Decidable (Data.Type.Predicate.Param.Found (Data.Type.Predicate.Param.AnyMatch f p))
instance Data.Type.Universe.Universe f => Data.Type.Predicate.Decidable (Data.Type.Predicate.Param.Found (Data.Type.Predicate.Param.InP f))
instance Data.Type.Predicate.Decidable (Data.Type.Universe.NotNull f Data.Type.Predicate.Logic.==> Data.Type.Predicate.Param.Found (Data.Type.Predicate.Param.InP f))
instance Data.Type.Predicate.Provable (Data.Type.Universe.NotNull f Data.Type.Predicate.Logic.==> Data.Type.Predicate.Param.Found (Data.Type.Predicate.Param.InP f))
instance Data.Type.Predicate.Decidable (Data.Type.Predicate.Param.Found (Data.Type.Predicate.Param.InP f) Data.Type.Predicate.Logic.==> Data.Type.Universe.NotNull f)
instance Data.Type.Predicate.Provable (Data.Type.Predicate.Param.Found (Data.Type.Predicate.Param.InP f) Data.Type.Predicate.Logic.==> Data.Type.Universe.NotNull f)
instance forall j v k (p :: Data.Type.Predicate.Param.ParamPred j v) (f :: k Data.Singletons.Internal.~> j). (Data.Type.Predicate.Decidable (Data.Type.Predicate.Param.Found p), Data.Singletons.Internal.SingI f) => Data.Type.Predicate.Decidable (Data.Type.Predicate.Param.Found (Data.Type.Predicate.Param.PPMap f p))
instance forall j v k (p :: Data.Type.Predicate.Param.ParamPred j v) (f :: k Data.Singletons.Internal.~> j). (Data.Type.Predicate.Provable (Data.Type.Predicate.Param.Found p), Data.Singletons.Internal.SingI f) => Data.Type.Predicate.Provable (Data.Type.Predicate.Param.Found (Data.Type.Predicate.Param.PPMap f p))
-- | Useful utilities for situations where you know that a predicate
-- P is satisfied for a specific a at compile-time.
module Data.Type.Predicate.Auto
-- | Automatically generate a witness for predicate p applied to
-- input a.
--
-- Mostly useful for situations where you know a at
-- compile-time, so you can just write auto directly in your
-- source code. The choice is intended to mirror the auto
-- keyword in languages like Idris.
--
-- Very close in nature to the Known typeclass in the
-- type-combinators library.
--
-- Admittedly this interface is a bit clunky and ad-hoc; at this point
-- you can just try writing auto in your code and praying that it
-- works. You always have the option, of course, to just manually write
-- proofs. If you have any inference rules to suggest, feel free to
-- submit a PR!
--
-- An important limitation of Auto is the Haskell type system
-- prevents "either-or" constraints; this could potentially be
-- implemented using compiler plugins.
--
-- One consequence of this is that it is impossible to automatically
-- derive Any f p and Not (All f
-- p).
--
-- For these, the compiler needs help; you can use autoAny and
-- autoNotAll for these situations.
class Auto (p :: Predicate k) (a :: k)
-- | Have the compiler generate a witness for p @@ a.
--
-- Must be called using type application syntax:
--
--
-- auto _ p @a
--
auto :: Auto p a => p @@ a
-- | An AutoNot p a constraint means that p @@ a
-- can be proven to not be true at compiletime.
type AutoNot (p :: Predicate k) = Auto (Not p)
-- | Disprove p @@ a at compiletime.
--
--
-- autoNot _ p a :: Not p @ a
--
autoNot :: forall k (p :: Predicate k) (a :: k). AutoNot p a => Not p @@ a
-- | Helper "predicate transformer" that gives you an instant auto
-- for any Provable instance.
--
-- For example, say you have predicate P that you know is
-- Provable, and you wish to generate a P @@ x, for some
-- specific x you know at compile-time. You can use:
--
--
-- auto _ (AutoProvable P) @x
--
--
-- to obtain a P @@ x.
--
-- AutoProvable is essentially the identity function.
data AutoProvable :: Predicate k -> Predicate k
-- | Typeclass representing Elems pointing to an a :: k
-- that can be generated automatically from type-level collection as
-- :: f k.
--
-- If GHC knows both the type-level collection and the element you want
-- to find at compile-time, this instance should allow it to find it.
--
-- Used to help in the instance of Auto for the In
-- predicate.
--
-- Example usage:
--
--
-- autoElem :: Index '[1,6,2,3] 2
-- -- IS (IS IZ) -- third spot
--
--
-- And when used with Auto:
--
--
-- auto _ (In [] '[1,6,2,3]) @2
-- -- IS (IS IZ)
--
class AutoElem f (as :: f k) (a :: k)
-- | Generate the Elem pointing to the a :: in a
-- type-level collection as :: f k.
autoElem :: AutoElem f as a => Elem f as a
-- | Helper class for deriving Auto instances for All
-- predicates; each Universe instance is expected to implement
-- these if possible, to get free Auto instaces for their
-- All predicates.
--
-- Also helps for Not Any predicates and Not
-- Found AnyMatch predicates.
class AutoAll f (p :: Predicate k) (as :: f k)
-- | Generate an All for a given predicate over all items in
-- as.
autoAll :: AutoAll f p as => All f p @@ as
-- | Helper function to generate an Any f p if you can pick
-- out a specific a in as where the predicate is
-- provable at compile-time.
--
-- This is used to get around a fundamental limitation of Auto as
-- a Haskell typeclass.
autoAny :: forall f p as a. Auto p a => Elem f as a -> Any f p @@ as
-- | Helper function to generate a Not (All f p) if
-- you can pick out a specific a in as where the
-- predicate is disprovable at compile-time.
--
-- This is used to get around a fundamental limitation of Auto as
-- a Haskell typeclass.
autoNotAll :: forall p f as a. (AutoNot p a, SingI as) => Elem f as a -> Not (All f p) @@ as
instance forall k j (p :: Data.Type.Predicate.Predicate j) (f :: k Data.Singletons.Internal.~> j) (a :: k). Data.Type.Predicate.Auto.AutoNot p (f Data.Singletons.Internal.@@ a) => Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.Not (Data.Type.Predicate.PMap f p)) a
instance forall k (p :: Data.Type.Predicate.Predicate k). Data.Type.Predicate.Auto.AutoAll [] p '[]
instance forall a1 (p :: Data.Type.Predicate.Predicate a1) (a2 :: a1) (as :: [a1]). (Data.Type.Predicate.Auto.Auto p a2, Data.Type.Predicate.Auto.AutoAll [] p as) => Data.Type.Predicate.Auto.AutoAll [] p (a2 : as)
instance forall k (p :: Data.Type.Predicate.Predicate k). Data.Type.Predicate.Auto.AutoAll GHC.Base.Maybe p 'GHC.Base.Nothing
instance forall a1 (p :: Data.Type.Predicate.Predicate a1) (a2 :: a1). Data.Type.Predicate.Auto.Auto p a2 => Data.Type.Predicate.Auto.AutoAll GHC.Base.Maybe p ('GHC.Base.Just a2)
instance forall k j (p :: Data.Type.Predicate.Predicate k) (e :: j). Data.Type.Predicate.Auto.AutoAll (Data.Either.Either j) p ('Data.Either.Left e)
instance forall b (p :: Data.Type.Predicate.Predicate b) (a :: b) j. Data.Type.Predicate.Auto.Auto p a => Data.Type.Predicate.Auto.AutoAll (Data.Either.Either j) p ('Data.Either.Right a)
instance forall a1 (p :: Data.Type.Predicate.Predicate a1) (a2 :: a1) (as :: [a1]). (Data.Type.Predicate.Auto.Auto p a2, Data.Type.Predicate.Auto.AutoAll [] p as) => Data.Type.Predicate.Auto.AutoAll GHC.Base.NonEmpty p (a2 'GHC.Base.:| as)
instance forall a (f :: * -> *) (g :: * -> *) (p :: a Data.Singletons.Internal.~> *) (ass :: f (g a)). Data.Type.Predicate.Auto.AutoAll f (Data.Type.Universe.All g p) ass => Data.Type.Predicate.Auto.AutoAll (f Data.Type.Universe.:.: g) p ('Data.Type.Universe.Comp ass)
instance forall k (p :: Data.Type.Predicate.Predicate k) (a :: k) j (w :: j). Data.Type.Predicate.Auto.Auto p a => Data.Type.Predicate.Auto.AutoAll ((,) j) p '(w, a)
instance forall k (f :: * -> *) (p :: Data.Type.Predicate.Predicate k) (as :: f k). Data.Type.Predicate.Auto.AutoAll f p as => Data.Type.Predicate.Auto.Auto (Data.Type.Universe.All f p) as
instance forall k (f :: * -> *) (as :: f k) (p :: Data.Type.Predicate.Predicate k). (Data.Singletons.Internal.SingI as, Data.Type.Predicate.Auto.AutoAll f (Data.Type.Predicate.Not p) as) => Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.Not (Data.Type.Universe.Any f p)) as
instance forall v k (f :: * -> *) (as :: f k) (p :: Data.Type.Predicate.Param.ParamPred k v). (Data.Singletons.Internal.SingI as, Data.Type.Predicate.Auto.AutoAll f (Data.Type.Predicate.Not (Data.Type.Predicate.Param.Found p)) as) => Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.Not (Data.Type.Predicate.Param.Found (Data.Type.Predicate.Param.AnyMatch f p))) as
instance forall k (a :: k) (as :: [k]). Data.Type.Predicate.Auto.AutoElem [] (a : as) a
instance forall k (as :: [k]) (a :: k) (b :: k). Data.Type.Predicate.Auto.AutoElem [] as a => Data.Type.Predicate.Auto.AutoElem [] (b : as) a
instance forall k (a :: k). Data.Type.Predicate.Auto.AutoElem GHC.Base.Maybe ('GHC.Base.Just a) a
instance forall k j (a :: k). Data.Type.Predicate.Auto.AutoElem (Data.Either.Either j) ('Data.Either.Right a) a
instance forall k (a :: k) (as :: [k]). Data.Type.Predicate.Auto.AutoElem GHC.Base.NonEmpty (a 'GHC.Base.:| as) a
instance forall k (as :: [k]) (a :: k) (b :: k). Data.Type.Predicate.Auto.AutoElem [] as a => Data.Type.Predicate.Auto.AutoElem GHC.Base.NonEmpty (b 'GHC.Base.:| as) a
instance forall k j (w :: j) (a :: k). Data.Type.Predicate.Auto.AutoElem ((,) j) '(w, a) a
instance forall k (f :: * -> *) (as :: f k) (a :: k). Data.Type.Predicate.Auto.AutoElem f as a => Data.Type.Predicate.Auto.Auto (Data.Type.Universe.In f as) a
instance forall k (p :: k Data.Singletons.Internal.~> *) (a :: k). (Data.Type.Predicate.Provable p, Data.Singletons.Internal.SingI a) => Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.Auto.AutoProvable p) a
instance forall k (a :: k). Data.Singletons.Internal.SingI a => Data.Type.Predicate.Auto.Auto Data.Type.Predicate.Evident a
instance forall k (a :: k). Data.Singletons.Internal.SingI a => Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.Not Data.Type.Predicate.Impossible) a
instance forall k (a :: k). Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.EqualTo a) a
instance forall k (p :: Data.Type.Predicate.Predicate k) (a :: k) (q :: Data.Type.Predicate.Predicate k). (Data.Type.Predicate.Auto.Auto p a, Data.Type.Predicate.Auto.Auto q a) => Data.Type.Predicate.Auto.Auto (p Data.Type.Predicate.Logic.&&& q) a
instance forall k (q :: Data.Type.Predicate.Predicate k) (a :: k) (p :: Data.Type.Predicate.Predicate k). Data.Type.Predicate.Auto.Auto q a => Data.Type.Predicate.Auto.Auto (p Data.Type.Predicate.Logic.==> q) a
instance forall k (a :: k) (as :: [k]). Data.Singletons.Internal.SingI a => Data.Type.Predicate.Auto.Auto (Data.Type.Universe.NotNull []) (a : as)
instance forall k (a :: k). Data.Singletons.Internal.SingI a => Data.Type.Predicate.Auto.Auto Data.Type.Universe.IsJust ('GHC.Base.Just a)
instance forall j k (a :: k). Data.Singletons.Internal.SingI a => Data.Type.Predicate.Auto.Auto Data.Type.Universe.IsRight ('Data.Either.Right a)
instance forall k (a :: k) (as :: [k]). Data.Singletons.Internal.SingI a => Data.Type.Predicate.Auto.Auto (Data.Type.Universe.NotNull GHC.Base.NonEmpty) (a 'GHC.Base.:| as)
instance forall k (a :: k) j (w :: j). Data.Singletons.Internal.SingI a => Data.Type.Predicate.Auto.Auto (Data.Type.Universe.NotNull ((,) j)) '(w, a)
instance forall k j v (p :: Data.Type.Predicate.Param.ParamPred j v) (f :: k Data.Singletons.Internal.~> j) (a :: k). Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.Param.Found p) (f Data.Singletons.Internal.@@ a) => Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.Param.Found (Data.Type.Predicate.Param.PPMap f p)) a
instance forall k j v (p :: Data.Type.Predicate.Param.ParamPred j v) (f :: k Data.Singletons.Internal.~> j) (a :: k). Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.Param.NotFound p) (f Data.Singletons.Internal.@@ a) => Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.Param.NotFound (Data.Type.Predicate.Param.PPMap f p)) a
instance forall k j (p :: Data.Type.Predicate.Predicate j) (f :: k Data.Singletons.Internal.~> j) (a :: k). Data.Type.Predicate.Auto.Auto p (f Data.Singletons.Internal.@@ a) => Data.Type.Predicate.Auto.Auto (Data.Type.Predicate.PMap f p) a
-- | Represent a decidable subset of a type-level collection.
module Data.Type.Universe.Subset
-- | A Subset f p is a predicate that some decidable subset
-- of an input as is true.
data Subset f :: (k ~> Type) -> (f k ~> Type)
-- | A WitSubset f p as describes a
-- decidable subset of type-level collection as.
newtype WitSubset f p (as :: f k)
WitSubset :: forall a. Elem f as a -> Decision (p @@ a) -> WitSubset f p
[runWitSubset] :: WitSubset f p -> forall a. Elem f as a -> Decision (p @@ a)
-- | Create a Subset from a predicate.
makeSubset :: forall f k p (as :: f k). Universe f => (forall a. Elem f as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Subset f p @@ as
-- | Subset intersection
intersection :: forall f p q. () => ((Subset f p &&& Subset f q) --> Subset f (p &&& q))
-- | Subset union
union :: forall f p q. () => ((Subset f p &&& Subset f q) --> Subset f (p ||| q))
-- | Symmetric subset difference
symDiff :: forall f p q. () => ((Subset f p &&& Subset f q) --> Subset f (p ^^^ q))
-- | Combine two subsets based on a decision function
mergeSubset :: forall f k p q r (as :: f k). () => (forall a. Decision (p @@ a) -> Decision (q @@ a) -> Decision (r @@ a)) -> Subset f p @@ as -> Subset f q @@ as -> Subset f r @@ as
-- | Combine two subsets based on a decision function
imergeSubset :: forall f k p q r (as :: f k). () => (forall a. Elem f as a -> Decision (p @@ a) -> Decision (q @@ a) -> Decision (r @@ a)) -> Subset f p @@ as -> Subset f q @@ as -> Subset f r @@ as
-- | Map a bidirectional implication over a subset described by that
-- implication.
--
-- Implication needs to be bidirectional, or otherwise we can't produce a
-- decidable subset as a result.
mapSubset :: Universe f => (p --> q) -> (q --> p) -> (Subset f p --> Subset f q)
-- | mapSubset, but providing an Elem.
imapSubset :: (forall a. Elem f as a -> p @@ a -> q @@ a) -> (forall a. Elem f as a -> q @@ a -> p @@ a) -> Subset f p @@ as -> Subset f q @@ as
-- | Turn a Subset into a list (or any Alternative) of
-- satisfied predicates.
--
-- List is meant to include no duplicates.
subsetToList :: forall f p t. (Universe f, Alternative t) => (Subset f p --># Any f p) t
-- | Restrict a Subset to a single (arbitrary) member, or fail if
-- none exists.
subsetToAny :: forall f p. Universe f => Subset f p -?> Any f p
-- | Test if a subset is equal to the entire original collection
subsetToAll :: forall f p. Universe f => Subset f p -?> All f p
-- | Test if a subset is empty.
subsetToNone :: forall f p. Universe f => Subset f p -?> None f p
-- | Construct an empty subset.
emptySubset :: forall f as. (Universe f, SingI as) => Subset f Impossible @@ as
-- | Construct a full subset
fullSubset :: forall f as. (Universe f, SingI as) => Subset f Evident @@ as
instance forall k (f :: * -> *) (p :: k Data.Singletons.Internal.~> *). (Data.Type.Universe.Universe f, Data.Type.Predicate.Decidable p) => Data.Type.Predicate.Decidable (Data.Type.Universe.Subset.Subset f p)
instance forall k (f :: * -> *) (p :: k Data.Singletons.Internal.~> *). (Data.Type.Universe.Universe f, Data.Type.Predicate.Decidable p) => Data.Type.Predicate.Provable (Data.Type.Universe.Subset.Subset f p)