Re: [Axiom-developer] non extending category

[Ralf Hemmecke]

On 02/12/2006 08:31 PM, Bill Page wrote:
> > > > I haven't found a definition for the "SubDomain" constructor
> > > > that appears in src/algebra/integer.spad. :-(
> > > Like SubsetCategory, SubDomain is apparently a compiler primative.
> > Hmm, that cannot be true.
>
> ??? But this is true. src/algebra/integer.spad is written in SPAD.
> Did you check the references in the interp/compiler.boot code that
> I sent you?

No I did not check. I don't speak "BOOT".
Now I checked and I know as much as I knew before. That code is not 
understandable to me. Although I tend to say that in

coerceSubset([x,m,e],m') ==
  isSubset(m,m',e) or m="Rep" and m'="$" => [x,m',e]
  m is ['SubDomain,=m',:.] => [x,m',e]
  (pred:= LASSOC(opOf m',get(opOf m,'SubDomain,e))) and INTEGERP x and
     -- obviously this is temporary
    eval substitute(x,"#1",pred) => [x,m',e]
  (pred:= isSubset(m',maxSuperType(m,e),e)) and INTEGERP x -- again 
temporary
    and eval substitute(x,"*",pred) =>
      [x,m',e]
  nil

(which is the only place where "SubDomain" appears) that does not look 
like a DEFINITION of "SubDomain", more like USE.

> > If I compile just with the Aldor compiler, then the SPAD compiler
> > is not involved.

> But src/algebra/integer.spad is involved indirectly through
> the Axiom library interface, I think.

That should certainly be true, but that code does not contain a 
definition of SubDomain. It must be defined somewhere else and that code 
must live in libaxiom.al since that is the only data that Aldor sees 
from Axiom.

> > So if the Aldor compiler does not complain, it must find
> > "SubDomain" in libaxiom.al. I am pretty sure that the Aldor
> > compiler does NOT know of "SubDomain" by itself.

> Perhaps it is true that stand alone Aldor does implement
> something like SubDomain in the algebra.

There are three relevant libraries around
1) libaldor.al (aldor.org)
2) libalgebra.al (aldor.org)
3) libaxiom.al (AXIOM)

Since I have access to the sources of the first two libraries, I can 
assure you that there is no definition of "SubDomain" there.

> Aldor, in a sense,
> is a more "primitive" compiler than SPAD, i.e. with fewer
> things built-in and more of "SPAD" actually coded in Aldor.

Right. That is the reason why it is actually easy to learn Aldor. There 
are only a few language constructs that you have to remember.
It is much harder to learn what is available through libraries.
Unfortunately, there are several libraries around and except that 
libalgebra.al builds upon libaldor.al, there are many incompatibilities 
between libaxiom and libalgebra.

To make things even more complicated... there is also a library 
libaxllib.al and basicmath.al. I haven't seen the latter one, but Marc 
Moreno Maza (who wrote most of it -- I believe) ported much code to 
libalgebra.al.

> > In integer.spad it says
> >
> > NonNegativeInteger: ...
> >    == SubDomain(Integer, #1 >= 0) add ...
> >
> > So, if I remember correctly, "#1 >=0" is an old way of declaring an 
> > anonymous function (without giving the types!!!)
> >
> > (x: Integer): Boolean +-> x >=0
>
> No. The expression '#1 >= 0' is a boolean expression which is
> saying something like "you can coerce an Integer to an NNI
> provided that the integer value is greater than or equal to
> zero".

OK. '#1 >= 0' is depending on the first argument of SubDomain. 
Otherwise, nobody could find out what the symbol '0' actually stands 
for. So I guess then an Aldor definition would look like

SubDomain: (T: Type, isElement?: T -> Boolean): ??? == { ... }

where ??? is some category that is quite hard to guess.
And the second entry of SubDomain is a Boolean valued function
(ie. '#1 >= 0' is a function).

> > But what does SubDomain return?

> SubDomain is an expression that defines a new domain.

That is a good guess. ;-)

> > And a much more interesting question: how does this work?

> For that you must consult the undocumented interp/compiler.boot
> source code. :(

Since SubDomain is not clearly defined, nobody will be able to use it 
properly except those few people who know about its semantics. For all 
the others it is guesswork and that totally contradicts the goal of 
Axiom to support a clear type hierarchy.

> > If I see Integer, than that is a blackbox for me. I only
> > know the interface, ie, its type or its category.
> >
> > Now what should SubDomain do? It takes, for example, the 
> > implementation of a function *: (%, %) -> % from Integer
> > and returns another implementation that checks whether the
> > input arguments are non-negative and the result is non-negative.
>
> No. I think it simply lifts all operations from Integer to NNI.

That is what I feared. It is like a hidden "pretend" somewhere.

In Aldor one could write it like

NNI: SomeCategory == Integer add {
  Rep == Integer;
  -- remaining functions
}

NNI then inherits anything from Integer that it does not explicitly 
override. So for example, if SomeCategory contains

-: (%, %) -> %

and NNI does not explicitly override it, then it is the - from Integer.
But that would clearly not be the intend of the programmer, since 3-4 is 
not a NNI. So one has to override it.

(a: %) - (b: %): % == {
  c: Rep := rep a - rep b;
  if c < 0 then throw NoNonNegativeIntegerException;
  per c;
}

I guess, what SubDomain does, is to add to each function that returns 
"%" (i.e. a NNI) a check that is given through the second argument of 
SubDomain.

That looks inefficient, given that there is no need for a check for the 
addition function. :-(

> > Oh, something interesting... After the definition of NNI in 
> > integer.spad it reads
> >
> >    {\bf NNI} depends on itself.
> >
> > That is not at all obvious for my eyes. If Integer would be 
> > implemented without referring to NNI (and that can be done),
> > then NNI could be implemented on top of Integer. So why is there
> > a need for a cycle here?
>
> I also do not understand this comment in the code.

Well, maybe it is a little like in the libraries of Aldor. In libaldor 
Integer is defined. But the concept of an AbelianMonoid is not yet 
there. Later, (in libalgebra) the category AbelianMonoid is introduced 
which contains the signature

        *: (Integer, %) -> %;

Again, later Integer is extended to belong o the category AbelianMonoid.
That looks like a circular definition for Integer, but by means of 
Aldor's "extend" keyword, that causes no problem at all.

Ralf