Lambda the Ultimate

I don't know a hard line to draw between DSLs and non-DSLs. The prototypical DSL we use in our paper is essentially the lambda calculus. The approach may or may not "remove the need for an advanced type system" in the host language depending on how advanced the type system of the object language is -- in general, the host language's type system only needs to be a little more advanced than the object language's type system, because the "tagless final" way doesn't add much indirection on top of the host language type system. For example, if the object language is the simply typed lambda calculus then the host language can be just Hindley-Milner.

Can this approach be meta-circular, ie. encode an object language whose type system is equivalent in power to the host language? Or does the host language's type system need to be strictly more powerful? I suspect the latter.

Can this approach be meta-circular, ie. encode an object language whose type system is equivalent in power to the host language?

Assuming the appropriate self-interpretation, could this approach expose the host language's compiler itself as a runtime module, and compile dynamic expressions at runtime ala staged computation? That would be quite a useful advancement, as it could express dynamic linking within any statically typed host language of sufficient power via a JITed bytecode (or directly from the source code). I think this would require that all language expressions be first-class, ie. first-class modules.

Thanks for the quick and thorough reply! I think I didn't express my question properly. The following should elucidate it:

What is the type of the AST that the parser returns? Doesn't it have to begin with a type-class quantifier, and aren't those restricted in a similar way as normal type variable quantifiers are restricted in Haskell 98? You would want a parser like:

parse :: String -> (Symantics a => something(a))

...but isn't there a restriction on type class quantifications that forces it to be

parse :: Symantics a => String -> something(a)

? That is, the Symantics you want to use must be decided at parsing time, rather than leaving that choice to later, when it may be resolved in multiple different ways.

My question really isn't specific to parsing or type-checking. It has to do with typing functions that manipulate ASTs, such that their results can be used with multiple Symantics interpretations later on.

