Ad-hoc polymorphism paper

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

_______________________________________________
Axiom-developer mailing list
[email protected]
https://lists.nongnu.org/mailman/listinfo/axiom-developer