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

[Ulf Norell]

On Nov 1, 2006, at 1:32 AM, Greg Buchholz wrote:

>     Thanks to everyone who replied (especially Dimitrios Vytiniotis  
> and
> Joost Visser).  I now know the standard way to write the GADT parser.
> But I'm still curious if anyone has comments pertaining to the version
> using type classes.  It seems so close to doing what we want, and  
> it is
> pretty straightforward to implement.  The best way I can think to
> describe it would be to say it uses the type system to find what it
> should parse next, and dies of a pattern match failure if something
> unexpected shows up, instead of checking to see if we can assemble a
> type safe tree from pre-parsed parts (does that make any sense?).
>
>     I'm curious if there could be a small change to the type system to
> make the fully general "my_read" possible, or if it suffers from an
> incurable defect.

I'm not sure what you're asking, but it's possible to get

   my_read :: .. => Expr -> Term a

Previously given code:

> -- 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
>
> my_readEx :: Expr -> TermEx
> getTerm   :: TermEx -> R a -> Term a

Given this you can define

 > class    Rep a    where rep :: R a
 > instance Rep Int  where rep = Rint
 > instance Rep Bool where rep = Rbool
 > instance (Rep a, Rep b) => Rep (a,b) where
 >   rep = Rpair rep rep
 >
 > my_read :: Rep a => Expr -> Term a
 > my_read e = getTerm (my_readEx e) rep

/ Ulf