[Agda] type checking in real-world algebra

[mechvel at scico.botik.ru]

Dear Agda developers,

I am trying to apply Agda to the verified computation in a  real-world 
algebra.
And have problems with the type checker performance in  Agda 2.6.0.1.

Over-commRing.agda
   implements arithmetic of multivariate polynomials (Pol) with 
coefficients
in an arbitrary CommutativeRing.
Also it implements parsing (Read, read) of a polynomial from String
and from a list of lexemes (Lexeme = String).

ParseTest.agda
   tests parsing for the polynomials over the coefficient domain  ℚ = 
Fraction ℤ
-- rational numbers built by applying a generic fraction constructor 
Fraction.
It uses the module  Over-commRing  parameterized by the instances 
related to ℚ:
ℚ-field, ℚ-Show, ℚ-Read.

ParseTest.agda  is small, and it has
  ...
  Lexemes = List String
  open Pol.Over-commRing ℚ-field ℚ-Show ℚ-Read vars n≢0 ppo  public
                                         using (Pol; 0ₚ; readMonPol)
  debug : Lexemes → Pol
  debug lexs  with readMonPol lexs
  ... | inj₁ (f , _) =  f
  ... | inj₂ _       =  0ₚ   -- zero Pol

For the coefficients of ℚ,
Over-commRing.readMonPol  parses a monic polynomial like this:

"(-2/41)*x*z^2"  -->  "(" ∷ "-2/41" ∷ ")" ∷ "*" ∷ "x" ∷
                       "*" ∷ "z" ∷ "^" ∷ "2" ∷ []
                       -->
                       inj₁ (a * x' * z' ^ 2 , remainingLexemes),

where  a = -2/41  : ℚ,
x' and z' : Pol  are the variables "x" and "z" converted to Pol,
_*_ and _^_  are the operations on Pol.


Over-commRing.agda  and all the needed modules are type-checked earlier,
and I run

   > agda $agdaLibOpt +RTS -M20G -RTS Pol/ParseTest.agda

It reaches all the 20G memory, hangs for 15 minutes,
and I interrupt it.

after changing the implementation to

        =  aux (readMonPol lexs)
   where
   aux : (Pol × Lexemes) ⊎ String → Pol
   aux (inj₁ (f , _)) =  f
   aux (inj₂ _)       =  0ₚ

it type-checks in  27 sec  in 3 Gb memory.


Further, if this  debug of `with'  is moved to the module Over-commRing,
there it becomes for arbitrary coefficients, and this version is
type-checked reasonably fast.

The above `debug' does not involve any complex computation,
but it uses complex type expressions and nested substitution for
module parameters.

I have the two observations on this.

(I) Substituting the instances of generic structures (Group, Ring ...)
     for ℤ, Fraction ℤ, Pol (Fraction ℤ) and trying to type-check there
     a simple function often leads to the performance problem in the
     type check.
(II) In such cases, using `with' aggravates this problem greatly.
      It is better to introduce a function instead.

What people, please, think of this?

Thanks,

------
Sergei