| Maintainer | Olaf Klinke |
|---|---|
| Stability | experimental |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Data.SubType
Description
Functions with codomain x, regardless of their domain,
can be encoded in the GADT
data Codomain :: Type -> Type where
Fun :: (y -> x) -> Codomain x
This module decorates this GADT with constraints on the domain y
and generalizes functions to morphisms of arbitrary categories.
Synopsis
- data SomeSubType :: (Type -> Constraint) -> Type -> Type where
- EmptySubType :: SomeSubType con t
- Embed :: con x => (x -> y) -> SomeSubType con y
- idSubType :: con t => SomeSubType con t
- runEmbedding :: (forall x. con x => rep -> Maybe x) -> SomeSubType con y -> rep -> Maybe y
- subDomain :: SomeSubType Typeable x -> SomeTypeRep
- runEmbeddingDynamic :: SomeSubType Typeable x -> Dynamic -> Maybe x
- data GSubType :: (k -> k -> Type) -> (k -> Constraint) -> k -> Type where
- idGSubType :: (Category cat, con x) => GSubType cat con x
- mapGSubType :: Category cat => cat x y -> GSubType cat con x -> GSubType cat con y
- runGEmbedding :: (forall g. con g => cat g f -> Dynamic -> Maybe (g ())) -> (forall s. cat s f -> s () -> f ()) -> GSubType cat con f -> Dynamic -> Maybe (f ())
Documentation
data SomeSubType :: (Type -> Constraint) -> Type -> Type where Source #
Constrained sub-types. This data type records the embedding function but hides its domain in an existential type. This allows us to compute an embedding at run-time. As an extra parameter, we pass a type class so that only those sub-types are representable that are member of this class.
Constructors
| EmptySubType :: SomeSubType con t | |
| Embed :: con x => (x -> y) -> SomeSubType con y |
Instances
| Functor (SomeSubType con) Source # | post-compose embeddings with functions. This allows us to nest embeddings. |
Defined in Data.SubType Methods fmap :: (a -> b) -> SomeSubType con a -> SomeSubType con b # (<$) :: a -> SomeSubType con b -> SomeSubType con a # | |
idSubType :: con t => SomeSubType con t Source #
embed a type into itself via the identity function.
runEmbedding :: (forall x. con x => rep -> Maybe x) -> SomeSubType con y -> rep -> Maybe y Source #
In order to run an embedding with unknown domain,
we need a function that can convert a single universal type rep
to any sub-type.
Nothing is returned if the rep value does not represent
an element of the sub-type, in particular if the sub-type is empty.
subDomain :: SomeSubType Typeable x -> SomeTypeRep Source #
The representation of the type of the domain of the sub-type embedding.
runEmbeddingDynamic :: SomeSubType Typeable x -> Dynamic -> Maybe x Source #
It is guaranteed that for every f :: y -> x with Typeable y,
runEmbeddingDynamic (Embed f) (toDyn y) = Just (f y)
data GSubType :: (k -> k -> Type) -> (k -> Constraint) -> k -> Type where Source #
Poly-kinded version of SomeSubType
generalized to arbitrary categories.
idGSubType :: (Category cat, con x) => GSubType cat con x Source #
the identiy morphism
mapGSubType :: Category cat => cat x y -> GSubType cat con x -> GSubType cat con y Source #
GSubType cat concat.