[Haskell-cafe] Re: An example of dependent types [was: Simple GADT parser for the eval example]

[Greg Buchholz]

oleg at 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