Hi Oleg, Many thanks for this, it is really brilliant stuff.
It is a pity that it cannot be used in an interpreter but it is a great trick to know for static compilation of DSLs. All the best, titto On Saturday 06 October 2007 08:55:36 [EMAIL PROTECTED] wrote: > The earlier message showed how to implement a typechecker from untyped > AST to wrapped typed terms. The complete code can be found at > http://okmij.org/ftp//Haskell/staged/TypecheckedDSL.hs > > The typechecker has the type > typecheck :: Gamma -> Exp -> Either String TypedTerm > where > data TypedTerm = forall t. TypedTerm (Typ t) (Term t) > > Upon success, the typechecker returns the typed term wrapped in an > existential envelope. Although we can evaluate that term, the result > is not truly satisfactory because the existential type is not > `real'. For example, given the parsed AST > > > te3 = EApp (EApp (EPrim "+") > > (EApp (EPrim "inc") (EDouble 10.0))) > > (EApp (EPrim "inc") (EDouble 20.0)) > > we might attempt to write > > > testr = either (error) (ev) (typecheck env0 te3) > > where ev (TypedTerm t e) = sin (eval e) > > We know that it should work. We know that e has the type Term Double, > and so (eval e) has the type Double, and so applying sin is correct. But > the typechecker does not see it this way. To the typechecker > Inferred type is less polymorphic than expected > Quantified type variable `t' escapes > that is, to the typechecker, the type of (eval e) is some abstract > type t, and that is it. > > As it turns out, we can use TH to convert from an existential to a > concrete type. This is equivalent to implementing an embedded > *compiler* for our DSL. > > The trick is the magic function > lift'self :: Term a -> ExpQ > that takes a term and converts it to the code of itself. Running the > resulting code recovers the original term: > $(lift'self term) === term > > There is actually little magic to lift'self. It takes only > four lines of code to define this function. > > We can now see the output of the compiler, the generated code > > *TypedTermLiftTest> show_code $ tevall te3 > TypecheckedDSLTH.App (TypecheckedDSLTH.App (TypecheckedDSLTH.Fun > (Language.Haskell.TH.Syntax.mkNameG_v "base" "GHC.Num" "+") (GHC.Num.+)) > (TypecheckedDSLTH.App (TypecheckedDSLTH.Fun > (Language.Haskell.TH.Syntax.mkNameG_v "main" "TypecheckedDSLTH" "inc") > TypecheckedDSLTH.inc) (TypecheckedDSLTH.Num (10%1)))) (TypecheckedDSLTH.App > (TypecheckedDSLTH.Fun (Language.Haskell.TH.Syntax.mkNameG_v "main" > "TypecheckedDSLTH" "inc") TypecheckedDSLTH.inc) (TypecheckedDSLTH.Num > (20%1))) > > [we should be glad this is not the machine code] > > Mainly, we can now do the following (in a different module: TH > requires splices to be used in a different module) > > > tte3 = $(tevall te3) > > > :t tte3 > > tte3 :: Term Double > This is the real Double type, rather some abstract type > > > ev_tte3 = eval tte3 > > -- 32.0 > > > > testr = sin (eval tte3) > > > > testr = sin (eval tte3) > > -- 0.5514266812416906 > > The complete code for the DSL compiler is available at > > http://okmij.org/ftp//Haskell/staged/TypecheckedDSLTH.hs > http://okmij.org/ftp//Haskell/staged/TypedTermLiftTest.hs _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe