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 oleg@pobox.com 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