[Agda] type check performance

[Sergei Meshveliani]

On Fri, 2017-01-13 at 19:55 +0100, Robbert Krebbers wrote:
> This may be related: having large chains of coercions is also 
> problematic in Coq, see [1]:
> 
>    There is also a severe efficiency issue: the complexity of Coq's
>    term comparison algorithm is exponential in the length of the
>    coercion chain. While this is clearly a problem specific to the
>    current Coq implementation, it is hard and unlikely to be
>    resolved soon, so it seems prudent to seek a design that does
>    not run into it.
> 
> The paper [1] describes another way of organizing algebraic hierarchies 
> in Coq so that these long chains of coercions can be avoided. It quite 
> crucially relies on Coq's canonical structures mechanism, so I have no 
> clue whether you can practically do something similar in Agda.
> 
> [1] François Garillot, Georges Gonthier, Assia Mahboubi, Laurence 
> Rideau. Packaging Mathematical Structures. TPHOLs'09.
> https://hal.inria.fr/inria-00368403v2
> 

I looked there. It is difficult for me to understand.
It is written in introduction

----------------------------------------------------------------------
"While this unbundling allows for maximal flexibility, it also induces a
prolif-eration 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.

Thus, at the very least, related operations and axioms should be packed
using Coq’s dependent records (Σ-types); we call such records mixins.
..."
--------------------------------------------------------------------

I am implementing a similar hierarchy for similar algorithms for
algebra. 
(But the goal is not any particular difficult theorem, but to express
classical algebraic structures + proofs for simple classical statements
for them, as they are given in simple textbooks). 
 
The authors write about C^n where n is the depth of the structure
nesting depth. They write that for Polynomials over Matrices over a
generic CommutativeRing, this makes it  C = 15,  and  n = 3,  and the
cost of  15^3.

So far I did in Agda only  n = 2 (Polynomial over a generic
CommutativeRing).
But in Haskell, I programmed computations in much more complex domains,
such as
Fraction -- Polynomial -- ResidueRing -- Polynomial -- Matrix ...,   (1)

with each of these domain constructors being supplied with appropriate
_instances_ of various classical categories (classes): Semigroup, Group,
Ring ...
And this is compiled fast in GHC, and it runs fast.
But type expressions in Agda and in Coq type checker are represented
more fully than in the GH compiler.

I doubt: what difficulty will appear with Agda when we program
operations with the data belonging to domains built by n constructors,
like n = 5 in the example of (1).

But we already have another, more close problem: 
representing nested generic structures having depth 15 -- 20. 
Thus DoCon-0.04.1 defines

            DSet          (DecSetoid + possible listing)
            |
        *<- Magma         (a DSet with a congruent binary operation _∙_)
        |   |
    -<- | - Semigroup  --> CommutativeSemigroup
    |   |   |
    |   |   Monoid     --> CommutativeMonoid
    |   |   |              |
    |   |   |              CCMonoid              (with cancellation)
    |   |   |              |
    |   |   Group          FactorizationMonoid   
    |   |   |
    |   |   CommutativeGroup
    |   |   |
    |    -> Ringoid
    |       |
    *-----> Ring
            |
            RingWithOne
            |
            CommutativeRing
            |
            IntegralRing         
            |       \    \
            |        \     ----- EuclideanRing
            |         \
            |           -------  GCDRing          (with gcd)
            |
            FactorizationRing  
            |
            Field              


If I skip lemma proofs there, and various instance implementation
(so that there remain only vocabularies, signatures), then this will
take, may be, 1 Gb to type-check (which looks large). 
Then, adding simple instance implementation and proofs relating to this
hierarchy makes type checking more eager, a minimum of 7 Gb needed.
 
What precisely is here the mechanism for the internal type expression
explosion -- I do not know.
Probably, we need a tool for measuring intermediate type expression
sizes in the type checker.
(?)

Regards,

------
Sergei




Another question 










> > Regards,
> >
> > ------
> > Sergei
> >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> >
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda