Copyright | (c) Justin Le 2018 |
---|---|
License | BSD3 |
Maintainer | justin@jle.im |
Stability | experimental |
Portability | non-portable |
Safe Haskell | None |
Language | Haskell2010 |
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
- data IJust (a :: Maybe k) (b :: k) where
- data IRight (a :: Either j k) (b :: k) where
- data NEIndex (a :: NonEmpty k) (b :: k) where
- data ISnd (a :: (j, k)) (b :: k) where
- data IIdentity (a :: Identity k) (b :: k) where
- data All f :: Predicate k -> Predicate (f k)
- newtype WitAll f p (as :: f k) = WitAll {}
- 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
- 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 #
type In (f :: Type -> Type) (as :: f k) = ElemSym1 f as Source #
is a predicate that a given input In
f asa
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.
:: 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 |
:: 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 |
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
Universe [] Source # | |
Defined in Data.Type.Universe 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 Maybe Source # | |
Defined in Data.Type.Universe 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 Identity Source # | The single-pointed universe. |
Defined in Data.Type.Universe 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 # | |
Defined in Data.Type.Universe 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 (Either j) Source # | |
Defined in Data.Type.Universe 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 # | |
Defined in Data.Type.Universe 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
into a proof that all Sing
asa
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 IS
s correspond to the item's position in the list.
IZ
::Index
'[5,10,2] 5IS
IZ
::Index
'[5,10,2] 10IS
(IS
IZ
) ::Index
'[5,10,2] 2
IZ :: forall k (b :: k) (as :: [k]). Index (b ': as) b | |
IS :: forall k (bs :: [k]) (b :: k) (b1 :: k). Index bs b -> Index (b1 ': bs) b |
Instances
Eq (Index as a) | |
Ord (Index as a) | |
Show (Index as a) | |
SDecide (Index as a) | |
SingKind (Index as a) | |
SingI ('IZ :: Index (a ': as) a) | |
Defined in Data.Type.Functor.Product | |
SingI i => SingI ('IS i :: Index (b ': bs) a) | |
Defined in Data.Type.Functor.Product | |
type Sing | |
Defined in Data.Type.Functor.Product | |
type Demote (Index as a) | |
Defined in Data.Type.Functor.Product |
data IJust (a :: Maybe k) (b :: k) where #
Instances
Eq (IJust as a) | |
Ord (IJust as a) | |
Read (IJust ('Just a) a) | |
Show (IJust as a) | |
SDecide (IJust as a) | |
SingKind (IJust as a) | |
SingI ('IJust :: IJust ('Just a) a) | |
Defined in Data.Type.Functor.Product | |
type Sing | |
Defined in Data.Type.Functor.Product | |
type Demote (IJust as a) | |
Defined in Data.Type.Functor.Product |
data IRight (a :: Either j k) (b :: k) where #
Instances
Eq (IRight as a) | |
Ord (IRight as a) | |
Defined in Data.Type.Functor.Product | |
Read (IRight ('Right a :: Either j k) a) | |
Show (IRight as a) | |
SDecide (IRight as a) | |
SingKind (IRight as a) | |
SingI ('IRight :: IRight ('Right a :: Either j k) a) | |
Defined in Data.Type.Functor.Product | |
type Sing | |
Defined in Data.Type.Functor.Product | |
type Demote (IRight as a) | |
Defined in Data.Type.Functor.Product |
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".
NEHead :: forall k (b :: k) (as :: [k]). NEIndex (b :| as) b | |
NETail :: forall k (as :: [k]) (b :: k) (b1 :: k). Index as b -> NEIndex (b1 :| as) b |
Instances
Eq (NEIndex as a) | |
Ord (NEIndex as a) | |
Defined in Data.Type.Functor.Product | |
Show (NEIndex as a) | |
SDecide (NEIndex as a) | |
SingKind (NEIndex as a) | |
SingI ('NEHead :: NEIndex (a :| as) a) | |
Defined in Data.Type.Functor.Product | |
SingI i => SingI ('NETail i :: NEIndex (b :| as) a) | |
Defined in Data.Type.Functor.Product | |
type Sing | |
Defined in Data.Type.Functor.Product | |
type Demote (NEIndex as a) | |
Defined in Data.Type.Functor.Product |
data ISnd (a :: (j, k)) (b :: k) where #
Trivially witness an item in the second field of a type-level tuple.
Instances
Eq (ISnd as a) | |
Ord (ISnd as a) | |
Defined in Data.Type.Functor.Product | |
Read (ISnd '(a, b) b) | |
Show (ISnd as a) | |
SDecide (ISnd as a) | |
SingKind (ISnd as a) | |
SingI ('ISnd :: ISnd '(a, b) b) | |
Defined in Data.Type.Functor.Product | |
type Sing | |
Defined in Data.Type.Functor.Product | |
type Demote (ISnd as a) | |
Defined in Data.Type.Functor.Product |
data IIdentity (a :: Identity k) (b :: k) where #
Trivially witness the item held in an Identity
.
Since: functor-products-0.1.3.0
Instances
Eq (IIdentity as a) | |
Ord (IIdentity as a) | |
Defined in Data.Type.Functor.Product 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 # | |
Read (IIdentity ('Identity a) a) | |
Show (IIdentity as a) | |
SDecide (IIdentity as a) | |
SingKind (IIdentity as a) | |
SingI ('IId :: IIdentity ('Identity x) x) | |
Defined in Data.Type.Functor.Product | |
type Sing | |
Defined in Data.Type.Functor.Product | |
type Demote (IIdentity as a) | |
Defined in Data.Type.Functor.Product |
Predicates
data All f :: Predicate k -> Predicate (f k) Source #
An
is a predicate testing a collection All
f pas :: 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) Source # | |
Universe f => DFunctor (All f :: Predicate k1 -> TyFun (f k1) Type -> Type) Source # | |
(Universe f, Provable p) => Provable (All f p :: TyFun (f k) Type -> Type) Source # | |
(Universe f, Decidable p) => Decidable (All f p :: TyFun (f k) Type -> Type) Source # | |
AutoAll f p as => Auto (All f p :: TyFun (f k) Type -> Type) (as :: f k) Source # | Since: 0.1.2.0 |
type Apply (All f p :: TyFun (f k) Type -> Type) (as :: f k) Source # | |
newtype WitAll f p (as :: f k) Source #
A
is a witness that the predicate WitAll
p asp a
is true for all
items a
in the type-level collection as
.
type NotAll f p = Not (All f p) :: Predicate (f k) Source #
A
is a predicate on a collection NotAll
f pas
that at least one
a
in as
does not satisfy predicate p
.
data Any f :: Predicate k -> Predicate (f k) Source #
An
is a predicate testing a collection Any
f pas :: 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
data WitAny f :: (k ~> Type) -> f k -> Type where Source #
A
is a witness that, for at least one item WitAny
p asa
in the
type-level collection as
, the predicate p a
is true.
type None f p = Not (Any f p) :: Predicate (f k) Source #
A
is a predicate on a collection None
f pas
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
Decisions and manipulations
:: 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.
:: 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.