Naming convention? about cubical HOT 8 CLOSED

In Agda, the example

open import Data.HITs.PropTrunc (||_||)
import Data.HITs.PropTrunc as PropTrunc

can be written

open import Data.HITs.PropTrunc as PropTrunc using (||_||)

from cubical.

Can you send me a link to the conventions for the standard library so that I can compare?

Haha, I wish we were this organised. There is a very bare-bones skeleton of a style guide here but mostly the convention is unspoken and is enforced by either @gallais or I coming down hard on names we don't like 😆 I'll try and flesh it out a bit more in the next couple of days.

from cubical.

I think having a function named elimPropTrunc is kind of superflous when it's already in the file PropTrunc/Properties.agda. It's better to just call it elim. Then when other files import it, they can change the qualified name.

import Data.HITs.PropTrunc as PropTrunc

foo = ... PropTrunc.elim ...

This also kinds of gives a structure to the names, which is nice.

from cubical.

Speaking of qualified import, I think we should avoid unqualifed import as much as possible, except for maybe things from Core. This practice from Haskell is nice:

open import Data.HITs.PropTrunc (||_||)
import Data.HITs.PropTrunc as PropTrunc

from cubical.

Yes, there is currently no naming convention. It might be a good idea to follow the HoTT-Agda convention (https://github.com/HoTT/HoTT-Agda) as we wouldn't have to think about changing names when porting developments from there.

Can you send me a link to the conventions for the standard library so that I can compare?

from cubical.

@MatthewDaggitt Thanks! I like the stylistic choices. I think I'll use the HoTT-Agda naming conventions and the stdlib style guide for things like indentation.

from cubical.

I don't find the HoTT-agda convention very readable. Perhaps its due to the use of unicode, but I would prefer a convention without too much unicode. However it is also the case that some names may get too long. I read more agda than I write, so readability is a big plus for me.

from cubical.

Closing this now that we finally merged #451

from cubical.