Deprecate and remove inductive ... :=

[david-christiansen]

Description

Today, Lean accepts all of the following:

inductive DogSound
  | woof
  | grr

inductive DogSound :=
  | woof
  | grr

inductive DogSound where
  | woof
  | grr

It seems that the overwhelming majority of declarations use the latter syntax (with where). In the interest of simplifying things, how about we deprecate the first two?

Context

The broad context here is that I'm writing the new reference manual with tooling that can let us know about undocumented tokens. The documentation should be comprehensive and describe what the language does.

Deprecating these two alternate syntaxes, rather than documenting them, would make Lean code more uniform and reduce the language surface area.

I'm not advocating immediate removal - a long deprecation period won't hurt anything - but a warning would be useful.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[m4lvin]

Why not enforce the first one and deprecate both := and where for inductive? I would find that more uniform because in a def it is also not allowed, i.e. the following is wrong:

def f : Nat → Nat where
  | 0 => 42
  | (.succ n) => f n

[digama0]

where after def is valid, and is used for defining structure instances:

def foo : Inhabited Nat where
  default := 0

[nomeata]

In the interested of pragmaticm, we should probably stick to “overwhelming majority of declarations use” and keep the one with where, even if inconsistent with the def-with-guards syntax

[kmill]

It looks like mathlib uses no-where and core Lean uses where. It'd be interesting knowing what's most commonly used in the wild if we're deciding by pragmatism.

I don't mind going with where though.

[digama0]

Beware of mathportisms when looking at mathlib code for common style. I just checked and no-where is mathport style, so this will disproportionately affect the measurement. (I don't recall giving thought to this when writing mathport, and have generally used where style in batteries et al.)

[kmill]

#5533 has a linter for no-where, with an exception for the no-constructor case. There's still the whole test directory to update, which seems to have a few hundred no-where inductive commands.

Do we want to be strict about where? I think it makes sense deprecating :=, but I'm thinking it would be less disruptive if where were to simply be optional.

[tydeu]

The where style just seems like a waste of space. It never disambiguates anything, right?

[david-christiansen]

The where style just seems like a waste of space. It never disambiguates anything, right?

I don't think it does. But I think the ship sailed long ago on discussing the merits of syntax choices other than by appeal to least disruption.

[tydeu]

@david-christiansen If the where is useless, doesn't it make the most sense to deprecate that style? I suspect the only reason core primarily uses it is because at one point the no-where style didn't exist (or something like that).

[digama0]

Note, in lean 3 there was only no-where syntax, so I think your theory doesn't match. I'm pretty sure that when where was introduced core used it across the board, and that's how we got where we are now.

[kmill]

I have hard numbers: 79% of inductives in core use where, 21% use no where, and 0% use :=.

Personally, if we have to deprecate two out of three, I would rather deprecate both := and where. If we wanted a keyword here, with would have been more appropriate. The where keyword is for structure/conjunctive data, and with (like in match) is for disjunctive data.

I'll make another PR that deprecates just :=, which is an easy decision! I'm going to deprecate it for structure as well unless there are any objections. Using := for structure is a Lean-3-ism. Edit: #5542

[kmill]

The := variants are now deprecated.

I don't really want to resolve whether where should be required or not at the moment, so what do you think about leaving it in the current state for now @david-christiansen, where where is optional?

[omentic]

I quite dislike where being optional - this was something that threw me for a loop as a language learner.

When where is omitted on inductive declarations, it behaves identically to as if it were present. When where is omitted on structure declarations, it produces a (valid) structure with zero fields - much different behavior than with the where! I had to ask about this on the Zulip a little while back to figure out just what was going on, because I was expecting inductive and structure declarations to behave relatively similarly to each other.

I would rather where be consistently enforced by a lint or otherwise. Personally I would much prefer it to be present (on analogy with structure, class, instance, and maybe other language constructs I haven't come across yet) but I think either consistently present or consistently not present is an improvement over the current mixture.