Stream: Coq devs & plugin devs

Topic: [stdlib] Naming convention for moving from Prop to Type

Olivier Laurent (Dec 03 2021 at 13:05):

In stdlib, we have at least 6 different ways of naming things related to Type when something analogous exists for Prop:

• sig -> sigT
• Logic -> Logic_Type
• excluded_middle -> excluded_middle_informative
• not_Zeq -> not_Zeq_inf
• relation -> crelation
• nat_ind -> nat_rect

It could be nice to have it more uniform. Any opinion or historical justification for one or another choice?

Gaëtan Gilbert (Dec 03 2021 at 13:18):

inf is bad because it looks like infinity
crelation is bad because who knows what the c is even supposed to mean

Pierre-Marie Pédrot (Dec 03 2021 at 13:20):

I think T-ending is nice, it's short and unmistakenable

Janno (Dec 03 2021 at 13:20):

I quite like sig -> sigT although I am guilty of defining things called ...T that have nothing to do with Prop versus Type.

Paolo Giarrusso (Dec 03 2021 at 14:19):

I was adopting fooT / foo.t as an OCaml-inspired suffix for data types, tho those are usually Sets or Types.

Alexander Gryzlov (Dec 03 2021 at 14:25):

If you want more than 1 letter, Tyseems rather unambiguous.

Paolo Giarrusso (Dec 03 2021 at 14:29):

Also, even if T might be used elsewhere, adding T to a Prop probably remains unambiguous.

Paolo Giarrusso (Dec 03 2021 at 14:31):

And we could probably update most of the cases above easily with deprecations — except for sigT and nat_rect, changes there would break almost everything.

Matthieu Sozeau (Dec 10 2021 at 19:32):

Gaëtan Gilbert said:

inf is bad because it looks like infinity
crelation is bad because who knows what the c is even supposed to mean

It's supposed to mean computational

Last updated: Sep 30 2023 at 15:01 UTC