[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