|
From: | Gabriel Dos Reis |
Subject: | Re: [Axiom-developer] Ad-hoc polymorphism paper |
Date: | Sat, 11 Mar 2017 23:00:41 -0800 |
not seem to be anywhere else. (see Santas paper) You can sayComputer Algebra (http://daly.axiom-developer.algebra 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 computerorg/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] |