[Template-haskell] Re: Partial evaluation using TH

[Duncan Coutts]

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