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

[Henri Tuhola]

Idris has a way to present equalities like this:

addition_unit : (a:Nat) -> (a + 0) = a
addition_s : (a,b:Nat) -> (a + S b) = S (a + b)
add_commutative : (a,b:Nat) -> (a + b = b + a)

They can be used to prove more things:

try_out : (x,y:Nat) -> ((x + 0) + y) = y + x
try_out x y = rewrite addition_unit x in add_commutative x y

It's rewriting the left expression to right expression, though you can
easily flip the direction. For clarity I show these few dissections:

try_out x y = ?a1
a1 : plus (plus x 0) y = plus y x

try_out x y = rewrite addition_unit x in ?a2
a2 : plus x y = plus y x

Idris has this feature called "Elaborator reflection". It allows you
to describe automated tactics for writing proofs/programs.
The "getGoal" and "getEnv" allow you to examine types in the context:

getGoal : Elab (TTName, TT)
getEnv : Elab (List (TTName, Binder TT))

The elaborator reflection also allows accessing the term rewriting. I
suppose that's all you need in order to write a program that
simplifies equations inside the type context?

-- Henri Tuhola

On Sat, 21 Sep 2019 at 11:50, Martin Baker <address@hidden> wrote:
>
> 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
> address@hidden
> https://lists.nongnu.org/mailman/listinfo/axiom-developer