Data.Type.Universe

Combinators for working with type-level predicates, along with typeclasses for canonical proofs and deciding functions.

Universe

type family Elem (f :: Type -> Type) :: f k -> k -> Type

A witness for membership of a given item in a type-level collection

Instances

type Elem []

Defined in Data.Type.Universe

type Elem [] = (Index :: [k] -> k -> Type)

type Elem Maybe

Defined in Data.Type.Universe

type Elem Maybe = (IJust :: Maybe k -> k -> Type)

type Elem NonEmpty

Defined in Data.Type.Universe

type Elem NonEmpty = (NEIndex :: NonEmpty k -> k -> Type)

type Elem (Either j)

Defined in Data.Type.Universe

type Elem (Either j) = (IRight :: Either j k -> k -> Type)

type Elem ((,) j)

Defined in Data.Type.Universe

type Elem ((,) j) = (ISnd :: (j, k) -> k -> Type)

type Elem (f :.: g)

Defined in Data.Type.Universe

type Elem (f :.: g) = (CompElem :: (f :.: g) k -> k -> Type)

type In (f :: Type -> Type) (as :: f k) = ElemSym1 f as

In f as is a predicate that a given input a is a member of collection as.

class Universe (f :: Type -> Type) where

Typeclass for a type-level container that you can quantify or lift type-level predicates over.

Minimal complete definition

idecideAny, idecideAll, igenAllA

Methods

idecideAny

Arguments

:: forall (p :: k ~> Type) (as :: f k). (forall a. Elem f as a -> Sing a -> Decision (p @@ a))

predicate on value

-> Sing as -> Decision (Any f p @@ as)

predicate on collection

decideAny, but providing an Elem.

idecideAll

Arguments

:: forall (p :: k ~> Type) (as :: f k). (forall a. Elem f as a -> Sing a -> Decision (p @@ a))

predicate on value

-> Sing as -> Decision (All f p @@ as)

predicate on collection

decideAll, but providing an Elem.

igenAllA

Arguments

:: forall (p :: k ~> Type) (as :: f k). Applicative h

=> (forall a. Elem f as a -> Sing a -> h (p @@ a))

predicate on value in context

-> Sing as -> h (All f p @@ as)

predicate on collection in context

genAllA, but providing an Elem.

Instances

Universe []

Defined in Data.Type.Universe

Methods

