What names should be used for qualified module imports? about agda-stdlib HOT 18 CLOSED

We're importing just Data.Nat.Properties as ℕₚ, ℕᵖ, ℕ, Nat, and ℕ-Prop...

from agda-stdlib.

This is definitely mostly my fault, I've definitely shifted over the years. My current go-to style is to import Data.Nat.Properties as simply as ℕ, as the reason you need to disambiguate the Properties files is to avoid clashes with other datatypes. So my proposal would be to:

• name the properties file Data.X.Properties after the name of the main datatype in Data.X.

from agda-stdlib.

I'd been groping towards @MatthewDaggitt 's proposal for a while, but not quite sure if one can simultaneously import Data.X.Base and Data.X.Properties both as X, but it seems as though you can...

Yup, there's no problem there.

That said, I would still prefer to import as literal X, and hence ASCII/UTF-8 as a (Unix) filename, rather than 'symbolic' X, ie Nat rather than ℕ, but it seems as though I'm in a minority on this one...?

Hmm so this would be naming if after the module name not the datatype name? Or do you mean the datatype name transcribed to ASCII, i.e. would Data.Foo.Properties with a datatype called \. in Data.Foo.Base be imported as Dot?

from agda-stdlib.

If we're naming the qualifier after the datatype, what should be the convention for datatypes with long names?

Do you have any examples? I'm not aware of any datatypes with ridiculously long names.

What about when we're importing two modules for datatypes with the same name, e.g., Data.Vec.Relation.Unary.All and Data.List.Relation.Unary.All?

I think these should be named after the same datatype as everything else, i.e. the main datatype in Data.X. So these would be named Vec and List respectively.

We very rarely ever have the case that datatypes have the same name. We usually disambiguate them somehow, e.g. binary naturals, unnormalised rationals etc. so I don't think we'll run into that problem.

from agda-stdlib.

We have a long tradition of using Xₚ for the qualified import of Data.X.Properties.

from agda-stdlib.

This is one of the areas where I'd lean hard on 'convention' rather than making the style 'standard'. In other words, we won't get complete uniformity, but we'll get a lot closer.

For example, points 2-3 above de facto end up being ASCII, so if we remove the first point (because we don't want to change the tradition wrt Data.X.Properties), it's still going to be mostly true.

from agda-stdlib.

Re: X_p and ASCII
There's still some discrepancy between Nat_p and \bN_p, and... so on.

And Fin never seems to be consistently named, Properties or otherwise...

from agda-stdlib.

I'm all for consistency. For sure we'd want to pick a single name for Data.Nat.Properties in stdlib.

from agda-stdlib.

I'd been groping towards @MatthewDaggitt 's proposal for a while, but not quite sure if one can simultaneously import Data.X.Base and Data.X.Properties both as X, but it seems as though you can...

That said, I would still prefer to import as literal X, and hence ASCII/UTF-8 as a (Unix) filename, rather than 'symbolic' X, ie Nat rather than ℕ, but it seems as though I'm in a minority on this one...?

from agda-stdlib.

Module name. Your thought experiment litmus test example would import as "Foo"... but thanks for the ingenuity of the challenge ;-)

from agda-stdlib.

Okay, so when you said

I'd been groping towards @MatthewDaggitt 's proposal for a while, but not quite sure if one can simultaneously import Data.X.Base and Data.X.Properties both as X, but it seems as though you can... That said, I would still prefer to import as literal X, and hence ASCII/UTF-8 as a (Unix) filename, rather than 'symbolic' X, ie Nat rather than ℕ, but it seems as though I'm in a minority on this one...?

you weren't supporting my proposal for naming it after the datatype (leaving aside ASCII/non-ASCII)?

My feeling is that we want the qualified names of the Base modules to be as short as possible. When you have big long equations with lots of qualified operators, you want them to be short. So I would strongly be against importing the Base names as Nat rather than ℕ. Given that, it would be weird to then call the Properties modules Nat rather than ℕ...

from agda-stdlib.

Ok, I see your point. I had been trying to argue for ASCII throughout, and you for datatype name (throughout?, Properties as well as Base? I'm not thrilled about the subscript p, FWIW) but I don't want to make this a hill on which to die. Consistency, and understanding/documenting the convention, are much more important, IMHO.

That said, can/should/will we then import the PropositionalEquality module(s) as ≡... I hope so. P and PropEq etc. don't do it for me...

from agda-stdlib.

The subscript p should definitely go!

That said, can/should/will we then import the PropositionalEquality module(s) as ≡... I hope so. P and PropEq etc. don't do it for me...

Yes, I think so! I think that falls neatly under my proposed scheme of naming the qualifier after the datatype.

from agda-stdlib.

If we're naming the qualifier after the datatype, what should be the convention for datatypes with long names? What about when we're importing two modules for datatypes with the same name, e.g., Data.Vec.Relation.Unary.All and Data.List.Relation.Unary.All?

from agda-stdlib.

Do we have examples of this in the library, where we need to name those modules for qualified import?

Nevertheless, the question stands, so I suppose we would need to agree a disambiguation scheme, eg in your example, to import as VecAll and ListAll? (again, using the datatype name as a root to the 'long' name...?)

from agda-stdlib.

Closed by #2270 ? Or worth keeping open as a reminder to enact the recommendations, both going forward, and when updating old modules...?

from agda-stdlib.

Yes to close, since the style guide has been updated. Opening a fresh issue with a list of the old modules that need to be updated would be a good idea.

from agda-stdlib.

The horror! The horror! What a list... and how to face tackling it... :-( will file an issue in some form or other eventually ;-)

from agda-stdlib.