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