[Axiom-developer] categorical design, aldor, and the type system

[Tim Daly]

Dylan, Bill,

re: Aldor rewrite. 

Many people, including myself, have tried to reconstruct and/or
rewrite the Axiom type system in Aldor. This is unlikely for at least
4 reasons.

First, the type system is reasonable but adhoc since it doesn't have a
one to one correspondence with theory. (e.g. what is a RNG?)

Second, there are types that are mathematical but their implementation
depends on various data structures for efficient implementation so
there isn't even a guiding theory.

Third, an Aldor implementation would be a library not an
interpreter/compiler combination so the user would have to perform
type coercion and simplification, which is very hard to get right.

Fourth, and to the last point, there are hundreds of man-years of
research in Axiom. A clean-room rewrite would need the many great
talents that have already contributed to Axiom (although there are new
talented people) and would never get funded (because computer algebra
"has been done"). And since Axiom work isn't usually recognized by
university departments (unlike, say, bourbaki contributions) it is
unlikely that such a massive, coordinated effort can exist. (A point
which I'm ignoring as I hope to attract free research for the love of
it :-) ).

Aldor is a great language and it is a very seductive idea to do Axiom
over and try to "get it right" but that implies covering a LOT of old
ground before you develop new work. Plus we don't even know or agree
about what is "right". I think there is a lot of new mathematics that
needs to be researched and a lot of mathematics (like symbolic
summation) that Axiom needs which exists but is not implemented in
Axiom.

re: type system

We need to examine what exists in depth and decide what the best
algorithms are for type conversion. I figure we can do this by
understanding the existing type lattice, codifying the adhoc
algorithms current in use, and developing a "coercion theory"
that shows what the algorithms should do. That way we aren't
just "patching" the problem. We're developing a theory that needs
to exist. To this end I've started collecting the raw data of
the existing type signatures so we can do the first step.

Tim