[Haskell-cafe] Typed TH

[Tillmann Rendel]

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