Zulip Chat Archive

Stream: general

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


view this post on Zulip 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?)

view this post on Zulip Mario Carneiro (Aug 12 2020 at 19:58):

I would say is_palindrome l and palindrome A for the subtype

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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"

view this post on Zulip Reid Barton (Aug 12 2020 at 21:07):

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

view this post on Zulip 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)

view this post on Zulip Reid Barton (Aug 12 2020 at 21:09):

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

view this post on Zulip 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".

view this post on Zulip Eric Wieser (Aug 12 2020 at 22:06):

Might people say "a group over the integers"?

view this post on Zulip 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.

view this post on Zulip Reid Barton (Aug 12 2020 at 22:15):

You can say "a group structure on the integers"

view this post on Zulip Eric Wieser (Aug 12 2020 at 22:17):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Eric Wieser (Aug 12 2020 at 22:18):

Indeed, that comment was regarding lean

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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: May 15 2021 at 02:11 UTC