{-# LANGUAGE TypeOperators, GADTs, FlexibleInstances, MultiParamTypeClasses, FlexibleContexts, UndecidableInstances, Rank2Types #-} {- | Module : Data.Yoko.InDT Copyright : (c) The University of Kansas 2011 License : BSD3 Maintainer : nicolas.frisby@gmail.com Stability : experimental Portability : see LANGUAGE pragmas (... GHC) Various universes determined by a data constructor type's suitability to be embedded in a data type. -} module Data.Yoko.InDT where import Type.Yoko import Data.Yoko.Generic import Data.Yoko.Reflect -- | A type @t@ inhabits @HasTagRepU tag c@ if @t@ is a 'DT' and there exists a @t@ -- constructor satisfying @'TagRepIs' tag c@. data HasTagRepU tag c t where HasTagRepU :: DT t => Exists (DCOf t :&& TagRepIs tag c) (DCs t) -> HasTagRepU tag c t instance (DT t, DCs t ::: Exists (DCOf t :&& TagRepIs tag c) ) => t ::: HasTagRepU tag c where inhabits = HasTagRepU inhabits -- | Given @HasTagRepU tag c t@, a trivially-mediated @c@ value can be embedded into -- @t@. hasTagRepU :: HasTagRepU tag c t -> RMI c -> t hasTagRepU (HasTagRepU d) = w d where w :: Exists (DCOf t :&& TagRepIs tag c) dcs -> RMI c -> t w (Here (x@(DCOf _) :&& TagRepIs)) = fr_DCOf x . obj w (OnLeft u) = w u; w (OnRight u) = w u -- | Often times, we're interested in the universe of types accomodating a data -- constructor's image under some type-function. type HasTagRepImageU fn dc = HasTagRepU (Tag dc) (CApp fn (Rep dc)) -- | A constructor type @dc@ inhabits @ImageHasTagRepU 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@ data ImageInDTU t fn dc where ImageInDTU :: (Generic dc, Rep dc ::: Domain (CMap fn IdM) ) => HasTagRepImageU (fn IdM) dc t -> ImageInDTU t fn dc instance (Generic dc, Rep dc ::: Domain (CMap fn IdM), t ::: HasTagRepImageU (fn IdM) dc ) => dc ::: ImageInDTU t fn where inhabits = ImageInDTU inhabits -- | Given @ImageInDTU t fn dc@, a trivially-mediated @dc@ value can be -- embedded into @t@. imageInDTU :: (forall t. fn IdM t) -> ImageInDTU t fn dc -> RMNI dc -> t imageInDTU fn (ImageInDTU d) = hasTagRepU d . apply (CMap fn) . rep -- | Same as @ImageInDTD@, but uses an implicitly applicative function. data ImageInDTDA t fn dc where ImageInDTDA :: (Generic dc, Rep dc ::: DomainA (CMap fn IdM) ) => HasTagRepImageU (fn IdM) dc t -> ImageInDTDA t fn dc instance (Generic dc, Rep dc ::: DomainA (CMap fn IdM), t ::: HasTagRepImageU (fn IdM) dc ) => dc ::: ImageInDTDA t fn where inhabits = ImageInDTDA inhabits imageInDTAU :: Functor (Idiom (fn IdM)) => (forall t. fn IdM t) -> ImageInDTDA t fn dc -> RMNI dc -> Idiom (fn IdM) t imageInDTAU fn (ImageInDTDA d) = fmap (hasTagRepU d) . applyA (CMap fn) . rep