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) :: 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 = (IJust :: Maybe k -> k -> Type)

type Elem NonEmpty

Defined in Data.Type.Universe

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

type Elem Identity

Defined in Data.Type.Universe

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

type Elem (Either j)

Defined in Data.Type.Universe

type Elem (Either j) = (IRight :: Either j k -> k -> Type)

type Elem ((,) j)

Defined in Data.Type.Universe

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

type Elem (Proxy :: Type -> Type)

Defined in Data.Type.Universe

type Elem (Proxy :: Type -> Type) = (IProxy :: Proxy k -> k -> Type)

type Elem (f :+: g)

Defined in Data.Type.Universe

type Elem (f :+: g) = (SumElem :: (f :+: g) k -> k -> Type)

type Elem (f :.: g)

Defined in Data.Type.Universe

type Elem (f :.: g) = (CompElem :: (f :.: g) 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 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 (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 Identity

The single-pointed universe. Note that this instance is really only usable in singletons-2.5 and higher (so GHC 8.6).

Defined in Data.Type.Universe

Methods

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

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

igenAllA :: Applicative h => (forall (a :: k). Elem Identity as a -> Sing a -> h (p @@ a)) -> Sing as -> h (All Identity 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)

Universe (Proxy :: Type -> Type)

The null universe

Defined in Data.Type.Universe

Methods

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

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

igenAllA :: Applicative h => (forall (a :: k). Elem Proxy as a -> Sing a -> h (p @@ a)) -> Sing as -> h (All Proxy p @@ as)

(Universe f, Universe g) => Universe (f :+: g)

Defined in Data.Type.Universe

Methods

idecideAny :: (forall (a :: k). Elem (f :+: g) as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (Any (f :+: g) p @@ as)

idecideAll :: (forall (a :: k). Elem (f :+: g) as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (All (f :+: g) p @@ as)

igenAllA :: Applicative h => (forall (a :: k). Elem (f :+: g) as a -> Sing a -> h (p @@ a)) -> Sing as -> h (All (f :+: g) p @@ as)

(Universe f, Universe g) => Universe (f :.: g)

Defined in Data.Type.Universe

Methods

idecideAny :: (forall (a :: k). Elem (f :.: g) as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (Any (f :.: g) p @@ as)

idecideAll :: (forall (a :: k). Elem (f :.: g) as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (All (f :.: g) p @@ as)

igenAllA :: Applicative h => (forall (a :: k). Elem (f :.: g) as a -> Sing a -> h (p @@ a)) -> Sing as -> h (All (f :.: g) 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 IJust :: Maybe k -> k -> Type where

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

Constructors

IJust :: IJust (Just a) a

Instances

(SingI as, SDecide k) => Decidable (TyPred (IJust as) :: Predicate k)

Defined in Data.Type.Universe

Methods

decide :: Decide (TyPred (IJust as))

Show (IJust as a)

Defined in Data.Type.Universe

Methods

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

show :: IJust as a -> String

showList :: [IJust as a] -> ShowS

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

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

Constructors

IRight :: IRight (Right a) a

Instances

(SingI as, SDecide k) => Decidable (TyPred (IRight as) :: Predicate k)

Defined in Data.Type.Universe

Methods

decide :: Decide (TyPred (IRight as))

Show (IRight as a)

Defined in Data.Type.Universe

Methods

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

show :: IRight as a -> String

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

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

Constructors

ISnd :: ISnd '(a, b) b

Instances

(SingI as, SDecide k) => Decidable (TyPred (ISnd as) :: Predicate k)

Defined in Data.Type.Universe

Methods

decide :: Decide (TyPred (ISnd as))

Show (ISnd as a)

Defined in Data.Type.Universe

Methods

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

show :: ISnd as a -> String

showList :: [ISnd as a] -> ShowS

data IProxy :: Proxy k -> k -> Type

There are no items of type a in a Proxy a.

Since: 0.1.3.0

Instances

Provable (Not (TyPred (IProxy (Proxy :: Proxy k1))) :: TyFun k1 Type -> Type)

Defined in Data.Type.Universe

Methods

prove :: Prove (Not (TyPred (IProxy Proxy0)))

Show (IProxy (Proxy :: Proxy k) a)

Defined in Data.Type.Universe

Methods

showsPrec :: Int -> IProxy Proxy0 a -> ShowS

show :: IProxy Proxy0 a -> String

showList :: [IProxy Proxy0 a] -> ShowS

data IIdentity :: Identity k -> k -> Type where

Trivially witness the item held in an Identity.

Since: 0.1.3.0

Constructors

IId :: IIdentity (Identity x) x

Instances

(SingI as, SDecide k) => Decidable (TyPred (IIdentity as) :: Predicate k)

Defined in Data.Type.Universe

Methods

decide :: Decide (TyPred (IIdentity as))

Show (IIdentity as a)

Defined in Data.Type.Universe

Methods

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

show :: IIdentity as a -> String

showList :: [IIdentity as a] -> ShowS

data CompElem :: (f :.: g) k -> k -> Type where

A pair of indices allows you to index into a nested structure.

Since: 0.1.2.0

Constructors

(:?) :: Elem f ass as -> Elem g as a -> CompElem (Comp ass) a

data SumElem :: (f :+: g) k -> k -> Type where

Index into a disjoint union by providing an index into one of the two possible options.

Since: 0.1.3.0

Constructors

IInL :: Elem f as a -> SumElem (InL as) a

IInR :: Elem f bs b -> SumElem (InR bs) b

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 :: (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 :: (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 :: (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 ((,)0 j) @@ (w, a)

Auto (NotNull g :: Predicate (g k)) bs => Auto (NotNull (f :+: g) :: Predicate ((f :+: g) k)) (InR bs :: (f :+: g) k)

Defined in Data.Type.Predicate.Auto

Methods

auto :: NotNull (f :+: g) @@ InR bs

Auto (NotNull f :: Predicate (f k)) as => Auto (NotNull (f :+: g) :: Predicate ((f :+: g) k)) (InL as :: (f :+: g) k)

Defined in Data.Type.Predicate.Auto

Methods

auto :: NotNull (f :+: g) @@ InL as

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

Universe Combination

data family Sing (a :: k) :: Type

The singleton kind-indexed data family.

Instances

Provable (Evident :: Predicate k1)

Defined in Data.Type.Predicate

Methods

prove :: Prove Evident

Decidable (Evident :: Predicate k1)

Defined in Data.Type.Predicate

Methods

decide :: Decide Evident

SingI a => Auto (Evident :: Predicate k) (a :: k)

Defined in Data.Type.Predicate.Auto

Methods

auto :: Evident @@ a

Provable (Not (Impossible :: Predicate k1) :: TyFun k1 Type -> Type)

Defined in Data.Type.Predicate

Methods

prove :: Prove (Not Impossible)

SingI a => Auto (Not (Impossible :: Predicate k) :: TyFun k Type -> Type) (a :: k)

Since: 0.1.2.0

Defined in Data.Type.Predicate.Auto

Methods

auto :: Not Impossible @@ a

Provable ((p &&& Not p) ==> (Impossible :: Predicate k1) :: TyFun k1 Type -> Type)

Since: 0.1.3.0

Defined in Data.Type.Predicate.Logic

Methods

prove :: Prove ((p &&& Not p) ==> Impossible)

Provable ((Impossible :: Predicate k1) ==> p :: TyFun k1 Type -> Type)

Defined in Data.Type.Predicate.Logic

Methods

prove :: Prove (Impossible ==> p)

Decidable ((Impossible :: Predicate k1) ==> p :: TyFun k1 Type -> Type)

Defined in Data.Type.Predicate.Logic

Methods

decide :: Decide (Impossible ==> p)

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

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 ((,)0 j) @@ (w, a)

Auto (NotNull g :: Predicate (g k)) bs => Auto (NotNull (f :+: g) :: Predicate ((f :+: g) k)) (InR bs :: (f :+: g) k)

Defined in Data.Type.Predicate.Auto

Methods

auto :: NotNull (f :+: g) @@ InR bs

Auto (NotNull f :: Predicate (f k)) as => Auto (NotNull (f :+: g) :: Predicate ((f :+: g) k)) (InL as :: (f :+: g) k)

Defined in Data.Type.Predicate.Auto

Methods

auto :: NotNull (f :+: g) @@ InL as

data Sing (a :: Bool)

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Bool) where

• SFalse :: forall (a :: Bool). Sing False
• STrue :: forall (a :: Bool). Sing True

data Sing (a :: Ordering)

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Ordering) where

• SLT :: forall (a :: Ordering). Sing LT
• SEQ :: forall (a :: Ordering). Sing EQ
• SGT :: forall (a :: Ordering). Sing GT

data Sing (n :: Nat)

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Nat) where

• SNat :: forall (n :: Nat). KnownNat n => Sing n

data Sing (n :: Symbol)

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Symbol) where

• SSym :: forall (n :: Symbol). KnownSymbol n => Sing n

data Sing (a :: ())

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: ()) where

• STuple0 :: forall (a :: ()). Sing ()

data Sing (a :: Void)

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Void)

data Sing (a :: All)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: All) where

• SAll :: forall (a :: All) (n :: Bool). {..} -> Sing (All n)

data Sing (a :: Any)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: Any) where

• SAny :: forall (a :: Any) (n :: Bool). {..} -> Sing (Any n)

data Sing (b :: [a])

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: [a]) where

• SNil :: forall a (b :: [a]). Sing ([] :: [a])
• SCons :: forall a (b :: [a]) (n1 :: a) (n2 :: [a]). Sing n1 -> Sing n2 -> Sing (n1 ': n2)

data Sing (b :: Maybe a)

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: Maybe a) where

• SNothing :: forall a (b :: Maybe a). Sing (Nothing :: Maybe a)
• SJust :: forall a (b :: Maybe a) (n :: a). Sing n -> Sing (Just n)

data Sing (b :: Min a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Min a) where

• SMin :: forall a (b :: Min a) (n :: a). {..} -> Sing (Min n)

data Sing (b :: Max a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Max a) where

• SMax :: forall a (b :: Max a) (n :: a). {..} -> Sing (Max n)

data Sing (b :: First a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: First a) where

• SFirst :: forall a (b :: First a) (n :: a). {..} -> Sing (First n)

data Sing (b :: Last a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Last a) where

• SLast :: forall a (b :: Last a) (n :: a). {..} -> Sing (Last n)

data Sing (a :: WrappedMonoid m)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: WrappedMonoid m) where

