| Maintainer | Olaf Klinke |
|---|---|
| Stability | experimental |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Data.Type.Refine
Description
This module defines classes
of refinable types and their Generic representations.
There are two ways to semi-automatically have a Refinable instance for a given type X:
Either the type is Generic, in which case a GRefine instance
can be derived for its Representation.
instance Refinable X where
If the type is not Generic, you can use the implementation
instance Refinable X where
refine = refineDeMorgan
that applies the deMorgan laws until the predicate is known to either cover or delete the type.
Synopsis
- type Refinement = GSubType GStone GRefine
- refinedTypeDef :: Refinement f -> SomeTypeRep
- runRefinement :: StoneSpace t => Refinement (Rep t) -> Dynamic -> Maybe t
- class Refinable c where
- class Typeable f => GRefine f where
- grefine :: Predicate f -> Refinement f
- refineDeMorgan :: GRefine f => Predicate f -> Refinement f
- module Data.Type.Predicate
Refinements
type Refinement = GSubType GStone GRefine Source #
Sub-types are given as the predicate transformer duals of embeddings where the domain is existentially quantified. The domain is required to be refinable, too.
refinedTypeDef :: Refinement f -> SomeTypeRep Source #
Extract the type definition of the refined sub-type.
runRefinement :: StoneSpace t => Refinement (Rep t) -> Dynamic -> Maybe t Source #
Since the refined sub-type is hidden inside an existential quantification,
we can run the embedding only detour via Dynamic.
It is ensured that all Dynamic values constructed from the type
given by refinedTypeDef will be mapped to a Just.
Executing a predicate transformer GStone requires the target to be a StoneSpace.
Refinable types
class Refinable c where Source #
Since Predicate has kind (Type -> Type) -> Type
we have to wrap a monomorphic type in a K1.
This is in line with the usage of constants on Generic types.
Minimal complete definition
Nothing
class Typeable f => GRefine f where Source #
Class of Representations of refinable types.
The default implementation has inexhaustive pattern matches
for any type with Predicates that go beyond the Boolean connectives
and should therefore be overridden.
Minimal complete definition
Nothing
Methods
grefine :: Predicate f -> Refinement f Source #
Instances
| GRefine (U1 :: Type -> Type) Source # | |
Defined in Data.Type.Refine | |
| GRefine f => GRefine (Rec1 f) Source # | |
Defined in Data.Type.Refine | |
| (GRefine f, GRefine g) => GRefine (f :*: g) Source # | |
Defined in Data.Type.Refine | |
| (GRefine f, GRefine g) => GRefine (f :+: g) Source # | |
Defined in Data.Type.Refine | |
| (Refinable c, Typeable c) => GRefine (K1 R c :: Type -> Type) Source # | |
Defined in Data.Type.Refine | |
| (GRefine f, Typeable i, Typeable m) => GRefine (M1 i m f) Source # | |
Defined in Data.Type.Refine | |
refineDeMorgan :: GRefine f => Predicate f -> Refinement f Source #
For types that have only the Boolean connectives as predicates,
the only possible sub-types are the empty type and the entire type.
Use this as default implementation of refine.
Predicates (re-export)
module Data.Type.Predicate