[Template-haskell] Non-typechecked reification brackets

[Ian Lynagh]

On Tue, Apr 08, 2003 at 01:48:24PM +0100, Simon Peyton-Jones wrote:
> I didn't understand this.  Care to elaborate, with some examples?

OK, the key point is that it is easier, should you want to build an
expression that doesn't type check, to have GHC do it for you than to
write App (Con "Tup") (...) by hand.

In this particular case (which is a reimplementation of pan) I have
(I've cut this down a lot):

data Piece = 
             -- Exp
             AppP Addr Addr
           | CondP Addr Addr Addr
           | TupP Addr
             -- DotDot
           | FromP Addr
             -- [a]
           | ListConsP Addr Addr
           | ListNilP

which I can use to represent the syntax trees as DAGs with a FiniteMap
in each direction (Piece -> Addr, Addr -> Piece).

Something I want to be able to do is to float ifs up as then I can
simplify more, e.g.,
    1 + (if g then 2 else 3)
to
    if g then 3 else 4

So I have a function make_opt_rule :: Exp -> Exp so, for example:

=======================
do rule <- runQ [| \g x y z -> App x (Cond g y z)
                               -->
                               Cond g (App x y) (App x z) |]
   putStrLn $ render $ pprExp $ make_opt_rule rule
=======================

produces:

=======================
\p -> case p of
          AppP x'1 aopt@1 ->i
              do popt@1 <- look_at aopt@1
                 case popt@1 of
                     CondP g'0 y'2 z'3 ->
                          do addr@0 <- local_opt (AppP x'1 y'2)
                             addr@1 <- local_opt (AppP x'1 z'3)
                             addr@2 <- local_opt (CondP g'0 addr@0 addr@1)
                             return (Just addr@2)
                     _ -> return Nothing
          _ -> return Nothing
=======================

Now, this one is fine because both sides of the rule correspond to valid
Haskell expressions. But I also want to rewrite
    (0, if g then 1 else 2, 3)
to
    if g then (0, 1, 3) else (0, 2, 3)

Now, as it turns out it is fine to do locally bad rewrites like

[| \g x y z -> (:) (Cond g x y) z --> Cond g ((:) x z) ((:) y z) |n],
[| \g x y z -> (:) x (Cond g y z) --> Cond g ((:) x y) ((:) x z) |n],

(which moves the Cond up through the list of expressions wrapped by Tup)
as when it gets to the top it will be rewritten again with

[| \g x y -> Tup (Cond g x y) --> Cond g (Tup x) (Tup y) |n],

and we are back with a valid datastructure represented by the DAG.
Turning off type checking allows me to tell GHC that I know that what I
am doing looks bad, but if it looks the other way for a minute it'll all
turn out OK in the end (both in terms of the code spliced in (which
operates on Pieces) and the DAG that will ultimately be flattened).


Did that make sense?


Thanks
Ian