• SWrapMonoid :: forall m (a :: WrappedMonoid m) (n :: m). {..} -> Sing (WrapMonoid n)

data Sing (b :: Option a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Option a) where

• SOption :: forall a (b :: Option a) (n :: Maybe a). {..} -> Sing (Option n)

data Sing (b :: Identity a)

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: Identity a) where

• SIdentity :: forall a (b :: Identity a) (n :: a). {..} -> Sing (Identity n)

data Sing (b :: First a)

Defined in Data.Singletons.Prelude.Monoid

data Sing (b :: First a) where

• SFirst :: forall a (b :: First a) (n :: Maybe a). {..} -> Sing (First n)

data Sing (b :: Last a)

Defined in Data.Singletons.Prelude.Monoid

data Sing (b :: Last a) where

• SLast :: forall a (b :: Last a) (n :: Maybe a). {..} -> Sing (Last n)

data Sing (b :: Dual a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Dual a) where

• SDual :: forall a (b :: Dual a) (n :: a). {..} -> Sing (Dual n)

data Sing (b :: Sum a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Sum a) where

• SSum :: forall a (b :: Sum a) (n :: a). {..} -> Sing (Sum n)

data Sing (b :: Product a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Product a) where

• SProduct :: forall a (b :: Product a) (n :: a). {..} -> Sing (Product n)

