
From:  Tim Daly 
Subject:  Re: [Axiomdeveloper] Adhoc polymorphism paper 
Date:  Sun, 12 Mar 2017 04:55:02 0400 
Reimplementing AXIOM systems with a HindleyMilner 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.axiomdeveloper.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/ )adhocpolymorphism.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 typeresolution machinery in Axiomwith a more formal approach. The compiler requires explicit typeseverywhere. The interpreter does type inference. It would be interestingto reimplement 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 hardcoded into the interpreter.
A theorybased machine would be much easier to prove correct.Tim_________________
Axiomdeveloper mailing list
address@hidden
https://lists.nongnu.org/mailman/listinfo/axiomdeveloper
[Prev in Thread]  Current Thread  [Next in Thread] 