[Top][All Lists]

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

Re: [Axiom-developer] non extending category

From: Ralf Hemmecke
Subject: Re: [Axiom-developer] non extending category
Date: Mon, 13 Feb 2006 01:05:08 +0100
User-agent: Thunderbird 1.5 (X11/20051201)

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) =>

(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 since that is the only data that Aldor sees from Axiom.

So if the Aldor compiler does not complain, it must find
"SubDomain" in 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) (
2) (
3) (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 builds upon, there are many incompatibilities between libaxiom and libalgebra.

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

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

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.


reply via email to

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