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