{-# 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 @HasTagRepDCD tag c@ if @t@ is a 'DT' and there exists a @t@ -- constructor satisfying @'TagRepIs' tag c@. data HasTagRepDCD tag c t where HasTagRepDCD :: DT t => Exists (DCOf t :&& TagRepIs tag c) (DCs t) -> HasTagRepDCD tag c t instance (DT t, DCs t ::: Exists (DCOf t :&& TagRepIs tag c) ) => t ::: HasTagRepDCD tag c where inhabits = HasTagRepDCD inhabits -- | Given @HasTagRepDCD tag c t@, a trivially-mediated @c@ value can be embedded into -- @t@. hasTagRepDCD :: HasTagRepDCD tag c t -> RMI c -> t hasTagRepDCD (HasTagRepDCD 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 HasTagRepDCImageD fn dc = HasTagRepDCD (Tag dc) (CApp fn (Rep dc)) -- | 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@ data ImageInDTD t fn dc where ImageInDTD :: (Generic dc, Rep dc ::: Domain (CMap fn IdM) ) => HasTagRepDCImageD (fn IdM) dc t -> ImageInDTD t fn dc instance (Generic dc, Rep dc ::: Domain (CMap fn IdM), t ::: HasTagRepDCImageD (fn IdM) dc ) => dc ::: ImageInDTD t fn where inhabits = ImageInDTD inhabits -- | Given @ImageInDTD t fn dc@, a trivially-mediated @dc@ value can be -- embedded into @t@. imageInDTD :: (forall t. fn IdM t) -> ImageInDTD t fn dc -> RMNI dc -> t imageInDTD fn (ImageInDTD d) = hasTagRepDCD 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) ) => HasTagRepDCImageD (fn IdM) dc t -> ImageInDTDA t fn dc instance (Generic dc, Rep dc ::: DomainA (CMap fn IdM), t ::: HasTagRepDCImageD (fn IdM) dc ) => dc ::: ImageInDTDA t fn where inhabits = ImageInDTDA inhabits imageInDTAD :: Functor (Idiom (fn IdM)) => (forall t. fn IdM t) -> ImageInDTDA t fn dc -> RMNI dc -> Idiom (fn IdM) t imageInDTAD fn (ImageInDTDA d) = fmap (hasTagRepDCD d) . applyA (CMap fn) . rep