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