Data.Type.Predicate.Auto

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

Automatically generate witnesses at compile-time

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

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

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

Must be called using type application syntax:

auto _ p @a

Instances

SingI a => Auto (Evident :: TyFun k Type -> Type) (a :: k)

Defined in Data.Type.Predicate.Auto

Methods

auto :: Evident @@ a

Auto (EqualTo a :: Predicate k) (a :: k)

Defined in Data.Type.Predicate.Auto

Methods

auto :: EqualTo a @@ a

SingI a => Auto (Not (Impossible :: Predicate k) :: TyFun k Type -> Type) (a :: k)

Since: 0.1.2.0

Defined in Data.Type.Predicate.Auto

Methods

auto :: Not Impossible @@ a

AutoNot p (f @@ a) => Auto (Not (PMap f p) :: TyFun k Type -> Type) (a :: k)

Since: 0.1.2.0

Defined in Data.Type.Predicate.Auto

Methods

auto :: Not (PMap f p) @@ a

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

Defined in Data.Type.Predicate.Auto

Methods

auto :: AutoProvable p @@ a

AutoElem f as a => Auto (In f as :: TyFun k Type -> Type) (a :: k)

Defined in Data.Type.Predicate.Auto

Methods

auto :: In f as @@ a

(Auto p a, Auto q a) => Auto (p &&& q :: TyFun k Type -> Type) (a :: k)

Defined in Data.Type.Predicate.Auto

Methods

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

Auto q a => Auto (p ==> q :: TyFun k Type -> Type) (a :: k)

Defined in Data.Type.Predicate.Auto

Methods

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

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

Since: 0.1.2.0

Defined in Data.Type.Predicate.Auto

Methods

auto :: Found (PPMap f p) @@ a

Auto (NotFound p) (f @@ a) => Auto (NotFound (PPMap f p) :: Predicate k) (a :: k)

Since: 0.1.2.0

Defined in Data.Type.Predicate.Auto

Methods

auto :: NotFound (PPMap f p) @@ a

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

Since: 0.1.2.0

Defined in Data.Type.Predicate.Auto

Methods

auto :: PMap f p @@ a

