decidable-0.1.1.0: Combinators for manipulating dependently-typed predicates.

Copyright(c) Justin Le 2018
LicenseBSD3
Maintainerjustin@jle.im
Stabilityexperimental
Portabilitynon-portable
Safe HaskellNone
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: decidable-0.1.1.0

Synopsis

Documentation

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.

Minimal complete definition

auto

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
SingI a => Auto (Evident :: Predicate k) (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 #

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

Defined in Data.Type.Predicate.Auto

Methods

auto :: AutoProvable p @@ a Source #

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

Defined in Data.Type.Predicate.Auto

Methods

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

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

Defined in Data.Type.Predicate.Auto

Methods

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

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

Defined in Data.Type.Predicate.Auto

Methods

auto :: In f as @@ a Source #

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)

Minimal complete definition

autoElem

Methods

autoElem :: Elem f as a Source #

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

Instances
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 [] 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 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 [] (b ': as :: [k]) (a :: k) Source # 
Instance details

Defined in Data.Type.Predicate.Auto

Methods

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

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
(Provable p, SingI a) => Auto (AutoProvable p :: TyFun k 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 -> *) (a :: k1) Source # 
Instance details

Defined in Data.Type.Predicate.Auto

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