[Axiom-developer] Ad-hoc polymorphism paper

[Tim Daly]

Jeremy,

I read Wadler's paper. I find it amusing because these ideas were

implemented in Axiom long before the paper was published.
(http://202.3.77.10/users/karkare/courses/2010/cs653/Papers/ad-hoc-polymorphism.pdf)

One advantage, though, is their formalization. In the computer

algebra world there was work by Santas "A Type System for

Computer Algebra (http://daly.axiom-developer.org/Sant95.pdf)

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.

Tim