[Agda] [lean-user] Re: [Coq-Club] Why dependent type theory?

[mechvel at scico.botik.ru]

On 2020-03-04 02:04, Jason Gross wrote:
> I'm confused by this.  Are you saying that in Agda typechecking is
> exponential in the number of files?  Or exponential in the number of
> nested abstractions?  Or something else?  Do you have a toy example
> demonstrating this behavior?
> 


No toy example, so far, but I think such can be provided.

I have a real-world example of the DoCon-A library for algebra:

   http://www.botik.ru/pub/local/Mechveliani/docon-A/2.02/

This is a small part of the intended general purpose library for algebra
(for algebra methods, it is very small, but comparing to the Agda 
practice, it is large).

It is written in  install.txt
"for the  -M15G  key  (15 Gb heap) installation takes about 50 minutes 
on a
  3 GHz personal computer.
"

It looks like the type checker has exponential cost in the depth of the 
tree of the
introduced parametric module instances.

There is a hierarchy of "classes" (classical abstract structures):
Magma, (commutative)Semigroup, (Commutative)Monoid, (Commutative)Group, 
... ,
(Commutative)Ring, Field, IntegralDomain, EuclideanDomain, GCDDomain, 
LeftModuleOverARing ...
-- this tree depth may grow up to, may be, about 25.

And there are domain constructors:  integer, vector, fraction, 
polynomial, residueRing ...
And these constructors are provided with instances of some of the above 
abstract structures.
These instances include implementation for their needed operations, with 
proofs.

The type checker deals with a hierarchy of such instances. And it 
performs evaluation
(normalization ...) with very large terms representing these instances.
For example, the Integer domain has may be 20 instances in it, and this 
large term is
substituted many times on other terms, because almost every domain uses 
some features of
the Integer domain. Anyway there appear internally very large terms that 
repeat many
times, and their embracing terms need to normalize.
Further, the domain

   Vector (EuclideanRingResidue f (Polynomial (Fraction Integer)))        
(D)

is supplied with five instances of Magma, five instances of Semigroup,
five instances of CommutativeSemigroup, five instances of Monoid,
five instances of CommutativeMonoid, and also many other instances.
And the class operations in these instances (and their proofs) are 
implemented
each in its individual way.
The number of different instances of the classical operations grows 
exponentially
in the constructor depth for the domains like (D).

I do not expect that in mathematical textbooks appear domain constructs 
as (D)
of the level greater than 10.
But Agda has practical difficulties with the level of about 4.
Because each construct like (D) is further substituted to different 
parametric modules.
Because the method M1 uses one item from (D), so it is implemented in 
the environment of
a parametric program module to which (D) is substituted for a parameter,
the method M2 uses another item from (D), and so on. And large subterms 
get internally copied.

In a mathematical textbook, all these substitutions are mentioned or 
presumed, and are
understood by the reader. So the informal "rigorous" proofs fit, say, 
200 pages
(~ 100 Kb of memory).
But when a type checker tries to understand these constructions, it 
creates many copies of large subterms and spends the cost in normalizing 
them.
And formal proofs take 15 Gb memory to check.

First, this copy eagerness can probably be reduced (probably, this is 
not easy to implement).
Second, something can be needed to arrange in the style of the 
application programs.
There is a paper of Coq about this style, I recall A.Mahboubi is among 
the authors.

So, there is a fundamental restriction -- which hopefully can be handled 
by introducing a certain
programming style (I never looked into this).
And also there is probably something to fix in the type checker in Agda.

Regards,

------
Sergei



>> There is a problem of the type checking cost in Agda, and probably
>> in Coq too.
>> I do not know of whether it is fundamental or technical. And I have
>> not seen an answer to this question, so far. On practice, it looks 
>> like
>> this:
>> Agda can type-check only a small part of the computer algebra
>> library of
>> methods (with full proofs). With implementing it further, with
>> increasing the hierarchy level of parameterized modules, the type
>> check cost seems to grow exponentially in the level.
>> So, after implementing in Agda an average textbook on computer
>> algebra
>> (where is known a constructive proof for each statement), say, of
>> 500 pages, it will not be type-checked in 100 years.
>> 
>> Probably, this is a difficult technical problem that will be
>> practically solved during several years.