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