who visited the Axiom group at IBM Research.
Axiom introduces the idea of "conditional categories" which does
not seem to be anywhere else. (see Santas paper) You can say
C0: Category == with (if % has Ring then Ring)
so you can assert Ring in the current Domain (called %)
if the Category chain includes Ring. Knowing that, the
Domain (Instance in Lean) can conditionally add functions
D0 : C0 ==
if % has Ring then
foo: % -> %
Axiom was far ahead of its time and once it has a proof mechanism
it will be far ahead of all other computer algebra systems.
I'd really like to replace the current type-resolution machinery in Axiom
with a more formal approach. The compiler requires explicit types
everywhere. The interpreter does type inference. It would be interesting
to re-implement it using a Hindley/Milner style machine. I suspect that
would raise some interesting research questions as Axiom implements
a very general coerce/convert mechanism. Even so, there are special
cases hard-coded into the interpreter.
A theory-based machine would be much easier to prove correct.