Isn't the explicit "forall" a GHC extension? Can you do this in Haskell 98? Since you already said you don't know of an analogous technique for dynamic representation of terms in vanilla OCaml, does this mean that, while your technique works in generic Haskell 98 and OCaml, it can be used for dynamically-built terms only with extensions to those languages? (I think most readers would assume that a technique for manipulating programs works for more than just a fixed set of programs entered in the source code of the program manipulator. I interpreted your comment on this in the paper as saying that you thought it was possible but didn't have space to go into it, not that the technique precluded it.)

Explicit "forall" is a common extension (Hugs supports it as well, I believe YHC's planning to) that's pretty certain to make it into haskell' - but yeah, it's not Haskell 98. Same goes for dynamics, though they're a far more common one because they only really require extending the runtime rather than the type system.

I'll try to clarify: this paper is about embedding a language in a statically typed host language. If we're self-interpreting, the host language is the one being embedded. This is similar to staging, though perhaps not as convenient, correct?

Using an algebraic representation of the term language, as is usually done, one uses an "eval" function to evaluate a constructed expression. I can similarly imagine a "compile" function which directly compiles the expression tree to remove all the interpretive overhead; for instance, .NET compiles such expression trees in LINQ.

So imagine some small bytecode language whose VM provides a basic JIT, but no dynamic loading facilities beyond a basic file read/write interface. Dynamic code loading can then be provided from within the language as a module which translates this bytecode into native terms using your Symantics module(s) [1].

I think that even in your tagless approach, there is still some small overhead in the constructed term as each host language value actually invokes a function. I was wondering whether there can be a similar "compile" function for this paper's term representation. Or perhaps partial evaluation Symantics module takes care of inlining all such small functions and so the overhead is non-existent? Although if I'm assuming the partial eval module, the language is already multistaged, so perhaps there's a simpler way to accomplish this.

On an unrelated note, I wasn't aware that MetaOCaml used C--. I hadn't seen much C-- activity lately, and thought that perhaps it wasn't being actively developed any longer.

[1] The point is to move as much as possible into the safer host language, rather than providing VM facilities which are invariably written in unsafe languages like C/C++.

On an unrelated note, I wasn't aware that MetaOCaml used C--. I hadn't seen much C-- activity lately, and thought that perhaps it wasn't being actively developed any longer.

There was a status report at the end of 2006 which indicated some uncertainty about the future. I don't know what's happened since then, although there are mentions of it in places like the GHC wiki's page about its new code generator.

Final clarification: I'm assuming here that the language is not multistaged, which means that your C Symantics module is not expressible [1]. I'm suggesting the C module be provided by the runtime, which builds a representation for the machine code emitter. Essentially, this adds multistaging capabilities without extending the language and complicating the type system, by reifying the JIT/compiler as a module.

[1] I'm currently reading Implementing Multi-stage Languages Using ASTs, Gensym, and Reflection, and multistaging adds considerable complexity to a language.

To answer your questions: indeed, staging is very complex. It is possible nevertheless to represent staging (including stage distinctions and the manipulation of `open' code) in an unstaged language. The price to pay is the number of administrative redices.

Which I believe can be removed by traditional compiler optimizations when jitting the resulting expression (constant propagation, etc.); coupled with the optimizations already performed by partial evaluation, I believe this reduces the need for some sophisticated optimization passes.

Assuming the language is capable of self-interpretation, multistaging becomes a source to source transformation using your Symantics interface.

Assuming the language is capable of self-interpretation, multistaging becomes a source to source transformation using your Symantics interface.

This leads me to wonder how much of the compiler pipeline can be embedded in the host language via a series of Symantics modules? How many of a compiler's IRs can be represented and plugged together and which pipeline stage must escape the host language to unsafely "cast" the constructed data to a function/data pointer? The more powerful the host language, the closer to a typed equivalent of the host machine's assembly one could get. I'm sure a typed assembly language written to a byte array is beyond a language like OCaaml, but I wonder how far off it is.

There just wasn't enough room to discuss all of that in the APLAS version. The journal version has extensive discussion of evaluation styles and a few other goodies.

A preliminary version (ie the one we submitted) also had a discussion of self-interpretation. Unfortunately, we don't know how to do get it to type in an ``elegant'' way; what we'd implemented worked, but required the user to do too much work to manually insert let bindings where one might otherwise expect functions to work. The problem is that a self-interpreter seems to need more polymorphism than is available in either Haskell or O'caml. In the end, we simply cut that out entirely of the final version.

You can download the preprint version of the JFP paper (the final version is typeset much more nicely by CUP, but they have not posted it online yet, I expect that to happen very soon).

Thanks for the link. There seem to be quite a few versions floating around. Thankfully, I had saved one with the self-interpretation section intact, but it's still shorter than the JFP version you just linked to, so I'm looking forward to going through this new one to see what else was added.

The problem is that a self-interpreter seems to need more polymorphism than is available in either Haskell or O'caml. In the end, we simply cut that out entirely of the final version.

Any thoughts on specifically what kind of additional polymorphism is required?

The issue is that if you have polymorphism in your object language, you need rank-2 polymorphism in your meta-language. But for self-interpretation, the object and meta-language have to have the same features, which means that you need rank-2 polymorphism in your object language, which requires rank-3, then rank-4, etc.

Another way solution is to use let-polymorphism to bind each part of the language; this basically lets type resolution happen 'in context' instead of globally, thereby requiring less explicit polymorphism. One can see this has having a "context with a hole", and you plug in your program into that hole *then* type the result. Using 'let' to create such a 'context with a hole' is sufficient to get the needed polymorphism.

The links are to 2 different versions: a shorter paper which appeared in the proceedings of APLAS, and a much longer version with lots more material (but not everything we had!) in JFP. We need to get back to the partial evaluation ideas which are in the code but not really fully explained even in the longer JFP paper.

One would think different titles would be appropriate for different papers...

One would think different titles would be appropriate for different papers...

To be fair to Jacques, Oleg and Chung-chieh (Ken), long time LtUers all, this practice is pretty commmon with academic papers.

Papers with the same name are often published in successive versions, sometimes with major revisions.

Version numbers might be nice (like software), but having to come up with similar but different names for each one is probably too much to ask.

Also extended journal versions of conference papers will usually have the same names, although journal versions can necessarily cover more content.