What names should be used for qualified module imports?

[jamesmckinna]

(Yet) Another style guide convention that it might be good to (try to) standardise... so discussion of what possible conventions might be good/useful/enforceable is in order?

Partly prompted by recent work on v2.0/v2.1 PRs, partly by the realisation that we don't even seem able to agree what to call the PropositionalEquality module when imported qualified...

Possible points:

• ASCII, not Unicode?
• Data.X imports via the name X?
• Use the last/penultimate (in the case of Core etc.) identifier in the long name otherwise
• ... etc.

[gallais]

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

[JacquesCarette]

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.

[jamesmckinna]

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...

[Taneb]

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

[JacquesCarette]

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

[MatthewDaggitt]

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.

[jamesmckinna]

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...?

[MatthewDaggitt]

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?

[jamesmckinna]

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

[MatthewDaggitt]

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 ℕ...

[jamesmckinna]

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...

[MatthewDaggitt]

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.

[Taneb]

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?

[jamesmckinna]

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...?)

[MatthewDaggitt]

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.

[jamesmckinna]

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

[JacquesCarette]

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.

[jamesmckinna]

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