abstract and opaque in the module declaration

[fredrik-bakke]

@lowasser @malarbol
Were you aware that it is possible to put the abstract and opaque words together with the where keyword in a module declaration? E.g.

module _
  {l : Level} {A : UU l}
  where opaque
  
  unfolding something
  
  is-prop-my-prop : is-prop my-prop
  is-prop-my-prop = ...

or

module _
  {l : Level} {A : UU l}
  where abstract
  
  is-prop-my-prop : is-prop my-prop
  is-prop-my-prop = ...

This is a pattern we don't currently use in the library, but which I believe we should use, especially now that we are taking these keywords more seriously. #1102 #1106 #1457 #1521 #1612

These keywords detract from the actual formalization and are not important to the reader, only the formalizer/implementer: an entry should mean the exact same to the reader whether it is abstract, opaque or transparent. As Martín Escardó more nicely put it recently in a mathstodon toot (which I am struggling to find atm), there's an inherent trade-off to using these keywords: on the one hand it helps the formalizer write and typecheck their code, and on the other hand it adds noise to the code that detracts the reader from the, shall we say, "essence". By using the pattern I propose above we reduce the noise, as the keywords take up less space, and we need less indentation.

I wanted to share this again even though it was discussed and rejected in the past. @VojtechStep

[VojtechStep]

I don't have much else to add to my previous objections. I don't think the keywords are noise, rather when I see an abstract definition I think "okay, that's either proving a Prop (which might not be immediate to see), or there is a good reason to not want it reducing, that's interesting", and similarly with opaque. Drowning the computationally very relevant keyword in a where abstract makes it that much more harder to debug why something doesn't reduce when working on a different part of the codebase. In fact, I think "now that we are taking these keywords more seriously" is an argument against making them less prominent.

The indentation is unfortunate, that is true.

[VojtechStep]

What's the current status of this? I thought we still considered it rejected. GitHub discussions unfortunately don't show which users upvoted a post, only the count; I thought you upvoted my comment in agreement of this style being rejected, but then you started using it in PRs.

[fredrik-bakke]

My current stance is that I'm not convinced either way on this matter. Generally I tend to upvote replies to show appreciation, though I guess this can be confusing. AFAICT I didn't upvote your previous reply, although I do appreciate it.

[fredrik-bakke]

If we force a conclusion to this question then I think the outcome is clear. However, as an opponent to that outcome, I'd like to keep the question open for a while longer...

[fredrik-bakke]

Either way it is very easy to change IMO.