search

agda / agda-categories

A new Categories library for Agda
https://agda.github.io/agda-categories
MIT License
363 stars 68 forks source link

Add pointwise tensor and categories of SMCs #304

Closed sstucki closed 3 years ago

sstucki commented 3 years ago

Type checking these two modules takes suspiciously long. I'm not sure what the reason is, but I suspect it is somehow related to monoidal natural transformations. I often have to expand their definitions for Agda to typecheck them at all (see comments in the code). No idea why that is, though.

Sorry for squeezing in a typo-fix as well, @JacquesCarette. But it seemed a bit silly to open a separate PR for that.

sstucki commented 3 years ago

Looks like the CI ran out of memory. 😞

I noticed we don't use --auto-inline in the Makefile (or the CI script). Apparently this was a default option prior to 2.6.2 and can help speed up type checking. Maybe it helps with heap usage too?

See https://github.com/agda/agda/blob/v2.6.2/CHANGELOG.md#pragmas-and-options

sstucki commented 3 years ago

WIP: added --auto-inline to the CI script via 46b79f8. If it passes, I'll submit the update as a separate PR.

sstucki commented 3 years ago

WIP: added --auto-inline to the CI script via 46b79f8...

Didn't help. Not sure what the next step should be. Bump the memory limits?

JacquesCarette commented 3 years ago

Hmm, it looks like the external limit is 6G but the one on CI is 3.5G. So that certainly can be changed.

Also: don't put equational proofs inline to a complex record. Agda seems to really not be happy with that.

Have you tried 'interactive highlighting' to see where things slow down? [That hasn't actually worked for me, but it's something NAD uses successfully.] I've got this hunch that typechecking isn't the problem, it's positivity and/or termination. Because the highlighting of some files is fast, but then there's a huge pause between the time that's done and it is marked as 'checked'. But this guess could be quite wrong. There various -v:profile options that might be worth trying.

sstucki commented 3 years ago

Hmm, it looks like the external limit is 6G but the one on CI is 3.5G. So that certainly can be changed.

OK, I'll give it a try and see if the CI finishes with more memory. If it does, I'll open a separate PR with the updated limits.

Also: don't put equational proofs inline to a complex record. Agda seems to really not be happy with that.

OK, I'll try to avoid that in the future then and update the PR accordingly. Though I'm a bit scared of the type signatures some of the separate definitions will require for concrete instances.

Do you have an explanation for why inline definitions degrade performance?

Have you tried 'interactive highlighting' to see where things slow down? [That hasn't actually worked for me, but it's something NAD uses successfully.]

I haven't, but it's worth a try, thanks for the suggestion. I noticed that the type checker spends quite some time already in the preamble (imports, private shortcuts, etc.) of the modules. So I'm curious what's going on there.

JacquesCarette commented 3 years ago

The heap size increase seems to have done the job. I'll review the details soon.

sstucki commented 3 years ago

Great, I filed a separate PR for the config changes as promised: #305

Also: don't put equational proofs inline to a complex record. Agda seems to really not be happy with that.

Follow up question: does it matter if the "un-inlined" definitions are in a where block beneath the record instance definition? That way, at least I don't have to duplicate all the parameters in the type signature? Or do I need to move them into separate definitions at the top level?

JacquesCarette commented 3 years ago

I think where blocks are fine. As to why not inline equational proofs, there was a discussion on the Zulip about that, and I think @laMudri was the one who had some interesting examples that showed the big difference.

sstucki commented 3 years ago

I think where blocks are fine. As to why not inline equational proofs, there was a discussion on the Zulip about that, and I think @laMudri was the one who had some interesting examples that showed the big difference.

OK, I'll continue refactoring into where blocks then. If either of you remember the name of the Zulip stream (or what exactly was discussed) that'd be great. I tried searching quickly but couldn't find anything.

sstucki commented 3 years ago

Quick update: I've started refactoring some of the definitions to move equational proofs out of record definitions. The result is not particularly pretty. As I suspected, it adds quite a bit of noise. Compare e.g. the definition of ⊗̇-unitorʳ (not refactored) to that of ⊗̇-braiding (refactored), or just look at the diff of the last commit (a40ab17). Any suggestions on how to improve this?

Done for today, will continue with the refactoring tomorrow.

laMudri commented 3 years ago

I don't think I'm involved, but I remember this from Very long checking times for equational proofs.

sstucki commented 3 years ago

Thanks for the pointer @laMudri!

I'm constantly putting proof terms directly into records, and I had no idea it's problematic. I suspect that, since everything's a record in agda-categories, there are tons of dependent types with record-valued indices that are constantly being normalized to WHNF for comparison. That probably impacts downstream performance everywhere.

We should probably put that link and/or the discussion in the README.md. We still don't have a contributor's guide, do we?

JacquesCarette commented 3 years ago

Oops, I misremembered who was involved... but it worked anyways, so I guess I don't feel too bad? Anyways, thanks!

We don't have a contributor's guide, no. And that really belongs in it, rather than directly in the README.md.

And yeah, there's probably a cascading effect going on here, where the basic records with proof terms are constantly being normalized, and this accumulates.

JacquesCarette commented 3 years ago

So is this ready to go, or are you still intending to do more refactorings?

Yes, this does make things lengthier, which is a shame. On the other hand, I don't know what kind of "bug report" to make on Agda that might cause things to be repaired so that user code doesn't have to bear this burden.

sstucki commented 3 years ago

There might be a compromise: it might help to just name/define the terms in where blocks without declaring their types (which is where most of the overhead comes from). Worth a try, I think. I'll push the update and clean up the PR when it's done.

sstucki commented 3 years ago

OK, I refactored the module as suggested, adding explicit definitions for many of the equational proofs. The style is a bit inconsistent (sometimes there are type signatures, sometimes there are not) essentially because I tried to minimize the "noise" off full signatures. For laws with implicit parameters, the signature can be avoided if the parameters are strategically (and explicitly) applied but I only did so if it didn't reduce the readability of the proof.

As far as I can tell, the changes did not affect compile times, but maybe it has good downstream effects, who knows.

From my side, this is ready to be merged now.

JacquesCarette commented 3 years ago

Out of curiosity, did the typechecking time go down between the initial PR and now?

sstucki commented 3 years ago

Out of curiosity, did the typechecking time go down between the initial PR and now?

I didn't notice any change. But I did not do any systematic measurements either. And if the problem with inline proofs is indeed linked to eta-expansion during equality checking, we probably wouldn't see it in the type checking times for this module, but rather in modules using the these definitions. 🤷