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™. On Thu Dec 18 2014 at 1:41:07 PM adam vogt wrote:

On Thu, Dec 18, 2014 at 12:43 PM, Tom Ellis wrote:

...

This is a great idea and looks very useful, which raises the following question: Why hasn't this already been done? Is there some fundamental obstruction? Perhaps someone who has tried this has some wisdom to share.

Sometimes I found myself using:

foldl appE :: ExpQ -> [ExpQ] -> ExpQ

If you try that with appE_, you end up with a type error "Occurs check: cannot construct the infinite type: t1 ~ t -> t1". It would type check if it was a foldl over a hlist, but I don't think that would be a preferred solution. Since appE_ doesn't work when you don't know how many times it will be used, I think people would just inline one possible definition:

appE_ :: Q (TExp (a -> b)) -> Q (TExp a) -> Q (TExp b) appE_ f x = [|| $$f $$x ||]

Secondly, it looks like you can only make a value of type "L String" by using stringL_, and only consume them with litE_, so I think that intermediate type does not really help. In other words, I think it is better to just use the following:

liftString_ :: String -> Q (TExp String) liftString_ = litE_ . stringL_

or just inline the following more general function:

lift_ :: Lift t => t -> Q (TExp t) lift_ x = [|| x ||]

I don't see those extra functions providing something that the typed bracket / quotation syntax doesn't already provide in a prettier way.

Regards, Adam _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

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