[Template-haskell] Non-typechecked reification brackets

Simon Peyton-Jones simonpj@microsoft.com
Wed, 9 Apr 2003 11:33:34 +0100


I don't fully understand this:

	- The Piece type uses CondP, ListConsP, whereas your
	quoted fragments use Cont, (:).

I think you are saying that you want to use Haskell syntax to write
rewrite rules, which are then munged into real Haskell by your make_rule
function.  I don't really understand what values are used in the quoted
stuff. =20

I'm rather dubious about switching off the type checker for quotations,
although I can see that (as you say) it's a pretty non-invasive change.
I suggest you discuss this with Oege, work on your examples, see if
there are any alternatives, and come back to the TH list if you're still
convinced.

Simon

|  -----Original Message-----
|  From: Ian Lynagh [mailto:igloo@earth.li]
|  Sent: 08 April 2003 14:26
|  To: Simon Peyton-Jones
|  Cc: template-haskell@haskell.org
| =20
|  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?
| =20
|  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.
| =20
|  In this particular case (which is a reimplementation of pan) I have
|  (I've cut this down a lot):
| =20
|  data Piece =3D
|               -- Exp
|               AppP Addr Addr
|             | CondP Addr Addr Addr
|             | TupP Addr
|               -- DotDot
|             | FromP Addr
|               -- [a]
|             | ListConsP Addr Addr
|             | ListNilP
| =20
|  which I can use to represent the syntax trees as DAGs with a
FiniteMap
|  in each direction (Piece -> Addr, Addr -> Piece).
| =20
|  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
| =20
|  So I have a function make_opt_rule :: Exp -> Exp so, for example:
| =20
|  =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D
|  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
|  =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D
| =20
|  produces:
| =20
|  =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D
|  \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
|  =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D
| =20
|  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)
| =20
|  Now, as it turns out it is fine to do locally bad rewrites like
| =20
|  [| \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],
| =20
|  (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
| =20
|  [| \g x y -> Tup (Cond g x y) --> Cond g (Tup x) (Tup y) |n],
| =20
|  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).
| =20
| =20
|  Did that make sense?
| =20
| =20
|  Thanks
|  Ian
| =20