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

Description

Useful utilities for situations where you know that a predicate P is satisfied for a specific a at compile-time.

Since: 0.1.1.0

Synopsis

Automatically generate witnesses at compile-time

class Auto (p :: Predicate k) (a :: k) where Source #

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.

Methods

auto :: p @@ a Source #

Have the compiler generate a witness for p @@ a.

Must be called using type application syntax:

auto _ p @a

Instances

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

Defined in Data.Type.Predicate.Auto

Methods

auto :: Evident @@ a Source #

Auto (EqualTo a :: Predicate k) (a :: k) Source # 
Instance details

Defined in Data.Type.Predicate.Auto

Methods

auto :: EqualTo a @@ a Source #

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 #

(Provable p, SingI a) => Auto (AutoProvable p :: TyFun k Type -> Type) (a :: k) Source # 
Instance details

Defined in Data.Type.Predicate.Auto

Methods

auto :: AutoProvable p @@ a Source #

AutoElem f as a => Auto (In f as :: TyFun k Type -> Type) (a :: k) Source # 
Instance details

Defined in Data.Type.Predicate.Auto

Methods

auto :: In f as @@ a Source #

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

Defined in Data.Type.Predicate.Auto

Methods

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

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

Defined in Data.Type.Predicate.Auto

Methods

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

Auto (Found p) (f @@ a) => Auto (Found (PPMap f p) :: TyFun k Type -> Type) (a :: k) Source #

Since: 0.1.2.0

Instance details

Defined in Data.Type.Predicate.Auto

Methods

auto :: Found (PPMap f p) @@ a 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 #

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

Since: 0.1.2.0

Instance details

Defined in Data.Type.Predicate.Auto

Methods

auto :: PMap f p @@ a 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 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 => Auto (TyPred (PIdentity (WrappedSing :: k -> Type)) :: Predicate (Identity k)) (as :: Identity k) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate.Auto

