[Haskell-cafe] Typed TH

[Ben Franksen]

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