RE: [Axiom-math] POLY INT =\\= UP(x, INT)

[Page, Bill]

On Wednesday, October 08, 2003 3:59 PM Dylan Thurston
address@hidden wrote:

> > ...
> > I am very interested in participating in a joint project
> > (with people more knowledgeable about AXIOM then myself!)
> > to provide a much more "categorial" type system. ...
> 
> Can you say what you mean by a more "categorial" type system?

Do you have the Axiom Book? If so take a look at the front
and back inside covers. If not look at the last few pages of
'axiom-tech-intro.pdf' in Axiom_Book at

  http://savannah.nongnu.org/files/?group=axiom

These diagrams are a little out of date and missing a few
details, but this level they are probably ok.

The Basic Algebra Hierarchy and the Data Structure Hierarchy
both show the category SetCategory (Category in Axiom's sense
and only "sort-of" in the sense of category theory. (I will
use the word "categorial" to refer to category theory when
possible.) at the top of the type hierarchy. On the concrete
side both Aggregate and SetCategory appear appear at the
top. SetCategory and the category Finite are unusual in that
they appears in both hierarchies.

It seems reasonable to think of the Algebra side as being
"abstract" and the Data Structure side as "concrete". I think
a lot of Axiom has to do with using the concrete side to
implement representations of the abstract side.

SetCategory exports only one function, = . The category
Finite adds the function 'size', 'lookup' (membership?) and
a few others. FiniteSetAggregate adds 'universe' and
'complement', etc. Finally, the domain SET itself is built
on FiniteSetAggregate and provides the rest of the structure
that we usually associate with finite sets.

There are other relationships shown in the diagram but this
is enough to make my point - which is that Axiom does all
this without ever have said formally anything about
functions or mappings! In fact nothing abstract is said
about mappings in this hierarchy at all. This is very
non-categorial and very classical in the role that SetCategory
plays.

I think a categorial type system would start very differently.
We would need an Axiom category named say, Category, at the
top of the Basic Algebra Hierarchy. And we would expect Category
to export at least "objects" and "morphisms" as well as
composition of morphisms. And there will be Axiom domains
which represent categorial categories in the category Category
and natural transformations which belong to the morphisms
of Category, etc. The terminology is a bit confusing
because Axiom's definitions do not quite fit exactly with
the modern categorial terms. But I think you must get my
basic idea.

We can put more algebraic structure "up top" and delay the
definition of sets etc. to somewhat later in the hierarchy.
Many (most?) abstract mathematical categories can be defined
without reference to these lower-level set-theoretic
properties. And at the same time we can establish a simpler
more direct relationship between the data structures in the
Data Structure Hierarchy and the finite concrete categories
on the Algebra side. At least that's the prospectus.

Actually, it is not *my* original idea, although I did
do some PhD work on the application of algebraic set theory
(topos categories) in the theory of database systems
with Michael Barr at McGill. Unfortunately it did not go
all the way ... (that's another story).

There are several people who have specifically discussed
the relationship between Axiom and category theory. See
for example:

  Computing with Category Theory (Youssef, BU 2001)
  http://physics.bu.edu/~youssef/homepage/talks/categories/categories.html
  http://nut.bu.edu/~youssef/index.htm


> From my point of view, the basic AXIOM type system seems
> reasonable; it's close to what I came up with myself when
> trying to design a basic type system for Haskell, for
> instance.

I agree that it is reasonable in it's own historical context.

> I haven't looked much past the lower levels of the hierarchy,
> however, and could certainly believe it needs work; but I
> don't know that thinking about it as an entire redesign of
> the type hierarchy would be helpful.

Perhaps you are right but that is more or less what the
category theorists did to Burbaki's master plan for
mathematics ...

> 
> In the case at hand, the types in question seem eminently
> reasonable. The one question in my head is why there's a
> need for the Polynomial constructor, polynomials with no
> specification as to the variables, given the presence of
> UP(x, ...) and so forth.

I agree that that is a good question.

> But AXIOM is actually able to make that cast (from
> POLY(FRAC INT) to UP(x, FRAC INT)) itself; the problem[1]
> is that it doesn't think if the cast from UP(x, INT) to
> UP(x, FRAC INT) automatically.

Yes, I see that you are right about that. From Tim's
description it seems clear that it was the Axiom designer's
intent that Axiom should be able to find this set of coercions.
Is it entirely accurate, do you think, to equate 'casts' in
the programming sense with 'coercions' in Axiom's sense?

> 
> This doesn't seem like a problem of the type hierarchy here;
> rather, it's something with the type inference engine.
> I don't think it could be fixed at the level you're thinking
> of.

I agree. These comments are not intended to address that
specific problem.

> 
> Peace,
>       Dylan
> 
> [1] Apart from the bug of sometimes giving wrong answers,
> which still needs to be investigated and fixed.

Do you mean the fact that in some cases partialFraction
returns things that are not technically partial fractions?
If so, then yes, I think that a better solution is needed
when partialFraction cannot produce a valid result.

Cheers,
Bill Page.