Re: [Axiom-developer] Axiom Sane musings (SEL4)

[Martin Baker]

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.