(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 => Auto (TyPred (NERec (WrappedSing :: k -> Type)) :: Predicate (NonEmpty k)) (as :: NonEmpty k) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate.Auto

(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 => Auto (TyPred (PMaybe (WrappedSing :: k -> Type)) :: Predicate (Maybe k)) (as :: Maybe k) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate.Auto

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

SingI as => Auto (TyPred (Rec (WrappedSing :: u -> Type)) :: Predicate [u]) (as :: [u]) Source #

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate.Auto

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

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 #

AutoAll f p as => Auto (All 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 :: All f p @@ as 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 => Auto (TyPred (PEither (WrappedSing :: k -> Type) :: 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

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

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

Since: 3.0.0

Instance details

Defined in Data.Type.Predicate.Auto

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 #

autoTC :: forall t a. Auto (TyPred t) a => t a Source #

A version of auto that "just works" with type inference, if the predicate is a type constructor.

Since: 0.2.1.0

type AutoNot (p :: Predicate k) = Auto (Not p) Source #

An AutoNot p a constraint means that p @@ a can be proven to not be true at compiletime.

Since: 0.1.2.0

autoNot :: forall k (p :: Predicate k) (a :: k). AutoNot p a => Not p @@ a Source #

Disprove p @@ a at compiletime.

autoNot @_ @p @a :: Not p @@ a

Since: 0.1.2.0

autoAny :: forall f p as a. Auto p a => Elem f as a -> Any f p @@ as Source #

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.

Since: 0.1.2.0

autoNotAll :: forall p f as a. (AutoNot p a, SingI as) => Elem f as a -> Not (All f p) @@ as Source #

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.

Since: 0.1.2.0

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

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.

Instances

Instances details
(Provable p, SingI a) => Auto (AutoProvable p :: TyFun k Type -> Type) (a :: k) Source # 
Instance details

Defined in Data.Type.Predicate.Auto

Methods

auto :: AutoProvable p @@ a Source #

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

Defined in Data.Type.Predicate.Auto

type Apply (AutoProvable p :: TyFun k1 Type -> Type) (a :: k1) = p @@ a

Helper classes

class AutoElem f (as :: f k) (a :: k) where Source #

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)

Methods

autoElem :: Elem f as a Source #

Generate the Elem pointing to the a :: in a type-level collection as :: f k.

Instances

Instances details
AutoElem Identity ('Identity a :: Identity k) (a :: k) Source # 
Instance details

Defined in Data.Type.Predicate.Auto

AutoElem Maybe ('Just a :: Maybe k) (a :: k) Source # 
Instance details

Defined in Data.Type.Predicate.Auto

Methods

autoElem :: Elem Maybe ('Just a) a Source #

AutoElem NonEmpty (a :| as :: NonEmpty k) (a :: k) Source # 
Instance details

Defined in Data.Type.Predicate.Auto

Methods

autoElem :: Elem NonEmpty (a :| as) a Source #

AutoElem [] as a => AutoElem NonEmpty (b :| as :: NonEmpty k) (a :: k) Source # 
Instance details

Defined in Data.Type.Predicate.Auto

Methods

autoElem :: Elem NonEmpty (b :| as) a Source #

AutoElem [] (a ': as :: [k]) (a :: k) Source # 
Instance details

Defined in Data.Type.Predicate.Auto

Methods

autoElem :: Elem [] (a ': as) a Source #

AutoElem [] as a => AutoElem [] (b ': as :: [k]) (a :: k) Source # 
Instance details

Defined in Data.Type.Predicate.Auto

Methods

autoElem :: Elem [] (b ': as) a Source #

AutoElem (Either j) ('Right a :: Either j k) (a :: k) Source # 
Instance details

Defined in Data.Type.Predicate.Auto

Methods

autoElem :: Elem (Either j) ('Right a) a Source #

AutoElem ((,) j) ('(w, a) :: (j, k)) (a :: k) Source #

Since: 0.1.2.0

Instance details

Defined in Data.Type.Predicate.Auto

Methods

autoElem :: Elem ((,) j) '(w, a) a Source #

class AutoAll f (p :: Predicate k) (as :: f k) where Source #

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.

Since: 0.1.2.0

Methods

autoAll :: All f p @@ as Source #

Generate an All for a given predicate over all items in as.

Instances

Instances details
AutoAll Maybe (p :: Predicate k) ('Nothing :: Maybe k) Source # 
Instance details

Defined in Data.Type.Predicate.Auto

AutoAll [] (p :: Predicate k) ('[] :: [k]) Source # 
Instance details

Defined in Data.Type.Predicate.Auto

Methods

autoAll :: All [] p @@ '[] Source #

Auto p a2 => AutoAll Identity (p :: Predicate a1) ('Identity a2 :: Identity a1) Source # 
Instance details

Defined in Data.Type.Predicate.Auto

Auto p a2 => AutoAll Maybe (p :: Predicate a1) ('Just a2 :: Maybe a1) Source # 
Instance details

Defined in Data.Type.Predicate.Auto

Methods

autoAll :: All Maybe p @@ 'Just a2 Source #

(Auto p a2, AutoAll [] p as) => AutoAll NonEmpty (p :: Predicate a1) (a2 :| as :: NonEmpty a1) Source # 
Instance details

Defined in Data.Type.Predicate.Auto

Methods

autoAll :: All NonEmpty p @@ (a2 :| as) Source #

(Auto p a2, AutoAll [] p as) => AutoAll [] (p :: Predicate a1) (a2 ': as :: [a1]) Source # 
Instance details

Defined in Data.Type.Predicate.Auto

Methods

autoAll :: All [] p @@ (a2 ': as) Source #

Auto p a => AutoAll (Either j) (p :: Predicate b) ('Right a :: Either j b) Source # 
Instance details

Defined in Data.Type.Predicate.Auto

Methods

autoAll :: All (Either j) p @@ 'Right a Source #

AutoAll (Either j) (p :: Predicate k) ('Left e :: Either j k) Source # 
Instance details

Defined in Data.Type.Predicate.Auto

Methods

autoAll :: All (Either j) p @@ 'Left e Source #

Auto p a => AutoAll ((,) j) (p :: Predicate k) ('(w, a) :: (j, k)) Source # 
Instance details

Defined in Data.Type.Predicate.Auto

Methods

autoAll :: All ((,) j) p @@ '(w, a) Source #