consider disabling eta expansion of records about agda-categories HOT 26 CLOSED

It is worth experimenting with. I would start with (say) NaturalTransformation and see what happens. Including for the typechecking timing of the whole library from scratch.

I don't think we ever make use of eta. The old library did, which is why things like opop just worked, and the Monad laws did not need coherence adjustments. So I think this might just work.

from agda-categories.

OK, I don't understand how the unification works. it breaks so much of the type inference that I don't understand why it fails.

For example, in monoidal category,

  field
    ⊗  : Bifunctor C C C
    unit : Obj

  _⊗- : Obj → Functor C C
  X ⊗- = appˡ {C = C} ⊗ X

  -⊗_ : Obj → Functor C C
  -⊗ X = appʳ ⊗ X

the partial application of bifunctor is defined to be

appˡ : Bifunctor C D E → Category.Obj C → Functor D E
appˡ {C = C} F c = F ∘F constˡ {C = C} c

_⊗- and -⊗_ fail to infer the categories from which the object is received, so -⊗_ in this case have unresolved meta. but ⊗ has clearly specified the category already! I don't understand why type inference of this part has anything to do with eta expansion.

from agda-categories.

and enabling eta expansion for Category would allow the category to be inferred. but why? it makes me feel that the unification is considering Category.Obj C before Bifunctor C D E.

from agda-categories.

Might be a bug. Might even be due to the use of generalized variables? Considering one before the other shouldn't matter, since the system to solve (via unification) should be equivalent, no? Definitely very weird that changing Category of all things is what helps. I think it's probably time to invoke the experts (but I won't @ them quite yet, I'll wait for you to do so).

from agda-categories.

I suspect that C is eta expanded before type checking. agda/agda#3912 shows some trait.

from agda-categories.

simply disabling eta for Functor, NaturalTransformation and NaturalIsomorphism helps nothing.

from agda-categories.

So what I did which seemed to make a big difference is to set
+RTS -N1 -M4G -H4G -A128M -RTS
as my runtime args for agda. The improvement was huge on my 8Gig machine. Reduced total time of
make clean
make
from 221s to 148s.

from agda-categories.

OK I just pushed something deadly.

on my own laptop, this is the stats:

 342,936,097,720 bytes allocated in the heap
  13,092,470,664 bytes copied during GC
   1,384,640,456 bytes maximum residency (10 sample(s))
       4,145,208 bytes maximum slop
            4504 MB total memory in use (0 MB lost due to fragmentation)

                                     Tot time (elapsed)  Avg pause  Max pause
  Gen  0       133 colls,     0 par    9.980s  10.301s     0.0774s    0.4326s
  Gen  1        10 colls,     0 par    4.874s   4.943s     0.4943s    1.1825s

  INIT    time    0.001s  (  0.001s elapsed)
  MUT     time  140.110s  (141.076s elapsed)
  GC      time   14.854s  ( 15.244s elapsed)
  EXIT    time    0.000s  (  0.000s elapsed)
  Total   time  154.966s  (156.321s elapsed)

  %GC     time       9.6%  (9.8% elapsed)

  Alloc rate    2,447,615,009 bytes per MUT second

  Productivity  90.4% of total user, 90.2% of total elapsed

I suppose 4G becomes quite marginal now, we might want to raise it.

On my slower desktop (which the school assigns to me), I just hung it by running Agda.

from agda-categories.

For comparison, following is the stats before my deadly commit:

 222,013,067,608 bytes allocated in the heap
  12,075,064,760 bytes copied during GC
   1,414,313,600 bytes maximum residency (10 sample(s))
       4,258,176 bytes maximum slop
            4446 MB total memory in use (0 MB lost due to fragmentation)

                                     Tot time (elapsed)  Avg pause  Max pause
  Gen  0        93 colls,     0 par    8.789s   9.143s     0.0983s    0.3570s
  Gen  1        10 colls,     0 par    4.794s   4.857s     0.4857s    1.1647s

  INIT    time    0.001s  (  0.001s elapsed)
  MUT     time   91.666s  ( 92.653s elapsed)
  GC      time   13.583s  ( 14.000s elapsed)
  EXIT    time    0.000s  (  0.000s elapsed)
  Total   time  105.251s  (106.655s elapsed)

  %GC     time      12.9%  (13.1% elapsed)

  Alloc rate    2,421,971,667 bytes per MUT second

  Productivity  87.1% of total user, 86.9% of total elapsed

from agda-categories.

