Data.Yoko.InDT

Various universes determined by a data constructor type's suitability to be embedded in a data type.

Documentation

data HasTagRepDCD tag c t where

A type t inhabits HasTagRepDCD tag c if t is a DT and there exists a t constructor satisfying TagRepIs tag c.

Constructors

HasTagRepDCD :: DT t => Exists (DCOf t :&& TagRepIs tag c) (DCs t) -> HasTagRepDCD tag c t

Instances

(DT t, (DCs t) ::: (Exists (:&& (DCOf t) (TagRepIs tag c)))) => t ::: (HasTagRepDCD tag c)

hasTagRepDCD :: HasTagRepDCD tag c t -> RMI c -> t

Given HasTagRepDCD tag c t, a trivially-mediated c value can be embedded into t.

type HasTagRepDCImageD fn dc = HasTagRepDCD (Tag dc) (CApp fn (Rep dc))

Often times, we're interested in the universe of types accomodating a data constructor's image under some type-function.

data ImageInDTD t fn dc where

A constructor type dc inhabits ImageHasTagRepDCD t fn if

1. fn can be mapped across the recursive occurrences in dc, and
2. t has a constructor isomorphic to the fn-image of dc

Constructors

ImageInDTD :: (Generic dc, (Rep dc) ::: (Domain (CMap fn IdM))) => HasTagRepDCImageD (fn IdM) dc t -> ImageInDTD t fn dc

Instances

(Generic dc, (Rep dc) ::: (Domain (CMap fn IdM)), t ::: (HasTagRepDCImageD (fn IdM) dc)) => dc ::: (ImageInDTD t fn)

imageInDTD :: (forall t. fn IdM t) -> ImageInDTD t fn dc -> RMNI dc -> t

Given ImageInDTD t fn dc, a trivially-mediated dc value can be embedded into t.

data ImageInDTDA t fn dc where

Same as ImageInDTD, but uses an implicitly applicative function.

Constructors

ImageInDTDA :: (Generic dc, (Rep dc) ::: (DomainA (CMap fn IdM))) => HasTagRepDCImageD (fn IdM) dc t -> ImageInDTDA t fn dc

Instances

(Generic dc, (Rep dc) ::: (DomainA (CMap fn IdM)), t ::: (HasTagRepDCImageD (fn IdM) dc)) => dc ::: (ImageInDTDA t fn)

imageInDTAD :: Functor (Idiom (fn IdM)) => (forall t. fn IdM t) -> ImageInDTDA t fn dc -> RMNI dc -> Idiom (fn IdM) t