> Are you aware of any LEAN4 design documents that addresses these questions?
No. The best reference for Lean's type system is Theorem Proving in Lean; a version has been ported to Lean 4. Jeremy On Fri, Dec 3, 2021 at 12:04 PM Tim Daly <axiom...@gmail.com> wrote: > 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? > >
