About parameters, indices, and inductive.autoPromoteIndices

Stream: new members

[Lauri Oksanen]

I am trying to understand how promotion of indices to parameters works precisely, using Eq as an example. It seems to me (based on #print) that these two definitions are the equivalent:

universe u

inductive Eq₁ {α : Sort u} : (a : α) → (b : α) → Prop where
  | refl (a : α) : Eq₁ a a

inductive Eq₂ {α : Sort u} : (b : α) → (a : α) → Prop where
  | refl (a : α) : Eq₂ a a

That is, names of arguments are irrelevant. Is this correct?

Another related question: Is it possible to define an inductive type that is equivalent to Eq while having inductive.autoPromoteIndices false? The following gets quite close, but its refl has two implicit parameters, rather than one implicit and one explicit.

set_option inductive.autoPromoteIndices false in
inductive Eq' {α : Sort u} (a : α) : (b : α) → Prop where
  | refl : Eq' a a

[Aaron Liu]

| refl (a) : Eq' a a

[Kyle Miller]

In case it's useful, just yesterday I merged some additional documentation for auto-promotion of indices: https://github.com/leanprover/lean4/blob/ace52b38f2d6c38fd112c6e903f79c9248fa9710/src/Lean/Elab/MutualInductive.lean#L426

[Kyle Miller]

Lauri Oksanen said:

That is, names of arguments are irrelevant. Is this correct?

Correct, only the types are relevant, and the order of arguments.

[Kyle Miller]

Aaron Liu said:

| refl (a) : Eq' a a

I think this doesn't work unfortunately; parameter binder kind updates are for structure fields. It might be reasonable adding it to inductive constructors too (and the structure constructor if that doesn't already work).

[Kyle Miller]

One workaround is to define a separate constructor with the correct binder kinds.

set_option inductive.autoPromoteIndices false in
inductive Eq' {α : Sort u} (a : α) : (b : α) → Prop where
  | rfl : Eq' a a

theorem Eq'.refl {α : Sort u} (a : α) : Eq' a a := Eq'.rfl

[Lauri Oksanen]

Thanks a lot! Right, I tried variations like

set_option inductive.autoPromoteIndices false in
inductive Eq' {α : Sort u} (a : α) : (b : α) → Sort (u + 1) where
  | refl (a) : Eq' a a

This doesn't compile (Mismatched inductive type parameter ...).

If I understand correctly the workaround is sort of swapping the roles of rfl and refl, right?

My guess at the beginning was that inductive.autoPromoteIndices true is just for convenience, but it seems now that it has some fundamental importance. Is this correct?

[Kyle Miller]

Lauri Oksanen said:

If I understand correctly the workaround is sort of swapping the roles of rfl and refl, right?

In particular, the workaround is to define a constructor with the binder kinds set up the way you desire them, to override the choices made by inductive. I just chose rfl/refl because those are the names you see for Eq.

Lauri Oksanen said:

it seems now that it has some fundamental importance. Is this correct?

No, it's for convenience. The fact that you can set the binder kinds for parameters in the constructors by taking advantage of inductive.autoPromoteIndices is more of an accidental feature.