data Sing (b :: Down a)

Defined in Data.Singletons.Prelude.Ord

data Sing (b :: Down a) where

• SDown :: forall a (b :: Down a) (n :: a). Sing n -> Sing (Down n)

data Sing (b :: NonEmpty a)

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: NonEmpty a) where

• (:%|) :: forall a (b :: NonEmpty a) (n1 :: a) (n2 :: [a]). Sing n1 -> Sing n2 -> Sing (n1 :| n2)

data Sing (b :: Endo a)

Defined in Data.Singletons.Prelude.Foldable

data Sing (b :: Endo a) where

• SEndo :: forall a (b :: Endo a) (x :: a ~> a). Sing x -> Sing (Endo x)

data Sing (b :: MaxInternal a)

Defined in Data.Singletons.Prelude.Foldable

data Sing (b :: MaxInternal a) where

• SMaxInternal :: forall a (b :: MaxInternal a) (x :: Maybe a). Sing x -> Sing (MaxInternal x)

data Sing (b :: MinInternal a)

Defined in Data.Singletons.Prelude.Foldable

data Sing (b :: MinInternal a) where

• SMinInternal :: forall a (b :: MinInternal a) (x :: Maybe a). Sing x -> Sing (MinInternal x)

data Sing (c :: Either a b)

Defined in Data.Singletons.Prelude.Instances

data Sing (c :: Either a b) where

• SLeft :: forall a b (c :: Either a b) (n :: a). Sing n -> Sing (Left n :: Either a b)
• SRight :: forall a b (c :: Either a b) (n :: b). Sing n -> Sing (Right n :: Either a b)

data Sing (c :: (a, b))

Defined in Data.Singletons.Prelude.Instances

data Sing (c :: (a, b)) where

• STuple2 :: forall a b (c :: (a, b)) (n1 :: a) (n2 :: b). Sing n1 -> Sing n2 -> Sing ((,) n1 n2)

data Sing (c :: Arg a b)

Defined in Data.Singletons.Prelude.Semigroup

data Sing (c :: Arg a b) where

• SArg :: forall a b (c :: Arg a b) (n1 :: a) (n2 :: b). Sing n1 -> Sing n2 -> Sing (Arg n1 n2)

data Sing (f :: k1 ~> k2)

Defined in Data.Singletons.Internal

data Sing (f :: k1 ~> k2) = SLambda {

• applySing :: forall (t :: k1). Sing t -> Sing (f @@ t)

}

data Sing (b :: StateL s a)

Defined in Data.Singletons.Prelude.Traversable

data Sing (b :: StateL s a) where

• SStateL :: forall s a (b :: StateL s a) (x :: s ~> (s, a)). Sing x -> Sing (StateL x)

data Sing (b :: StateR s a)

Defined in Data.Singletons.Prelude.Traversable

data Sing (b :: StateR s a) where

• SStateR :: forall s a (b :: StateR s a) (x :: s ~> (s, a)). Sing x -> Sing (StateR x)

data Sing (d :: (a, b, c))

Defined in Data.Singletons.Prelude.Instances

data Sing (d :: (a, b, c)) where

• STuple3 :: forall a b c (d :: (a, b, c)) (n1 :: a) (n2 :: b) (n3 :: c). Sing n1 -> Sing n2 -> Sing n3 -> Sing ((,,) n1 n2 n3)

data Sing (c :: Const a b)

Defined in Data.Singletons.Prelude.Const

data Sing (c :: Const a b) where

• SConst :: forall k a (b :: k) (c :: Const a b) (a1 :: a). {..} -> Sing (Const a1 :: Const a b)

data Sing (e :: (a, b, c, d))

Defined in Data.Singletons.Prelude.Instances

data Sing (e :: (a, b, c, d)) where

• STuple4 :: forall a b c d (e :: (a, b, c, d)) (n1 :: a) (n2 :: b) (n3 :: c) (n4 :: d). Sing n1 -> Sing n2 -> Sing n3 -> Sing n4 -> Sing ((,,,) n1 n2 n3 n4)

data Sing (k :: (f :+: g) a)

Defined in Data.Type.Universe

data Sing (k :: (f :+: g) a) where

• SInL :: forall k (f :: k -> Type) (g :: k -> Type) (a :: k) (k :: (f :+: g) a) (x :: f a). Sing x -> Sing (InL x :: (f :+: g) a)
• SInR :: forall k (f :: k -> Type) (g :: k -> Type) (a :: k) (k :: (f :+: g) a) (y :: g a). Sing y -> Sing (InR y :: (f :+: g) a)

data Sing (f :: (a, b, c, d, e))

Defined in Data.Singletons.Prelude.Instances

data Sing (f :: (a, b, c, d, e)) where

• STuple5 :: forall a b c d e (f :: (a, b, c, d, e)) (n1 :: a) (n2 :: b) (n3 :: c) (n4 :: d) (n5 :: e). Sing n1 -> Sing n2 -> Sing n3 -> Sing n4 -> Sing n5 -> Sing ((,,,,) n1 n2 n3 n4 n5)

data Sing (k :: (f :.: g) a)

Defined in Data.Type.Universe

data Sing (k :: (f :.: g) a) where

• SComp :: forall k (f :: k -> Type) k (g :: k -> k) (a :: k) (k :: (f :.: g) a) (x :: f (g a)). Sing x -> Sing (Comp x)

data Sing (g :: (a, b, c, d, e, f))

Defined in Data.Singletons.Prelude.Instances

data Sing (g :: (a, b, c, d, e, f)) where

• STuple6 :: forall a b c d e f (g :: (a, b, c, d, e, f)) (n1 :: a) (n2 :: b) (n3 :: c) (n4 :: d) (n5 :: e) (n6 :: f). Sing n1 -> Sing n2 -> Sing n3 -> Sing n4 -> Sing n5 -> Sing n6 -> Sing ((,,,,,) n1 n2 n3 n4 n5 n6)

data Sing (h :: (a, b, c, d, e, f, g))

Defined in Data.Singletons.Prelude.Instances

data Sing (h :: (a, b, c, d, e, f, g)) where

• STuple7 :: forall a b c d e f g (h :: (a, b, c, d, e, f, g)) (n1 :: a) (n2 :: b) (n3 :: c) (n4 :: d) (n5 :: e) (n6 :: f) (n7 :: g). Sing n1 -> Sing n2 -> Sing n3 -> Sing n4 -> Sing n5 -> Sing n6 -> Sing n7 -> Sing ((,,,,,,) n1 n2 n3 n4 n5 n6 n7)

Universe Composition

data (f :.: g) a

Compose two Functors. Is the same as Compose and :.:, except with a singleton and meant to be used at the type level. Will be redundant if either of the above gets brought into the singletons library.

Note that because this is a higher-kinded data constructor, there is no SingKind instance; if you need fromSing and toSing, try going through Comp and getComp and SComp and sGetComp.

Note that Identity acts as an identity.

Since: 0.1.2.0

Constructors

Comp

Fields

• getComp :: f (g a)

Instances

AutoAll f (All g p) ass => AutoAll (f :.: g) (p :: Predicate a) (Comp ass :: (f :.: g) a)

Defined in Data.Type.Predicate.Auto

Methods

autoAll :: All (f :.: g) p @@ Comp ass

(Functor f, Functor g) => Functor (f :.: g)

Defined in Data.Type.Universe

Methods

fmap :: (a -> b) -> (f :.: g) a -> (f :.: g) b

(<$) :: a -> (f :.: g) b -> (f :.: g) a

(Foldable f, Foldable g) => Foldable (f :.: g)

Defined in Data.Type.Universe

Methods

fold :: Monoid m => (f :.: g) m -> m

foldMap :: Monoid m => (a -> m) -> (f :.: g) a -> m

foldr :: (a -> b -> b) -> b -> (f :.: g) a -> b

foldr' :: (a -> b -> b) -> b -> (f :.: g) a -> b

foldl :: (b -> a -> b) -> b -> (f :.: g) a -> b

foldl' :: (b -> a -> b) -> b -> (f :.: g) a -> b

foldr1 :: (a -> a -> a) -> (f :.: g) a -> a

foldl1 :: (a -> a -> a) -> (f :.: g) a -> a

toList :: (f :.: g) a -> [a]

null :: (f :.: g) a -> Bool

length :: (f :.: g) a -> Int

elem :: Eq a => a -> (f :.: g) a -> Bool

maximum :: Ord a => (f :.: g) a -> a

minimum :: Ord a => (f :.: g) a -> a

sum :: Num a => (f :.: g) a -> a

product :: Num a => (f :.: g) a -> a

(Traversable f, Traversable g) => Traversable (f :.: g)

Defined in Data.Type.Universe

Methods

traverse :: Applicative f0 => (a -> f0 b) -> (f :.: g) a -> f0 ((f :.: g) b)

sequenceA :: Applicative f0 => (f :.: g) (f0 a) -> f0 ((f :.: g) a)

mapM :: Monad m => (a -> m b) -> (f :.: g) a -> m ((f :.: g) b)

sequence :: Monad m => (f :.: g) (m a) -> m ((f :.: g) a)

(Universe f, Universe g) => Universe (f :.: g)

Defined in Data.Type.Universe

Methods

