Copyright | (c) Justin Le 2018 |
---|---|
License | BSD3 |
Maintainer | justin@jle.im |
Stability | experimental |
Portability | non-portable |
Safe Haskell | None |
Language | Haskell2010 |
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 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.
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 # | |
Auto (EqualTo a :: Predicate k) (a :: k) Source # | |
(Provable p, SingI a) => Auto (AutoProvable p :: TyFun k Type -> *) (a :: k) Source # | |
Defined in Data.Type.Predicate.Auto auto :: AutoProvable p @@ a Source # | |
Auto q a => Auto (p ==> q :: TyFun k Type -> *) (a :: k) Source # | |
(Auto p a, Auto q a) => Auto (p &&& q :: TyFun k Type -> *) (a :: k) Source # | |
AutoElem f as a => Auto (In f as :: TyFun k Type -> *) (a :: k) Source # | |
class AutoElem f (as :: f k) (a :: k) where Source #
Typeclass representing Elem
s 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)
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 # | |
AutoElem [] as a => AutoElem NonEmpty (b :| as :: NonEmpty k) (a :: k) Source # | |
AutoElem NonEmpty (a :| as :: NonEmpty k) (a :: k) Source # | |
AutoElem [] as a => AutoElem [] (b ': as :: [k]) (a :: k) Source # | |
Defined in Data.Type.Predicate.Auto | |
AutoElem [] (a ': as :: [k]) (a :: k) Source # | |
Defined in Data.Type.Predicate.Auto | |
AutoElem (Either j) (Right a :: Either j k) (a :: k) 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 # | |
Defined in Data.Type.Predicate.Auto auto :: AutoProvable p @@ a Source # | |
type Apply (AutoProvable p :: TyFun k1 Type -> *) (a :: k1) Source # | |
Defined in Data.Type.Predicate.Auto |