RE: [Axiom-developer] categorical design

[Bill Page]

Tim,

On Thursday, October 09, 2003 10:25 AM you wrote:
> 
> It is perfectly possible to develop an independent type 
> hierarchy that lives along side of the existing hierarchy. 
> Indeed the could interact where convenient (e.g. using data 
> structures in common so already-implemented algorithms can be
> used).
> 

Yes, this is (more or less) what I was contemplating,
although it may be that for a "categorial" imlementation
in the long run very little of the algebra that now exists in
Axiom would be of much use because the changes must occur
at a very top level in the type lattice - at the level of
SetCategory.

Note: I used the word "categorial" (not a typing error).
This was a convention used by a few category theorists some
years ago when there was the possibility of being confused
over other uses of the word "category" and especially to
avoid the use of the word "categorical" which sounds
unnecessarily pejorative and non-technical. <grin>

More specifically, I am thinking that it may be possible to
build on Axiom by intially going even higher up to define
a new categorial level at the top and then building up to
SetCategory on which almost all the rest of Axiom currently
hangs. (This might include Aggregate and some other top level
Axiom categories as well.) So initially only SetCategory and
Aggregate become defined in terms of this new deeper level.
But gradually one could redefine some of the lower types to
depend on types higher up in the new categorial level. And
this way gradually shift SetCategory and it's properly related
types lower down in the hierachy.

This might sound fairly simple, but the problem of course
is that really the category SET is a rather complex object
categorially speaking.

But even more speculatively speaking, I have come to realize
that what we more or less naturally assume to be a type hierachy
(lattice) is not really a lattice at all in the case of Axiom -
it contains loops! Your current method of "breaking" these
loops is quite simple since in most respects the existing
loops in Axiom are quite simple (This is a claim that I can
not yet actually substantiate.) But if we can assume a more
general approach to "solving" such specification loops (e.g.
by the iterative "fixed point" approach I mentioned many
emails ago). Then *maybe* it makes sense to actually begin
now by redefining SetCategory (and a few other top level
Axiom categories) in terms of some of the lower level ones.

This latter strategy would of course introduce some serious
and potentially non-trivial loops in the "hierachy". And
the trouble is that I am really not sure I understand well
enough what it means to deal in general terms with type
specifications given in this manner. Now that seems like a
serious mathematical/computer science research subject to
me!

I would like to hear more from you (and other longer term
Axiom builders/hackers) about the loops in Axiom's type
system. Are these "errors" which need to be eliminated?
Or are they a new more powerful method of defining types?

Is it true that recent formal developments in mathematics
support the idea that such loops are really a necessary
and fundamental part of mathematics? What do you think
Bertfried? I think it was you who suggested this first here.

Cheers,
Bill Page.