Jeremy, 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 computer who visited the Axiom group at IBM Research. C0: 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, the Domain (Instance in Lean) can conditionally add functions D0 : C0 == if % has Ring then foo: % -> % Axiom was far ahead of its time and once it has a proof mechanism it will be far ahead of all other computer algebra systems. I'd really like to replace the current type-resolution machinery in Axiom with a more formal approach. The compiler requires explicit types everywhere. The interpreter does type inference. It would be interesting to re-implement it using a Hindley/Milner style machine. I suspect that would raise some interesting research questions as Axiom implements a very general coerce/convert mechanism. Even so, there are special cases hard-coded into the interpreter. A theory-based machine would be much easier to prove correct. Tim _______________________________________________ Axiom-developer mailing list [hidden email] https://lists.nongnu.org/mailman/listinfo/axiom-developer |
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.
-- Gaby On Fri, Mar 3, 2017 at 4:21 PM, Tim Daly <[hidden email]> wrote:
_______________________________________________ Axiom-developer mailing list [hidden email] https://lists.nongnu.org/mailman/listinfo/axiom-developer |
Indeed. Apparently the bleeding edge is actually Homotopy Type Theory. I'm taking a course from Robert Harper on the subject now. I'm meetingwith a couple profs over spring break (this week), hoping to interest them in Axiom. Unfortunately there is no grant funding behind Axiom so I'm not sure if anything will come of it. and Interactive Theorem Proving. I've been reading the source code of the Lean kernel to try to understand how it works. are types defined in the Category, requiring proof in the Domain. Tim On Sun, Mar 12, 2017 at 3:00 AM, Gabriel Dos Reis <[hidden email]> wrote:
_______________________________________________ Axiom-developer mailing list [hidden email] https://lists.nongnu.org/mailman/listinfo/axiom-developer |
Free forum by Nabble | Edit this page |