Andrew Hunter
All well and good, but it seems to me that if I'm embedding the DSl, shouldn't I be able to use the host language's facilities--for example, function abstractions and applications--directly?
Indeed. Using binding in the host language to represent binding in the embedded language is called higher-order abstract syntax (HOAS).
Well, I tried this, and it seems it works OK, like so:
data Expr = Var String | Const Int | Plus Expr Expr | Quantified Range (Int -> Expr)
(Do you still need or even want "Var String"?)
... I could write something like:
refine (Quantified range pred) = Quantified range pred' where pred' = \c -> refine (pred c)
But the problem is that this refines the term, again, every time I apply an argument to pred' ...
The paper by Jacques Carette, Oleg Kiselyov, and me http://www.cs.rutgers.edu/~ccshan/tagless/jfp.pdf (revised version to appear in JFP) shows how to perform partial evaluation (which is an optimization, like your refinement) using HOAS. However, it's a bit tricky, in a language like Haskell (98) without so-called metaprogramming or staging facilities at the term level, to make the optimizations happen only once (rather than every time the embedded abstraction is invoked). It can be done! Let me point you to some code that we only mention in passing in that paper, which performs type-checking using HOAS. The type-checking happens only once; then the type-checked term can be interpreted many times. http://okmij.org/ftp/tagless-final/ http://okmij.org/ftp/tagless-final/IncopeTypecheck.hs Hope this helps. -- Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig 2008-11-25 Elimination of Violence Against Women http://unifem.org/vaw/ 1948-12-10 Universal Declaration of Human Rights http://everyhumanhasrights.org