Thanks to everyone who has contributed to the discussion about transformation rules. There is clearly something inteeresting going on here! There is clearly a huge spectrum of possibilities, ranging from nothing at all to a full theorem-proving system. In adding rules to GHC I'm trying to start with something very modest. The rules I've implemented so far operate solely by pattern matching, have no side conditions, do not guarantee confluence or termination, and must have a global constant (usually a function) in the head. None of this is particularly original, but I'm not aware of any optimising compiler that provides such a facility. I think of it as a way of specifying domain-specific transformations that go with a library you write. I'm interested to see what can be done with this simple system before doing anything more elaborate. One difficulty about going further is that it is easier to say the *kind* of thing one might like than to specify it precisely. My hope is that experience from a concrete implementation may give us better ideas of what to do next. Anyway, first I have to tidy up the implementation, document more precisely what it does, and check it in so the brave among you can play with it. Simon
