[Aldor-l] Axioms in Aldor [was: Re: "has" and "with" and bug]

[Ralf Hemmecke]

>>> It would be nice if there were any better means in Aldor to state  
>>> axioms for functions than just creating a category (like AbelianMonoid).
>> Axioms seem rather redundant to me.  What's the problem with introducing  
>> a category like:

>>   define CommutativeTimes: Category == with { *: (%,%) -> % }

Oh, that is not the same thing. That just defines a name. The properties 
of what "commutative" actually means are hidden in the documentation. 
What I want is some formal expression (also available to the compiler) 
that says "forall a,b:% it holds a*b=b*a". Note that there is even the 
"=" function involved here.

> I am not saying that Mathematica is superior to Aldor, but Mathematica has  
> for example Attributes that can be applied to _functions_:
> http://reference.wolfram.com/mathematica/tutorial/Attributes.html

> Thereby, you can specify that you expect f( a, b ) to be equivalent to  
> f( b, a ) by attaching the "Orderless" Attribute to "f".
> Mathematica in turn can exploit this knowledge to speed things up.

But such an attribute is not very much different from Martin's 
CommutativeTimes above. One just has to attach it to "*". But all this 
completely fails to do some formal proving about that all. Where would 
be the equation "a*b=b*a" that explains everything?

Ralf