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

[William Sit]

Bill Page wrote:
> 
> Martin,
> 
> I think you have a rather beautiful idea... but I see some
> problems.
> 
> On March 9, 2006 11:08 AM you wrote:
> >
> > I am satisfied now:
> > -----------------
> > #include "axiom"
> >
> > MyMonoid(T: Type, m: (T, T) -> T): Category == with {
> >    square: T-> T;
> >    default {square(t: T): T == m(t, t)}
> > }
> 
> This definition of the category MyMonoid looks quite strange
> because it does not export any binary operation!

Correct, but if the goal is to allow the domains to define the notations for the
structure operations, then the domain must export it. The category would have no
way to know.
 

> The exported binary operation that we normally think of as
> belonging to the monoid, had to be declared in the definition
> of this domain. This does not see right.
> We could define it like this:
> 
> MyMonoid(T: Type, m: (T, T) -> T): Category == with {
>    * : (%,%) -> %;
>    square: %-> %;
>    default {
>      (x:%)*(y:%):% == m(x pretend T, y pretend T) pretend %;
>      square(t: %): % == m(t pretend T, t pretend T) pretend %
>    }
> }

This, in fact, is exactly what Axiom now have, except for the fact that both T
and m are anonymous and implicitly mapped to % and * when one writes:

    Word: Monoid == ...

In your code above, there is no explicit relation between T and %, the code x
pretend T may or may not work.

> MyWord: with {
>    coerce: String -> %;
> }
>    == add {
>    Rep == String;
>    coerce(a: String): % == per(a);
> }
> 
> import from MyWord;
> extend MyWord: MyMonoid(String, concat$String) == add;
> 
This illustrates my comment above. The Rep == String (or Rep:=String) is not
visible externally, and hence your extend statement may have a problem.

> But then we have fixed the symbol * to denote the monoid operation.
> This was something we were trying to avoid, right?

That is right. But you can't have both (at least, we haven't found a way and it
seems very unlikely given the current compiler restraints), and this is why the
exports must come from the domain, unless some default notation is chosen in the
category itself.

William