[Agda] notes on type check performance

[Sergei Meshveliani]

On Fri, 2017-05-12 at 21:43 +0300, Sergei Meshveliani wrote:
> [..]
> 
> These are several notes concerning the type check performance.
> [..]

> The following is about the source of the type check cost which has a 
> fundamental origin and is common to Agda and Coq.
> 
> [..]
> [1] François Garillot, Georges Gonthier, Assia Mahboubi, Laurence
> Rideau. Packaging Mathematical Structures. 
> TPHOLs'09. https://hal.inria.fr/inria-00368403v2 
> ----------------------------------------------------------------------
> 
> 
> The paper [1] writes in introduction:
> "
> While this unbundling allows for maximal flexibility, it also induces a
> proliferation of arguments that is rapidly overwhelming. A typical 
> algebraic structure, such as a ring, involves half a dozen constants and
> even more axioms. Moreover such structures are often nested, e.g., for 
> the Cayley-Hamilton theorem one needs to consider the ring of
> polynomials over the ring of matrices over a general commutative ring.
> The size of the terms involved grows as C^n , where C is the number of
> separate components of a structure, and  n  is the structure nesting
> depth. For Cayley-Hamilton we would have  C = 15  and  n = 3,  and thus
> terms large enough to make theorem proving impractical, given that
> algorithms in user-level tactics are more often than not nonlinear.
> "
> 
> 
> I am trying to understand this example, and thus to understand the
> nature of this particular source of the exponent cost grow effect.
> 
> It is about the construction of
> 
>       Pol (SquareMatrix (R : CommutativeRing)),
> 
> [..]


> The paper authors write: 
> "The size of the terms involved grows as C^n".



In my last letter I agree with this estimation.

[1] gives above an example of the depth  n = 3  for the domain instance composition.
When type-checking DoCon-A-0.04.1, there is possible the depth may be
about 5 (for example, parametrized module instances compose). 
Probably this is why it takes so much heap x time.

Further project development has to add many instances, but its
type-checking will hardly require any essential depth growth
(but considering subtle examples may increase it). 

Now, in the above estimation  C^n  there is hidden the copying expense 
estimation  C'^n.
The whole estimation is something like
                                  C^n * C'^n,

where  C'  is the copying coefficient,
C' = (average size of a subterm t) * (average number of copies).

C' depends on the implementation of the type checker.
So that, probably, introducing some sharing representation of a term
will reduce the cost many times.

Regards,

------
Sergei



> II.2. What DoCon-A has with this respect
> ========================================
> 
> * DoCon-0.04.1  has the generic tower from  Semigroup and Monoid up to 
> CommutativeRing, IntegralRing, FactorizationMonoid, FactorizationRing, 
> UniqueFactorizationRing, Field.
> 
> * FactorizationRing  relies on the structure of Multiset and on the 
> instance of  CommutativeMonoid for  (Multiset D)  for D : DecSetoid and
> for the sum operation on multisets.
> Various theorems rely on the instance of  CommutativeMonoid Nonzero 
> for multipication on nonzero elements in any  R : IntegralRing.
> 
> * There are implemented all the above instances for Integer, except
> Field.
> And the (FactorizationRing Integer) instance is implemented via 
> (FactorizationNonoid (Nat \ 0)).
> 
> This concerns _only an ordinary textbook on basic algebra_, a book of
> about, say, 200 pages.
> 
> For this particular textbook, the depth of term for the instances
> involved is bounded. 
> The depth in the above example from [1] is  3.
> 
> (1) A similar depth bound in  DoCon-A-0.04.1  is somewhat about  5.
> 
> (2) Now, DoCon-A-0.04.1 needs  8 Gb memory and 64 minutes to type-check 
> on a 3 GHz machine.
> 
> (3) On the other hand, the corresponding definitions and rigorous 
> constructive proofs take only about 200 pages in a textbook, and a human
> checks these proofs by reading this book. A human will check it,
> probably, in 20 days. But the type checker processes the text millions
> times faster. 
> 
> We see that the checker of (3) takes a small resource on this term of
> size C^5, while that checker of (2) takes a large resource.
> 
> May be, this inefficiency can be improved by introducing the let-in 
> representation of terms.
> 
> The paper [1] describes a certain subtle approach taken in Coq which 
> handles the problem. So far, I do not understand it
> (I need to look further into the paper). 
> And I wonder, why did not they simply apply the let-in representation of
> terms.
> 
> 
> II.3. Comparing to Glasgow Haskell
> ==================================
> 
> DoCon (written in Haskell) has been tested on computing in the domains 
> like
>       Matrix (Pol [x, y] ((Pol t (Fraction Integer)) / (f))),
> 
> which have a greater term size.
> And there are examples in practice that have sense and that have even
> more levels in the domain construct. And we need to assume that the
> depth in this tower of constructs is not bounded - similarly as the data
> item in Agda may have arbitrary many constructor occurrences.
> 
> Glasgow Haskell compiles fast the above constructs of a great depth 
> (with nested classes and instances).
> Though, without dependent type, the problem is, probably, easier.