Naming convention and coding style
Closed this issue · 21 comments
Here are some potentially relevant naming conventions in other proof assistant libraries:
- For Agda's stdlib: https://github.com/agda/agda-stdlib/blob/master/notes/style-guide.md
- For Coq-HoTT library: https://github.com/HoTT/Coq-HoTT/blob/master/STYLE.md#1-conventions-and-style-guide
- A more general style guide for Coq: https://vstyle.readthedocs.io/en/latest/
- Mathlib naming conventions for Lean 3: https://leanprover-community.github.io/contribute/naming.html#general-conventions
We have also had some discussion in #9, which I will replicate here:
I think we have briefly considered several code styles and were leaning towards Coq-HoTT code style.
However, we did not yet take any steps towards formatting and renaming existing code.
Perhaps, we should do that in a separate PR, applying to the entire codebase.Originally posted by @fizruk in #9 (comment)
I should say, I'm clearly partial to
agda-unimath, but I do believe its style conventions would benefit this project. Particularly since some of the code used in this project is derived from it. And also, for instance, I don't see why it should be necessary to write comments in the code at all, as you're using a literate format.Originally posted by @fredrik-bakke in #9 (comment)
Hey! Sorry to be so slow to weigh in. I've been crisscrossing the UK on trains with terrible wifi.
Regarding the naming/commenting conventions, I agree it's time to make clearer style conventions. Fredrik could you say a bit more about what you prefer about agda-unimath to Coq-HoTT? I'm open to being persuaded.
Regarding the commenting, I agree that the comments we've been using on arguments, eg the annotations on the variables p and q below, aren't so useful.
-- path composition by induction on the second path #def concat (p : x = y) -- A path from x to y in A. (q : y = z) -- A path from y to z in A. : (x = z) := idJ(A, y, \z' q' -> (x = z'), p, z, q) -- an alternative construction of path composition by induction on the first path -- this is useful in situations where it's easier to induct on the first path #def altconcat (p : x = y) -- A path from x to y in A. : (y = z) -> (x = z) := idJ(A, x, \y' p' -> (y' = z) -> (x = z), \q' -> q', y, p)But I do like the comments before the definitions that explain the main idea. Did you object to those as well?
Originally posted by @emilyriehl in #9 (comment)
My 2 cents regarding code comments:
-
Argument comments may be used by IDE to (better) explain what is expected in some hole. They are also useful for beginners who need periodic reminders even for simple arguments like
(p : x = y). I agree though that some descriptions are straightforward and, perhaps, can be automatically generated or revealed on demand. -
I think code comment/annotation preceding the definition is supposed to be like a figure/listing caption in a paper. This is in contrast to a detailed description or a reference in the main text. So I am in favour of keeping both.
I'll paste this here in the meantime:
Thanks! I'll try and make a case tomorrow. Perhaps the main points I'd like to get across is that I think your comments should just be written out in prose outside of the coding environment instead. The other use case for comments, i.e. as annotations, should be very small with a good enough naming and style convention and is also something one generally wants little of in other comparable media like on wikis and in articles. In my experience, contributing to agda-unimath, I've never once found a need to comment on my code inside of the coding environment.
Alright, so I was asked to compare agda-unimath's conventions to Coq-HoTT by @emilyriehl. I'll do that here. This comment primarily touches on the style guidelines with regard to the actual code, I'll try and elaborate a bit more on other things in a second comment.
Maybe the first point I should make against using conventions from the Coq (or Lean) language is the following. Term constructions in Coq look very different than in Rzk, which is much closer to Agda in this regard. Here the very strict Lisp-like convention of agda-unimath can help you out making the code more readable and maintainable. Just compare the before and after formatting of the following:
Before:
-- In a Segal type, initial objects are isomorphic.
#def initial-iso
(A : U)
(AisSegal : isSegal A)
(a b : A)
(ainitial : isInitial A a)
(binitial : isInitial A b)
: Iso A AisSegal a b
:= (first (ainitial b),
((first (binitial a),
contractible-connecting-htpy (hom A a a) (ainitial a) (Segal-comp A AisSegal a b a (first (ainitial b)) (first (binitial a))) (id-arr A a))
,
(first (binitial a),
contractible-connecting-htpy (hom A b b) (binitial b) (Segal-comp A AisSegal b a b (first (binitial a)) (first (ainitial b))) (id-arr A b))
))
After (Lisp-like):
#def initial-iso
(A : U)
(AisSegal : isSegal A)
(a b : A)
(ainitial : isInitial A a)
(binitial : isInitial A b)
: Iso A AisSegal a b
:=
( ( first (ainitial b)) ,
( ( ( first (binitial a)) ,
( contractible-connecting-htpy
( hom A a a)
( ainitial a)
( Segal-comp A AisSegal a b a
( first (ainitial b))
( first (binitial a)))
( id-arr A a))) ,
( ( first (binitial a)) ,
( contractible-connecting-htpy
( hom A b b)
( binitial b)
( Segal-comp A AisSegal b a b
( first (binitial a))
( first (ainitial b)))
( id-arr A b)))))
As you can see, the structure of the second proof is quite easy to discern. Moreover, by habitually following this style, you may find that writing proofs becomes easier, as you get less bogged down in details surrounding parenthization and comma placements.
This was perhaps the primary point I would like to make. Note that if you were to actually follow agda-unimath's style to the dot, I would write:
#def iso-is-initial-is-segal
( A : U)
( is-segal-A : is-segal A)
( a b : A)
( is-initial-a : is-initial A a)
( is-initial-b : is-initial A b)
: iso A is-segal-A a b
:=
( ( first (is-initial-a b)) ,
( ( ( first (is-initial-b a)) ,
( eq-is-contr
( hom A a a)
( is-initial-a a)
( comp-is-segal A is-segal-A a b a
( first (is-initial-a b))
( first (is-initial-b a)))
( id-arr A a))) ,
( ( first (is-initial-b a)) ,
( eq-is-contr
( hom A b b)
( is-initial-b b)
( comp-is-segal A is-segal-A b a b
( first (is-initial-b a))
( first (is-initial-a b)))
( id-arr A b)))))
There are multiple things to point out here. First, our naming scheme is such that it should be possible to guess the name of a theorem from its type. This is particularly important when the project scales in size. The convention goes something as follows:
We start with the initial assumption, then working our way to the conclusion, prepending every central assumption to the name, and finally the conclusion. So the name iso-is-initial-is-segal should read like we get an iso of something which is initial given that something is segal. The true reading should then be obvious. This convention has the advantage that names always start with the conclusion, which is the most defining property of that construction. You may already see the benefit of this in the above code. For instance, you can quickly see by glancing over the proof that it involves two equality proofs (eq-is-contr) and two instances of composites (comp-is-segal).
Moreover, I may note that we use the is- prefix for the proposition that something is something, and then omit the prefix when talking of the sigma type of all such things. E.g. the Sigma type of initial objects in A would be initial A. Another thing you may have noticed is that we avoid using capital letters in most textual names. E.g. is-segal as opposed to is-Segal. The reason for this is a little involved. We usually use capitalized words for the name of a subuniverse. So the type of Segal types would be named Segal. Now, when a construction is internal to a subuniverse, we usually append the name of the subuniverse. For instance, the fact that the functor type between Segal types is Segal could be recorded as fun-Segal with type (A B : Segal) : Segal in Rzk. This is in contrast to the related construction is-segal-fun-is-segal, which perhaps you can guess what would be. Now, since we would append Segal to the name here, it might not be obvious when glancing over a name like iso-is-initial-is-Segal whether it would be defined in terms of a term of Segal, or a type A and then a term of is-Segal.
Regardless of your conviction about the use of capitalized words, we think it is best practice to include a separator like - between words. This avoids issues with 1-letter words and acronyms, which read awkwardly without the added separators.
EDIT: I may add that the naming scheme perhaps takes a little bit of time to get used to since things are ordered in the opposite way you may be used to, but once you do, naming things and navigating the code base should become easier.
Also, another place we use capitalized names is when defining a term which is itself the type of a statement. For instance, extension extensionality would be named Extext (ExtExt could also be considered), and then the corresponding proof would be extext. Another benefit of this naming scheme is that we avoid the need for fully capitalized names like EXTEXT. Depending on your preferences, fully capitalized words may be something you want, however. After all, Rzk already has fully capitalized names for some built-in sorts.
As a direct response to your question yesterday, I would much rather format it as follows than having comments in the code:
We define path composition by induction on the second path as follows.
#def concat (p : x = y) (q : y = z) : (x = z) := idJ(A, y, \z' q' -> (x = z'), p, z, q)There is also an alternative construction of path composition by induction on the first path. This is useful in situations where it's easier to induct on the first path:
#def altconcat (p : x = y) : (y = z) -> (x = z) := idJ(A, x, \y' p' -> (y' = z) -> (x = z), \q' -> q', y, p)
Perhaps with a full stop rather than a colon in the second paragraph.
I have looked at the Library coding style for agda-unimath. Indeed, I like what I see there a lot. I would probably adjust a few minor things for Rzk, but generally, it looks great and I agree that a good coding style for Agda fits Rzk more than a coding style for Coq.
Also I do not quite understand yet, how to properly rename some definitions, e.g. those in https://emilyriehl.github.io/yoneda/simplicial-hott/05-segal-types.rzk/
Perhaps, there needs to be an extra convention for referring to the use of shapes in the type of a definition.
@fredrik-bakke can you say how much of these, if any, are enforced by IDE tools/extensions?
Oh excuse me, I should have provided a link as well. 😅 I'm glad you like it though! And yeah I expect some things will need to be adjusted. For instance, I quite like your choice of starting the final line in a type signature with : as opposed to ending the previous line with it, which would be the way to do it in agda-unimath.
To answer your question, the naming conventions themselves are only enforced by humans. Some of the formatting is done automatically, though not much with regard to the Lisp-like convention.
Let me see if I can suggest some names for 05-segal-types for you:
hom->homhom2->hom2isSegal->is-segal(and then I would also define the Sigma typeSegaland make additional definitions later where appropriate)Segal-comp->hom-comp-is-segal(andhom-comp-Segal)(I realized on second inspection this should probably be the name to accommodate the next constructions, and becausecomp-is-segalreads more naturally as the full composition term)Segal-comp-witness->is-comp-hom-comp-is-segal(andis-comp-hom-comp-Segal)Segal-comp-uniqueness->unique-hom-comp-is-segal(is-contr-comp-is-segalwould just be the Segal condition itself)horn->hom-hornperhaps?horn-restriction->horn-restriction(orprecomp-horn-inclusion)isSegal'->is-segal'(you could also consider naming it the more descriptiveis-local-horn-inclusion)compositions-are-horn-fillings->equiv-horn-filling-comp(osition)(I prefer the nameequivfor the type of equivalences.Eqis too easy to confuse with equality.)restriction-equiv->equiv-tot-horn-filling-2-simplex(not entirely convinced by this one)Segal-restriction-equiv->equiv-horn-restriction-is-segalSegal-function-types->is-segal-function-type-is-segal(andfunction-type-Segal, the latter would presumably assume that the domain is Segal as well)Segal-extension-types->is-segal-extension-type-is-segal(andextension-type-Segal)
I agree that some of these names are a bit awkward. Especially the one involving the 2-simplex. Feel free to suggest other names as well. :) And I don't think it is necessary to follow the naming convention for absolutely every single definition.
Thanks for this discussion. It seems we're converging on a convention, which is mostly agda-unimath-like with some exceptions (like the placement of the colon on the same line of the type the term we are defining belongs to).
I have a few remaining questions:
(i) Regarding @fredrik-bakke's reference to move most in text comments outside the code blocks, is this compatible with sections? See for example the comments in the code in the section "Coherence data from an invertible map" of "Equivalences". I'm still in agreement with @fizruk that it can be useful to include some comments in sections.
(ii) Where should literature references be placed? Not in section titles, certainly, but on this point I'm open to either having them inside or outside the code blocks.
(iii) Is there any way to make names any shorter? Eg could you elaborate on your preference for "hom-comp-is-segal" over "comp-is-segal"? I'd be in favor, generally, of deviating from the conventions slightly for names we use over and over again.
(iv) The terms I found the hardest to names were auxiliary paths/equalities or equivalences constructed in a long proof. I realize in other libraries these might not be given as separate definitions at all, but in rzk it's harder to know where you are in the midst of writing a proof, so if I'm ultimately going to need to compose 12 paths, I'd rather just define the 12 paths first. For an example of this, see the proof that in the sectino "Half adjoint equivalences are contractible" in "Fibers". What should these terms have been called?
Let me try to answer your questions.
(i) To my limited understanding, what happens when a literate file is typechecked is that the markdown code is discarded, so it will be treated like it is not even there. This means that a section will remain open until it is explicitly closed in the code, even if that is in a later code block. Thus, you can exit a code block to insert prose even without terminating your current rzk section.
When it comes to the idea that comments should be unnecessary, I don't feel like I've given you the entire story, so maybe another example could be enlightening. For instance, the following is your current section defining invertible maps:
## Invertible maps
```rzk
-- the following type of more coherent equivalences is not a proposition
#def hasInverse
(A B : U)
(f : A -> B)
: U
:= ∑ (g : B -> A), -- A two-sided inverse
(prod
(homotopy A A (composition A B A g f)(identity A)) -- The retracting homotopy
(homotopy B B (composition B A B f g)(identity B))) -- The section homotopy
```The first comment here, I think is easy to pull out of the code block, and it would perhaps not be so controversial to do so. However, the other comments in this code carry extra information that I assume you want to keep. My view, however, is that this should not just be information carried by comments, but information carried by the code. I probably don't want to have to remember which projection to use for the retracting homotopy and which to use for the section homotopy. Instead, I would want to write:
## Invertible maps
An **invertible map** is a map `f : A → B` equipped with the _structure_ of a
two-sided inverse, i.e. a map `g : B → A` that is both a retraction and a
section of `f`. Such a structure is not in general a proposition.
```rzk
#def is-invertible
(A B : U)
(f : A -> B)
: U
:=
Σ ( g : B -> A) ,
( prod
( homotopy A A (composition A B A g f) (identity A))
( homotopy B B (composition B A B f g) (identity B)))
```
### Invertibility data
```rzk
#def map-inv-is-invertible
(A B : U)
(f : A -> B)
(is-invertible-f : is-invertible A B f)
: B -> A
:= first is-invertible-f
#def is-section-is-invertible
(A B : U)
(f : A -> B)
(is-invertible-f : is-invertible A B f)
: homotopy A A
( composition A B A (map-inv-is-invertible A B f is-invertible-f) f)
( identity A)
:= first (second is-invertible-f)
#def is-retraction-is-invertible
(A B : U)
(f : A -> B)
(is-invertible-f : is-invertible A B f)
: homotopy B B
( composition B A B f (map-inv-is-invertible A B f is-invertible-f))
( identity B)
:= second (second is-invertible-f)
```This way, I can refer to the retracting homotopy by name, instead of by position.
(ii) I'm not so sure about this. To be honest, I would be fine with having these as code comments, but it would probably look better as part of the markdown. How they would look best, however, I don't know.
Thanks for this illustrative example. I like this style in general but I've found the auxiliary functions a bit less practical to use without implicit arguments. It's much shorter to write "first second is-invertible-f" then to write is-section-is-invertible A B f is-invertible-f" but of course the latter is more readable which is the more important thing.
(iii) I agree that the code can become somewhat verbose, but I am not convinced that should be a large concern. To quote Egbert:
Our naming conventions are not to ensure the shortest possible names, and neither to ensure the least amount of typing by the implementers of the library, but to display as accurately as possible what concepts are applied, and hence improve the readability.
Of course, constructions known best by special names should usually be given those names, and if you want more terse names, I don't have very much against that.
The reason that I changed preference to hom-comp-is-segal is because, to me, comp-is-segal reads more naturally as giving a term of type
Σ (h : hom A x z) , (hom2 A x y z f g h)
i.e. a "composition term", as opposed to the hom of this term, i.e. the first projection. This, moreover, makes the formulation is-comp-hom-comp-is-segal make sense in terms of actual definitions, where is-comp is taken to mean a term of type hom2 (as a predicate on triangles of arrows).
Another comparable example would be the triple Segal, type-Segal, and is-segal-type-Segal. This is a pattern we see all the time over at agda-unimath, e.g. here. So keeping this convention rigid helps keep the code base navigatable. But again, I am not particularly against breaking this pattern for Segal composites.
Thanks for this illustrative example. I like this style in general but I've found the auxiliary functions a bit less practical to use without implicit arguments. It's much shorter to write "first second is-invertible-f" then to write is-section-is-invertible A B f is-invertible-f" but of course the latter is more readable which is the more important thing.
This is an unfortunate consequence of not having implicit arguments. However, making the definitions for is-retraction-is-invertible and is-section-is-invertible does not lock you out of using first and second if you prefer.
EDIT: In agda-unimath, the convention would be to prefer is-retraction-is-invertible and is-section-is-invertible, but I don't think that is reasonable in rzk given the lack of implicit arguments.
(iv) For technical lemmas like this, where the chance they will be reused is low, I don't think the particular names matter that much. Again, you may find the original naming scheme I outlined somewhat useful. Otherwise, you might as well resort to numbering them I think. I'm astonished that you need to concatenate twelve paths though. If it helps, agda-unimath has a proof of this fact here, although I assume you have already looked at this.
Thanks for this illustrative example. I like this style in general but I've found the auxiliary functions a bit less practical to use without implicit arguments. It's much shorter to write "first second is-invertible-f" then to write is-section-is-invertible A B f is-invertible-f" but of course the latter is more readable which is the more important thing.
This is an unfortunate consequence of not having implicit arguments.
Please, correct me if I'm wrong, but it seems that let-expressions (rzk-lang/rzk#23) or (perhaps better) where-blocks should help with auxiliary definitions more than implicit arguments. They should also be much easier to add to the language. That said, I do plan to add implicit arguments in Rzk.
Both implicit arguments and let-expressions and where-blocks would help limit redundancy in the formalizations. In the particular instance we were discussing in the quoted comments, I don't think let and where could help, but in the case of the long proof for half-adjoint equivalences, they surely would!
EDIT: The issue is that you would rather want to write is-section-is-invertible is-invertible-f; particularly when A, B or f are complicated expressions.
In light of this discussion, I'd be happy to move forward with the agda-unimath naming conventions, but with a minor tweak to the formatting (in the position of the colon). I'd prefer to continue to experiment with comments both in and out of the code blocks. I think as things evolve later we may settle on a preference for one style over another.
@fizruk do you have any further suggestions or objections? If not, then @fredrik-bakke would you draft a style guide file for us to use (adopted from the one you've used already)?
Sure, I can do this! I'm quite busy at the moment, but I can try and find the time in the second half of next week.
I'm sorry, I've been preoccupied with other things and haven't had the time to work on this. I will find the time next week if it is not time critical for you.
I think there is no rush. If I get to it sooner (this week(end)), I will let you know.
Yes, no problem at all. Sorry to have put this on your plate, but it seemed to me that with your experience you'd do this best ;)
Don't get me wrong, I would still love to do this! I just haven't had the surplus energy and time. I appreciate that you are involving me.