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 Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer
