axiom-developer
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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 %

although apparently the compiler does not worry about this since
your representation of the domain MyWord below is the same as the
operation that you pass to MyMonoid.

> 
> MyWord: with { 
>    coerce: String -> %;
>    c:(%, %) -> %
> }
>    == add {
>    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 -> %;
}
   == add {
   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.






reply via email to

[Prev in Thread] Current Thread [Next in Thread]