Ad-hoc polymorphism paper

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
3 messages Options
Reply | Threaded
Open this post in threaded view
|

Ad-hoc polymorphism paper

Tim Daly
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
[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer
Reply | Threaded
Open this post in threaded view
|

Re: Ad-hoc polymorphism paper

Gabriel Dos Reis
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:
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
[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer



_______________________________________________
Axiom-developer mailing list
[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer
Reply | Threaded
Open this post in threaded view
|

Re: Ad-hoc polymorphism paper

Tim Daly
Indeed. Apparently the bleeding edge is actually Homotopy Type Theory.

I'm taking a course from Robert Harper on the subject now. I'm meeting
with 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.

I'm also taking a course with Jeremy Avigad on the details of Lean
and Interactive Theorem Proving. I've been reading the source code
of the Lean kernel to try to understand how it works.

So much to know, so little time.

It is clear, however, that there is a nice mapping between these ideas
and Axiom's ideas. The goal is to get a "thin thread" through the system
that involves a proof of the GCD but to do it in such a way that proofs
become first-class objects, implemented in the Domain and propositions
are types defined in the Category, requiring proof in the Domain.

The idea of 'typeclass' matches the idea of Category (Axiom) nicely.
The idea of 'instance' matches the idea of Domain nicely.

Tim


On Sun, Mar 12, 2017 at 3:00 AM, Gabriel Dos Reis <[hidden email]> wrote:
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:
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
[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer




_______________________________________________
Axiom-developer mailing list
[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer