nonempty instance linter #5171

Stream: mathlib4

[Kim Morrison]

In Lean 3 we used to have a linter that required that for every type you defined a Nonempty instance (for at least some specialization of the arguments!).

It isn't implemented in Lean 4, and there are many porting notes, linking to #5171, about its absence.

I don't think we miss this linter much ...? It's occasionally useful, but mostly only in alerting you that your definition is wrong, which if you do anything nontrivial you'll find out about soon enough.

I propose that we just delete all these porting notes.

[Kim Morrison]

#20824

[Yaël Dillies]

Story time: Two years ago I defined binomial random graphs as those graph-valued random variables G : Ω → SimpleGraph V for some measure space Ω such that the law of fun ω ↦ (G ω).edgeSet is a sequence of Bernoulli measures. Just last week, @Yijun Leng noticed (in LeanCamCombi#16) that this is nonsense: I was asking each self-loop (edges s(v, v) from a vertex v to itself) to exist with probability p. You can see the fix in LeanCamCombi#17.

[Yaël Dillies]

Concretely, I had written down a predicate which was (almost) never true, and which stayed around in my repository for several years.

[Yaël Dillies]

Having the nonempty linter around probably wouldn't have saved me though. The only way to show that binomial random graphs exist over any ground set V is to build the product measure, which is done in KolmogorovExtension (but not yet upstreamed to mathlib), so I would likely have simply nolinted my definition anyway.

[Eric Wieser]

I think linters that remind people to write instances are a generally good thing

[Eric Wieser]

Especially since we now have partial as a language feature that depends on Nonempty

[Eric Wieser]

So my vote would be to implement the linter rather than dropping the porting notes

[Kim Morrison]

@Eric Wieser, if there is a concrete plan to implement said linter, I'd be happy to wait for it. But if not, I don't think there is anything to be gained from waiting. Note that the porting notes here about about @[nolint]s that were removed, so if we were to implement such a linter, it would of course tell us exactly where such @[nolint]s need to be restored.

[Kim Morrison]

Given we are a year and a half after the port, with no evidence of anyone being interested in writing such a linter, I don't think we can assume it is going to happen without positive evidence.

[Michael Rothgang]

How difficult would writing that linter be? Is there some description would it would do (other than trying to read the Lean 3 code... which I would rather not do)?

[Kim Morrison]

As indicated above, I am happier not having this linter, I think it was counterproductive.

But the spec was (I think):

• for every structure or inductive C x y z
• check that there exists a definition marked instance in the environment with type after binders Nonempty (C x y z) for some values of x y z. (it's fine if these are specialized arbitrarily, even to constants)

[Eric Wieser]

That spec sounds right to me

[Eric Wieser]

Maybe swap "every structure" for "every declaration of type Type*"

[Kim Morrison]

That sounds even more unpleasant to me. :-)

[Eric Wieser]

I guess that would be annoying in category theory, but for thinks like MulOpposite would be painless

[Jireh Loreaux]

I think it's not worth having a linter. The problem it solves is very minor, and I think it's not worth the (even very small!) associated computational cost.

[Eric Wieser]

I think the computational cost is negligeable; the human cost to write it is probably not justified by the linter itself, but seems like a nice metaprogramming exercise that ends up providing non-zero value for someone who wants practice

[Thomas Murrills]

How funny—I drafted message yesterday offering to clear some debt by porting this very linter just as something fun to do, but was holding off on sending it :)

I think it might be worth having a general "missing instance" linter—Nonempty and Inhabited are a bit specialized, but maybe we want to know about other instances as well.

The useful question here is "what instances do we generally want when possible?"

[Thomas Murrills]

This is actually a little tricky once you start thinking about Nonempty and Inhabited. (The following is from my draft.)

Since Inhabited Foo gets us Nonempty Foo, it's clear in the case of non-parameterized instances that we want Inhabited when possible, and Nonempty otherwise.

But for parameterized "container-like" types, it seems we actually want two instances. Consider

structure Foo (α) where
  a : α
deriving Inhabited

This gives us instInhabitedFoo {α} [Inhabited α] : Inhabited (Foo α).

But let's say we only have Nonempty α. This is not sufficient to give us Nonempty (Foo α), since we can't provide the Inhabited α required by instInhabitedFoo.

I'd hazard that, in this case, we also want to make sure we have e.g.

instance {α} [Nonempty α] : Nonempty (Foo α) :=
  .intro ⟨Classical.choice ‹_›⟩

(or whichever way is best to write the term itself), possibly with (priority := low) if we want to get Nonempty from Inhabited when possible.

[Kim Morrison]

Jireh Loreaux said:

I think it's not worth having a linter. The problem it solves is very minor, and I think it's not worth the (even very small!) associated computational cost.

It's not the computational cost that matters, it is having to turn off the annoying linter!!

[Jireh Loreaux]

I agree the linter could be annoying, but as we saw not long ago, there is non-negligible startup cost from all the (probably only syntax?) linters we have running, and since we run CI all the time, even an environment linter gets a bunch of use. I realize this may not be high computational cost, but my claim is that the linter isn't even worth the low computational cost (let alone the annoyance).

[Kyle Miller]

Here's my understanding of the history of this linter:

• Originally, Gabriel added an Inhabited linter, because many basic types were missing Inhabited instances. That helped push people toward implementing them.
• Near the end of the Lean 3 days, we realized that Inhabited instances for most types were really arbitrary. We compromised and switched it to a Nonempty linter, since that at least didn't pollute the Inhabited instances with random values just to satisfy the linter. (Inhabited doesn't have a spec, but it makes sense for it to be, in some sense, the "default" value for a type.)
• Now in the Lean 4 days we've been surviving without any such linter. Maybe its need has passed.

In my experience, the big problem with the Inhabited/Nonempty linter is that it would incentivize creating useless Inhabited/Nonempty instances just to appease the linter. It felt like cheating to turn the linter off for a particular type.

[Kyle Miller]

Have we had any issues with missing Inhabited/Nonempty instances recently? If not, then it sounds like we don't need it anymore. Mathlib's grown up :-)

[Johan Commelin]

Kim Morrison said:

Note that the porting notes here about about @[nolint]s that were removed, so if we were to implement such a linter, it would of course tell us exactly where such @[nolint]s need to be restored.

This sounds like an excellent argument to remove the porting notes. We're not really throwing away any information.
I'm going to merge delegate the PR now, and we can see later whether the linter reappears or not.
(I personally think we should not have the linter.)