More on rules and properties.
Imagine the improved language Haskell-2. I suggested for its library
(see "basic algebra proposal" on haskell.org)
the classes Additive (with +), Multiplicative (with *).
And it appears now, the implementors think of dealing with the rules.
This arranges *almost* everything. For example,
class (Eq a,Multiplicative a) => MulGroup a
where
unity :: a
inv :: a -> a -- inversion
{properties x==x, x==y ==> y==x, x==y & y==z ==> x==z,
x==y ==> x*z == y*z
}
{rules (x*y)*z = x*(y*z),
unity*x = x, x*unity = x,
x*(inv x) = unity, (inv x)*x = unity
}
{rules..}, {properties..} explain explicitly the compiler that
these operations have to satisfy certain laws. These laws define a
group (do i forget something?).
For Haskell-98, they are the *commentary* and presumed conditions.
In Haskell-improved, they are real.
It is hard for the compiler to use {properties..}.
But, in principle, it could exploit them sometimes.
{rules..} are the particular kind of properties, extremely useful.
The compiler simply applies (rewrites) them from left-hand to
right-hand, down to the bottom of each expression <e>, while <e> has
anything to rewrite.
It is up to the programmer to set the rules with the rewriting
termination.
Thus, in above MulGroup, the rewriting terminates.
If we add
{rules ... x*y = y*x},
- to express a commutative group, - the termination breaks.
But this can be improved by certain equational reasoning.
The rewriting to normal form itself, it does not provide the compiler
with the full notion of a group. But with very essential part of it.
Exploiting the completion technique, AC unification, and such, the
compiler could do a real *equational reasoning* - starting from the
rules. For, the rules, they define certain equality, close to above
(==), that can be partially solved.
Such an equational reasoning can be a good tool for the program
optimization.
Thus, imagine the compiler simplifying
(x^5+x^4+x^3+x^2+x+1)*(x-1) to x^6-1.
{rules..}, {properties..}
may appear not only inside a class declaration.
But when they are inside a class declaration, the type contexts
are often taken automatically from `class <context>'.
{properties..} can be any, but *equations* are especially welcome
for algorithms.
{rules..} is the particular kind of equational properties which
are again, more useful in algorithms then the mere
equations.
If the compiler incorporates such kind of reasoning, it would be a
great deal if the developers separate the equation and property
processing into a library written in Haskell. Because, if it is done
culturally, it presents a good piece of computer algebra, symbolic
logic, and such, and can be exploited explicitly by applications.
At least, this could save the code.
To say the truth, such a tool has to be developed apart, by the
symbolic computation designers, and then, used by the compiler too.
There exist such systems, only written not in Haskell, and maybe, not
adopted to "typeful" rewriting.
Personally, i am uncertain about *types*.
A couple of papers on rewrite rules, that i had read long ago,
treated only the typeless case.
The main tool here is a choice of substitution in unification.
Say, for the above class MulGroup and a rule x*(inv x) = unity,
*any* expression E can be substituted for x.
And in Haskell, E should be of certain type.
But i hope, there exist a theory for the "typeful" rewriting as well.
Maybe, not so much to change, i do not know.
------------------
Sergey Mechveliani
[EMAIL PROTECTED]
