
From:  Gabriel Dos Reis 
Subject:  Re: [Axiomdeveloper] Adhoc 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.axiomdeveloper.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/adhocpolymorphism.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 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/axiom developer
[Prev in Thread]  Current Thread  [Next in Thread] 