| Maintainer | Olaf Klinke |
|---|---|
| Stability | experimental |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Data.Type.Predicate
Description
This module defines the GADT Predicate
and the category of predicate transformers.
Synopsis
- data Predicate :: (Type -> Type) -> Type where
- Wildcard :: Predicate ty
- Neg :: Predicate ty -> Predicate ty
- (:\/) :: Predicate ty -> Predicate ty -> Predicate ty
- (:/\) :: Predicate ty -> Predicate ty -> Predicate ty
- Fst :: Predicate f -> Predicate (f :*: g)
- Snd :: Predicate g -> Predicate (f :*: g)
- Case :: Predicate f -> Predicate g -> Predicate (f :+: g)
- RecP :: Predicate f -> Predicate (Rec1 f)
- MetaP :: Predicate f -> Predicate (M1 i m f)
- ConstP :: (Generic c, Rep c ~ f) => Predicate f -> Predicate (K1 i c)
- eval :: Predicate ty -> ty p -> Bool
- insL :: Predicate (f :+: g) -> Predicate f
- insR :: Predicate (f :+: g) -> Predicate g
- first :: (Predicate f -> Predicate g) -> Predicate (f :*: h) -> Predicate (g :*: h)
- second :: (Predicate f -> Predicate g) -> Predicate (h :*: f) -> Predicate (h :*: g)
- mapRec :: Predicate (Rec1 f) -> Predicate f
- mapMeta :: Predicate (M1 i m f) -> Predicate f
- mapConst :: Generic c => Predicate (K1 i c) -> Predicate (Rep c)
- newtype GStone f g = GStone (Predicate g -> Predicate f)
- gDomain :: forall f g. Typeable (f ()) => GStone f g -> SomeTypeRep
- universalProd :: (Predicate a -> Predicate z) -> (Predicate b -> Predicate z) -> Predicate (a :*: b) -> Predicate z
- universalUnion :: (Predicate z -> Predicate a) -> (Predicate z -> Predicate b) -> Predicate z -> Predicate (a :+: b)
Predicates on polynomial types
data Predicate :: (Type -> Type) -> Type where Source #
Predicates on Generic representations of polynomial types.
The only way to evaluate predicates on unions is to do Case analysis.
All predicates on products must eventually extract the first or second component.
Constructors
| Wildcard | |
Fields
| |
| Neg | |
| (:\/) | |
| (:/\) | |
| Fst :: Predicate f -> Predicate (f :*: g) | |
| Snd :: Predicate g -> Predicate (f :*: g) | |
| Case :: Predicate f -> Predicate g -> Predicate (f :+: g) | |
| RecP :: Predicate f -> Predicate (Rec1 f) | |
| MetaP :: Predicate f -> Predicate (M1 i m f) | |
| ConstP :: (Generic c, Rep c ~ f) => Predicate f -> Predicate (K1 i c) | |
Predicate transformers
first :: (Predicate f -> Predicate g) -> Predicate (f :*: h) -> Predicate (g :*: h) Source #
Stone dual of Control.Arrow.first
second :: (Predicate f -> Predicate g) -> Predicate (h :*: f) -> Predicate (h :*: g) Source #
Stone dual of Control.Arrow.second
gDomain :: forall f g. Typeable (f ()) => GStone f g -> SomeTypeRep Source #
The monomorphic type representation
of the domain f of the morphism,
instantiated at parameter ().