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