[Haskell-cafe] Re: Typed DSL compiler,
or converting from an existential to a concrete type
Pasqualino 'Titto' Assini
tittoassini at gmail.com
Sat Oct 6 07:32:20 EDT 2007
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
More information about the Haskell-Cafe
mailing list