Axiom allows the user to dynamically create dependent types.
For example, matrix(3,3) is a 3x3 matrix. This may
seem trivial but it is not.
Consider that to construct the "domain" (as it is called
in Axiom) of 3x3 matrices you need to evaluate the
arguments. Again, in this case it is trivial but, in general,
it is not. Among other things it defines what functions
are available to manipulate 3x3 matrices, e.g. inverse.
Several issues arise. One is the "representation" (aka
"carriers" in logic-speak). There is no reason to assume
that the entries are integers. In the new Axiom (aka SANE)
the "representation" is orthogonal to the domain and can
be specified at construction.
Axiom allows matrices that contain anything. When
constructing a new matrix, e.g. [[2.3,...],[4.4,...]..] the
entries may be from other "domains", in this case the
floats. But they could just as well be polynomials. So
from matrix(3,3) you need to dynamically construct
matrix(3,3,FLOAT).
Another issue is inheriting theorems and definitions that
support the newly constructed domain. In the new Axiom,
the theorems and definitions are associated with the
"category hierarchy". They are inherited based on the
dynamically constructed domain. These are available to
prove functions in the constructed domain.
A matrix(3,3) is commutative but matrix(3,4) is not. The
property of commutativity is inherited from the hierarchy
but only for square matrices. This has to be decided at
the time the domain is constructed.
This allows proofs of functions in the 3x3 domain to use
the commutative theorems of square matrices. These
are not available for functions in the 3x4 domain.
So, clearly, we need to evaluate the arguments when
constructing the domain.
Ah, but evaluating the arguments of a dependent type is
NOT trivial in general. You could, for example, construct
domains which contain themselves in the argument,
such as matrix(matrix(...
More fun exists because one could, for example, introduce
a new "category" into the hierarchy that has additional
definitions and theorems related to square matrices over
some new domain. These have to be dynamically inherited
in particular cases.
Worse yet, the elements don't have to be PROP but
could be anywhere in the type hierarchy. The elements
could be functors, for example.
I've spent a great deal of time pondering these problems.
My current "solution path" involves constructing objects
in CLOS (Common Lisp Object System) which allows me
to achieve very fine-grained control due to the MOP
(Meta Object Protocol). In addition, I'm trying to make the
domains as "declarative" as possible so that most of the
details are not hidden in obscure code.
CLOS allows both dynamic construction and dynamic
re-shaping. I have no idea how LEAN4 will handle these
without the MOP.
Are you aware of any LEAN4 design documents that addresses
these questions?