Judgmental rational addition

[lowasser]

I was mentioning to someone or another the difficulty of taking reciprocals of natural numbers, or doing anything significant with them, and part of the problem is that things may be a little too abstract -- in particular, one-Q +Q one-Q is not judgmentally equal to rational-Z (int-N 2).

Making more things abstract for rational numbers is definitely good for build performance, but this makes constants very hard to work with, e.g. one-half-Q + one-half-Q = one-Q. This is, in particular, why we have double-le-Q the way it is.

This is mostly a reminder to work on this myself.

[fredrik-bakke]

I recently mentioned to Egbert that there are serious performance drawbacks to our current definition of rational numbers, since the fractions have to be reduced between every operation (a discussion I saw happen before over at 1lab). He mentioned he is contributing another definition of the rational numbers in #1211, and there are other definitions to explore too, such as the set-quotient definition. I'm not saying that we should change our definition, I'm just pointing out the performance drawback.

I don't personally see a problem with unabstracting certain definitions such as constants, but I don't work much directly with rationals, so don't have a good sense for which things can safely be non-abstract.

[EgbertRijke]

While it's true that our current rational numbers are slow, I think we have to be careful about how we come to our conclusions about why that is.

Bringing fractions to lowest terms is probably not the issue, I would find that hard to believe, because that can be done very fast with Euclid's algorithm. The problem is more likely not that we're bringing fractions to lowest terms, but that we don't use Euclid's algorithm to do so.

Another thing that I would be more inclined to believe as a cause for slowing down type checking is that we've set up our definitions so that Agda has to check definitional equality too often. This was an issue with the structure identity principle too, which is why it looks like you have to provide unnecessarily many arguments. This is to avoid the type checker to check for judgmental equality when it doesn't have to.

I'm including some performance related changes in #1211, but I haven't gotten to the rational numbers yet. I think I'd rather first finish up #1211

[EgbertRijke]

The data definition of the rational numbers represents rational numbers as Farey fractions. I think this should be fast, but I have no idea how hard it is to show that the rational numbers are a discrete field with this definition.

[fredrik-bakke]

While it's true that our current rational numbers are slow, I think we have to be careful about how we come to our conclusions about why that is.

Bringing fractions to lowest terms is probably not the issue, I would find that hard to believe, because that can be done very fast with Euclid's algorithm. The problem is more likely not that we're bringing fractions to lowest terms, but that we don't use Euclid's algorithm to do so.

Right, apologies, I should have been more clear with assumptions. Agda has an arsenal of performance analysis tools that can help us determine what is slowing down type-checking. That is something to look into to avoid acting on false assumptions.

[EgbertRijke]

It would be very nice to incorporate more performance analysis in our work flow, to see what are the bottle necks in agda-unimath. This page on the readthedocs site gives some tools

https://agda.readthedocs.io/en/latest/tools/performance.html

which we could start using more.

[lowasser]

The problem is more likely not that we're bringing fractions to lowest terms, but that we don't use Euclid's algorithm to do so.

This is correct. I've observed goals reducing down to calls here.

[EgbertRijke]

My PR about ideals in semirings is an attempt towards refactoring the definition of the GCD.

[VojtechStep]

Do you plan on keeping the current version around for expository reasons? The implementation details are documented in section 8.4 in your book.