Re: [Axiom-developer] Curiosities with Axiom mathematical structures

[Gabriel Dos Reis]

Ralf Hemmecke <address@hidden> writes:

[...]

| Yes, one has to rethink that quite a lot. The problem with your
| suggestion is the following
| 
| 1) You cannot simply ask
| 
|    Integer has Monoid
| 
| because you have to give a parameter.

yes, that is alright.  The question

    Integer has Monoid

is an underspecified question.

| 2) If you say something like
| 
| MyMonoid(T: Type, m: (T, T) -> T): Category == with {
|    square: T-> T;
|    default {square(t: T): T == m(t, t)}
| }
| 
| then it is perfect Aldor.
| Then, however, you ask
| 
|    Integer has MyMonoid(Integer, *)
| 
| and it will return true only if you have said
| 
| extend Integer: MyMonoid(Integer, *) == add;
| 
| somewhere.

That is fine! -- I don't expect Aldor to read my mind :-)

| (But probably you had something else in mind.)
| 
| Although I don't really like that an AbelianMonoid is not a Monoid,
| and although I think that renaming during inheritance would be nearer
| to mathematics...

I still don't follow that path.  Please could you explain with more
examples?  The understanding of renaming I have causes more trouble
than it solves problem.

|  after all the discussion here, I somehow think that
| the design in Axiom is not really bad. The reason is that I have not
| seen a clear case where renaming would be over-advantageous.
| 
| I'd like to say
| 
|    Integer has Monoid
| 
| instead of
| 
|    Integer has Monoid(*, 1);
|    Integer has Monoid(+, 0);

I would not.  The question

     Integer has Monoid

gives me no clue about what is going on.  

In fact, in situations where when I ask the question

    Integer has Group(op)

I'm more interested interested in retrieving the inverse operation and
neutral element of op, than just the mere question is it a Group.

Consider computing the nth "power" of x (of type T).  First of, one
can have a general (helper) implementation of "power" for a monoid (or
even just a semigroup or a magma) see page 99 of

     http://www.stepanovpapers.com/notes.pdf

and onwards.  If n is negative and T is a group, then one can just
take the "positive" power of the inverse of x -- reuse known
abstraction. 

| Simply think of a category Foo with hundreds of exported function,
| would you like to write
| 
|    Dom has Foo(f1, f2, ..., f100)
| 
| ??? That is not really handy.

quite; but I believe my first idea can be refined (as I did):  I doubt
all of the hundreds parameters for Foo are independent.  In pratice,
the number of indenpendent parameters for the algebraic structure does
nto exceed 5 or six.  However, many of the "exported" functions are 
"functions" of those independent parameters.

-- Gaby