|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
karkare/courses/2010/cs653/ Papers/ad-hoc-polymorphism.pdf )
One advantage, though, is their formalization. In the computer
org/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
|[Prev in Thread]||Current Thread||[Next in Thread]|