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 <axiom...@gmail.com> wrote:
> Jeremy,
>
> I read Wadler's paper. I find it amusing because these ideas were
> implemented in Axiom long before the paper was published.
> (http://202.3.77.10/users/karkare/courses/2010/cs653/
> Papers/ad-hoc-polymorphism.pdf)
>
> One advantage, though, is their formalization. In the computer
> algebra world there was work by Santas "A Type System for
> Computer Algebra (http://daly.axiom-developer.org/Sant95.pdf)
> who visited the Axiom group at IBM Research.
>
> Axiom introduces the idea of "conditional categories" which does
> not seem to be anywhere else. (see Santas paper) You can say
>
> 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
> axiom-develo...@nongnu.org
> https://lists.nongnu.org/mailman/listinfo/axiom-developer
>
>
------------------------------------------------------------------------------
Announcing the Oxford Dictionaries API! The API offers world-renowned
dictionary content that is easy and intuitive to access. Sign up for an
account today to start using our lexical data to power your apps and
projects. Get started today and enter our developer competition.
http://sdm.link/oxford
_______________________________________________
open-axiom-devel mailing list
open-axiom-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
