|Portability||see LANGUAGE pragmas (... GHC)|
Various universes determined by a data constructor type's suitability to be embedded in a data type.
- data HasTagRepDCD tag c t where
- hasTagRepDCD :: HasTagRepDCD tag c t -> RMI c -> t
- type HasTagRepDCImageD fn dc = HasTagRepDCD (Tag dc) (CApp fn (Rep dc))
- data ImageInDTD t fn dc where
- imageInDTD :: (forall t. fn IdM t) -> ImageInDTD t fn dc -> RMNI dc -> t
- data ImageInDTDA t fn dc where
- imageInDTAD :: Functor (Idiom (fn IdM)) => (forall t. fn IdM t) -> ImageInDTDA t fn dc -> RMNI dc -> Idiom (fn IdM) t
HasTagRepDCD tag c t, a trivially-mediated
c value can be embedded into
Often times, we're interested in the universe of types accomodating a data constructor's image under some type-function.
A constructor type
ImageHasTagRepDCD t fn if
fncan be mapped across the recursive occurrences in
thas a constructor isomorphic to the
|ImageInDTD :: (Generic dc, (Rep dc) ::: (Domain (CMap fn IdM))) => HasTagRepDCImageD (fn IdM) dc t -> ImageInDTD t fn dc|
ImageInDTD t fn dc, a trivially-mediated
dc value can be
ImageInDTD, but uses an implicitly applicative function.
|ImageInDTDA :: (Generic dc, (Rep dc) ::: (DomainA (CMap fn IdM))) => HasTagRepDCImageD (fn IdM) dc t -> ImageInDTDA t fn dc|