Hi, 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). 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. There's also work in the dependently typed community about reflection and meta-programming in dependently typed languages, such as: Chapman, Dagand, McBride, and Morris (2010). The gentle art of levitation. In Proc. of ICFP. and various others. Tillmann