axiom-developer
[Top][All Lists]

## RE: [Axiom-developer] BINGO, Curiosities with Axiom mathematical structu

 From: Bill Page Subject: RE: [Axiom-developer] BINGO, Curiosities with Axiom mathematical structures Date: Thu, 9 Mar 2006 16:21:41 -0500

```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!

Also, I think you should write:

square: % -> %;
default {square(t: %): % == m(t pretend T, t pretend T) pretend %

your representation of the domain MyWord below is the same as the
operation that you pass to MyMonoid.

>
> MyWord: with {
>    coerce: String -> %;
>    c:(%, %) -> %
> }
>    Rep == String;
>    import from String;
>    coerce(a: String): % == per(a);
>    c(a: %, b: %):%  == coerce(concat(rep(a), rep(b))\$String) }
>
> import from MyWord;
> extend MyWord: MyMonoid(MyWord, c) == add;
> -----------------
>

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 %
}
}

MyWord: with {
coerce: String -> %;
}
Rep == String;
coerce(a: String): % == per(a);
}

import from MyWord;
extend MyWord: MyMonoid(String, concat\$String) == add;

-----------

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

Regards,
Bill Page.

```