Reimplementing AXIOM systems with a Hindley-Milner style polymorphism will take the computer algebra community at least three or four decades back -- with no improvement.
-- Gaby On Fri, Mar 3, 2017 at 4:21 PM, Tim Daly <axiom...@gmail.com> wrote: > 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 > >
_______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer
