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

Data.Type.Universe

Description

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

Synopsis

Universe

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

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

Instances
 type Elem [] Source # Instance detailsDefined in Data.Type.Universe type Elem [] = (Index :: [k] -> k -> Type) type Elem Maybe Source # Instance detailsDefined in Data.Type.Universe type Elem Maybe = (IsJust :: Maybe k -> k -> Type) type Elem NonEmpty Source # Instance detailsDefined in Data.Type.Universe type Elem NonEmpty = (NEIndex :: NonEmpty k -> k -> Type) type Elem (Either j) Source # Instance detailsDefined in Data.Type.Universe type Elem (Either j) = (IsRight :: Either j k -> k -> Type) type Elem ((,) j) Source # Instance detailsDefined in Data.Type.Universe type Elem ((,) j) = (Snd :: (j, k) -> k -> Type)

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

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

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

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

Minimal complete definition

Methods

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.

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.

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 [] Source # Instance detailsDefined in Data.Type.Universe MethodsidecideAny :: (forall (a :: k). Elem [] as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (Any [] p @@ as) Source #idecideAll :: (forall (a :: k). Elem [] as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (All [] p @@ as) Source #igenAllA :: Applicative h => (forall (a :: k). Elem [] as a -> Sing a -> h (p @@ a)) -> Sing as -> h (All [] p @@ as) Source # Source # Instance detailsDefined in Data.Type.Universe MethodsidecideAny :: (forall (a :: k). Elem Maybe as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (Any Maybe p @@ as) Source #idecideAll :: (forall (a :: k). Elem Maybe as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (All Maybe p @@ as) Source #igenAllA :: Applicative h => (forall (a :: k). Elem Maybe as a -> Sing a -> h (p @@ a)) -> Sing as -> h (All Maybe p @@ as) Source # Source # Instance detailsDefined in Data.Type.Universe MethodsidecideAny :: (forall (a :: k). Elem NonEmpty as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (Any NonEmpty p @@ as) Source #idecideAll :: (forall (a :: k). Elem NonEmpty as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (All NonEmpty p @@ as) Source #igenAllA :: Applicative h => (forall (a :: k). Elem NonEmpty as a -> Sing a -> h (p @@ a)) -> Sing as -> h (All NonEmpty p @@ as) Source # Source # Instance detailsDefined in Data.Type.Universe MethodsidecideAny :: (forall (a :: k). Elem (Either j) as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (Any (Either j) p @@ as) Source #idecideAll :: (forall (a :: k). Elem (Either j) as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (All (Either j) p @@ as) Source #igenAllA :: Applicative h => (forall (a :: k). Elem (Either j) as a -> Sing a -> h (p @@ a)) -> Sing as -> h (All (Either j) p @@ as) Source # Universe ((,) j) Source # Instance detailsDefined in Data.Type.Universe MethodsidecideAny :: (forall (a :: k). Elem ((,) j) as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (Any ((,) j) p @@ as) Source #idecideAll :: (forall (a :: k). Elem ((,) j) as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (All ((,) j) p @@ as) Source #igenAllA :: Applicative h => (forall (a :: k). Elem ((,) j) as a -> Sing a -> h (p @@ a)) -> Sing as -> h (All ((,) j) p @@ as) Source #

Instances

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

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) Source # Instance detailsDefined in Data.Type.Universe Methodsdecide :: Decide (TyPred (Index as)) Source # Show (Index as a) Source # Instance detailsDefined in Data.Type.Universe MethodsshowsPrec :: Int -> Index as a -> ShowS #show :: Index as a -> String #showList :: [Index as a] -> ShowS #

data IsJust :: Maybe k -> k -> Type where Source #

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

Constructors

 IsJust :: IsJust (Just a) a
Instances
 (SingI as, SDecide k) => Decidable (TyPred (IsJust as) :: Predicate k) Source # Instance detailsDefined in Data.Type.Universe Methodsdecide :: Decide (TyPred (IsJust as)) Source # Show (IsJust as a) Source # Instance detailsDefined in Data.Type.Universe MethodsshowsPrec :: Int -> IsJust as a -> ShowS #show :: IsJust as a -> String #showList :: [IsJust as a] -> ShowS #

data IsRight :: Either j k -> k -> Type where Source #

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

Constructors

 IsRight :: IsRight (Right a) a
Instances
 (SingI as, SDecide k) => Decidable (TyPred (IsRight as) :: Predicate k) Source # Instance detailsDefined in Data.Type.Universe Methodsdecide :: Decide (TyPred (IsRight as)) Source # Show (IsRight as a) Source # Instance detailsDefined in Data.Type.Universe MethodsshowsPrec :: Int -> IsRight as a -> ShowS #show :: IsRight as a -> String #showList :: [IsRight as a] -> ShowS #

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

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) Source # Instance detailsDefined in Data.Type.Universe Methodsdecide :: Decide (TyPred (NEIndex as)) Source # Show (NEIndex as a) Source # Instance detailsDefined in Data.Type.Universe MethodsshowsPrec :: Int -> NEIndex as a -> ShowS #show :: NEIndex as a -> String #showList :: [NEIndex as a] -> ShowS #

data Snd :: (j, k) -> k -> Type where Source #

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

