I'm a fan of both Axiom and Idris. I think my ideal would be Axiom
mathematics build on top of the Idris type system.
The Axiom type system was incredibly advanced for its time but I suspect
the Idris type system has finally caught up and overtaken it? Correct me
if I'm wrong but I think the Axiom type system does not have the
following capabilities that Idris does:
* Enforcement of pure functions.
* Ability to flag a function as total as opposed to partial (automatic
in some cases).
* Universes (types of types hierarchy).
I'm no expert but I would have guessed these things would be almost
indispensable for proving Axiom correct?
Also Idris makes it far more practical to use these things, I don't
think Axiom can implement category theory constructs like monads. Also,
although both have dependent types, Axiom does not use them for say,
preventing the addition of a 2D vector to a 3D vector. In Idris this is
more likely to be compile time error than a runtime error, I know there
are theoretical limits to this but I think Idris has capabilities to
make this practical in more cases.
I don't pretend I know how an Idris type system could be used with Axiom
in practice. For instance I think the proofs Henri is talking about are
equalities in the type system (propositions as types). So how would
these equations relate to equations acted on by equation solvers (which
might be an element of some equation type). Could there be some way to
lift equations into the type system and back?
Sorry if I'm confusing things here but I just have an intuition that
there is something even more powerful here if all this could be put
together.
Martin
On 21/09/2019 04:28, Tim Daly wrote:
Axiom has type information everywhere. It is strongly
dependently typed. So give a Polynomial type, which
Axiom has, over a Ring or Field, such as
Polynomial(Integer) or Polynomial(Fraction(Integer))
we can use theorems from the Ring while proving
properties of Polynomials.
_______________________________________________
Axiom-developer mailing list
Axiom-developer@nongnu.org
https://lists.nongnu.org/mailman/listinfo/axiom-developer