Your laptop is faster than mine - a full build takes 231s on mine, with -M5G (which I don't think is make a real difference).

from agda-categories.

this is the deadly commit I was talking about. in particular, I will put all my blame to this line. however, I don't see why it is this slow. I can only say probably it is unfolding something shouldn't be.

natural transformation related again. I find that if something is slow, the chances are it has something to do with bifunctor.

from agda-categories.

Might be due to loss of sharing.

from agda-categories.

I think I want to draw the attention of @nad @UlfNorell @jespercockx and @andreasabel to this issue. Advice on how to make things faster would be welcome - I know that, for example, changing the order of some parameters can be a huge difference [mysteriously so, IMHO, but so be it]. If nothing else, this can be a test case (see the 1 line pointed to above) that helps profile what's going on.

I'm quite willing to run all sorts of experiments, if I am told which ones to run and how.

from agda-categories.

I'm afraid I don't know much about performance debugging aside from the usual advice: use no-eta-equality; make as many things abstract as possible (either with abstract or as module parameters); and increase heap size when necessary.

There is also the --no-syntactic-equality flag which is unlikely to make things faster but should make performance more stable under small changes, so it's useful to turn on while performance debugging.

The problem that @HuStmpHrrr mentions with unsolved metas appearing when enabling no-eta-equality indeed seems like it could be a bug. Would it be possible to narrow it down to a small test case?

from agda-categories.

Also running Agda with -vprofile:7 might give a (very rough) idea of what parts of typechecking Agda is spending a lot of time on.

from agda-categories.

I'll try to do a full compile of the agda-categories library with -vprofile:7 to see if that gives any insight.

On keeping things abstract, I have one question: is (C : Category) as a module parameter somehow "more abstract" that (C : Category) as a function parameter? [I don't think we can actually use abstract itself].

We've already increased heap size a lot, we'd need larger machines if we truly need to go higher. I hope not.

from agda-categories.

is (C : Category) as a module parameter somehow "more abstract" that (C : Category) as a function parameter?

I don't think there is a difference, no.

from agda-categories.

new performance stats as of 12/01/2019:

 765,118,766,384 bytes allocated in the heap
  84,548,887,648 bytes copied during GC
   7,348,867,336 bytes maximum residency (15 sample(s))
      20,741,880 bytes maximum slop
           20790 MB total memory in use (0 MB lost due to fragmentation)

                                     Tot time (elapsed)  Avg pause  Max pause
  Gen  0      3255 colls,     0 par   68.710s  68.936s     0.0212s    0.9734s
  Gen  1        15 colls,     0 par   35.004s  37.986s     2.5324s    7.3661s

  INIT    time    0.002s  (  0.002s elapsed)
  MUT     time  384.630s  (386.260s elapsed)
  GC      time  103.714s  (106.922s elapsed)
  EXIT    time    0.000s  (  0.000s elapsed)
  Total   time  488.346s  (493.185s elapsed)

  %GC     time      21.2%  (21.7% elapsed)

  Alloc rate    1,989,231,231 bytes per MUT second

  Productivity  78.8% of total user, 78.3% of total elapsed

from agda-categories.

Given the discussion at agda/agda#4560 I think that we ought to turn eta-equality back on for various records.

Regarding performance, I've been able to understand certain things a bit better. I'll document that elsewhere, this issue is getting to be a monster.

from agda-categories.

eta-equality is always on. we actually rely on this quite a lot.

from agda-categories.

By the way, no-eta-equality alone might not improve performance a lot, since if the elements you are comparing reduce to something defined with record { .. } or the record constructor the typechecker will still compare the equality of the fields.

To get equality to work more on a by name basis you need to define things with copatterns.

postulate
  A : Set
  a : A

record R : Set where
  no-eta-equality
  constructor con
  field
    f : A
    g : A


test : R
test = record { f = a ; g = a }

works : (P : R → Set) → P test → P (con a a)
works P p = p



test2 : R
test2 .R.f = a
test2 .R.g = a

-- fails : (P : R → Set) → P test2 → P (con a a)
-- fails P p = p

-- test2 != con a a of type R
-- when checking that the expression p has type P (con a a)

from agda-categories.

So copatterns are not desugared into record definitions? 🤯

I always assumed the two ways to define a record were basically equivalent. Now I'm curious how the definition of test2 is represented internally by Agda? Using some special sort of case tree?

from agda-categories.

You haven't read our paper yet?? https://jesper.sikanda.be/files/elaborating-dependent-copattern-matching.pdf

from agda-categories.

Whoops, you caught me there... 😜
I guess it's high time then. Thanks for the pointer!

from agda-categories.

So copatterns are not desugared into record definitions? 🤯

I seem to recall that, in some cases, Agda does the opposite translation.

from agda-categories.

Although there are definitely still efficiency issues, I don't think this issue is a good place to discuss them. Various issues have already been found and fixed (but by no means all), so efficiency needs a fresh look.

from agda-categories.