[Agda] type check cost

[Sergei Meshveliani]

I wrote

> Now, each step in developing the library will probably increase the 
> memory requirement on somewhat 1/4.
>
> On the other hand, DoCon-A-2.00 supports only about 1/100 of the 
> methods in the DoCon library written in Haskell in 1990-ies
> (but it contains many definitions and proofs which are not in DoCon).
> [..]
> I expect that anyone who tries to implement any essential generic 
> mathematical library in Agda will be stopped by this barrier.


As it is written in a certain paper cited in this list, Coq has a
similar problem. I had a look into this paper, and confirm the following
fundamental estimation.
If abstract domain definitions in some application library have  N
abstract operations, then the number of different _instances_ of this
operations has the order of  N^d  
(for the worst case), where  d  is the depth of the domain construction
used in this application.  

On the other hand:
(1) very large mathematical algorithm libraries are accompanied by books
and papers that contain proofs, formal/complete or not so
formal/complete. And these proofs are somewhat read and verified by
human, in a real time.

(2) The above paper writes that Coq handles the problem by a certain
specific technology 
(so far I do not understand -- how, may be I would need to read and to
try once more). 

I explain this effect so that the cost is   a * (N^(b*d)),  and in the
areas (1) and (2) there are discovered approaches that reduce the
constants a and b. 

And I suspect, that Agda implementation can reach this in a simpler way,
by bringing some sharing to the internal type term representation.

Regards,

------
Sergei