When Simon P. Jones mentioned the *rules*,
i asked the list, why the examples deal only with transformations like
(map f).(map g) -> map (f.g),
why not deal with algebraic simplification, say,
(x^2+x+1)*(x-1) -> x^3-1.
And the language extension is suggested, illustrated by the example
class (Eq a,Multiplicative a) => MulGroup a --multiplicative group
where
unity :: a
inv :: a -> a -- inversion
{properties x==x ... }
{rules (x*y)*z = x*(y*z) ...}
Marc Van Dongen,
D.Tweed <[EMAIL PROTECTED]>,
Arvind <[EMAIL PROTECTED]>,
and others came with helpful remarks. Thank you.
It becomes clear i had forgotten of *bottom*.
Indeed, say, x - x --> 0
may occur incorrect, because x may become an un-defined value.
I knew of these "bottom" affairs, but just had forgotten of them when
wrote the letter!
Still i think it is good to allow such rules.
First reply
-----------
Let us consider the above MulGroup as the programmer class, not
proposed for standard. As the programmer sets the above rules, like
x*(inv x) -> unity, why, this means one *wants* them to apply to
the program, the compiler obeys. The programmer chooses certain order
of computation. Are not you doing the same when you write in
Haskell-98
head (map (\n->4/n)) [a,b,c]
?
You know that b may occur 0, and you choose certain order of
computation.
One may also add MulGroup', with mul',inv' - without rules.
Again, this is *not* a bug in compiler to optimize the program
"around bottom" and throw the "bottom" out. This is done according to
user program, that may arrange rules this or that way.
And this is not necessarily an optimization. It is often hard to
control whether the rules make the program worse.
The problem is that it is often hard to control the effect of rules.
One also needs a tool that would help to improve rules, sometimes it
is possible. For example, improving the above MulGroup rules, the
completion algorithm can produce several nice rules for the group
theory, possessing the confluency property.
But even without such property, the rules may do good.
Trying to generalize solution
-----------------------------
class (Eq a) => Set a where belongs :: a -> Bool
class (Set a,Multiplicative a) => MulGroup a
where
unity :: a
inv :: a -> a -- inversion
{properties
belongs unity,
(belongs x & belongs y & belongs z ==>
belongs (x*y) & belongs (inv x) &
x==x & (x==y ==> y==x) & (x==y & y==z ==> x==z) &
(x==y ==> x*z == y*z)
)
}
{rules belongs x & belongs y & belongs z ==>
(x*y)*z = x*(y*z) &
unity*x = x & x*unity = x
x*(inv x) = unity & (inv x)*x = unity
}
Here `belongs' is the operation from the *standard* class Set.
Defining `belongs' means taking the subset of a type `a'.
Let us call it a base set.
Here, for MulGroup, we call it G - a subset of type `a'.
(belongs x) means x is *defined* and belongs to G.
The compiler has to understand the above `properties', `rules'
respectively. Say,
"if x,y (are defined and) belong to G,
then
x*y, inv x (are defined and) belong to G,
satisfy the above equations, and should be simplified as it is
arranged in rules
".
How the compiler could use `belongs'?
For example,
data NZRatio = NZR Rational deriving(Eq, many things desirable)
-- non-zero rational
instance Set NZRatio where belongs (NZR r) = r /= 0
-- multiplicative group of Rational has its set G = Rational \ {0}
-- - not the whole type
instance Multiplicative NZRatio where (NZR x)*(NZR y) = NZR (x*y)
instance MulGroup NZRatio where unity = NZR 1
inv (NZR x) = NZR (1/x)
Then, processing
f :: NZRatio -> [NZRatio]
f x = let (a,b,c) = (NZR 1, inv (NZR 2), inv (NZR 0))
in
(x*(inv x)):(c*(inv c)):(map ((NZR 2)*) [a,b])
the compiler proceeds with
(\x-> [x*(inv x), (NZR 0)*(inv (NZR 0)), (NZR 2)*(NZR 1),
(NZR 2)*(inv (NZR 2))]
),
(\x-> [x*(inv x), (NZR 0)*(inv (NZR 0)), (NZR 2)*(NZR 1), NZR 1]
),
maybe, even
(\x-> [x*(inv x), (NZR 0)*(inv (NZR 0)), NZR 2, NZR 1]
)
Here `x*(inv x)' cannot simplify because the conditional `inv' rule
fails to test statically x==0.
The second of this list does not simplify for the same reason, only
0 is detected surely.
But (NZR 2)*(inv (NZR 2)) gets simplified.
I do not know. Could the compiler handle such things systematically?
There exists the rewrite rule theory for conditional rewriting.
How simple and applicable is it?
Domain declaration
------------------
- in addition to type declaration (?)
The way out may be to extend the language to allow also
f :: NZRatio -> [NZRatio]
f x =
{properties belongs x} --***
let (a,b,c) = (NZR 1, inv (NZR 2), inv (NZR 0))
...
Similarly as we declare a type of variable x, we could declare the
membership of x to base set.
This applies to each instance of standard class Set. So the compiler
gets to strong rewriting mode with `x' (condition satisfied), and it
would convert the above x*(inv x) to NZR 1.
In this manner many things can be solved at compile time.
If the programmer wants to express another situation with f - when
x may occur zero, then let one skip the {properties..} line.
Such declarations, joined with rules, can force many expressions to
simplify or not, depending on `belongs x' is set or not for certain
variable.
Am i missing something?
Also D.Tweed <[EMAIL PROTECTED]> writes
> [..] it may dramatically affect the size of expressions held
> temporarily, eg
>
> tipsOfTheDay
> = map addCopyrightLogo (map toUppercase (map addHaveANiceDay
> [tip1,tip2,tip3,........,tip_n]))
>
> will, if I understand correctly, transform given the rules
> generally envisaged
>
> map f . map g ==> map (f.g)
> map f (x:xs) ==> f x:map f xs
>
> into
>
> tipsOfTheDay=[addCopyrightLogo(toUppercase(addHaveANiceDay tip1)),......
> addCopyrightLogo(toUppercase(addHaveANiceDay tip_n))]
>
> even if n is 1000 but only three or four tips are ever actually used in
> the program, with the consequent increase in the number of closures
> stored. [..]
But the rules apply at compile time. Do i understand correct?
In this particular example the compilation cost is proportional to the
list length [tip1,tip2,tip3,........,tip_n].
And the programmer does not set `tip_n', one sets the concrete data,
not very long, say, [tip1,tip2,tip3,tip4,tip5].
Still it would be easy to forget of the `rules' power and obtain too
large expressions when compiling. Maybe, one needs a tool to mark the
scopes for the `rule' application in the program.
------------------
Sergey Mechveliani
[EMAIL PROTECTED]
