Re: [Axiom-developer] Unions in Spad

[William Sit]

Dear Bill:

Before we get into more category theory, the prerequisite
for even talking about colimits (or limits) is the very
simple idea of a family of morphisms (as well as objects) as
required in these constructions (for example, the notion of
a diagram). This is no more than an indexed set and a map
from the indexed set to a set of maps  (morphisms) or
domains (objects). The implementation problems are already
glaring. Let's solve some practical problems first.

Category theory is beautiful, but when we start
implementing, the great generality of category theory
becomes more of a hindrance than a help. No doubt it
clarifies many algebraic constructions by carefully
describing the conditions, and duality makes it easy to
accept results with half the effort.  In this respect, CT is
quite similar to Model Theory in logic. Powerful
mathematics, no doubt, and essential to the understanding of
mathematical structures, notions such as various dimensions,
and algorithms. But when it comes to application, one still
has to unwind all the definitions in the specific category
and interpret the results there. Without getting notions
back to the less abstract, and reducing the details to
computer science, it's just idealism. I'm sure the earlier
Axiom developers all know category theory (and the results
you mentioned which have been known long long time ago) and
were much influenced by it. But from what we know about
Axiom implementation, the details and technical difficulties
pretty much forced certain unpleasant choices. The case of
Union (untagged and tagged) is one such compromise.  The
proliferation of different data representations to make
computation efficient for specific problems is another. None
of this can be helped by CT.

However, I would be interested to hear how you plan to
create a basic computer algebra system from scratch based on
category theory. Specifically, how does duality help with
say implementation of products and coproducts when their
data representation cannot be dualized? ( I know duality
would help with how one should specify exports, which is
important; but how does duality help with implementation?)
What do we have now that the earlier developers don't have
that makes you think this time around, we can do better
(other than because computers are faster)?

William