Constructors

 Snd :: Snd '(a, b) b
Instances
 (SingI as, SDecide k) => Decidable (TyPred (Snd as) :: Predicate k) Source # Instance detailsDefined in Data.Type.Universe Methodsdecide :: Decide (TyPred (Snd as)) Source # Show (Snd as a) Source # Instance detailsDefined in Data.Type.Universe MethodsshowsPrec :: Int -> Snd as a -> ShowS #show :: Snd as a -> String #showList :: [Snd as a] -> ShowS #

Predicates

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

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 -> *) Source # Instance detailsDefined in Data.Type.Universe Methodstmap :: (p --> q) -> All f p --> All f q Source # Universe f => DFunctor (All f :: (k1 ~> Type) -> TyFun (f k1) Type -> *) Source # Instance detailsDefined in Data.Type.Universe Methodsdmap :: (p -?> q) -> All f p -?> All f q Source # (Universe f, Provable p) => Provable (All f p :: TyFun (f k) Type -> *) Source # Instance detailsDefined in Data.Type.Universe Methodsprove :: Prove (All f p) Source # (Universe f, Decidable p) => Decidable (All f p :: TyFun (f k) Type -> *) Source # Instance detailsDefined in Data.Type.Universe Methodsdecide :: Decide (All f p) Source # type Apply (All f p :: TyFun (f k) Type -> *) (as :: f k) Source # Instance detailsDefined 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) Source #

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 FieldsrunWitAll :: forall a. Elem f as a -> p @@ a

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

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 -> *) Source # Instance detailsDefined in Data.Type.Universe Methodstmap :: (p --> q) -> Any f p --> Any f q Source # Provable p => Provable ((NotNull f :: Predicate (f k)) ==> Any f p :: TyFun (f k) Type -> *) Source # Instance detailsDefined in Data.Type.Universe Methodsprove :: Prove (NotNull f ==> Any f p) Source # Provable (Found (InP f :: ParamPred (f v) v) ==> (NotNull f :: Predicate (f v)) :: TyFun (f v) Type -> *) Source # Instance detailsDefined in Data.Type.Predicate.Param Methods Provable ((NotNull f :: Predicate (f k)) ==> Found (InP f :: ParamPred (f k) k) :: TyFun (f k) Type -> *) Source # Instance detailsDefined in Data.Type.Predicate.Param Methods (Universe f, Provable p) => Decidable ((NotNull f :: Predicate (f k)) ==> Any f p :: TyFun (f k) Type -> *) Source # Instance detailsDefined in Data.Type.Universe Methodsdecide :: Decide (NotNull f ==> Any f p) Source # (Universe f, Decidable p) => Decidable (Any f p :: TyFun (f k) Type -> *) Source # Instance detailsDefined in Data.Type.Universe Methodsdecide :: Decide (Any f p) Source # Decidable (Found (InP f :: ParamPred (f v) v) ==> (NotNull f :: Predicate (f v)) :: TyFun (f v) Type -> *) Source # Instance detailsDefined in Data.Type.Predicate.Param Methods Decidable ((NotNull f :: Predicate (f k)) ==> Found (InP f :: ParamPred (f k) k) :: TyFun (f k) Type -> *) Source # Instance detailsDefined in Data.Type.Predicate.Param Methods type Apply (Any f p :: TyFun (f k) Type -> *) (as :: f k) Source # Instance detailsDefined 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 Source #

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)) Source #

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)) Source #

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

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

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

Decisions and manipulations

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.

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.

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.

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.

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 Source #

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 Source #

foldMapUni but with access to the 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) Source #

Automatically generate a witness for a member, if possible

Defunctionalization symbols

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

Instances
 type Apply (ElemSym0 f :: TyFun (f k) (k ~> Type) -> *) (as :: f k) Source # Instance detailsDefined 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 Source #

Instances
 AutoElem f as a => Auto (In f as :: TyFun k Type -> *) (a :: k) Source # Instance detailsDefined in Data.Type.Predicate.Auto Methodsauto :: In f as @@ a Source # Provable (Found (InP f :: ParamPred (f v) v) ==> (NotNull f :: Predicate (f v)) :: TyFun (f v) Type -> *) Source # Instance detailsDefined in Data.Type.Predicate.Param Methods Provable ((NotNull f :: Predicate (f k)) ==> Found (InP f :: ParamPred (f k) k) :: TyFun (f k) Type -> *) Source # Instance detailsDefined in Data.Type.Predicate.Param Methods Decidable (Found (InP f :: ParamPred (f v) v) ==> (NotNull f :: Predicate (f v)) :: TyFun (f v) Type -> *) Source # Instance detailsDefined in Data.Type.Predicate.Param Methods Decidable ((NotNull f :: Predicate (f k)) ==> Found (InP f :: ParamPred (f k) k) :: TyFun (f k) Type -> *) Source # Instance detailsDefined in Data.Type.Predicate.Param Methods Universe f => Decidable (Found (InP f :: ParamPred (f v) v) :: TyFun (f v) Type -> *) Source # Instance detailsDefined in Data.Type.Predicate.Param Methodsdecide :: Decide (Found (InP f)) Source # type Apply (ElemSym1 f as :: TyFun k Type -> *) (a :: k) Source # Instance detailsDefined 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 Source #