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

[Pasqualino 'Titto' Assini]

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