Copyright	(c) Justin Le 2018
License	BSD3
Maintainer	justin@jle.im
Stability	experimental
Portability	non-portable
Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.Type.Universe

Contents

Universe
- Instances
- Predicates
  - Specialized
Decisions and manipulations

Description

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

Synopsis

type family Elem (f :: Type -> Type) = (i :: f k -> k -> Type) | i -> f
type In (f :: Type -> Type) (as :: f k) = ElemSym1 f as
class FProd f => Universe (f :: Type -> Type) where
- idecideAny :: forall k (p :: k ~> Type) (as :: f k). (forall a. Elem f as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (Any f p @@ as)
- idecideAll :: forall k (p :: k ~> Type) (as :: f k). (forall a. Elem f as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (All f p @@ as)
- 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
singAll :: forall f k (as :: f k). Universe f => Sing as -> All f Evident @@ as
data Index (a :: [k]) (b :: k) where
- 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
data IJust (a :: Maybe k) (b :: k) where
- IJust :: forall {k} (b :: k). IJust ('Just b) b
data IRight (a :: Either j k) (b :: k) where
- IRight :: forall {k} {j} (b :: k). IRight ('Right b :: Either j k) b
data NEIndex (a :: NonEmpty k) (b :: k) where
- 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
data ISnd (a :: (j, k)) (b :: k) where
- ISnd :: forall {j} {k} (a1 :: j) (b :: k). ISnd '(a1, b) b
data IIdentity (a :: Identity k) (b :: k) where
- IId :: forall {k} (b :: k). IIdentity ('Identity b) b
data All f :: Predicate k -> Predicate (f k)
newtype WitAll f p (as :: f k) = WitAll {
- runWitAll :: forall a. Elem f as a -> p @@ a
}
type NotAll f p = Not (All f p) :: Predicate (f k)
data Any f :: Predicate k -> Predicate (f k)
data WitAny f :: (k ~> Type) -> f k -> Type where
- WitAny :: Elem f as a -> (p @@ a) -> WitAny f p as
type None f p = Not (Any f p) :: Predicate (f k)
type Null f = None f Evident :: Predicate (f k)
type NotNull f = Any f Evident :: Predicate (f k)
type IsJust = NotNull Maybe :: Predicate (Maybe k)
type IsNothing = Null Maybe :: Predicate (Maybe k)
type IsRight = NotNull (Either j) :: Predicate (Either j k)
type IsLeft = Null (Either j) :: Predicate (Either j k)
decideAny :: forall f k (p :: k ~> Type). Universe f => Decide p -> Decide (Any f p)
decideAll :: forall f k (p :: k ~> Type). Universe f => Decide p -> Decide (All f p)
genAll :: forall f k (p :: k ~> Type). Universe f => Prove p -> Prove (All f p)
igenAll :: forall f k (p :: k ~> Type) (as :: f k). Universe f => (forall a. Elem f as a -> Sing a -> p @@ a) -> Sing as -> All f p @@ as
splitSing :: forall f k (as :: f k). Universe f => Sing as -> All f (TyPred Sing) @@ as
pickElem :: forall f k (as :: f k) a. (Universe f, SingI as, SingI a, SDecide k) => Decision (Elem f as a)

Universe

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

Instances

Instances details

type Elem Identity
Instance details Defined in Data.Type.Functor.Product type Elem Identity = IIdentity :: Identity k -> k -> Type
type Elem NonEmpty
Instance details Defined in Data.Type.Functor.Product type Elem NonEmpty = NEIndex :: NonEmpty k -> k -> Type
type Elem Maybe
Instance details Defined in Data.Type.Functor.Product type Elem Maybe = IJust :: Maybe k -> k -> Type
type Elem []
Instance details Defined in Data.Type.Functor.Product type Elem [] = Index :: [k] -> k -> Type
type Elem (Either j)
Instance details Defined in Data.Type.Functor.Product type Elem (Either j) = IRight :: Either j k -> k -> Type
type Elem ((,) j)
Instance details Defined in Data.Type.Functor.Product type Elem ((,) j) = ISnd :: (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 FProd f => Universe (f :: Type -> Type) where Source #

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

Methods

idecideAny Source #

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

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

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

Instances

Instances details

Universe Identity Source #	The single-pointed universe.
Instance details 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) Source # 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) Source # allProd :: forall {k} (p :: Predicate k) g. (forall (a :: k). Sing a -> (p @@ a) -> g a) -> All Identity p --> TyPred (Prod Identity g) Source # 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 Source #
Universe NonEmpty Source #
Instance details 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) Source # 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) Source # allProd :: forall {k} (p :: Predicate k) g. (forall (a :: k). Sing a -> (p @@ a) -> g a) -> All NonEmpty p --> TyPred (Prod NonEmpty g) Source # 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 Source #
Universe Maybe Source #
Instance details 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) Source # 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) Source # allProd :: forall {k} (p :: Predicate k) g. (forall (a :: k). Sing a -> (p @@ a) -> g a) -> All Maybe p --> TyPred (Prod Maybe g) Source # 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 Source #
Universe [] Source #
Instance details 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) Source # 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) Source # allProd :: forall {k} (p :: Predicate k) g. (forall (a :: k). Sing a -> (p @@ a) -> g a) -> All [] p --> TyPred (Prod [] g) Source # prodAll :: forall {k} (p :: Predicate k) g (as :: [k]). (forall (a :: k). g a -> p @@ a) -> Prod [] g as -> All [] p @@ as Source #
Universe (Either j) Source #
Instance details 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) Source # 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) Source # 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) Source # 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 Source #
Universe ((,) j) Source #
Instance details 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) Source # 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) Source # allProd :: forall {k} (p :: Predicate k) g. (forall (a :: k). Sing a -> (p @@ a) -> g a) -> All ((,) j) p --> TyPred (Prod ((,) j) g) Source # 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 Source #

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

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

Instances details

Show (Index as a)
Instance details Defined in Data.Type.Functor.Product Methods showsPrec :: Int -> Index as a -> ShowS # show :: Index as a -> String # showList :: [Index as a] -> ShowS #
Eq (Index as a)
Instance details 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)
Instance details 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 #
SingKind (Index as a)
Instance details 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) #
SDecide (Index as a)
Instance details Defined in Data.Type.Functor.Product Methods (%~) :: forall (a0 :: Index as a) (b :: Index as a). Sing a0 -> Sing b -> Decision (a0 :~: b) #
SingI ('IZ :: Index (a ': as) a)
Instance details Defined in Data.Type.Functor.Product Methods sing :: Sing 'IZ #
SingI i => SingI ('IS i :: Index (b ': bs) a)
Instance details Defined in Data.Type.Functor.Product Methods sing :: Sing ('IS i) #
type Demote (Index as a)
Instance details Defined in Data.Type.Functor.Product type Demote (Index as a) = Index as a
type Sing
Instance details Defined in Data.Type.Functor.Product type Sing = SIndex 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

Instances details

Read (IJust ('Just a) a)
Instance details 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)
Instance details Defined in Data.Type.Functor.Product Methods showsPrec :: Int -> IJust as a -> ShowS # show :: IJust as a -> String # showList :: [IJust as a] -> ShowS #
Eq (IJust as a)
Instance details 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)
Instance details 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 #
SingKind (IJust as a)
Instance details 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) #
SDecide (IJust as a)
Instance details Defined in Data.Type.Functor.Product Methods (%~) :: forall (a0 :: IJust as a) (b :: IJust as a). Sing a0 -> Sing b -> Decision (a0 :~: b) #
SingI ('IJust :: IJust ('Just a) a)
Instance details Defined in Data.Type.Functor.Product Methods sing :: Sing 'IJust0 #
type Demote (IJust as a)
Instance details Defined in Data.Type.Functor.Product type Demote (IJust as a) = IJust as a
type Sing
Instance details Defined in Data.Type.Functor.Product type Sing = SIJust 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

Instances details

Read (IRight ('Right a :: Either j k) a)
Instance details 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)
Instance details Defined in Data.Type.Functor.Product Methods showsPrec :: Int -> IRight as a -> ShowS # show :: IRight as a -> String # showList :: [IRight as a] -> ShowS #
Eq (IRight as a)
Instance details 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)
Instance details 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 #
SingKind (IRight as a)
Instance details 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) #
SDecide (IRight as a)
Instance details Defined in Data.Type.Functor.Product Methods (%~) :: forall (a0 :: IRight as a) (b :: IRight as a). Sing a0 -> Sing b -> Decision (a0 :~: b) #
SingI ('IRight :: IRight ('Right a :: Either j k) a)
Instance details Defined in Data.Type.Functor.Product Methods sing :: Sing 'IRight0 #
type Demote (IRight as a)
Instance details Defined in Data.Type.Functor.Product type Demote (IRight as a) = IRight as a
type Sing
Instance details Defined in Data.Type.Functor.Product type Sing = SIRight 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

Instances details

Show (NEIndex as a)
Instance details Defined in Data.Type.Functor.Product Methods showsPrec :: Int -> NEIndex as a -> ShowS # show :: NEIndex as a -> String # showList :: [NEIndex as a] -> ShowS #
Eq (NEIndex as a)
Instance details 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)
Instance details 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 #
SingKind (NEIndex as a)
Instance details 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) #
SDecide (NEIndex as a)
Instance details Defined in Data.Type.Functor.Product Methods (%~) :: forall (a0 :: NEIndex as a) (b :: NEIndex as a). Sing a0 -> Sing b -> Decision (a0 :~: b) #
SingI ('NEHead :: NEIndex (a :\| as) a)
Instance details Defined in Data.Type.Functor.Product Methods sing :: Sing 'NEHead #
SingI i => SingI ('NETail i :: NEIndex (b :\| as) a)
Instance details Defined in Data.Type.Functor.Product Methods sing :: Sing ('NETail i) #
type Demote (NEIndex as a)
Instance details Defined in Data.Type.Functor.Product type Demote (NEIndex as a) = NEIndex as a
type Sing
Instance details Defined in Data.Type.Functor.Product type Sing = SNEIndex 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

Instances details

Read (ISnd '(a, b) b)
Instance details 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)
Instance details Defined in Data.Type.Functor.Product Methods showsPrec :: Int -> ISnd as a -> ShowS # show :: ISnd as a -> String # showList :: [ISnd as a] -> ShowS #
Eq (ISnd as a)
Instance details 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)
Instance details 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 #
SingKind (ISnd as a)
Instance details 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) #
SDecide (ISnd as a)
Instance details Defined in Data.Type.Functor.Product Methods (%~) :: forall (a0 :: ISnd as a) (b :: ISnd as a). Sing a0 -> Sing b -> Decision (a0 :~: b) #
SingI ('ISnd :: ISnd '(a, b) b)
Instance details Defined in Data.Type.Functor.Product Methods sing :: Sing 'ISnd0 #
type Demote (ISnd as a)
Instance details Defined in Data.Type.Functor.Product type Demote (ISnd as a) = ISnd as a
type Sing
Instance details Defined in Data.Type.Functor.Product type Sing = SISnd 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

Instances details

Read (IIdentity ('Identity a) a)
Instance details 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)
Instance details Defined in Data.Type.Functor.Product Methods showsPrec :: Int -> IIdentity as a -> ShowS # show :: IIdentity as a -> String # showList :: [IIdentity as a] -> ShowS #
Eq (IIdentity as a)
Instance details 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)
Instance details 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 #
SingKind (IIdentity as a)
Instance details 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) #
SDecide (IIdentity as a)
Instance details Defined in Data.Type.Functor.Product Methods (%~) :: forall (a0 :: IIdentity as a) (b :: IIdentity as a). Sing a0 -> Sing b -> Decision (a0 :~: b) #
SingI ('IId :: IIdentity ('Identity x) x)
Instance details Defined in Data.Type.Functor.Product Methods sing :: Sing 'IId #
type Demote (IIdentity as a)
Instance details Defined in Data.Type.Functor.Product type Demote (IIdentity as a) = IIdentity as a
type Sing
Instance details Defined in Data.Type.Functor.Product type Sing = SIIdentity as a

Predicates

data All f :: Predicate k -> Predicate (f k) 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

Instances details

Universe f => DFunctor (All f :: Predicate k1 -> TyFun (f k1) Type -> Type) Source #
Instance details Defined in Data.Type.Universe Methods dmap :: forall (p :: k10 ~> Type) (q :: k10 ~> Type). (p -?> q) -> All f p -?> All f q Source #
Universe f => TFunctor (All f :: Predicate k1 -> TyFun (f k1) Type -> Type) Source #
Instance details Defined in Data.Type.Universe Methods tmap :: forall (p :: k10 ~> Type) (q :: k10 ~> Type). (p --> q) -> All f p --> All f q Source #
(Universe f, Decidable p) => Decidable (All f p :: TyFun (f k) Type -> Type) Source #
Instance details Defined in Data.Type.Universe Methods decide :: Decide (All f p) Source #
(Universe f, Provable p) => Provable (All f p :: TyFun (f k) Type -> Type) Source #
Instance details Defined in Data.Type.Universe Methods prove :: Prove (All f p) Source #
AutoAll f p as => Auto (All f p :: TyFun (f k) Type -> Type) (as :: f k) Source #	Since: 0.1.2.0
Instance details Defined in Data.Type.Predicate.Auto Methods auto :: All f p @@ as Source #
type Apply (All f p :: TyFun (f k) Type -> Type) (as :: f k) Source #
Instance details 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) 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
Fields runWitAll :: forall a. Elem f as a -> p @@ a

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

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

