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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
