Zulip Chat Archive

Stream: general

Topic: Noun/adjective/verb naming conventions for defs in mathlib

Eric Wieser (Aug 12 2020 at 19:56):

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 (Aug 12 2020 at 19:58):

I would say is_palindrome l and palindrome A for the subtype

Eric Wieser (Aug 12 2020 at 20:11):

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

Chris Hughes (Aug 12 2020 at 20:45):

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 (Aug 12 2020 at 21:03):

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

Reid Barton (Aug 12 2020 at 21:07):

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

Reid Barton (Aug 12 2020 at 21:07):

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

Kevin Buzzard (Aug 12 2020 at 21:08):

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 (Aug 12 2020 at 21:09):

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

Chris Hughes (Aug 12 2020 at 21:16):

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 (Aug 12 2020 at 22:06):

Might people say "a group over the integers"?

Eric Wieser (Aug 12 2020 at 22:11):

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 (Aug 12 2020 at 22:15):

You can say "a group structure on the integers"

Eric Wieser (Aug 12 2020 at 22:17):

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

Reid Barton (Aug 12 2020 at 22:17):

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

Reid Barton (Aug 12 2020 at 22:18):

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 (Aug 12 2020 at 22:18):

Indeed, that comment was regarding lean

Eric Wieser (Aug 12 2020 at 22:19):

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 (Aug 12 2020 at 22:20):

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

Chris Wong (Aug 13 2020 at 02:38):

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 (Aug 13 2020 at 10:48):

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 (Aug 13 2020 at 10:50):

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 (Aug 13 2020 at 11:04):

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 (Aug 13 2020 at 11:05):

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

Rob Lewis (Aug 13 2020 at 11:33):

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 (Aug 13 2020 at 16:13):

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.

Last updated: Aug 03 2023 at 10:10 UTC