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 = (IsJust :: 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) = (IsRight :: Either j k -> k -> Type)

type Elem ((,) j)

Defined in Data.Type.Universe

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

type In (f :: Type -> Type) (as :: f k) = TyCon1 (Elem 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)

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 IsJust :: Maybe k -> k -> Type where

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)

Defined in Data.Type.Universe

Methods

decide :: Decide (TyPred (IsJust as))

Show (IsJust as a)

Defined in Data.Type.Universe

Methods

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

show :: IsJust as a -> String

showList :: [IsJust as a] -> ShowS

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

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)

Defined in Data.Type.Universe

Methods

decide :: Decide (TyPred (IsRight as))

Show (IsRight as a)

Defined in Data.Type.Universe

Methods

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

show :: IsRight as a -> String

showList :: [IsRight 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 Snd :: (j, k) -> k -> Type where

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)

Defined in Data.Type.Universe

Methods

decide :: Decide (TyPred (Snd as))

Show (Snd as a)

Defined in Data.Type.Universe

Methods

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

show :: Snd as a -> String

showList :: [Snd as a] -> ShowS

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)

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

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

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

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.

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

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

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