Home

Directly Reflective Meta-Programming

I was recently pointed to the following fascinating paper:

Directly Reflective Meta-Programming, Aaron Stump (HOSC 22(2), June 2009).

Existing meta-programming languages operate on encodings of programs as data. This paper presents a new meta-programming language, based on an untyped lambda calculus, in which structurally reflective programming is supported directly, without any encoding. The language features call-by-value and call-by-name lambda abstractions, as well as novel reflective features enabling the intensional manipulation of arbitrary program terms. The language is scope safe, in the sense that variables can neither be captured nor escape their scopes. The expressiveness of the language is demonstrated by showing how to implement quotation and evaluation operations, as proposed by Wand. The language's utility for meta-programming is further demonstrated through additional representative examples. A prototype implementation is described and evaluated.

Meta-programming without any encoding at all. The only minor drawback that I can see is that this language is untyped - and designing a type system for it would be extremely challenging.

By Jacques Carette at 2010-11-13 15:37 | Meta-Programming | other blogs | 16652 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

The 4 core extensions

The 4 core extensions enumerated in Figure 1 look pretty straightforward. Definitely an interesting approach.

As for meta-programming in general, I always thought a tagless self-interpreter would be a good addition to this space. Programs are normally evaluated in the interpreter at full speed, but since all programs are now lifted into a "Language" type class, metaprograms over arbitrary terms can also be written. This language would probably need a carefully designed syntax so it all hangs together nicely. F#'s computation expressions and Haskell's do-notation demonstrate one approach using syntactic sugar.

Jacques pointed out at the time that the required polymorphism is beyond current languages, but it seems much more straightforward to design a type system to handle this specific case, some kind of "contextual polymorphism". You seem to enjoy most of the properties this paper describes using this approach, and you benefit from full typing, but please correct me if I'm wrong!

By naasking at Sat, 2010-11-13 17:22 | login or register to post comments

GADTs not enough?

Why, with GADTs in OCaml, wouldn't MetaOCaml+GADTs be enough? (ETA: I should read the paper then.)

By lukstafi at Sat, 2010-11-13 19:42 | login or register to post comments

Not for the tagless encoding

Not for the tagless encoding described in the paper in that thread. The paper is explicitly about how a final algebra seems to be a better fit for describing and interpreting DSLs than initial algebras like GADTs.

By naasking at Sat, 2010-11-13 20:02 | login or register to post comments

interpreter and examples

I have just posted the interpreter and the examples mentioned in this paper, on the "Papers" section of my U. Iowa web page. The paper refers to these by a URL at my previous institution, which unfortunately no longer works. The new URL is:

http://www.cs.uiowa.edu/~astump/papers/archon.tgz

By aaron.stump at Sat, 2010-11-13 23:05 | login or register to post comments

ADT

Is this equivalent to exposing AST as ADT with 4 operations defined on it rather than usual concrete data types?

By Eugene Toder at Sun, 2010-11-14 04:39 | login or register to post comments

Ideal Archon

Interesting. Maybe the four operations could get a little more polish (eg. open (lambda x.x) (lambda var body.body body) evaluates to (lambda x.x x), shouldn't it be statued that body cannot be passed to an arbitrary function -- eliminating the need for special casing?)

I would have liked a description of an ideal Archon language before going into the details of the arbitrary choices made by the implementors.

By Denis Bredelet -jido at Wed, 2010-11-17 00:36 | login or register to post comments