On April 22 1999, Simon Peyton-Jones wrote:
> [...] I have finally bitten the bullet
> and added a fairly general mechanism that allows the programmer
> to specify rewrite rules. For example:
>
> {-# RULES
> "map/map" forall f,g,x. map f (map g x) = map (f.g) x
> #-}
>
> The compiler applies the rules left -> right, in the expectation
> that each is an optimisation of some kind.
[...]
> I'd be very interested if anyone can think of useful applications
> for this kind of thing.
> [..]
Your examples concern the simplification of expressions made of
constructors and the functions like `map'.
Naturally, they are useful.
And what about algebraic simplification? Say,
{-# rules
"+assoc" AddSemigroup a => (x+y)+z = x+(y+z)
"0" AddMonoid a => x+zeroG = x,
"neg" AddGroup a => x+(negate x) = zeroG,
#-}
may do the algebraic simplification, like
map ((x+1)+) [1,-1,-1-x] --> [x+2,x,0].
Though the programmer would not write directly a+(-a),
such expressions, you know, often appear due to the same reasons as
in your examples.
The particular point here is that the functions are the class
operations (+,negate,zeroG..).
x,y,z are the variables that range over expressions of type ..=> a
- probably, they are similar as f,g,x is your example.
Could the compiler handle this?
Also consider the `rules' inside a class declaration:
class Num a => AddGroup a
where
{-# rules "+assocToRight" (x+y)+z = x+(y+z),
"0r" x+0 = x,
"0l" 0+x = x,
"negR" x+(negate x) = 0
"negL" (negate x)+x = 0
#-}
- here the context `AddGroup =>' is common.
If the compiler can handle this, this would mean a great lot.
A considerable part of *presumed algebraic axioms* related to a class
declaration by the programmer, - and ignored by compiler, - becomes
almost a real category declaration.
This is an upgrade of the scientific range of compiler. It starts to
understand algebra.
The class declaration means that, say, +, negate, ...
have certain types and arities - only this.
The real category declaration `AddGroup a =>' has to mean much more:
x + (-x) == zeroG, and certain other things. It means the
*properties*, more complex and informative than the mere membership to
types.
Its algorithmic part is actually a *calculus*, the rules to transform
expressions.
Further complication (and benefits) may bring the equivalence and
bi-directed rules. Say,
"+commut" (AddSemigroup a) => x+y == y+x
joined to other rules, makes possible simplifications like
x+(x+1-x)-x --> 1.
You know, there is a lot of useful theory on rewrite rules:
AC-unification, Knuth-Bendix completion, and so on.
And sorry for the naive question, i do not understand the meaning of
the words `pragma',`{-#'.
One could alternatively extend the language with the construct
{rules ...}, `rules' being a new reserved word, the compiler
understanding type contexts inside {rules }. What is the difference
to `pragma' ?
The Haskell-98 compilers that do not understand {-# rules..}, would
act:
"i know `{-#', do not know `rules', so ignore the whole {..} thing",
and this would not change the result of the program.
And {rules..} changes the language so that the old compilers report
an error. Is this the difference?
------------------
Sergey Mechveliani
[EMAIL PROTECTED]
