search

agda / cubical

An experimental library for Cubical Agda
https://agda.github.io/cubical/Cubical.README.html
Other
452 stars 138 forks source link

CommAlgebras as CommRingHoms #1145

Open felixwellen opened 3 months ago

felixwellen commented 3 months ago

This is an experiment to see if algebras work better when they are defined as homomorphisms of rings.

felixwellen commented 2 months ago

I did some random benchmarking (this PR is not really about type checking speed, but I made some changes while I rewrote code). In summary, the two modules in CommAlgebra with comparable content have signficantly lower type checking times now, while there is no significant change for the modules in Ring and CommRing I checked.

* Ring/Quotient
*New*

Deserialization            2,471ms (3,109ms)
Typing                         3ms   (580ms)

*master*

Deserialization            2,449ms (3,086ms)
Typing                         5ms   (535ms)

* CommRing/Localisation/PullbackSquare
*New*

Typing                                       1ms (8,193ms)
Deserialization                          4,001ms (5,061ms)

*master*
Typing                                       1ms (7,534ms)
Deserialization                          3,809ms (4,842ms)

* CommAlgebra/Localisation
*New*

Deserialization                         4,537ms (5,754ms)
Typing                                      4ms (1,357ms)

*master*
Deserialization                         4,721ms (5,998ms)
Typing                                      5ms (3,354ms)

* CommAlgebra/QuotientAlgebra
*New* 
Deserialization            3,431ms (4,312ms)
Typing                         4ms   (656ms)

*master*
Deserialization                         3,610ms (4,553ms)
Typing                                      1ms (2,131ms)