Refactor library to use λ where

[fredrik-bakke]

Also adds a new rule removing blank lines right before where keywords.

[fredrik-bakke]

I also remembered that we don't actually have a script focused on best practices for agda code, and I won't bother making one now just for this convention.

[fredrik-bakke]

This one's ready now. At some point in the future, when there are fewer pull requests in the pipeline, I'd like to go through the repository to change most instances of pair with _,_ using replace patterns like

• (?<!-)pair (?!of)([^`()\s]+)( |$) -> $1 ,$2

[EgbertRijke]

This one's ready now. At some point in the future, when there are fewer pull requests in the pipeline, I'd like to go through the repository to change most instances of pair with _,_ using replace patterns like

• (?<!-)pair (?!of)([^`()\s]+)( |$) -> $1 ,$2

Aren't there some instances where pair is nicer than _,_?

[fredrik-bakke]

I agree, when both arguments span multiple lines*, I think pair is nicer than _,_. But I thought I saw you recently say that we always preferred the latter? Either way, the pattern I presented only matches instances where pair and its first argument are on the same line. In this case I think _,_ will generally be nicer. I don't feel too strongly about cases where we have

 x , 
 y
   z
   w

So if you want, I can restrict to only replacing instances where both arguments of pair appear on the same line.

[EgbertRijke]

I feel like we should still include some guidelines about what options we have to type-set lambdas. Eg we could mention that we always wrap the lambda-expression in parentheses, even if it is the last argument of a function and therefore not strictly required. Then we could mention that there are several lambda-styles available:

1. regular lambda
2. pattern-matching lambda without { } as in lambda (x , y) -> ...
3. pattern-matching lambda with { }
4. lambda-where

and we could mention that whenever lambdas 2-4 appear in an entry we mark it as abstract. We could also mention that while these fancy lambdas are permitted in our code, in many common situations it might be preferable to factor out that lambda-expression into a separate definition. And then we could also say that the formatting guidelines for these lambdas are not quite cleared up yet, just to be upfront.

[EgbertRijke]

@VojtechStep also mentioned some lambda-styles that we don't use in our library. I already forgot about them, but we could include those too in our style guide and say that we don't use them.

[VojtechStep]

2. pattern-matching lambda without { } as in lambda (x , y) -> ...

I don't think this is technically a pattern-matching lambda - it's only allowed for record types with eta equality (which, to be fair, covers many of our use cases, except path induction).

[EgbertRijke]

The conventions you use for lambda-where look very reasonable. They may not exactly fit uniformly in our indentation conventions, but I think we can stick with them if we explain it in the guidelines.

[fredrik-bakke]

Am I correct that @VojtechStep intended to update the guidelines regarding pattern-matching lambdas, or did you want me to do it here?

[EgbertRijke]

I don't know if Vojtech was planning to do that, but since this PR introduces lambda-where globally to the library, the natural PR to include some formatting guidelines seems to be this one.

[fredrik-bakke]

Okay, that makes sense. And then I guess he will write the guidelines for the other proposed instance where he wanted to use pattern-matching lambdas.

[fredrik-bakke]

I changed the title back because I don't think it should cause trouble. If it does, then we need to address that another way in any case I think.

[EgbertRijke]

Man, type-checking the whole library is getting quite slow

Strange! Do you know why it is getting slow?

[fredrik-bakke]

IDK, my guess is a large code base. Maybe it would be a good idea to keep a log of type-checking time for the whole library after each PR to keep a watch on it

[EgbertRijke]

IDK, my guess is a large code base. Maybe it would be a good idea to keep a log of type-checking time for the whole library after each PR to keep a watch on it

Do you mean that it is generally taking a long time to compile the library, or that something in this PR happened that makes it take longer to compile?

[fredrik-bakke]

Hard for me to say if it's gotten slower with this PR. It may just be that I'm type-checking a lot while working on this PR, hence noticing the slow

[fredrik-bakke]

Let me know what you think of the new convention

[EgbertRijke]

Let me know what you think of the new convention

Beautiful!