[Haskell-cafe] Simple GADT parser for the eval example

[Ulf Norell]

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