Lean4 and dependent type theory

--0000000000009db1e005d240e4d6
Content-Type: text/plain; charset="UTF-8"

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?

--0000000000009db1e005d240e4d6
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr"><div>Axiom allows the user to dynamically create dependent=
 types.</div><div>For example, matrix(3,3) is a 3x3 matrix. This may</div><=
div>seem trivial but it is not.</div><div><br></div><div>Consider that to c=
onstruct the &quot;domain&quot; (as it is called</div><div>in Axiom) of 3x3=
 matrices you need to evaluate the</div><div>arguments. Again, in this case=
 it is trivial but, in general,</div><div>it is not. Among other things it =
defines what functions</div><div>are available to manipulate 3x3 matrices, =
e.g. inverse.<br></div><div><br></div><div>Several issues arise. One is the=
 &quot;representation&quot; (aka</div><div>&quot;carriers&quot; in logic-sp=
eak). There is no reason to assume <br></div><div>that the entries are inte=
gers. In the new Axiom (aka SANE)</div><div>the &quot;representation&quot; =
is orthogonal to the domain and can</div><div>be specified at construction.=
<br></div><div><br></div><div>Axiom allows matrices that contain anything. =
When</div><div>constructing a new matrix, e.g. [[2.3,...],[4.4,...]..] the<=
/div><div>entries may be from other &quot;domains&quot;, in this case the</=
div><div>floats. But they could just as well be polynomials. So</div><div>f=
rom matrix(3,3) you need to dynamically construct</div><div>matrix(3,3,FLOA=
T).<br></div><div><br></div><div>Another issue is inheriting theorems and d=
efinitions that</div><div>support the newly constructed domain. In the new =
Axiom,</div><div>the theorems and definitions are associated with the</div>=
<div>&quot;category hierarchy&quot;. They are inherited based on the <br></=
div><div>dynamically constructed domain. These are available to</div><div>p=
rove functions in the constructed domain.<br></div><div><br></div><div>A ma=
trix(3,3) is commutative but matrix(3,4) is not. The</div><div>property of =
commutativity is inherited from the hierarchy</div><div>but only for square=
 matrices. This has to be decided at</div><div>the time the domain is const=
ructed.<br></div><div><br></div><div>This allows proofs of functions in the=
 3x3 domain to use</div><div>the commutative theorems of square matrices. T=
hese</div><div>are not available for functions in the 3x4 domain.<br></div>=
<div>So, clearly, we need to evaluate the arguments when</div><div>construc=
ting the domain.</div><div><br></div><div>Ah, but evaluating the arguments =
of a dependent type is</div><div>NOT trivial in general. You could, for exa=
mple, construct</div><div>domains which contain themselves in the argument,=
</div><div>such as matrix(matrix(... <br></div><div><br></div><div>More fun=
 exists because one could, for example, introduce</div><div>a new &quot;cat=
egory&quot; into the hierarchy that has additional</div><div>definitions an=
d theorems related to square matrices over</div><div>some new domain. These=
 have to be dynamically inherited</div><div>in particular cases.<br></div><=
div><br></div><div>Worse yet, the elements don&#39;t have to be PROP but <b=
r></div><div>could be anywhere in the type hierarchy. The elements</div><di=
v>could be functors, for example.<br></div><div><br></div><div>I&#39;ve spe=
nt a great deal of time pondering these problems.</div><div><br></div><div>=
My current &quot;solution path&quot; involves constructing objects</div><di=
v>in CLOS (Common Lisp Object System) which allows me</div><div>to achieve =
very fine-grained control due to the MOP</div><div>(Meta Object Protocol). =
In addition, I&#39;m trying to make the</div><div>domains as &quot;declarat=
ive&quot; as possible so that most of the</div><div>details are not hidden =
in obscure code. <br></div><div><br></div><div>CLOS allows both dynamic con=
struction and dynamic <br></div><div>re-shaping. I have no idea how LEAN4 w=
ill handle these <br></div><div>without the MOP.<br></div><div><br></div><d=
iv>Are you aware of any LEAN4 design documents that addresses</div><div>the=
se questions?<br></div><div><br></div></div>

--0000000000009db1e005d240e4d6--