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

[mechvel at scico.botik.ru]

On 2020-03-04 14:22, mechvel at scico.botik.ru wrote:
> 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.
> "


I am sorry.

I need to add the following.
This as about the Agda versions of about  2017.

It may occur that the current Agda version improves something there.
This needs testing, needs more effort in porting the library.
I use the last Agda versions, but on certain smaller projects.

------
Sergei



> 
> 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.