[Template-haskell] On reifing functions and partial evaluation

[Duncan Coutts]

All,

So I'd like to persuade people of the desirability of being able to
reify values/functions. :-)

I've now got two ways of potentially doing partial evaluation using
Template Haskell, they correspond to two different types for our
specialisation function mix.

To describe the types, I'm going to pretend that TH is typed. Just erase
the phantom type to get real TH (ie Exp a --> ExpQ).

mix1 :: Exp (a -> b) -> Exp a -> Exp b

eg
mix1 [| isJust |] [| Nothing |]

This is where we do abstract interpretation of the function on its
static argument. Unless the function is a textually a lambda abstraction
we can't look at its definition to to the interpretation.

The other way that might work has this type:

mix2 :: Exp (a -> b) -> a -> Exp b

eg
mix2 [| isJust |] Nothing

Here, the static argument is a value rather than a syntax tree
representing a value. It would be desirable to have mix with this type
because it avoids the heavy double encoding that we get with mix1 when
we apply it to itself. With mix1 we would do

cogen = $( mix1  [| mix1 |]  [|[| mix1 |]|] )

where as with mix2 we can do

cogen = $( mix2  [| mix2 |]  [| mix2 |] )

To implement mix with this type, what we do is construct the generating
extension of the function we are specialising, apply it to its static
argument and splice in the resulting code. For example for isJust, we
need to do the following transformation:

isJust = \m -> case m of
                 Nothing -> False
                 Just _  -> True
-->

genex-isJust = \m -> case m of 
                       Nothing -> [| False |]
                       Just _  -> [| True |]

Now, genex-isJust Nothing = ConE GHC.Base.False
(ignoring the Q monad)

We could define genex simply as
genex f = (\e -> [| e |]) . f

But then it would only work for liftable values - ie not functions. Of
course with partial evaluation it is functions that are particularly
interesting. We typically specialise functions of several arguments on
just one or two static arguments - the remaining arguments are accepted
at runtime.

So, instead of just composing with wrap = (\e -> [| e |]) :: a -> Exp a
we'll need genex :: Exp (a -> b) -> Exp (a -> Exp b)
and it will have to inspect the definitions of functions/values.

Another example:

foo s d = case s of
            Nothing -> False
            Just _ -> case d of
                        Nothing -> False
                        Just _ -> True

-->

genex-foo s d = case s of
                  Nothing -> [| False |]
                  Just _  -> [| case d of
                                  Nothing -> False
                                  Just _  -> True
                              |]

The bits in the quasi-quote brackets [| |] are the fragments of the
computation that will be deferred to runtime because they depend on an
argument to the function that is not known (static) at compile time.

We can also get nested $() and [| |] if there are static subexpressions
inside a dynamic expression.

bar s d = case d of
            Nothing -> False
            Just _ -> case d of
                        Nothing -> False
                        Just _ -> True

-->

genex-bar s d = [| case d of
                     Nothing -> False
                     Just _  -> $( case s of
                                     Nothing -> [| False |]
                                     Just _  -> [| True  |]
                                 )
                 |]

This is an example where Ian's idea of adding QQuot and Splice as Exp
constructors would make things easier, but it's not essential so long as
encodings are possible.


On a related issue, I recall Simon PJ wondered about the best way of
reifying values in patterns, like:
let (a,b) = e

reify "a" = ???

What about just applying the appropriate projection

reify "a" = [| (\(x,_)->x) e |]

I guess there's a danger of people duplicating computations by
carelessly manipulating such expressions. ie inadvertently doing the
following transformation:

let (a,b) = e
-->
let a = fst e
    b = snd e

Duncan