Being able to override binder kinds using the syntax that Aaron was hopeful would work is a likely feature at some point. Deciding whether or not to implement that feature will not take this behavior of inductive.autoPromoteIndices into consideration. (What I mean is, relying on index autopromotion isn't intended to be the way you control implicitness/explicitness.)

[Lauri Oksanen]

Thanks a lot! It could be argued that Eq' is not quite the same as Eq as the constructors play a special role (and also there is an extra definition in its namespace). So are we forced to conclude that Eq, a very fundamental type, relies on an accidental feature? I am writing lecture notes on basics of Lean, and I don't quite know how to explain this.

[Kyle Miller]

I think it can also be argued that Eq' and Eq are the same, since implicit/explicit annotations are for elaboration purposes.

[Kyle Miller]

If Eq didn't rely on autoPromoteIndices, you'd probably see Eq.rfl as the constructor and Eq.refl as the theorem.

I also could be wrong about motivations during early Lean development; I'm speaking from the perspective of someone who thinks Aaron's feature ought to exist. I see that Leo in this commit did intentionally use autoPromoteIndices. I don't know if he took advantage of it as a hack, or if this is what autoPromoteIndices is for.

[Kyle Miller]

I can see in the history that Leo did make a couple of fixes to autoPromoteIndices before removing this {} Lean-3-era constructor feature and then changing Eq. As far as I can tell though, the intent was to remove the {} feature rather than being the intent of autoPromoteIndices itself.

[Kyle Miller]

Lauri Oksanen said:

I am writing lecture notes on basics of Lean, and I don't quite know how to explain this.

Perhaps you could talk about a different type? This seems like a quirk that's subject to change rather than something fundamental about Lean.

[Kyle Miller]

Here's an explanation though, without getting into the quirks potential for engineering specific binder kinds: "For parameters, Lean will make them be implicit for each constructor. When indices are promoted to parameters, Lean won't override the explicit/implicit binders you've already given constructor fields."

[Lauri Oksanen]

It's a good point that Eq' and Eq don't differ from the point of view of the kernel. Perhaps I will just tell the story with refl and rfl swapped. I have been sticking to Nat, Prod and Eq in all my examples. Also I want to explain how equality really works, and reimplementing it illustrates this pretty well. I wouldn't like to explain autoPromoteIndices though.

[Kyle Miller]

The original motivation for autoPromoteIndices is the autoImplicits feature: https://github.com/leanprover/lean4/commit/4ee131981d7fe5d410ebdd31593c4e889a0d8e3b

[Kyle Miller]

The problem is that if autoimplicits are created after the colon, they might likely be better as parameters.

[Kyle Miller]

This has an impact on universe levels for the inductive type. Any type autoimplicits that remain as indices will need to be constructor fields, which forces the inductive type's universe level to be large enough to accommodate these types.

If they can be promoted to be parameters, then this universe level constraint goes away.

[Kyle Miller]

This universe consideration does not apply to Eq (nor does it involve any autoimplicits).

[Kyle Miller]

Here's a way you can work around needing to say anything about autoPromoteIndices itself:

1. Everything before the colon in the inductive type header is implicitly added as additional parameters to every constructor
2. The parameters of an inductive type consist of the largest prefix of parameters shared by the type constructor and all the constructors. Certainly this includes everything added in 1. When computing this prefix only the types matter (up to definitional equality).
3. In the type constructor, everything after the parameters are type indices. In the constructors, everything after the parameters are constructor fields.

Then autopromotion isn't a special feature. There's nothing inherently special about the colon in an inductive type definition — it's convention that this is where parameters stop and indices begin, without needing to devise new syntax.

[Kyle Miller]

Pedagogically, I wonder if initially presenting an index-only way to define types makes sense, like

inductive Prod' : Type u -> Type v -> Type (max u v) where
  | mk {α : Type u} {β : Type v} (x : α) (y : β) : Prod' α β

Then since α and β are the same across all constructors, and line up with the first parameters to Prod', Lean sees this as being a parameterized family of types. These first two fields aren't "stored" by the Prod'.mk constructor, so the universe of Prod' doesn't need to be Type (max (u + 1) (v + 1)). Moving the parameters before the : is a convenience:

inductive Prod' (α : Type u) (β : Type v) : Type (max u v) where
  | mk (x : α) (y : β) : Prod' α β

with the caveat that Lean now chooses binders for these parameters to be implicit for you. An additional convenience is that it gives you the assurance that these parameters won't bump the universe level.

I know this is all backwards historically when it comes to inductive families, but maybe it's not backwards for presenting it?

[Kyle Miller]

(I have to admit that with this index-first perspective I'm starting to come around to your idea that autoPromoteIndices is of fundamental importance :slight_smile:)

[Lauri Oksanen]

I like your idea a lot. In the case of functions, I already framed moving arguments before : as syntactic sugar.

Here is my draft in the hope that you have time to read it.

/-
# Type constructors with arguments

The encoding of Cartesian product is an example of an inductive type with parameters. It can be
defined as follows.
-/
universe u v
namespace Demo

inductive Prod : Type u → Type v → Type (max u v) where
  | mk : {α : Type u} → {β : Type v} →
    (fst : α) → (snd : β) → Prod α β

end Demo
/-

We view the type constructor `Prod` as a function taking two arguments and having the codomain
`Type (max u v)`.
-/
example : Type u → Type v → Type (max u v) := Prod
/-
The only constructor `Prod.mk` has the type
-/
example :
  (α : Type u) → (β : Type v) →
  (fst : α) → (snd : β) → Prod α β := @Prod.mk
/-
In terms of the types of their arguments, `Prod` and `@Prod.mk` have the common prefix
`Type u → Type v`. We can even write
-/
example :
  (α : Type u) → (β : Type v) →
  Type (max u v) := Prod
/-
The _parameters_ of an inductive type consist of the largest prefix of arguments shared by the type
constructor and all the constructors. The remaining arguments of the type constructor are called
_indices_, and the remaining arguments of a constructor are called _fields_. `Prod` has the
parameters `Type u` and `Type v`, but no indices. The fields of `Prod.mk` are `fst : α` and `snd : β`.

Earlier we considered the product of ℕ with itself and used the notation `(0, 1)`, which is syntactic
sugar for `Prod.mk 0 1`.
-/
example : (0, 1) = Prod.mk 0 1 := rfl
/-

The following syntax is also provided.{margin}[This can not quite be called syntactic sugar, see
[promotion of indices][auto-promote-indices] to parameters.]

[auto-promote-indices]: https://lean-lang.org/doc/reference/latest/The-Type-System/Inductive-Types/#inductive___autoPromoteIndices

-/
inductive Prod'
  (α : Type u) (β : Type v) : Type (max u v)
  where
  | mk (fst : α) (snd : β) : Prod' α β
/-


# Parameters and indices

{ref "sec-definitional-equality-naive"}[Recall] that `a = a` is syntactic sugar for `Eq a a`. `Eq` can
be defined as follows.
-/
namespace Demo

inductive Eq : {α : Sort u} → α → α → Prop where
  | refl {α : Sort u} (a : α) : Eq a a

end Demo
/-
We view `@Eq` as a function taking three arguments and having the codomain `Prop`.
-/
example : (α : Sort u) → (a : α) → α → Prop := @Eq
/-
The only constructor `@Eq.refl` has the type
-/
example : (α : Sort u) → (a : α) → Eq a a := @Eq.refl
/-
The common prefix is `(α : Sort u) → (a : α)`. Hence, `α` and `a` are parameters, while the third
argument of `@Eq` is an index. The constructor `@Eq.refl` has no fields.

The evaluation of the constructor `Eq.refl` at an expression `a` gives `Eq a a`, where the
parameter and index of type `α` take the same value `a`. As a result, we can construct terms of
type `Eq a a` for any expression `a`, but we cannot construct terms of type `Eq a b` when `a` and
`b` are distinct (modulo definitional equality). In this way, `Eq` encodes the equality between
expressions.
-/

[Kyle Miller]

(Correction to my earlier messages, which I've updated: I misremembered the logic, and parameters always become implicit in constructors. In any case, @Aaron Liu's suggestion for binder updates is now implemented in lean4#12603)