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,