Noun/adjective/verb naming conventions for defs in mathlib

Stream: general

[Eric Wieser]

Brought up by https://github.com/leanprover-community/mathlib/pull/3729#discussion_r469345718, the mathlib naming conventions page doesn't seems to discuss naming of defs

Taking the example there, what is the right name for a def of type list α → Prop that determines if a list is a palindrome?

• palindrome l
• palindromic l
• is_palindrome l
• is_palindromic l

I find the first of these rather odd, as it suggests to me that the term is some type that holds palindromes

It seems like there should be some distinct guidelines for defs T → Prop (adjective-ish?), T → U (verb-ish?), and T → Type (noun-ish?)

[Mario Carneiro]

I would say is_palindrome l and palindrome A for the subtype

[Eric Wieser]

So (aside from breaking a lot of code) would it make sense to rename function.left_inverse to function.is_left_inverse?

[Chris Hughes]

I would say drop the is unless the subtype is actually defined and there's reason for confusion. I prefer palindrome over palindromic just for familiarity.

[Kevin Buzzard]

Isn't having both set X and subgroup X inconsistent? Surely if we're describing the terms it should be subset X?

[Reid Barton]

In math you can say either "a subset of $\mathbb{N}$" or "a set of natural numbers"

[Reid Barton]

But I agree subset would be a lot easier for new users

[Kevin Buzzard]

When you're defining the type rather than the terms you want to call it powerset X. In topology we consider a set of subsets of X and its type is set (set X)

[Reid Barton]

subset (subset X) would be pretty bad I guess.

[Chris Hughes]

It can't be a subset because X is a type not a set I suppose. People still say "a set of reals", but nobody says "a group of integers".

[Eric Wieser]

Might people say "a group over the integers"?

[Eric Wieser]

Regarding Kevin's point, I would expect a hypothetical subset to be a subtype like \Pi (u: set T), Type := {v : set T // v \sub u}. Subset is an operation on sets not types, and nat is not a set.

[Reid Barton]

You can say "a group structure on the integers"

[Eric Wieser]

I suppose group_structure int is rather too verbose, and would impact most type classes

[Reid Barton]

In the context of ordinary mathematical parlance, nat is the natural numbers and the natural numbers form a set.

[Reid Barton]

In general Type corresponds to what mathematicians call a set (with the possible exception of set theorists) and this makes set a confusing name

[Eric Wieser]

Indeed, that comment was regarding lean

[Eric Wieser]

Perhaps it is worth emphasing somdwhere in the docs for mathematicians coming from set theory that the set corresponding to a type T is set.univ T

[Eric Wieser]

But this sounds like something for another thread, I've seen this exact conversation derail threads over and over.

[Chris Wong]

Going back to the original topic, what's the consensus on the name? (Personally I haven't found use for a subtype yet, so out of YAGNI I'd support sticking with the original name.)

[Iain Monro]

Using "is" (or "has", or whatever) to make a function that implements a predicate sound like it implements a predicate is a common standard, and reasonably so, to the point that I think if you're going to depart from it you should probably have a decent reason.

[Iain Monro]

Speaking for myself, I don't like the idea of having to know whether or not someone wanted a typeclass for a thing, to know whether I need to prefix the function I want with "is_" - I'd rather just have a consistent global standard.

[Jasmin Blanchette]

At the software company where I used to work, Trolltech (now the Qt Company), we at one point had a mixture of is- and no is-. It was a mess (we like to be able to guess APIs without having to look them up), and often the is-less name would obscure a useful concept, as in Mario's example. So we standardized on is- (within reason) and never looked back.

[Jasmin Blanchette]

The English language, which often overloads words to be nouns, adjectives, verbs, etc., seems to make this necessary in general.

[Rob Lewis]

FYI, I merged the PR in question, but if we converge on is_palindrome instead of palindrome it's an easy change to make.

[Eric Wieser]

I opened this thread primarily to ask about deciding on a convention, not enforcing it in that particular PR. From what I've seen so far, mathlib doesn't (yet) care much about people being broken by definitions changing name, so merging that PR first was fine.