oleg@pobox.com wrote:
Greg Buchholz has posed an interesting problem of writing a typechecker. Given untyped terms of the form
...snip...
We show the solution that uses no GADTs and no representation types. We retain however the eval function in the previous message that uses GADT. Our solution uses type classes. It seems to some the type-checking rules stated as instances of the TypeCheck class take a particular natural form.
...snip...
rather than the original terms Exp. The conversion is straightforward, via Template Haskell:
type F = Q TH.Exp parse :: Expr -> F parse (ELit x) = [e| FLit $(litE . integerL . fromIntegral $ x) |] parse (EInc x) = [e| FInc $(parse x) |] parse (EIsZ x) = [e| FIsZ $(parse x) |]
t1' = $(parse . read $ e1) t2' = $(parse . read $ e2)
*G> :t t1' t1' :: FIf FLit FLit FLit *G> :t t2' t2' :: FIf (FIsZ FLit) (FInc FLit) (FFst (FPair FLit FLit))
Nice. But using TH means we have to know everthing about the strings we want to evaluate at compile time right? So you can't do something like... main = do l <- getLine print $ (eval.typecheck) ($(parse . read $ l)) ...right? (Even if you can get around GHC complaining about a 'stage restriction'). Whereas, it would be possible with with the "my_read" and other versions. Anyway, as long as we're going down that route, we might as well get rid of the GADTs and go for a pure type class version of "eval"... http://lambda-the-ultimate.org/node/1787 ...(great minds think alike, right? ;-) I guess I should have mentioned that thread in my first message. Thanks, Greg Buchholz