|
From: | Tim Daly |
Subject: | Re: [Axiom-developer] Ad-hoc polymorphism paper |
Date: | Sun, 12 Mar 2017 04:55:02 -0400 |
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.-- GabyOn Fri, Mar 3, 2017 at 4:21 PM, Tim Daly <address@hidden> wrote:______________________________not seem to be anywhere else. (see Santas paper) You can sayComputer Algebra (http://daly.axiom-developer.oalgebra world there was work by Santas "A Type System forJeremy,implemented in Axiom long before the paper was published.
I read Wadler's paper. I find it amusing because these ideas were
(http://202.3.77.10/users/karkare/courses/2010/cs653/Papers/ )ad-hoc-polymorphism.pdf
One advantage, though, is their formalization. In the computerrg/Sant95.pdf )who visited the Axiom group at IBM Research.Axiom introduces the idea of "conditional categories" which doesC0: 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, theDomain (Instance in Lean) can conditionally add functionsD0 : C0 ==if % has Ring thenfoo: % -> %Axiom was far ahead of its time and once it has a proof mechanismit will be far ahead of all other computer algebra systems.I'd really like to replace the current type-resolution machinery in Axiomwith a more formal approach. The compiler requires explicit typeseverywhere. The interpreter does type inference. It would be interestingto re-implement it using a Hindley/Milner style machine. I suspect thatwould raise some interesting research questions as Axiom implementsa very general coerce/convert mechanism. Even so, there are specialcases hard-coded into the interpreter.
A theory-based machine would be much easier to prove correct.Tim_________________
Axiom-developer mailing list
address@hidden
https://lists.nongnu.org/mailman/listinfo/axiom-developer
[Prev in Thread] | Current Thread | [Next in Thread] |