On Oct 31, 2006, at 2:19 AM, Dimitrios Vytiniotis wrote:
-- Give a GADT for representation types data R a where Rint :: R Int Rbool :: R Bool Rpair :: R a -> R b -> R (a,b)
-- Give an existential type with a type representation data TermEx where MkTerm :: R a -> Term a -> TermEx
-- we use Weirich's higher-order type-safe cast to avoid deep traversals -- one can replace the type_cast with a more simple traversal-based -- version.
...complicated higher order stuff... For instance:
data a :==: b where Refl :: a :==: a
(===) :: Monad m => R a -> R b -> m (a :==: b) Rint === Rint = return Refl Rbool === Rbool = return Refl Rpair a b === Rpair c d = do Refl <- a === c Refl <- b === d return Refl a === b = fail $ show a ++ " =/= " ++ show b
cast :: a :==: b -> c a -> c b cast Refl x = x
In particular one wants to extract the Term part of a TermEx:
getTerm :: Monad m => TermEx -> R a -> m (Term a) getTerm (MkTerm r' t) r = do Refl <- r === r' return t
/ Ulf