idecideAny :: (forall (a :: k). Elem (f :.: g) as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (Any (f :.: g) p @@ as)

idecideAll :: (forall (a :: k). Elem (f :.: g) as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (All (f :.: g) p @@ as)

igenAllA :: Applicative h => (forall (a :: k). Elem (f :.: g) as a -> Sing a -> h (p @@ a)) -> Sing as -> h (All (f :.: g) p @@ as)

Eq (f (g a)) => Eq ((f :.: g) a)

Defined in Data.Type.Universe

Methods

(==) :: (f :.: g) a -> (f :.: g) a -> Bool

(/=) :: (f :.: g) a -> (f :.: g) a -> Bool

Ord (f (g a)) => Ord ((f :.: g) a)

Defined in Data.Type.Universe

Methods

compare :: (f :.: g) a -> (f :.: g) a -> Ordering

(<) :: (f :.: g) a -> (f :.: g) a -> Bool

(<=) :: (f :.: g) a -> (f :.: g) a -> Bool

(>) :: (f :.: g) a -> (f :.: g) a -> Bool

(>=) :: (f :.: g) a -> (f :.: g) a -> Bool

max :: (f :.: g) a -> (f :.: g) a -> (f :.: g) a

min :: (f :.: g) a -> (f :.: g) a -> (f :.: g) a

Show (f (g a)) => Show ((f :.: g) a)

Defined in Data.Type.Universe

Methods

showsPrec :: Int -> (f :.: g) a -> ShowS

show :: (f :.: g) a -> String

showList :: [(f :.: g) a] -> ShowS

Generic ((f :.: g) a)

Defined in Data.Type.Universe

Associated Types

type Rep ((f :.: g) a) :: Type -> Type

Methods

from :: (f :.: g) a -> Rep ((f :.: g) a) x

to :: Rep ((f :.: g) a) x -> (f :.: g) a

SingI ass => SingI (Comp ass :: (f :.: g) a)

Defined in Data.Type.Universe

Methods

sing :: Sing (Comp ass)

type Elem (f :.: g)

Defined in Data.Type.Universe

type Elem (f :.: g) = (CompElem :: (f :.: g) k -> k -> Type)

type Apply (GetCompSym0 :: TyFun ((f :.: g) k3) (f (g k3)) -> Type) (Comp ass :: (f :.: g) k3)

Defined in Data.Type.Universe

type Apply (GetCompSym0 :: TyFun ((f :.: g) k3) (f (g k3)) -> Type) (Comp ass :: (f :.: g) k3) = ass

type Rep ((f :.: g) a)

Defined in Data.Type.Universe

type Rep ((f :.: g) a) = D1 (MetaData ":.:" "Data.Type.Universe" "decidable-0.1.4.0-L069M6H8crv32lYIvdPsSi" False) (C1 (MetaCons "Comp" PrefixI True) (S1 (MetaSel (Just "getComp") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (f (g a)))))

data Sing (k :: (f :.: g) a)

Defined in Data.Type.Universe

data Sing (k :: (f :.: g) a) where

• SComp :: forall k (f :: k -> Type) k (g :: k -> k) (a :: k) (k :: (f :.: g) a) (x :: f (g a)). Sing x -> Sing (Comp x)

sGetComp :: Sing a -> Sing (GetComp a)

Singletonized witness for GetComp

Since: 0.1.2.0

type family GetComp c where ...

getComp lifted to the type level

Since: 0.1.2.0

Equations

GetComp (Comp a) = a

allComp :: (All f (All g p) @@ as) -> All (f :.: g) p @@ Comp as

Turn a composition of All into an All of a composition.

Since: 0.1.2.0

compAll :: (All (f :.: g) p @@ Comp as) -> All f (All g p) @@ as

Turn an All of a composition into a composition of All.

Since: 0.1.2.0

anyComp :: (Any f (Any g p) @@ as) -> Any (f :.: g) p @@ Comp as

Turn a composition of Any into an Any of a composition.

Since: 0.1.2.0

compAny :: (Any (f :.: g) p @@ Comp as) -> Any f (Any g p) @@ as

Turn an Any of a composition into a composition of Any.

Since: 0.1.2.0

Universe Disjunction

data (f :+: g) a

Disjoint union of two Functors. Is the same as Sum and :+:, except with a singleton and meant to be used at the type level. Will be redundant if either of the above gets brought into the singletons library.

Note that because this is a higher-kinded data constructor, there is no SingKind instance; if you need fromSing and toSing, consider manually pattern matching.

Note that Proxy acts as an identity.

Since: 0.1.3.0

Constructors

InL (f a)

InR (g a)

Instances

AutoAll g p bs => AutoAll (f :+: g) (p :: Predicate a) (InR bs :: (f :+: g) a)

Defined in Data.Type.Predicate.Auto

Methods

autoAll :: All (f :+: g) p @@ InR bs

AutoAll f p as => AutoAll (f :+: g) (p :: Predicate a) (InL as :: (f :+: g) a)

Defined in Data.Type.Predicate.Auto

Methods

autoAll :: All (f :+: g) p @@ InL as

AutoElem g bs b => AutoElem (f :+: g) (InR bs :: (f :+: g) k) (b :: k)

Defined in Data.Type.Predicate.Auto

Methods

autoElem :: Elem (f :+: g) (InR bs) b

AutoElem f as a => AutoElem (f :+: g) (InL as :: (f :+: g) k) (a :: k)

Defined in Data.Type.Predicate.Auto

Methods

autoElem :: Elem (f :+: g) (InL as) a

(Functor f, Functor g) => Functor (f :+: g)

Defined in Data.Type.Universe

Methods

fmap :: (a -> b) -> (f :+: g) a -> (f :+: g) b

(<$) :: a -> (f :+: g) b -> (f :+: g) a

(Foldable f, Foldable g) => Foldable (f :+: g)

Defined in Data.Type.Universe

Methods

fold :: Monoid m => (f :+: g) m -> m

foldMap :: Monoid m => (a -> m) -> (f :+: g) a -> m

foldr :: (a -> b -> b) -> b -> (f :+: g) a -> b

foldr' :: (a -> b -> b) -> b -> (f :+: g) a -> b

foldl :: (b -> a -> b) -> b -> (f :+: g) a -> b

foldl' :: (b -> a -> b) -> b -> (f :+: g) a -> b

foldr1 :: (a -> a -> a) -> (f :+: g) a -> a

foldl1 :: (a -> a -> a) -> (f :+: g) a -> a

toList :: (f :+: g) a -> [a]

null :: (f :+: g) a -> Bool

length :: (f :+: g) a -> Int

elem :: Eq a => a -> (f :+: g) a -> Bool

maximum :: Ord a => (f :+: g) a -> a

minimum :: Ord a => (f :+: g) a -> a

sum :: Num a => (f :+: g) a -> a

product :: Num a => (f :+: g) a -> a

(Traversable f, Traversable g) => Traversable (f :+: g)

Defined in Data.Type.Universe

Methods

traverse :: Applicative f0 => (a -> f0 b) -> (f :+: g) a -> f0 ((f :+: g) b)

sequenceA :: Applicative f0 => (f :+: g) (f0 a) -> f0 ((f :+: g) a)

mapM :: Monad m => (a -> m b) -> (f :+: g) a -> m ((f :+: g) b)

sequence :: Monad m => (f :+: g) (m a) -> m ((f :+: g) a)

(Universe f, Universe g) => Universe (f :+: g)

Defined in Data.Type.Universe

Methods

idecideAny :: (forall (a :: k). Elem (f :+: g) as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (Any (f :+: g) p @@ as)

idecideAll :: (forall (a :: k). Elem (f :+: g) as a -> Sing a -> Decision (p @@ a)) -> Sing as -> Decision (All (f :+: g) p @@ as)

igenAllA :: Applicative h => (forall (a :: k). Elem (f :+: g) as a -> Sing a -> h (p @@ a)) -> Sing as -> h (All (f :+: g) p @@ as)

(Eq (f a), Eq (g a)) => Eq ((f :+: g) a)

Defined in Data.Type.Universe

Methods

(==) :: (f :+: g) a -> (f :+: g) a -> Bool

(/=) :: (f :+: g) a -> (f :+: g) a -> Bool

(Ord (f a), Ord (g a)) => Ord ((f :+: g) a)

Defined in Data.Type.Universe

Methods

compare :: (f :+: g) a -> (f :+: g) a -> Ordering

(<) :: (f :+: g) a -> (f :+: g) a -> Bool

(<=) :: (f :+: g) a -> (f :+: g) a -> Bool

(>) :: (f :+: g) a -> (f :+: g) a -> Bool

(>=) :: (f :+: g) a -> (f :+: g) a -> Bool

max :: (f :+: g) a -> (f :+: g) a -> (f :+: g) a

min :: (f :+: g) a -> (f :+: g) a -> (f :+: g) a

(Show (f a), Show (g a)) => Show ((f :+: g) a)

Defined in Data.Type.Universe

Methods

showsPrec :: Int -> (f :+: g) a -> ShowS

show :: (f :+: g) a -> String

showList :: [(f :+: g) a] -> ShowS

Generic ((f :+: g) a)

Defined in Data.Type.Universe

Associated Types

type Rep ((f :+: g) a) :: Type -> Type

Methods

from :: (f :+: g) a -> Rep ((f :+: g) a) x

to :: Rep ((f :+: g) a) x -> (f :+: g) a

Auto (NotNull g :: Predicate (g k)) bs => Auto (NotNull (f :+: g) :: Predicate ((f :+: g) k)) (InR bs :: (f :+: g) k)

Defined in Data.Type.Predicate.Auto

Methods

auto :: NotNull (f :+: g) @@ InR bs

Auto (NotNull f :: Predicate (f k)) as => Auto (NotNull (f :+: g) :: Predicate ((f :+: g) k)) (InL as :: (f :+: g) k)

Defined in Data.Type.Predicate.Auto

Methods

auto :: NotNull (f :+: g) @@ InL as

type Elem (f :+: g)

Defined in Data.Type.Universe

type Elem (f :+: g) = (SumElem :: (f :+: g) k -> k -> Type)

type Rep ((f :+: g) a)

Defined in Data.Type.Universe

type Rep ((f :+: g) a) = D1 (MetaData ":+:" "Data.Type.Universe" "decidable-0.1.4.0-L069M6H8crv32lYIvdPsSi" False) (C1 (MetaCons "InL" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (f a))) :+: C1 (MetaCons "InR" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (g a))))

data Sing (k :: (f :+: g) a)

Defined in Data.Type.Universe

data Sing (k :: (f :+: g) a) where

• SInL :: forall k (f :: k -> Type) (g :: k -> Type) (a :: k) (k :: (f :+: g) a) (x :: f a). Sing x -> Sing (InL x :: (f :+: g) a)
• SInR :: forall k (f :: k -> Type) (g :: k -> Type) (a :: k) (k :: (f :+: g) a) (y :: g a). Sing y -> Sing (InR y :: (f :+: g) a)

anySumL :: (Any f p @@ as) -> Any (f :+: g) p @@ InL as

Turn an Any of f into an Any of f :+: g.

anySumR :: (Any g p @@ bs) -> Any (f :+: g) p @@ InR bs

Turn an Any of g into an Any of f :+: g.

sumLAny :: (Any (f :+: g) p @@ InL as) -> Any f p @@ as

Turn an Any of f :+: g into an Any of f.

sumRAny :: (Any (f :+: g) p @@ InR bs) -> Any g p @@ bs

Turn an Any of f :+: g into an Any of g.

allSumL :: (All f p @@ as) -> All (f :+: g) p @@ InL as

Turn an All of f into an All of f :+: g.

allSumR :: (All g p @@ bs) -> All (f :+: g) p @@ InR bs

Turn an All of g into an All of f :+: g.

sumLAll :: (All (f :+: g) p @@ InL as) -> All f p @@ as

Turn an All of f :+: g into an All of f.

sumRAll :: (All (f :+: g) p @@ InR bs) -> All g p @@ bs

Turn an All of f :+: g into an All of g.

Defunctionalization symbols

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

Instances

type Apply (ElemSym0 f :: TyFun (f k) (k ~> Type) -> Type) (as :: f k)

Defined in Data.Type.Universe

type Apply (ElemSym0 f :: TyFun (f k) (k ~> Type) -> Type) (as :: f k) = ElemSym1 f as

data ElemSym1 (f :: Type -> Type) :: f k -> k ~> Type

Instances

AutoElem f as a => Auto (In f as :: TyFun k Type -> Type) (a :: k)

Defined in Data.Type.Predicate.Auto

Methods

auto :: In f as @@ a

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

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

Universe f => Decidable (Found (InP f :: ParamPred (f v) v) :: TyFun (f v) Type -> Type)

Defined in Data.Type.Predicate.Param

Methods

decide :: Decide (Found (InP f))

type Apply (ElemSym1 f as :: TyFun k Type -> Type) (a :: k)

Defined in Data.Type.Universe

type Apply (ElemSym1 f as :: TyFun k Type -> Type) (a :: k) = Elem f as a

type ElemSym2 (f :: Type -> Type) (as :: f k) (a :: k) = Elem f as a

data GetCompSym0 :: (f :.: g) k ~> f (g k)

Instances

type Apply (GetCompSym0 :: TyFun ((f :.: g) k3) (f (g k3)) -> Type) (Comp ass :: (f :.: g) k3)

Defined in Data.Type.Universe

type Apply (GetCompSym0 :: TyFun ((f :.: g) k3) (f (g k3)) -> Type) (Comp ass :: (f :.: g) k3) = ass

type GetCompSym1 a = GetComp a