[Agda] type check cost

Sergei Meshveliani mechvel at botik.ru
Sun Oct 11 20:08:52 CEST 2015


Nils wrote on October 7

> During the last Agda meeting we implemented some optimisations that
> might be useful for you. However, AFAIR they have not been released yet.
> I suggest that you try the development version of Agda.


Thank you. I have tested  Development Agda of October 8, 2015  

on type-checking of a certain DoCon-A-oct8-2015-reduced,
with comparing it to 
                     Agda 2.4.2.4.

1) It takes  1.8  times less space in type checking this example than  
   Agda 2.4.2.4 takes.

2) Its maximal performance 
   (achieved for  space > 13 Gb for Agda-oct8,  > 17 Gb for Agda 2.4.2.4)
   is  2 times higher. 

3) For  -M12G,  it type-checks in 448 sec. on a  3 GHz machine.


The code and README.agda  are in 
     
    http://www.botik.ru/pub/local/Mechveliani/agdaNotes/costRep-oct8-2015.zip

Still, the situation is as follows.

DoCon-A-oct8-2015 is obtained by un-commenting numerous function implementation 
that are `postulated' in DoCon-A-oct8-2015-reduced,
and development Agda still needs more than 16 Gb to type check DoCon-A-oct8-2015
in 30 minutes.
The project is close to being stuck.

Here follow other notes.


Testig the type check performance of Agda
=========================================

Agda-o8-2015 is compared to Agda-2.4.2.4
at the library  DoConA-oct8-2015-reduced.

1. Apply
   > agda $agdaLibOpt +RTS -M<large>G -RTS  Goal.agda

2. Remove  Goal.agdai

3. Apply
   > time  agda $agdaLibOpt +RTS -M..G -RTS  Goal.agda

This gives timing for type-checking  Goal.agda
presuming that all the imported modules are already type-checked.

The option  -M<N>G  corresponds to  N Gb  space given.

This table presents the time table for type-checking  Goal.agda  on a
3 GHz machine, 24 Gb RAM.

            Agda-o8-2015  |  Agda-2.4.2.4
            -------------------------------                                     
space [Gb]  time [sec]    |
-------------------------------------------                                     
18          393           |  1002
16                        |  980
14          383           |  1653
12          448           |
11          488           |
10          626           |
 9         1246           |


The nature of the test
----------------------                                                          
It defines the notion of a  Ring with Unique Factorization
and proves certain simple lemmata about the related objects.
It follows the discourse given in textbooks on algebra, with certain
special provision for algorithms.

It consists of  35  .agda files,
having parametrized modules, types, and functions.
It defines a hierarchy of the notions involved.

But:  it is a contrived and reduced code.
Namely, all lengthy functions (in particular, proofs) are replaced
with `postulate'.
(the last Goal.agda is an exception, but still it is small).

There remain only small functions, for example, like this:

  ++assoc : ∀ {α} {A : Set α} → (xs ys zs : List A) →
                                    (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
  ++assoc []       ys zs = PE.refl
  ++assoc (x ∷ xs) ys zs =
    ≡begin
      (x ∷ (xs ++ ys)) ++ zs    ≡[ PE.refl ]
      x ∷ ((xs ++ ys) ++ zs)    ≡[ PE.cong (_∷_ x) $ ++assoc xs ys zs ]
      x ∷ (xs ++ (ys ++ zs))    ≡[ PE.refl ]
      (x ∷ xs) ++ (ys ++ zs)
    ≡end

So: the test consists mainly of many  record  declarations,
where records are nested: a record contains fields of records of a
lower level, the nesting level is about 20.

There are also parametrized modules that are intensively imported,
with giving recursively different types for parameters.

It is considerably smaller than Standard library, but has (by occasion, not
intended) something that gives much work to the current type checker. 

It does not suggest to compute anything.
But its type check (I guess) implies computations with type expressions
including values expressed as variables.


The current problem of Agda
---------------------------                                                     

The example of  Goal.agda  is only a toy one.
Any real library for symbolic computation is thousands of times larger
and douzens of times more complex.


Possible inefficiency source
----------------------------                                                    

1. Type normalization strategy.

Consider the recent Peter's example with  foldl comb  with the combining
function

   comb a x =  suc (a + x) ∸ a

Lazy computation of
                    foldl comb 0 (replicate n 1)

deals with the values like

   e3 = let a1 = suc (0 + 1) ∸ 0
            a2 = suc (a1 + 1) ∸ a1
            a3 = suc (a2 + 1) ∸ a2
        in
        foldl comb (suc (a3 + 1) ∸ a3) (replicate (n ∸ 3) 1)

Glasgow Haskell is also for lazy computation.
And it computes the `let' part

       ( a2  <-->  λa.(suc (a + 1) ∸ a) a1 )

for  e_i  so that the intermediate size of the current expression for  a
is not large, and the whole cost is linear on  n.

And in Agda, it costs  ~ 2^n.

I do not recall precisely what is  call by need  vs  call by name,
but probably, this is the source of the difference.

And I suspect that  call by need  will be enough to reduce 50 times the
cost in the example of  Goal.agda

(it looks like there is a certain hindrance for this known to the Agda
developers and not known to me).


2. Type comparison.

People say, type checking often involves comparing type expressions for
equality (with normalizing these expressions).

Consider a particular example of the Goal.agda test.
It contains fragments similar to this:

  fooRing : (R : Ring) → Ring.Carrier R → Ring
  fooRing R a =  ...

  module M1 (R : Ring)
    where
    open Ring R using (Carrier ...)

    record Rec1 : Set _ where
                        field  op1 : Op₂ Carrier
                        ...

  module M2 (R : Ring) (a : Ring.Carrier R)
    where
    R1 = fooRing R a

    open M1 R1 using (Rec1) renaming (Carrier to C)

    f : C → C
    f x =  ...


In the body of  M2 and f,  the type expressions are taken from  M1,
with substituting for  Rec1 and Carrier  some expressions produced
by the  fooRing  functor (constructor).

When type-checking items in  M2,  will it involve comparing for equality
these produced large type expressions, with their normalization being
expensive
?
I mean this particular example of  Goal.agda.

If there indeed appear large type expressions, is not this, again, due to
the "call by name" way to compute them, where expressions are copied eagerly
in full?


3. Is this type check cost problem a technical one,
   or it has the cost  >= O(n^2)  which cannot be fixed in principle
   ?

   Has Coq (Gallina)  a similar problem?


Please, look into the code. Can the Agda developers tell what particular 
large expression appear there, and why?

Thanks,

------
Sergei




More information about the Agda mailing list