Instances details

Universe f => TFunctor (Any f :: Predicate k1 -> TyFun (f k1) Type -> Type) Source #
Instance details Defined in Data.Type.Universe Methods tmap :: forall (p :: k10 ~> Type) (q :: k10 ~> Type). (p --> q) -> Any f p --> Any f q Source #
SingI a => Auto (IsJust :: Predicate (Maybe k)) ('Just a :: Maybe k) Source #	Since: 0.1.2.0
Instance details Defined in Data.Type.Predicate.Auto Methods auto :: IsJust @@ 'Just a Source #
(SingI as, AutoAll f (Not p) as) => Auto (Not (Any f p) :: TyFun (f k) Type -> Type) (as :: f k) Source #	Since: 0.1.2.0
Instance details Defined in Data.Type.Predicate.Auto Methods auto :: Not (Any f p) @@ as Source #
SingI a => Auto (NotNull Identity :: Predicate (Identity k)) ('Identity a :: Identity k) Source #
Instance details Defined in Data.Type.Predicate.Auto Methods auto :: NotNull Identity @@ 'Identity0 a Source #
SingI a => Auto (NotNull NonEmpty :: Predicate (NonEmpty k)) (a :\| as :: NonEmpty k) Source #	Since: 0.1.2.0
Instance details Defined in Data.Type.Predicate.Auto Methods auto :: NotNull NonEmpty @@ (a :\| as) Source #
SingI a => Auto (NotNull [] :: Predicate [k]) (a ': as :: [k]) Source #	Since: 0.1.2.0
Instance details Defined in Data.Type.Predicate.Auto Methods auto :: NotNull [] @@ (a ': as) Source #
Decidable ((NotNull f :: Predicate (f k)) ==> Found (InP f :: ParamPred (f k) k) :: TyFun (f k) Type -> Type) Source #
Instance details Defined in Data.Type.Predicate.Param Methods decide :: Decide (NotNull f ==> Found (InP f)) Source #
(Universe f, Provable p) => Decidable ((NotNull f :: Predicate (f k)) ==> Any f p :: TyFun (f k) Type -> Type) Source #
Instance details Defined in Data.Type.Universe Methods decide :: Decide (NotNull f ==> Any f p) Source #
(Universe f, Decidable p) => Decidable (Any f p :: TyFun (f k) Type -> Type) Source #
Instance details Defined in Data.Type.Universe Methods decide :: Decide (Any f p) Source #
Decidable (Found (InP f :: ParamPred (f v) v) ==> (NotNull f :: Predicate (f v)) :: TyFun (f v) Type -> Type) Source #
Instance details Defined in Data.Type.Predicate.Param Methods decide :: Decide (Found (InP f) ==> NotNull f) Source #
Provable ((NotNull f :: Predicate (f k)) ==> Found (InP f :: ParamPred (f k) k) :: TyFun (f k) Type -> Type) Source #
Instance details Defined in Data.Type.Predicate.Param Methods prove :: Prove (NotNull f ==> Found (InP f)) Source #
Provable p => Provable ((NotNull f :: Predicate (f k)) ==> Any f p :: TyFun (f k) Type -> Type) Source #
Instance details Defined in Data.Type.Universe Methods prove :: Prove (NotNull f ==> Any f p) Source #
Provable (Found (InP f :: ParamPred (f v) v) ==> (NotNull f :: Predicate (f v)) :: TyFun (f v) Type -> Type) Source #
Instance details Defined in Data.Type.Predicate.Param Methods prove :: Prove (Found (InP f) ==> NotNull f) Source #
SingI a => Auto (IsRight :: Predicate (Either j k)) ('Right a :: Either j k) Source #	Since: 0.1.2.0
Instance details Defined in Data.Type.Predicate.Auto Methods auto :: IsRight @@ 'Right a Source #
SingI a => Auto (NotNull ((,) j) :: Predicate (j, k)) ('(w, a) :: (j, k)) Source #	Since: 0.1.2.0
Instance details Defined in Data.Type.Predicate.Auto Methods auto :: NotNull ((,) j) @@ '(w, a) Source #
type Apply (Any f p :: TyFun (f k) Type -> Type) (as :: f k) Source #
Instance details 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 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.

Specialized

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

Test that a Maybe is Just.

Since: 0.1.2.0

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

Test that a Maybe is Nothing.

Since: 0.1.2.0

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

Test that an Either is Right

Since: 0.1.2.0

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

Test that an Either is Left

Since: 0.1.2.0

Decisions and manipulations

decideAny Source #

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

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

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

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

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

Automatically generate a witness for a member, if possible