|
From: | Martin Baker |
Subject: | Re: [Axiom-developer] Axiom Sane musings (SEL4) |
Date: | Sat, 21 Sep 2019 09:49:37 +0100 |
User-agent: | Mozilla/5.0 (X11; Linux x86_64; rv:60.0) Gecko/20100101 Thunderbird/60.8.0 |
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.
[Prev in Thread] | Current Thread | [Next in Thread] |