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: decidable-0.1.1.0

Documentation

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.

Minimal complete definition

auto

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 :: Predicate k) (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

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

Defined in Data.Type.Predicate.Auto

Methods

auto :: AutoProvable p @@ a

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

Defined in Data.Type.Predicate.Auto

Methods

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

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

Defined in Data.Type.Predicate.Auto

Methods

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

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

Defined in Data.Type.Predicate.Auto

Methods

auto :: In f as @@ a

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)

Minimal complete definition

autoElem

Methods

autoElem :: Elem f as a

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

Instances

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

Defined in Data.Type.Predicate.Auto

Methods

autoElem :: Elem Maybe (Just a) 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 NonEmpty (a :| as :: NonEmpty k) (a :: k)

Defined in Data.Type.Predicate.Auto

Methods

autoElem :: Elem NonEmpty (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 [] (a ': as :: [k]) (a :: k)

Defined in Data.Type.Predicate.Auto

Methods

autoElem :: Elem [] (a ': 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

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 -> *) (a :: k)

Defined in Data.Type.Predicate.Auto

Methods

auto :: AutoProvable p @@ a

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

Defined in Data.Type.Predicate.Auto

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