SingI a => Auto (IsJust :: Predicate (Maybe k)) ('Just a :: Maybe k)

Since: 0.1.2.0

Defined in Data.Type.Predicate.Auto

Methods

auto :: IsJust @@ 'Just a

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

Since: 3.0.0

Defined in Data.Type.Predicate.Auto

Methods

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

SingI as => Auto (TyPred (PIdentity (WrappedSing :: k -> Type)) :: Predicate (Identity k)) (as :: Identity k)

Since: 3.0.0

Defined in Data.Type.Predicate.Auto

Methods

auto :: TyPred (PIdentity WrappedSing) @@ as

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

Since: 3.0.0

Defined in Data.Type.Predicate.Auto

Methods

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

SingI as => Auto (TyPred (NERec (WrappedSing :: k -> Type)) :: Predicate (NonEmpty k)) (as :: NonEmpty k)

Since: 3.0.0

Defined in Data.Type.Predicate.Auto

Methods

auto :: TyPred (NERec WrappedSing) @@ as

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

Since: 3.0.0

Defined in Data.Type.Predicate.Auto

Methods

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

SingI as => Auto (TyPred (PMaybe (WrappedSing :: k -> Type)) :: Predicate (Maybe k)) (as :: Maybe k)

Since: 3.0.0

Defined in Data.Type.Predicate.Auto

Methods

auto :: TyPred (PMaybe WrappedSing) @@ as

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

Since: 3.0.0

Defined in Data.Type.Predicate.Auto

Methods

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

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

Since: 3.0.0

Defined in Data.Type.Predicate.Auto

Methods

auto :: TyPred (Rec WrappedSing) @@ as

(SingI as, AutoAll f (Not (Found p)) as) => Auto (Not (Found (AnyMatch f p)) :: TyFun (f k) Type -> Type) (as :: f k)

Since: 0.1.2.0

Defined in Data.Type.Predicate.Auto

Methods

auto :: Not (Found (AnyMatch f p)) @@ as

(SingI as, AutoAll f (Not p) as) => Auto (Not (Any f p) :: TyFun (f k) Type -> Type) (as :: f k)

Since: 0.1.2.0

Defined in Data.Type.Predicate.Auto

Methods

auto :: Not (Any f p) @@ as

SingI a => Auto (NotNull Identity :: Predicate (Identity k)) ('Identity a :: Identity k)

Defined in Data.Type.Predicate.Auto

Methods

auto :: NotNull Identity @@ 'Identity0 a

SingI a => Auto (NotNull NonEmpty :: Predicate (NonEmpty k)) (a :| as :: NonEmpty k)

Since: 0.1.2.0

Defined in Data.Type.Predicate.Auto

Methods

auto :: NotNull NonEmpty @@ (a :| as)

SingI a => Auto (NotNull [] :: Predicate [k]) (a ': as :: [k])

Since: 0.1.2.0

Defined in Data.Type.Predicate.Auto

Methods

auto :: NotNull [] @@ (a ': as)

AutoAll f p as => Auto (All f p :: TyFun (f k) Type -> Type) (as :: f k)

Since: 0.1.2.0

Defined in Data.Type.Predicate.Auto

Methods

auto :: All f p @@ as

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

Since: 3.0.0

Defined in Data.Type.Predicate.Auto

Methods

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

SingI as => Auto (TyPred (PEither (WrappedSing :: k -> Type) :: Either j k -> Type) :: Predicate (Either j k)) (as :: Either j k)

Since: 3.0.0

Defined in Data.Type.Predicate.Auto

Methods

auto :: TyPred (PEither WrappedSing) @@ as

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

Since: 3.0.0

Defined in Data.Type.Predicate.Auto

Methods

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

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

Since: 3.0.0

Defined in Data.Type.Predicate.Auto

Methods

auto :: TyPred (PTup WrappedSing) @@ as

SingI a => Auto (IsRight :: Predicate (Either j k)) ('Right a :: Either j k)

Since: 0.1.2.0

Defined in Data.Type.Predicate.Auto

Methods

auto :: IsRight @@ 'Right a

SingI a => Auto (NotNull ((,) j) :: Predicate (j, k)) ('(w, a) :: (j, k))

Since: 0.1.2.0

Defined in Data.Type.Predicate.Auto

Methods

auto :: NotNull ((,) j) @@ '(w, a)

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

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)

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

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

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

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

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

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

Defined in Data.Type.Predicate.Auto

Methods

auto :: AutoProvable p @@ a

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

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

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

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

Instances

AutoElem Identity ('Identity a :: Identity k) (a :: k)

Defined in Data.Type.Predicate.Auto

Methods

autoElem :: Elem Identity ('Identity0 a) a

AutoElem Maybe ('Just a :: Maybe k) (a :: k)

Defined in Data.Type.Predicate.Auto

Methods

autoElem :: Elem Maybe ('Just a) a

AutoElem NonEmpty (a :| as :: NonEmpty k) (a :: k)

Defined in Data.Type.Predicate.Auto

Methods

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

AutoElem [] as a => AutoElem NonEmpty (b :| as :: NonEmpty k) (a :: k)

Defined in Data.Type.Predicate.Auto

Methods

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

AutoElem [] (a ': as :: [k]) (a :: k)

Defined in Data.Type.Predicate.Auto

Methods

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

AutoElem [] as a => AutoElem [] (b ': as :: [k]) (a :: k)

Defined in Data.Type.Predicate.Auto

Methods

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

AutoElem (Either j) ('Right a :: Either j k) (a :: k)

Defined in Data.Type.Predicate.Auto

Methods

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

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

Since: 0.1.2.0

Defined in Data.Type.Predicate.Auto

Methods

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

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

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

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

Instances

AutoAll Maybe (p :: Predicate k) ('Nothing :: Maybe k)

Defined in Data.Type.Predicate.Auto

Methods

autoAll :: All Maybe p @@ 'Nothing

AutoAll [] (p :: Predicate k) ('[] :: [k])

Defined in Data.Type.Predicate.Auto

Methods

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

Auto p a2 => AutoAll Identity (p :: Predicate a1) ('Identity a2 :: Identity a1)

Defined in Data.Type.Predicate.Auto

Methods

autoAll :: All Identity p @@ 'Identity0 a2

Auto p a2 => AutoAll Maybe (p :: Predicate a1) ('Just a2 :: Maybe a1)

Defined in Data.Type.Predicate.Auto

Methods

autoAll :: All Maybe p @@ 'Just a2

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

Defined in Data.Type.Predicate.Auto

Methods

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

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

Defined in Data.Type.Predicate.Auto

Methods

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

Auto p a => AutoAll (Either j) (p :: Predicate b) ('Right a :: Either j b)

Defined in Data.Type.Predicate.Auto

Methods

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

AutoAll (Either j) (p :: Predicate k) ('Left e :: Either j k)

Defined in Data.Type.Predicate.Auto

Methods

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

Auto p a => AutoAll ((,) j) (p :: Predicate k) ('(w, a) :: (j, k))

Defined in Data.Type.Predicate.Auto

Methods

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