[Haskell-cafe] Typed DSL compiler, or converting from an existential to a concrete type

[oleg at pobox.com]

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