Data.Type.Universe

A type family for "containers", intended for allowing lifting of predicates on k to be predicates on containers f k.

Universe

type family Elem (f :: Type -> Type) = (i :: f k -> k -> Type) | i -> f

Instances

type Elem Identity

Defined in Data.Type.Functor.Product

type Elem Identity = IIdentity :: Identity k -> k -> Type

type Elem NonEmpty

Defined in Data.Type.Functor.Product

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

type Elem []

Defined in Data.Type.Functor.Product

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

type Elem Maybe

Defined in Data.Type.Functor.Product

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

type Elem ((,) j)

Defined in Data.Type.Functor.Product

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

type Elem (Either j)

Defined in Data.Type.Functor.Product

type Elem (Either j) = IRight :: Either j 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 FProd f => Universe (f :: Type -> Type) where

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

Methods

idecideAny

Arguments

:: forall k (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 k (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.

allProd :: forall p g. (forall a. Sing a -> (p @@ a) -> g a) -> All f p --> TyPred (Prod f g)

prodAll :: forall p g as. (forall a. g a -> p @@ a) -> Prod f g as -> All f p @@ as

Instances

Universe []

Defined in Data.Type.Universe

Methods

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

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

allProd :: forall k (p :: Predicate k) g. (forall (a :: k). Sing a -> (p @@ a) -> g a) -> All [] p --> TyPred (Prod [] g)

prodAll :: forall k (p :: Predicate k) g (as :: [k]). (forall (a :: k). g a -> p @@ a) -> Prod [] g as -> All [] p @@ as

Universe Maybe

Defined in Data.Type.Universe

Methods

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

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

allProd :: forall k (p :: Predicate k) g. (forall (a :: k). Sing a -> (p @@ a) -> g a) -> All Maybe p --> TyPred (Prod Maybe g)

prodAll :: forall k (p :: Predicate k) g (as :: Maybe k). (forall (a :: k). g a -> p @@ a) -> Prod Maybe g as -> All Maybe p @@ as

Universe Identity

The single-pointed universe.

Defined in Data.Type.Universe

Methods

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

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

allProd :: forall k (p :: Predicate k) g. (forall (a :: k). Sing a -> (p @@ a) -> g a) -> All Identity p --> TyPred (Prod Identity g)

prodAll :: forall k (p :: Predicate k) g (as :: Identity k). (forall (a :: k). g a -> p @@ a) -> Prod Identity g as -> All Identity p @@ as

Universe NonEmpty

Defined in Data.Type.Universe

Methods

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

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

allProd :: forall k (p :: Predicate k) g. (forall (a :: k). Sing a -> (p @@ a) -> g a) -> All NonEmpty p --> TyPred (Prod NonEmpty g)

prodAll :: forall k (p :: Predicate k) g (as :: NonEmpty k). (forall (a :: k). g a -> p @@ a) -> Prod NonEmpty g as -> All NonEmpty p @@ as

Universe (Either j)

Defined in Data.Type.Universe

Methods

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

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

allProd :: forall k (p :: Predicate k) g. (forall (a :: k). Sing a -> (p @@ a) -> g a) -> All (Either j) p --> TyPred (Prod (Either j) g)

prodAll :: forall k (p :: Predicate k) g (as :: Either j k). (forall (a :: k). g a -> p @@ a) -> Prod (Either j) g as -> All (Either j) p @@ as

Universe ((,) j)

Defined in Data.Type.Universe

Methods

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

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

allProd :: forall k (p :: Predicate k) g. (forall (a :: k). Sing a -> (p @@ a) -> g a) -> All ((,) j) p --> TyPred (Prod ((,) j) g)

prodAll :: forall k (p :: Predicate k) g (as :: (j, k)). (forall (a :: k). g a -> p @@ a) -> Prod ((,) j) g as -> All ((,) j) p @@ as

singAll :: forall f k (as :: f k). Universe f => Sing as -> All f Evident @@ as

Split a Sing as into a proof that all a in as exist.

Instances

data Index (a :: [k]) (b :: k) where

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

The number of ISs correspond to the item's position in the list.

IZ         :: Index '[5,10,2] 5
IS IZ      :: Index '[5,10,2] 10
IS (IS IZ) :: Index '[5,10,2] 2

Constructors

IZ :: forall k (b :: k) (as :: [k]). Index (b ': as) b

IS :: forall k (bs :: [k]) (b :: k) (b1 :: k). Index bs b -> Index (b1 ': bs) b

Instances

Eq (Index as a)

Defined in Data.Type.Functor.Product

Methods

(==) :: Index as a -> Index as a -> Bool

(/=) :: Index as a -> Index as a -> Bool

Ord (Index as a)

Defined in Data.Type.Functor.Product

Methods

compare :: Index as a -> Index as a -> Ordering

(<) :: Index as a -> Index as a -> Bool

(<=) :: Index as a -> Index as a -> Bool

(>) :: Index as a -> Index as a -> Bool

(>=) :: Index as a -> Index as a -> Bool

max :: Index as a -> Index as a -> Index as a

min :: Index as a -> Index as a -> Index as a

Show (Index as a)

Defined in Data.Type.Functor.Product

Methods

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

show :: Index as a -> String

showList :: [Index as a] -> ShowS

SDecide (Index as a)

Defined in Data.Type.Functor.Product

Methods

(%~) :: forall (a0 :: Index as a) (b :: Index as a). Sing a0 -> Sing b -> Decision (a0 :~: b)

SingKind (Index as a)

Defined in Data.Type.Functor.Product

Associated Types

type Demote (Index as a) = (r :: Type)

Methods

fromSing :: forall (a0 :: Index as a). Sing a0 -> Demote (Index as a)

toSing :: Demote (Index as a) -> SomeSing (Index as a)

SingI ('IZ :: Index (a ': as) a)

Defined in Data.Type.Functor.Product

Methods

sing :: Sing 'IZ

SingI i => SingI ('IS i :: Index (b ': bs) a)

Defined in Data.Type.Functor.Product

Methods

sing :: Sing ('IS i)

type Sing

Defined in Data.Type.Functor.Product

type Sing = SIndex as a

type Demote (Index as a)

Defined in Data.Type.Functor.Product

type Demote (Index as a) = Index as a

data IJust (a :: Maybe k) (b :: k) where

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

Constructors

IJust :: forall k (b :: k). IJust ('Just b) b

Instances

Eq (IJust as a)

Defined in Data.Type.Functor.Product

Methods

(==) :: IJust as a -> IJust as a -> Bool

(/=) :: IJust as a -> IJust as a -> Bool

Ord (IJust as a)

Defined in Data.Type.Functor.Product

Methods

compare :: IJust as a -> IJust as a -> Ordering

(<) :: IJust as a -> IJust as a -> Bool

(<=) :: IJust as a -> IJust as a -> Bool

(>) :: IJust as a -> IJust as a -> Bool

(>=) :: IJust as a -> IJust as a -> Bool

max :: IJust as a -> IJust as a -> IJust as a

min :: IJust as a -> IJust as a -> IJust as a

Read (IJust ('Just a) a)

Defined in Data.Type.Functor.Product

Methods

readsPrec :: Int -> ReadS (IJust ('Just a) a)

readList :: ReadS [IJust ('Just a) a]

readPrec :: ReadPrec (IJust ('Just a) a)

readListPrec :: ReadPrec [IJust ('Just a) a]

Show (IJust as a)

Defined in Data.Type.Functor.Product

Methods

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

show :: IJust as a -> String

showList :: [IJust as a] -> ShowS

SDecide (IJust as a)

Defined in Data.Type.Functor.Product

Methods

(%~) :: forall (a0 :: IJust as a) (b :: IJust as a). Sing a0 -> Sing b -> Decision (a0 :~: b)

SingKind (IJust as a)

Defined in Data.Type.Functor.Product

Associated Types

type Demote (IJust as a) = (r :: Type)

Methods

fromSing :: forall (a0 :: IJust as a). Sing a0 -> Demote (IJust as a)

toSing :: Demote (IJust as a) -> SomeSing (IJust as a)

SingI ('IJust :: IJust ('Just a) a)

Defined in Data.Type.Functor.Product

Methods

sing :: Sing 'IJust0

type Sing

Defined in Data.Type.Functor.Product

type Sing = SIJust as a

type Demote (IJust as a)

Defined in Data.Type.Functor.Product

type Demote (IJust as a) = IJust as a

data IRight (a :: Either j k) (b :: k) where

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

Constructors

IRight :: forall k j (b :: k). IRight ('Right b :: Either j k) b

Instances

Eq (IRight as a)

Defined in Data.Type.Functor.Product

Methods

(==) :: IRight as a -> IRight as a -> Bool

(/=) :: IRight as a -> IRight as a -> Bool

Ord (IRight as a)

Defined in Data.Type.Functor.Product

Methods

compare :: IRight as a -> IRight as a -> Ordering

(<) :: IRight as a -> IRight as a -> Bool

(<=) :: IRight as a -> IRight as a -> Bool

(>) :: IRight as a -> IRight as a -> Bool

(>=) :: IRight as a -> IRight as a -> Bool

max :: IRight as a -> IRight as a -> IRight as a

min :: IRight as a -> IRight as a -> IRight as a

Read (IRight ('Right a :: Either j k) a)

Defined in Data.Type.Functor.Product

Methods

readsPrec :: Int -> ReadS (IRight ('Right a) a)

readList :: ReadS [IRight ('Right a) a]

readPrec :: ReadPrec (IRight ('Right a) a)

readListPrec :: ReadPrec [IRight ('Right a) a]

Show (IRight as a)

Defined in Data.Type.Functor.Product

Methods

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

show :: IRight as a -> String

showList :: [IRight as a] -> ShowS

SDecide (IRight as a)

Defined in Data.Type.Functor.Product

Methods

(%~) :: forall (a0 :: IRight as a) (b :: IRight as a). Sing a0 -> Sing b -> Decision (a0 :~: b)

SingKind (IRight as a)

Defined in Data.Type.Functor.Product

Associated Types

type Demote (IRight as a) = (r :: Type)

Methods

fromSing :: forall (a0 :: IRight as a). Sing a0 -> Demote (IRight as a)

toSing :: Demote (IRight as a) -> SomeSing (IRight as a)

SingI ('IRight :: IRight ('Right a :: Either j k) a)

Defined in Data.Type.Functor.Product

Methods

sing :: Sing 'IRight0

type Sing

Defined in Data.Type.Functor.Product

type Sing = SIRight as a

type Demote (IRight as a)

Defined in Data.Type.Functor.Product

type Demote (IRight as a) = IRight as a

data NEIndex (a :: NonEmpty k) (b :: k) 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 :: forall k (b :: k) (as :: [k]). NEIndex (b :| as) b

NETail :: forall k (as :: [k]) (b :: k) (b1 :: k). Index as b -> NEIndex (b1 :| as) b

Instances

Eq (NEIndex as a)

Defined in Data.Type.Functor.Product

Methods

(==) :: NEIndex as a -> NEIndex as a -> Bool

(/=) :: NEIndex as a -> NEIndex as a -> Bool

Ord (NEIndex as a)

Defined in Data.Type.Functor.Product

Methods

compare :: NEIndex as a -> NEIndex as a -> Ordering

(<) :: NEIndex as a -> NEIndex as a -> Bool

(<=) :: NEIndex as a -> NEIndex as a -> Bool

(>) :: NEIndex as a -> NEIndex as a -> Bool

(>=) :: NEIndex as a -> NEIndex as a -> Bool

max :: NEIndex as a -> NEIndex as a -> NEIndex as a

min :: NEIndex as a -> NEIndex as a -> NEIndex as a

Show (NEIndex as a)

Defined in Data.Type.Functor.Product

Methods

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

show :: NEIndex as a -> String

showList :: [NEIndex as a] -> ShowS

SDecide (NEIndex as a)

Defined in Data.Type.Functor.Product

Methods

(%~) :: forall (a0 :: NEIndex as a) (b :: NEIndex as a). Sing a0 -> Sing b -> Decision (a0 :~: b)

SingKind (NEIndex as a)

Defined in Data.Type.Functor.Product

Associated Types

type Demote (NEIndex as a) = (r :: Type)

Methods

fromSing :: forall (a0 :: NEIndex as a). Sing a0 -> Demote (NEIndex as a)

toSing :: Demote (NEIndex as a) -> SomeSing (NEIndex as a)

SingI ('NEHead :: NEIndex (a :| as) a)

Defined in Data.Type.Functor.Product

Methods

sing :: Sing 'NEHead

SingI i => SingI ('NETail i :: NEIndex (b :| as) a)

Defined in Data.Type.Functor.Product

Methods

sing :: Sing ('NETail i)

type Sing

Defined in Data.Type.Functor.Product

type Sing = SNEIndex as a

type Demote (NEIndex as a)

Defined in Data.Type.Functor.Product

type Demote (NEIndex as a) = NEIndex as a

data ISnd (a :: (j, k)) (b :: k) where

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

Constructors

ISnd :: forall j k (a1 :: j) (b :: k). ISnd '(a1, b) b

Instances

Eq (ISnd as a)

Defined in Data.Type.Functor.Product

Methods

(==) :: ISnd as a -> ISnd as a -> Bool

(/=) :: ISnd as a -> ISnd as a -> Bool

Ord (ISnd as a)

Defined in Data.Type.Functor.Product

Methods

compare :: ISnd as a -> ISnd as a -> Ordering

(<) :: ISnd as a -> ISnd as a -> Bool

(<=) :: ISnd as a -> ISnd as a -> Bool

(>) :: ISnd as a -> ISnd as a -> Bool

(>=) :: ISnd as a -> ISnd as a -> Bool

max :: ISnd as a -> ISnd as a -> ISnd as a

min :: ISnd as a -> ISnd as a -> ISnd as a

Read (ISnd '(a, b) b)

Defined in Data.Type.Functor.Product

Methods

readsPrec :: Int -> ReadS (ISnd '(a, b) b)

readList :: ReadS [ISnd '(a, b) b]

readPrec :: ReadPrec (ISnd '(a, b) b)

readListPrec :: ReadPrec [ISnd '(a, b) b]

Show (ISnd as a)

Defined in Data.Type.Functor.Product

Methods

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

show :: ISnd as a -> String

showList :: [ISnd as a] -> ShowS

SDecide (ISnd as a)

Defined in Data.Type.Functor.Product

Methods

(%~) :: forall (a0 :: ISnd as a) (b :: ISnd as a). Sing a0 -> Sing b -> Decision (a0 :~: b)

SingKind (ISnd as a)

Defined in Data.Type.Functor.Product

Associated Types

type Demote (ISnd as a) = (r :: Type)

Methods

fromSing :: forall (a0 :: ISnd as a). Sing a0 -> Demote (ISnd as a)

toSing :: Demote (ISnd as a) -> SomeSing (ISnd as a)

SingI ('ISnd :: ISnd '(a, b) b)

Defined in Data.Type.Functor.Product

Methods

sing :: Sing 'ISnd0

type Sing

Defined in Data.Type.Functor.Product

type Sing = SISnd as a

type Demote (ISnd as a)

Defined in Data.Type.Functor.Product

type Demote (ISnd as a) = ISnd as a

data IIdentity (a :: Identity k) (b :: k) where

Trivially witness the item held in an Identity.

Since: functor-products-0.1.3.0

Constructors

IId :: forall k (b :: k). IIdentity ('Identity b) b

Instances

Eq (IIdentity as a)

Defined in Data.Type.Functor.Product

Methods

(==) :: IIdentity as a -> IIdentity as a -> Bool

(/=) :: IIdentity as a -> IIdentity as a -> Bool

Ord (IIdentity as a)

Defined in Data.Type.Functor.Product

Methods

compare :: IIdentity as a -> IIdentity as a -> Ordering

(<) :: IIdentity as a -> IIdentity as a -> Bool

(<=) :: IIdentity as a -> IIdentity as a -> Bool

(>) :: IIdentity as a -> IIdentity as a -> Bool

(>=) :: IIdentity as a -> IIdentity as a -> Bool

max :: IIdentity as a -> IIdentity as a -> IIdentity as a

min :: IIdentity as a -> IIdentity as a -> IIdentity as a

Read (IIdentity ('Identity a) a)

Defined in Data.Type.Functor.Product

Methods

readsPrec :: Int -> ReadS (IIdentity ('Identity a) a)

readList :: ReadS [IIdentity ('Identity a) a]

readPrec :: ReadPrec (IIdentity ('Identity a) a)

readListPrec :: ReadPrec [IIdentity ('Identity a) a]

Show (IIdentity as a)

Defined in Data.Type.Functor.Product

Methods

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

show :: IIdentity as a -> String

showList :: [IIdentity as a] -> ShowS

SDecide (IIdentity as a)

Defined in Data.Type.Functor.Product

Methods

(%~) :: forall (a0 :: IIdentity as a) (b :: IIdentity as a). Sing a0 -> Sing b -> Decision (a0 :~: b)

SingKind (IIdentity as a)

Defined in Data.Type.Functor.Product

Associated Types

type Demote (IIdentity as a) = (r :: Type)

Methods

fromSing :: forall (a0 :: IIdentity as a). Sing a0 -> Demote (IIdentity as a)

toSing :: Demote (IIdentity as a) -> SomeSing (IIdentity as a)

SingI ('IId :: IIdentity ('Identity x) x)

Defined in Data.Type.Functor.Product

Methods

sing :: Sing 'IId

type Sing

Defined in Data.Type.Functor.Product

type Sing = SIIdentity as a

type Demote (IIdentity as a)

Defined in Data.Type.Functor.Product

type Demote (IIdentity as a) = IIdentity as a

Predicates

data All f :: Predicate k -> Predicate (f k)

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 :: Predicate k1 -> TyFun (f k1) Type -> Type)

Defined in Data.Type.Universe

Methods

tmap :: forall (p :: k10 ~> Type) (q :: k10 ~> Type). (p --> q) -> All f p --> All f q

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

Defined in Data.Type.Universe

Methods

dmap :: forall (p :: k10 ~> Type) (q :: k10 ~> Type). (p -?> q) -> All f p -?> All f q

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

Defined in Data.Type.Universe

Methods

prove :: Prove (All f p)

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

Defined in Data.Type.Universe

Methods

decide :: Decide (All f p)

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

Since: 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 -> Type) (as :: f k)

Defined in Data.Type.Universe

type Apply (All f p :: TyFun (f k) Type -> 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 :: Predicate k -> Predicate (f k)

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 :: Predicate k1 -> TyFun (f k1) Type -> Type)

Defined in Data.Type.Universe

Methods

tmap :: forall (p :: k10 ~> Type) (q :: k10 ~> Type). (p --> q) -> Any f p --> Any f q

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

Since: 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 -> Type) (as :: f k)

Since: 0.1.2.0

Defined in Data.Type.Predicate.Auto

Methods

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

SingI a => Auto (NotNull Identity :: Predicate (Identity k)) ('Identity a :: Identity k)

Defined in Data.Type.Predicate.Auto

Methods

auto :: NotNull Identity @@ 'Identity0 a

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

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

Defined in Data.Type.Predicate.Auto

Methods

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

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

Defined in Data.Type.Universe

type Apply (Any f p :: TyFun (f k) Type -> 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: 0.1.2.0

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

Test that a Maybe is Nothing.

Since: 0.1.2.0

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

Test that an Either is Right

Since: 0.1.2.0

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

Test that an Either is Left

Since: 0.1.2.0

Decisions and manipulations

decideAny

Arguments

:: forall f k (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 f k (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.

genAll

Arguments

:: forall f k (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 f k (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.

splitSing :: forall f k (as :: f k). Universe f => Sing as -> All f (TyPred Sing) @@ as

Split a Sing as into a proof that all a in as exist.

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