idecideAny :: (forall (a :: k). Elem [] as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (Any [] p @@ as)

idecideAll :: (forall (a :: k). Elem [] as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (All [] p @@ as)

igenAllA :: Applicative h => (forall (a :: k). Elem [] as a -> Sing a -> h (p @@ a)) -> Sing as -> h (All [] p @@ as)

Universe Maybe

Defined in Data.Type.Universe

Methods

idecideAny :: (forall (a :: k). Elem Maybe as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (Any Maybe p @@ as)

idecideAll :: (forall (a :: k). Elem Maybe as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (All Maybe p @@ as)

igenAllA :: Applicative h => (forall (a :: k). Elem Maybe as a -> Sing a -> h (p @@ a)) -> Sing as -> h (All Maybe p @@ as)

Universe NonEmpty

Defined in Data.Type.Universe

Methods

idecideAny :: (forall (a :: k). Elem NonEmpty as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (Any NonEmpty p @@ as)

idecideAll :: (forall (a :: k). Elem NonEmpty as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (All NonEmpty p @@ as)

igenAllA :: Applicative h => (forall (a :: k). Elem NonEmpty as a -> Sing a -> h (p @@ a)) -> Sing as -> h (All NonEmpty p @@ as)

Universe (Either j)

Defined in Data.Type.Universe

Methods

idecideAny :: (forall (a :: k). Elem (Either j) as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (Any (Either j) p @@ as)

idecideAll :: (forall (a :: k). Elem (Either j) as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (All (Either j) p @@ as)

igenAllA :: Applicative h => (forall (a :: k). Elem (Either j) as a -> Sing a -> h (p @@ a)) -> Sing as -> h (All (Either j) p @@ as)

Universe ((,) j)

Defined in Data.Type.Universe

Methods

idecideAny :: (forall (a :: k). Elem ((,) j) as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (Any ((,) j) p @@ as)

idecideAll :: (forall (a :: k). Elem ((,) j) as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (All ((,) j) p @@ as)

igenAllA :: Applicative h => (forall (a :: k). Elem ((,) j) as a -> Sing a -> h (p @@ a)) -> Sing as -> h (All ((,) j) p @@ as)

(Universe f, Universe g) => Universe (f :.: g)

Defined in Data.Type.Universe

Methods

idecideAny :: (forall (a :: k). Elem (f :.: g) as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (Any (f :.: g) p @@ as)

idecideAll :: (forall (a :: k). Elem (f :.: g) as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (All (f :.: g) p @@ as)

igenAllA :: Applicative h => (forall (a :: k). Elem (f :.: g) as a -> Sing a -> h (p @@ a)) -> Sing as -> h (All (f :.: g) p @@ as)

Instances

data Index :: [k] -> k -> Type where

Witness an item in a type-level list by providing its index.

Constructors

IZ :: Index (a ': as) a

IS :: Index bs a -> Index (b ': bs) a

Instances

(SingI as, SDecide k) => Decidable (TyPred (Index as) :: Predicate k)

Defined in Data.Type.Universe

Methods

decide :: Decide (TyPred (Index as))

Show (Index as a)

Defined in Data.Type.Universe

Methods

showsPrec :: Int -> Index as a -> ShowS

show :: Index as a -> String

showList :: [Index as a] -> ShowS

data IJust :: Maybe k -> k -> Type where

Witness an item in a type-level Maybe by proving the Maybe is Just.

Constructors

IJust :: IJust (Just a) a

Instances

(SingI as, SDecide k) => Decidable (TyPred (IJust as) :: Predicate k)

Defined in Data.Type.Universe

Methods

decide :: Decide (TyPred (IJust as))

Show (IJust as a)

Defined in Data.Type.Universe

Methods

showsPrec :: Int -> IJust as a -> ShowS

show :: IJust as a -> String

showList :: [IJust as a] -> ShowS

data IRight :: Either j k -> k -> Type where

Witness an item in a type-level Either j by proving the Either is Right.

Constructors

IRight :: IRight (Right a) a

Instances

(SingI as, SDecide k) => Decidable (TyPred (IRight as) :: Predicate k)

Defined in Data.Type.Universe

Methods

decide :: Decide (TyPred (IRight as))

Show (IRight as a)

Defined in Data.Type.Universe

Methods

showsPrec :: Int -> IRight as a -> ShowS

show :: IRight as a -> String

showList :: [IRight as a] -> ShowS

data NEIndex :: NonEmpty k -> k -> Type where

Witness an item in a type-level NonEmpty by either indicating that it is the "head", or by providing an index in the "tail".

Constructors

NEHead :: NEIndex (a :| as) a

NETail :: Index as a -> NEIndex (b :| as) a

Instances

(SingI as, SDecide k) => Decidable (TyPred (NEIndex as) :: Predicate k)

Defined in Data.Type.Universe

Methods

decide :: Decide (TyPred (NEIndex as))

Show (NEIndex as a)

Defined in Data.Type.Universe

Methods

showsPrec :: Int -> NEIndex as a -> ShowS

show :: NEIndex as a -> String

showList :: [NEIndex as a] -> ShowS

data ISnd :: (j, k) -> k -> Type where

Trivially witness an item in the second field of a type-level tuple.

Constructors

ISnd :: ISnd '(a, b) b

Instances

(SingI as, SDecide k) => Decidable (TyPred (ISnd as) :: Predicate k)

Defined in Data.Type.Universe

Methods

decide :: Decide (TyPred (ISnd as))

Show (ISnd as a)

Defined in Data.Type.Universe

Methods

showsPrec :: Int -> ISnd as a -> ShowS

show :: ISnd as a -> String

showList :: [ISnd as a] -> ShowS

data CompElem :: (f :.: g) k -> k -> Type where

A pair of indices allows you to index into a nested structure.

Since: decidable-0.1.2.0

Constructors

(:?) :: Elem f ass as -> Elem g as a -> CompElem (Comp ass) a

Predicates

data All f :: (k ~> Type) -> f k ~> Type

An All f p is a predicate testing a collection as :: f a for the fact that all items in as satisfy p. Represents the "forall" quantifier over a given universe.

This is mostly useful for its Decidable, Provable, and TFunctor instances, which lets you lift predicates on p to predicates on All f p.

Instances

Universe f => TFunctor (All f :: (k1 ~> Type) -> TyFun (f k1) Type -> *)

Defined in Data.Type.Universe

Methods

tmap :: (p --> q) -> All f p --> All f q

Universe f => DFunctor (All f :: (k1 ~> Type) -> TyFun (f k1) Type -> *)

Defined in Data.Type.Universe

Methods

dmap :: (p -?> q) -> All f p -?> All f q

(Universe f, Provable p) => Provable (All f p :: TyFun (f k) Type -> *)

Defined in Data.Type.Universe

Methods

prove :: Prove (All f p)

(Universe f, Decidable p) => Decidable (All f p :: TyFun (f k) Type -> *)

Defined in Data.Type.Universe

Methods

decide :: Decide (All f p)

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

Since: decidable-0.1.2.0

Defined in Data.Type.Predicate.Auto

Methods

auto :: All f p @@ as

type Apply (All f p :: TyFun (f k) Type -> *) (as :: f k)

Defined in Data.Type.Universe

type Apply (All f p :: TyFun (f k) Type -> *) (as :: f k) = WitAll f p as

newtype WitAll f p (as :: f k)

A WitAll p as is a witness that the predicate p a is true for all items a in the type-level collection as.

Constructors

WitAll

Fields

• runWitAll :: forall a. Elem f as a -> p @@ a

type NotAll f p = (Not (All f p) :: Predicate (f k))

A NotAll f p is a predicate on a collection as that at least one a in as does not satisfy predicate p.

data Any f :: (k ~> Type) -> f k ~> Type

An Any f p is a predicate testing a collection as :: f a for the fact that at least one item in as satisfies p. Represents the "exists" quantifier over a given universe.

This is mostly useful for its Decidable and TFunctor instances, which lets you lift predicates on p to predicates on Any f p.

Instances

Universe f => TFunctor (Any f :: (k1 ~> Type) -> TyFun (f k1) Type -> *)

Defined in Data.Type.Universe

Methods

tmap :: (p --> q) -> Any f p --> Any f q

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

Since: decidable-0.1.2.0

Defined in Data.Type.Predicate.Auto

Methods

auto :: IsJust @@ Just a

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

Since: decidable-0.1.2.0

Defined in Data.Type.Predicate.Auto

Methods

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

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

Since: decidable-0.1.2.0

Defined in Data.Type.Predicate.Auto

Methods

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

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

Since: decidable-0.1.2.0

Defined in Data.Type.Predicate.Auto

Methods

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

Provable p => Provable ((NotNull f :: Predicate (f k)) ==> Any f p :: TyFun (f k) Type -> *)

Defined in Data.Type.Universe

Methods

prove :: Prove (NotNull f ==> Any f p)

Provable (Found (InP f :: ParamPred (f v) v) ==> (NotNull f :: Predicate (f v)) :: TyFun (f v) Type -> *)

Defined in Data.Type.Predicate.Param

Methods

prove :: Prove (Found (InP f) ==> NotNull f)

Provable ((NotNull f :: Predicate (f k)) ==> Found (InP f :: ParamPred (f k) k) :: TyFun (f k) Type -> *)

Defined in Data.Type.Predicate.Param

Methods

prove :: Prove (NotNull f ==> Found (InP f))

(Universe f, Provable p) => Decidable ((NotNull f :: Predicate (f k)) ==> Any f p :: TyFun (f k) Type -> *)

Defined in Data.Type.Universe

Methods

decide :: Decide (NotNull f ==> Any f p)

(Universe f, Decidable p) => Decidable (Any f p :: TyFun (f k) Type -> *)

Defined in Data.Type.Universe

Methods

decide :: Decide (Any f p)

Decidable (Found (InP f :: ParamPred (f v) v) ==> (NotNull f :: Predicate (f v)) :: TyFun (f v) Type -> *)

Defined in Data.Type.Predicate.Param

Methods

decide :: Decide (Found (InP f) ==> NotNull f)

Decidable ((NotNull f :: Predicate (f k)) ==> Found (InP f :: ParamPred (f k) k) :: TyFun (f k) Type -> *)

Defined in Data.Type.Predicate.Param

Methods

decide :: Decide (NotNull f ==> Found (InP f))

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

Since: decidable-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: decidable-0.1.2.0

Defined in Data.Type.Predicate.Auto

Methods

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

type Apply (Any f p :: TyFun (f k) Type -> *) (as :: f k)

Defined in Data.Type.Universe

type Apply (Any f p :: TyFun (f k) Type -> *) (as :: f k) = WitAny f p as

data WitAny f :: (k ~> Type) -> f k -> Type where

A WitAny p as is a witness that, for at least one item a in the type-level collection as, the predicate p a is true.

Constructors

WitAny :: Elem f as a -> (p @@ a) -> WitAny f p as

type None f p = (Not (Any f p) :: Predicate (f k))

A None f p is a predicate on a collection as that no a in as satisfies predicate p.

type Null f = (None f Evident :: Predicate (f k))

Predicate that a given as :: f k is empty and has no items in it.

type NotNull f = (Any f Evident :: Predicate (f k))

Predicate that a given as :: f k is not empty, and has at least one item in it.

Specialized

type IsJust = (NotNull Maybe :: Predicate (Maybe k))

Test that a Maybe is Just.

Since: decidable-0.1.2.0

type IsNothing = (Null Maybe :: Predicate (Maybe k))

Test that a Maybe is Nothing.

Since: decidable-0.1.2.0

type IsRight = (NotNull (Either j) :: Predicate (Either j k))

Test that an Either is Right

Since: decidable-0.1.2.0

type IsLeft = (Null (Either j) :: Predicate (Either j k))

Test that an Either is Left

Since: decidable-0.1.2.0

Decisions and manipulations

decideAny

Arguments

:: forall (p :: k ~> Type). Universe f

=> Decide p

predicate on value

-> Decide (Any f p)

predicate on collection

Lifts a predicate p on an individual a into a predicate that on a collection as that is true if and only if any item in as satisfies the original predicate.

That is, it turns a predicate of kind k ~> Type into a predicate of kind f k ~> Type.

Essentially tests existential quantification.

decideAll

Arguments

:: forall (p :: k ~> Type). Universe f

=> Decide p

predicate on value

-> Decide (All f p)

predicate on collection

Lifts a predicate p on an individual a into a predicate that on a collection as that is true if and only if all items in as satisfies the original predicate.

That is, it turns a predicate of kind k ~> Type into a predicate of kind f k ~> Type.

Essentially tests universal quantification.

genAllA

Arguments

:: forall (p :: k ~> Type) (as :: f k). (Universe f, Applicative h)

=> (forall a. Sing a -> h (p @@ a))

predicate on value in context

-> Sing as -> h (All f p @@ as)

predicate on collection in context

If p a is true for all values a in as under some (Applicative) context h, then you can create an All p as under that Applicative context h.

Can be useful with Identity (which is basically unwrapping and wrapping All), or with Maybe (which can express predicates that are either provably true or not provably false).

In practice, this can be used to iterate and traverse and sequence actions over all "items" in as.

genAll

Arguments

:: forall (p :: k ~> Type). Universe f

=> Prove p

always-true predicate on value

-> Prove (All f p)

always-true predicate on collection

If p a is true for all values a in as, then we have All p as. Basically witnesses the definition of All.

igenAll

Arguments

:: forall (p :: k ~> Type) (as :: f k). Universe f

=> (forall a. Elem f as a -> Sing a -> p @@ a)

always-true predicate on value

-> Sing as -> All f p @@ as

always-true predicate on collection

genAll, but providing an Elem.

foldMapUni :: forall f k (as :: f k) m. (Universe f, Monoid m) => (forall (a :: k). Sing a -> m) -> Sing as -> m

A foldMap over all items in a collection.

ifoldMapUni :: forall f k (as :: f k) m. (Universe f, Monoid m) => (forall a. Elem f as a -> Sing a -> m) -> Sing as -> m

foldMapUni but with access to the index.

index

Arguments

:: Universe f

=> Elem f as a

Witness

-> Sing as

Collection

-> Sing a

Extract the item from the container witnessed by the Elem

pickElem :: forall f k (as :: f k) a. (Universe f, SingI as, SingI a, SDecide k) => Decision (Elem f as a)

Automatically generate a witness for a member, if possible

Universe Composition

data (f :.: g) a

Compose two Functors. Is the same as Compose and :.:, except with a singleton and meant to be used at the type level. Will be redundant if either of the above gets brought into the singletons library.

Note that because this is a higher-kinded data constructor, there is no SingKind instance; if you need fromSing and toSing, try going through Comp and getComp and SComp and sGetComp.

Since: decidable-0.1.2.0

Constructors

Comp

Fields

• getComp :: f (g a)

Instances

AutoAll f (All g p) ass => AutoAll (f :.: g) (p :: a ~> Type) (Comp ass :: (f :.: g) a)

Defined in Data.Type.Predicate.Auto

Methods

autoAll :: All (f :.: g) p @@ Comp ass

(Functor f, Functor g) => Functor (f :.: g)

Defined in Data.Type.Universe

Methods

fmap :: (a -> b) -> (f :.: g) a -> (f :.: g) b

(<$) :: a -> (f :.: g) b -> (f :.: g) a

(Foldable f, Foldable g) => Foldable (f :.: g)

Defined in Data.Type.Universe

Methods

fold :: Monoid m => (f :.: g) m -> m

foldMap :: Monoid m => (a -> m) -> (f :.: g) a -> m

foldr :: (a -> b -> b) -> b -> (f :.: g) a -> b

foldr' :: (a -> b -> b) -> b -> (f :.: g) a -> b

foldl :: (b -> a -> b) -> b -> (f :.: g) a -> b

foldl' :: (b -> a -> b) -> b -> (f :.: g) a -> b

foldr1 :: (a -> a -> a) -> (f :.: g) a -> a

foldl1 :: (a -> a -> a) -> (f :.: g) a -> a

toList :: (f :.: g) a -> [a]

null :: (f :.: g) a -> Bool

length :: (f :.: g) a -> Int

elem :: Eq a => a -> (f :.: g) a -> Bool

maximum :: Ord a => (f :.: g) a -> a

minimum :: Ord a => (f :.: g) a -> a

sum :: Num a => (f :.: g) a -> a

product :: Num a => (f :.: g) a -> a

(Traversable f, Traversable g) => Traversable (f :.: g)

Defined in Data.Type.Universe

Methods

traverse :: Applicative f0 => (a -> f0 b) -> (f :.: g) a -> f0 ((f :.: g) b)

sequenceA :: Applicative f0 => (f :.: g) (f0 a) -> f0 ((f :.: g) a)

mapM :: Monad m => (a -> m b) -> (f :.: g) a -> m ((f :.: g) b)

sequence :: Monad m => (f :.: g) (m a) -> m ((f :.: g) a)

(Universe f, Universe g) => Universe (f :.: g)

Defined in Data.Type.Universe

Methods

idecideAny :: (forall (a :: k). Elem (f :.: g) as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (Any (f :.: g) p @@ as)

idecideAll :: (forall (a :: k). Elem (f :.: g) as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (All (f :.: g) p @@ as)

igenAllA :: Applicative h => (forall (a :: k). Elem (f :.: g) as a -> Sing a -> h (p @@ a)) -> Sing as -> h (All (f :.: g) p @@ as)

Eq (f (g a)) => Eq ((f :.: g) a)

Defined in Data.Type.Universe

Methods

(==) :: (f :.: g) a -> (f :.: g) a -> Bool

(/=) :: (f :.: g) a -> (f :.: g) a -> Bool

Ord (f (g a)) => Ord ((f :.: g) a)

Defined in Data.Type.Universe

Methods

compare :: (f :.: g) a -> (f :.: g) a -> Ordering

(<) :: (f :.: g) a -> (f :.: g) a -> Bool

(<=) :: (f :.: g) a -> (f :.: g) a -> Bool

(>) :: (f :.: g) a -> (f :.: g) a -> Bool

(>=) :: (f :.: g) a -> (f :.: g) a -> Bool

max :: (f :.: g) a -> (f :.: g) a -> (f :.: g) a

min :: (f :.: g) a -> (f :.: g) a -> (f :.: g) a

Show (f (g a)) => Show ((f :.: g) a)

Defined in Data.Type.Universe

Methods

showsPrec :: Int -> (f :.: g) a -> ShowS

show :: (f :.: g) a -> String

showList :: [(f :.: g) a] -> ShowS

Generic ((f :.: g) a)

Defined in Data.Type.Universe

Associated Types

type Rep ((f :.: g) a) :: * -> *

Methods

from :: (f :.: g) a -> Rep ((f :.: g) a) x

to :: Rep ((f :.: g) a) x -> (f :.: g) a

SingI ass => SingI (Comp ass :: (f :.: g) a)

Defined in Data.Type.Universe

Methods

sing :: Sing (Comp ass)

type Elem (f :.: g)

Defined in Data.Type.Universe

type Elem (f :.: g) = (CompElem :: (f :.: g) k -> k -> Type)

type Rep ((f :.: g) a)

Defined in Data.Type.Universe

type Rep ((f :.: g) a) = D1 (MetaData ":.:" "Data.Type.Universe" "decidable-0.1.2.0-46wg9BwkRKCIWZxpt8cweW" False) (C1 (MetaCons "Comp" PrefixI True) (S1 (MetaSel (Just "getComp") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (f (g a)))))

data Sing (k :: (f :.: g) a)

Defined in Data.Type.Universe

data Sing (k :: (f :.: g) a) where

• SComp :: Sing (Comp x)

type Apply (GetCompSym0 :: TyFun ((f :.: g) k3) (f (g k3)) -> *) (Comp ass :: (f :.: g) k3)

Defined in Data.Type.Universe

type Apply (GetCompSym0 :: TyFun ((f :.: g) k3) (f (g k3)) -> *) (Comp ass :: (f :.: g) k3) = ass

data family Sing (a :: k) :: *

The singleton kind-indexed data family.

Instances

Provable (Evident :: Predicate k1)

Defined in Data.Type.Predicate

Methods

prove :: Prove Evident

Decidable (Evident :: Predicate k1)

Defined in Data.Type.Predicate

Methods

decide :: Decide Evident

SingI a => Auto (Evident :: Predicate k) (a :: k)

Defined in Data.Type.Predicate.Auto

Methods

auto :: Evident @@ a

Provable (Not (Impossible :: Predicate k1) :: TyFun k1 Type -> *)

Defined in Data.Type.Predicate

Methods

prove :: Prove (Not Impossible)

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

Since: decidable-0.1.2.0

Defined in Data.Type.Predicate.Auto

Methods

auto :: Not Impossible @@ a

Provable ((Impossible :: Predicate k1) ==> p :: TyFun k1 Type -> *)

Defined in Data.Type.Predicate.Logic

Methods

prove :: Prove (Impossible ==> p)

Decidable ((Impossible :: Predicate k1) ==> p :: TyFun k1 Type -> *)

Defined in Data.Type.Predicate.Logic

Methods

decide :: Decide (Impossible ==> p)

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

Since: decidable-0.1.2.0

Defined in Data.Type.Predicate.Auto

Methods

auto :: IsJust @@ Just a

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

Since: decidable-0.1.2.0

Defined in Data.Type.Predicate.Auto

Methods

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

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

Since: decidable-0.1.2.0

Defined in Data.Type.Predicate.Auto

Methods

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

Provable p => Provable ((NotNull f :: Predicate (f k)) ==> Any f p :: TyFun (f k) Type -> *)

Defined in Data.Type.Universe

Methods

prove :: Prove (NotNull f ==> Any f p)

Provable (Found (InP f :: ParamPred (f v) v) ==> (NotNull f :: Predicate (f v)) :: TyFun (f v) Type -> *)

Defined in Data.Type.Predicate.Param

Methods

prove :: Prove (Found (InP f) ==> NotNull f)

Provable ((NotNull f :: Predicate (f k)) ==> Found (InP f :: ParamPred (f k) k) :: TyFun (f k) Type -> *)

Defined in Data.Type.Predicate.Param

Methods

prove :: Prove (NotNull f ==> Found (InP f))

(Universe f, Provable p) => Decidable ((NotNull f :: Predicate (f k)) ==> Any f p :: TyFun (f k) Type -> *)

Defined in Data.Type.Universe

Methods

decide :: Decide (NotNull f ==> Any f p)

Decidable (Found (InP f :: ParamPred (f v) v) ==> (NotNull f :: Predicate (f v)) :: TyFun (f v) Type -> *)

Defined in Data.Type.Predicate.Param

Methods

decide :: Decide (Found (InP f) ==> NotNull f)

Decidable ((NotNull f :: Predicate (f k)) ==> Found (InP f :: ParamPred (f k) k) :: TyFun (f k) Type -> *)

Defined in Data.Type.Predicate.Param

Methods

decide :: Decide (NotNull f ==> Found (InP f))

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

Since: decidable-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: decidable-0.1.2.0

Defined in Data.Type.Predicate.Auto

Methods

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

data Sing (z :: Bool)

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: Bool) where

• SFalse :: Sing False
• STrue :: Sing True

data Sing (z :: Ordering)

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: Ordering) where

• SLT :: Sing LT
• SEQ :: Sing EQ
• SGT :: Sing GT

data Sing (n :: Nat)

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Nat) where

• SNat :: Sing n

data Sing (n :: Symbol)

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Symbol) where

• SSym :: Sing n

data Sing (z :: ())

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: ()) where

• STuple0 :: Sing ()

data Sing (z :: Void)

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: Void)

data Sing (z :: [a])

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: [a]) where

• SNil :: Sing ([] :: [a])
• SCons :: Sing (n1 ': n2)

data Sing (z :: Maybe a)

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: Maybe a) where

• SNothing :: Sing (Nothing :: Maybe a)
• SJust :: Sing (Just n)

data Sing (z :: NonEmpty a)

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: NonEmpty a) where

• (:%|) :: Sing (n1 :| n2)

data Sing (z :: Either a b)

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: Either a b) where

• SLeft :: Sing (Left n :: Either a b)
• SRight :: Sing (Right n :: Either a b)

data Sing (z :: (a, b))

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: (a, b)) where

• STuple2 :: Sing ((,) n1 n2)

data Sing (f :: k1 ~> k2)

Defined in Data.Singletons.Internal

data Sing (f :: k1 ~> k2) = SLambda {

• applySing :: forall (t :: k1). Sing t -> Sing (f @@ t)

}

data Sing (z :: (a, b, c))

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: (a, b, c)) where

• STuple3 :: Sing ((,,) n1 n2 n3)

data Sing (z :: (a, b, c, d))

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: (a, b, c, d)) where

• STuple4 :: Sing ((,,,) n1 n2 n3 n4)

data Sing (z :: (a, b, c, d, e))

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: (a, b, c, d, e)) where

• STuple5 :: Sing ((,,,,) n1 n2 n3 n4 n5)

data Sing (k :: (f :.: g) a)

Defined in Data.Type.Universe

data Sing (k :: (f :.: g) a) where

• SComp :: Sing (Comp x)

data Sing (z :: (a, b, c, d, e, f))

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: (a, b, c, d, e, f)) where

• STuple6 :: Sing ((,,,,,) n1 n2 n3 n4 n5 n6)

data Sing (z :: (a, b, c, d, e, f, g))

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: (a, b, c, d, e, f, g)) where

• STuple7 :: Sing ((,,,,,,) n1 n2 n3 n4 n5 n6 n7)

sGetComp :: Sing a -> Sing (GetComp a)

Singletonized witness for GetComp

Since: decidable-0.1.2.0

type family GetComp c where ...

getComp lifted to the type level

Since: decidable-0.1.2.0

Equations

GetComp (Comp a) = a

allComp :: (All f (All g p) @@ as) -> All (f :.: g) p @@ Comp as

Turn a composition of All into an All of a composition.

Since: decidable-0.1.2.0

compAll :: (All (f :.: g) p @@ Comp as) -> All f (All g p) @@ as

Turn an All of a composition into a composition of All.

Since: decidable-0.1.2.0

anyComp :: (Any f (Any g p) @@ as) -> Any (f :.: g) p @@ Comp as

Turn a composition of Any into an Any of a composition.

Since: decidable-0.1.2.0

compAny :: (Any (f :.: g) p @@ Comp as) -> Any f (Any g p) @@ as

Turn an Any of a composition into a composition of Any.

Since: decidable-0.1.2.0

Defunctionalization symbols

data ElemSym0 (f :: Type -> Type) :: f k ~> (k ~> Type)

Instances

type Apply (ElemSym0 f :: TyFun (f k) (k ~> Type) -> *) (as :: f k)

Defined in Data.Type.Universe

type Apply (ElemSym0 f :: TyFun (f k) (k ~> Type) -> *) (as :: f k) = ElemSym1 f as

data ElemSym1 (f :: Type -> Type) :: f k -> k ~> Type

Instances

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

Provable (Found (InP f :: ParamPred (f v) v) ==> (NotNull f :: Predicate (f v)) :: TyFun (f v) Type -> *)

Defined in Data.Type.Predicate.Param

Methods

prove :: Prove (Found (InP f) ==> NotNull f)

Provable ((NotNull f :: Predicate (f k)) ==> Found (InP f :: ParamPred (f k) k) :: TyFun (f k) Type -> *)

Defined in Data.Type.Predicate.Param

Methods

prove :: Prove (NotNull f ==> Found (InP f))

Decidable (Found (InP f :: ParamPred (f v) v) ==> (NotNull f :: Predicate (f v)) :: TyFun (f v) Type -> *)

Defined in Data.Type.Predicate.Param

Methods

decide :: Decide (Found (InP f) ==> NotNull f)

Decidable ((NotNull f :: Predicate (f k)) ==> Found (InP f :: ParamPred (f k) k) :: TyFun (f k) Type -> *)

Defined in Data.Type.Predicate.Param

Methods

decide :: Decide (NotNull f ==> Found (InP f))

Universe f => Decidable (Found (InP f :: ParamPred (f v) v) :: TyFun (f v) Type -> *)

Defined in Data.Type.Predicate.Param

Methods

decide :: Decide (Found (InP f))

type Apply (ElemSym1 f as :: TyFun k Type -> *) (a :: k)

Defined in Data.Type.Universe

type Apply (ElemSym1 f as :: TyFun k Type -> *) (a :: k) = Elem f as a

type ElemSym2 (f :: Type -> Type) (as :: f k) (a :: k) = Elem f as a

data GetCompSym0 :: (f :.: g) k ~> f (g k)

Instances

type Apply (GetCompSym0 :: TyFun ((f :.: g) k3) (f (g k3)) -> *) (Comp ass :: (f :.: g) k3)

Defined in Data.Type.Universe

type Apply (GetCompSym0 :: TyFun ((f :.: g) k3) (f (g k3)) -> *) (Comp ass :: (f :.: g) k3) = ass

type GetCompSym1 a = GetComp a