Lagging far behind as usual with reading the cafe... Tillmann Rendel wrote:
Edward Amsden wrote:
Relevant paper to typed quotation:
http://repository.cmu.edu/cgi/viewcontent.cgi?article=2969&context=compsci
I'm very interested in metaprogramming in typed languages, and this paper seems to suggest that it is a Hard Problem™.
You mention Pfenning and Lee (1989) above. If you want to read more about this, there has been some progress in the tradition of that paper in recent years, including:
Carette, Kiselyov, and Shan (2009). Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages. Journal of Functional Programming 19(4): 509-543. (Extended version of a 2007 conference paper).
I don't remember all the details but the trick that Carette, Kiselyov, and Shan use to achieve partial evaluation is certainly ingenious, given that staging in MetaML is purely generative: there are no primitives to inspect code pieces once they have been constructed.
Rendel, Ostermann, and Hofer (2009). Typed self-representation. In Proc. of PLDI.
Jay and Palsberg (2011). Typed self-interpretation by pattern matching. In Proc. of ICFP.
Brown and Palsberg (2015). Self-representation in Girard's System U. To appear in Proc. of POPL.
These papers explore various tricks to avoid the fundamental hardness of expressing the rules of a sane type system in the same type system itself. For our own work on typed self-representation, we always hoped that it would lead to better macro systems for statically typed languages, but so far, we never figured out how to make it practical enough. I fear the situation is similar for the other papers.
I recently read this one and found it quite promising in that regard: Steve Ganz, Amr Sabry, Walid Taha Macros as Multi-Stage Computations: Type-Safe, Generative, Binding Macros in MacroML http://www.cs.indiana.edu/~sabry/papers/macroml.pdf They use translation to MetaML to show that their language is well-behaved. Cheers Ben -- "There are two ways of constructing a software design: One way is to make it so simple that there are obviously no deficiencies and the other way is to make it so complicated that there are no obvious deficiencies. The first method is far more difficult." ― C.A.R. Hoare