Duncan Interesting. I'm ccing the TH mailing list. What do TH-afficionados think? Nested brackets ~~~~~~~~~~ | > evalProg' = [| evalProg |] --same evalProg as before | | > compileProg :: ExpQ -> ExpQ | > compileProg = $( cogen [| evalProg' |] ) I'm very keen that TH should obey the beta rule. That is, given x = e you can always replace x by e. So in this case you ought to be able to write compileProg = $(cogen [| [| evalProg |] |]) I'm not saying anything about efficiency yet -- but it ought to be correct. ===> Conclusion 1: TH should allow nested brackets (and presumably nested $'s). Quoting ~~~~~ Consider v1 = [| x * 7 + x |] We get a wodge of syntax tree for v1. But consider this: w = x*7 + x v2 = [| w |] We get a tiny syntax tree for v2. How has this happened? Because every client of v2 (who might say $v) can also "see" w. We can't do this so easily if x is local: v3 x = [| x*7 + x |] Now if we say $(v3 5) we'll get a syntax tree. We can still try lifting the body out: v3 x = let w = x*7 + x in [| w |] Actually this will work if w is "liftable". When we call $(v3 5), we'll build the code [| 40 |]. Hmm. ===> Observation 2. Something I didn't realise: this forces w. So substituting for w might change strictness behaviour. Sigh. However, if w's type is not liftable (e.g. it's Exp, or Tree), then the program will be rejected as ill typed. ====> Observation 3. I wonder if it's a coincidence that you got away with the lift-to-top-level trick. In a more general setting you might not be able to, and then you'd get very heavy encoding. Double encoding ~~~~~~~~~~ You ask for a function enc :: Exp t -> Exp (Exp t) Well that's easy, isn't it? enc x = return x I'm not sure if that's what you want. Indeed, you say " So, the thing that concerns me is the double encoding. I can't intuitively see the need for it..." Maybe you can give the intuition for why you can't see the need for it? I don't think I understand all the issues nearly well enough to comment further. Maybe you can chew on it with Ian, who is pretty au fait with TH. Simon
On Wed, Dec 31, 2003 at 05:54:08PM -0000, Simon Peyton-Jones wrote:
Nested brackets ~~~~~~~~~~
| > evalProg' = [| evalProg |] --same evalProg as before | | > compileProg :: ExpQ -> ExpQ | > compileProg = $( cogen [| evalProg' |] )
I'm very keen that TH should obey the beta rule. That is, given x = e you can always replace x by e. So in this case you ought to be able to write
compileProg = $(cogen [| [| evalProg |] |])
OK, but if I have something like $( do e <- [| evalProg' |] do_something e ) then I would expect do_something to be given a (VarE n) for some name n. It doesn't make sense for the compiler to be able to apply the beta rule in this case. Are you thinking [| [| 5 |] |] would be equivlent to return $ return $ LitE $ intL 5 or return $ QuoteE $ LitE $ intL 5 (data Exp = ... | QuotedE Exp) ?
===> Conclusion 1: TH should allow nested brackets (and presumably nested $'s).
I think these have to be run innermost first. There is the meaning of things like f x = [| [| $x |] |] g x = $(f 5) to consider too. I think what makes most sense here depends on which choice for nested quasi-quotes means above is chosen. For the first I think g has to be equivalent to g x = [| [| 5 |] |] Although neither alternative is unreasonable if we take the second alternative, I think g x = [| $x |] makes more sense (as if I looked at the value of [| [| $x |] |] I would expect to see (Splice some-name-for-x) in the middle). Maybe if we took this path then there should be a way to escape $s, giving the choice to the programmer. Say "f = [| [| \$x |] |]" would give "g x = [| $x |]" but "f = [| [| $x |] |]" would give "g x = [| [| 5 |] |]" (with an extra \ for each layer of quotes).
Double encoding ~~~~~~~~~~ You ask for a function enc :: Exp t -> Exp (Exp t)
Well that's easy, isn't it?
enc x = return x
I'm not sure if that's what you want. Indeed, you say " So, the thing that concerns me is the double encoding. I can't intuitively see the need for it..." Maybe you can give the intuition for why you can't see the need for it?
I don't think I understand all the issues nearly well enough to comment further. Maybe you can chew on it with Ian, who is pretty au fait with TH.
I'm not sure I got the need for the double encoding either. Talking it over in person sounds like a good idea, Duncan. Thanks Ian
Dear all, Krzysztof Czarnecki, John O'Donnell, Jorg Striegnitz, and myself are currently working on a short article with the above title. The latest draft can be found at: http://www.cs.rice.edu/~taha/publications/preprints/2003-12-01.pdf Naturally, we are very interested in your feedback. Walid.
On Wed, 2003-12-31 at 17:54, Simon Peyton-Jones wrote:
====> Observation 3. I wonder if it's a coincidence that you got away with the lift-to-top-level trick. In a more general setting you might not be able to, and then you'd get very heavy encoding.
Which is something I'd like to avoid. People have struggled with the problem of heavy encodings when doing partial evaluation in typed languages. Another observation that I might make is that we would need to be able to reify functions to be able to do proper (rather than trivial) partial evaluation. The only other way I can think of is some kind of low level black magic where you 'run' a function on some of its input and inspect the results.
Double encoding ~~~~~~~~~~ You ask for a function enc :: Exp t -> Exp (Exp t)
Well that's easy, isn't it?
enc x = return x
I don't understand what you mean here. How would you write that in the TH version? Ian and I worked out a double encoding for at least the special case of [| [| evalProg |] |] enc :: ExpQ -> ExpQ enc e = do VarE name <- e [| varE |] `appE` litE (StringL name) so then we can define cogen :: ExpQ -> ExpQ cogen = $(mix mix' mix'') . enc Now that it takes only a singly encoded function, we can use it like so: compileProg :: ExpQ -> ExpQ compileProg = $( cogen [| evalProg |] ) where as before we needed to do: compileProg :: Hs.ExpQ -> Hs.ExpQ compileProg = $( cogen [| evalProg' |] ) evalProg' = [| evalProg |] You'll notice that the enc function only works with the non-abstract representation of names. With the new abstract name type in the ghc 6.3+ TH, such a function might need to be primitive, or the Name data type might need to be an instance of Lift or something similar.
I'm not sure if that's what you want. Indeed, you say " So, the thing that concerns me is the double encoding. I can't intuitively see the need for it..." Maybe you can give the intuition for why you can't see the need for it?
Actually, having thought it over, it does make sense - although it is still annoying. It is for the same reason that mix'' is doubly encoded in the definition cogen = $(mix mix' mix'') = $(mix [| mix |] [| [| mix |] |]) mix applies an encoded function to an encoded argument, so it's like doing mix' mix'' Again, since the first argument to mix is encoded, then mix'' must be doubly encoded. If we look at another example; defining compileProg We can do this in two ways, using either the 2nd or 3rd Futamura projections. The example I gave before was using the 3rd Futamura projection: compileProg = $(cogen [| [| evalProg |] |]) but, we could use the 2nd: compileProg = $(mix mix' [| [| evalProg |] |]) Now we're using evalProg as the second argument to (mix mix') so it must be double encoded (by the argument above, or just by inspecting the types). Since mix mix' is semantically equal to $(mix mix' mix''), that explains why it's argument must also be doubly encoded. Duncan
participants (4)
-
Duncan Coutts -
Ian Lynagh -
Simon Peyton-Jones -
Walid Taha