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

[Page, Bill]

On Monday, March 13, 2006 7:32 PM Gaby wrote:

> ...
> Bill Page writes:
> 
> > 
> > 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.
> 
> we should also probably find a way to minimize the "pretend"s :-)
> 

The use of 'pretend' has to do with the issue of representation.
I suppose it would be better to write:

   default {
     Rep == T;
     square(t: %): % == per(m(rep(t), rep(t))
   }

Really this is mostly sugar since we know that rep and per
are just implemented as macros involve Rep, %, and pretend.
But I suppose that a more type-safe implementation might
be possible.

It seems to me that both SPAD and Aldor are more specific about
representation than most other languages (at least those that
I know sufficiently well). I think the semantics are motivated
by the mathematical example of an abstract group and it's
underlying representation, e.g. as a matrix with a particular
structure. But I am still rather unsure about how best to
understand this construct. And further 'Rep', 'rep' and 'per'
do not seem to be "properly distinquished" syntactically
given the important role they play in the construction of
domains.

I would be very interested in your thoughts about this.

-------

Probably what we really want to write here is:

  MyMonoid(m: (%, %) -> %): Category == with {
     square: %-> %;
     default {square(t: %): % == m(t, t)}
  }

In which case

  extend MyWord: MyMonoid(c)

can only make sense if c is defined in MyWord (% in this
context means the domain). This is kind of an "inner"
extension of the domain.

Unfortunately neigther Aldor nor SPAD can compile something
quite this generic.

Regards,
Bill Page.