Type theory has advanced considerably in recent years. It appears
that there is a correspondence between Axiom's world and the formal
theory world.
Axiom has "Categories", which correspond the "Typeclasses".
Axiom had "Domains", which correspond to "Instances".
However, I've adusted the "Typeclasses" and "Instances" ideas
a bit to better match Axiom's construction.
Typeclasses have 3 parts:
carrier -- the representation data structure
signatures -- the functions
propositions -- the logical type requirements
In Axiom we currently only have signatures in Categories.
We put the "carrier" in the Domain as the Rep.
Consider the Axiom Domain NonNegativeInteger. NNI roughly
corresponds to the Type theory "Nat" construction. They differ
in that Axiom uses Lisp Integers whereas Type theory uses
Peano arithmetic (a zero and a successor function) but for
our purposes this does not matter at the moment.
NNI inherits a requirement for an "=" signature from the BasicType
Category. Type theory expects that "=" should satisfy three
propositions,
reflexive: x = x
symmetric: x = y iff y = x
transitive: x = y and y = z implies x = z
But these propositions are "types", per Curry-Howard. That means
that we can state these "types" in BasicType. They are no
different from the signatures we currently use.
reflexive: x:% = x:%
symmetric: x:% = y:% <-> y:% = x:%
transitive: x:% = y:% /\ y:% = z:% -> x:% = z:%
But that implies that when we create an Axiom Domain we need
to do three things:
1) we need to define the "carrier" (Axiom's Rep) which we already do
2) we need to implement the function signature (we already do)
3) we need to provide proofs for each proposition and since the
inherited propositions are type signatures that means we need
to prove each one using operations and elements from the
Domain we are creating.
We currently do not write Category propositions, nor do we yet have
a proof language for the Domain proofs.
can operate in "server mode".
Which means that it might be possible to include the Category level
propositions as comments and the Domain level proofs as comments.
The compiler can pass these comments to the proof server and get
back a verification that the proof is correct. This is a short term
solution which is not "first class".
At present Axiom extracts these during the build and calls the
proof checker (COQ) to show that the proofs are correct. I am
trying to get a "thin thread" all the way through the system in
order to prove propositions about the NNI GCD function.
In the ideal case Axiom implements a trusted kernel in Lisp and
the propositions and proofs are native to the compiler/interpreter.
I'm currently studying the "trusted kernel" source code of various
systems to see what it would take to implement this.
A secondary effort involves coercions and conversions. Type theory
doesn't seem to say a lot about these operations. Fortenbacher
wrote a short paper years ago. Coercions are orthogonal to Types.
We really need a strong theory of coercions, most notably to
formalize their role in the interpreter.
Anyway, that's the current "state of the art" with respect to Axiom.
Tim