decidable-0.3.1.0: Combinators for manipulating dependently-typed predicates.
Copyright(c) Justin Le 2018
LicenseBSD3
Maintainerjustin@jle.im
Stabilityexperimental
Portabilitynon-portable
Safe HaskellSafe-Inferred
LanguageHaskell2010

Data.Type.Universe

Description

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

Synopsis

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

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

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

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

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