parameters and universe levels

Stream: general

[Jireh Loreaux]

My type theory understanding is fuzzy in various places. Here's one that I don't understand. Why does this first list implementation not require a universe bump, but the second does? I would have thought they were the same, but Lean complains.

prelude

universe u

inductive list (α : Type u) : Type u
| nil : list
| cons : α → list → list

inductive list' : Type u → Type (u + 1)
| nil (α : Type u) : list' α
| cons (α : Type u) : α → list' α → list' α

[Reid Barton]

They are isomorphic, yes, but by syntactic restrictions belong to different universes.
Consider the following variation, which is genuinely larger:

inductive list'' : Type u → Type (u + 1)
| nil (α : Type u) : list'' nat
| cons (α : Type u) : α → list'' nat → list'' nat

[Jireh Loreaux]

Hmm... I think I must have a fundamental misunderstanding here, because I would have exepected list'' : Type u → Type (max u 0) since nat : Type 0. And what exactly is the "syntactic restriction" that occurs with list'?

[Reid Barton]

One of the fields of the list''.cons constructor is of type Type u : Type (u+1), so the whole type belongs to universe u+1.

[Reid Barton]

Yes in actuality for a specific α the only value of Type u that can appear in a cons value of type list' α is α itself--but Lean doesn't care about that.

[Bart Michels]

This is explained a little bit in §7.8 of "Theorem Proving in Lean" (v 3.23.0): If your inductive family has a constructor with an argument of type β : Type v, then the types of the family need to be of type Type v at least.
In the example, there is an argument α of type Type u : Type (u + 1).

[Bart Michels]

The way I understand it is as a safeguard against defining something like the "union" of everything of type Type u and then declaring that to be still of type Type u, which seems dangerous.

[Jireh Loreaux]

(deleted)

[Jireh Loreaux]

Thanks both, I think I understand now. Let me try to explain my current conception to see if it matches reality.

list takes a parameter α which is fixed throughout the entirety of the inductive definition. The list.cons constructor has type α → list → list which must live in universe level imax u v where list : Type v. Of course, list.nil : α and α : Type u, so we have two conditions: imax u v ≤ v and u ≤ v, and it is possible to satisfy these conditions by taking v = u, which is why it makes sense for list : Type u.

In contrast, α is and index in list' (and list''), which means that it can vary throughout the inductive constructors. So, list'.cons : Π (α : Type u), α → list' α → list' α and since α → list' α → list' α : Type (imax u v), then Π (α : Type u), α → list' α → list' α : Type ((imax u v) + 1). Likewise the type of the constructor list'.nil lives in universe level u+1. Consequently, we have two constraints, (imax u v) + 1 ≤ v and u + 1 ≤ v, and so the minimum possible universe level for v is u+1.

Finally, list'' is highlighing / using the fact that the index α can vary (and in this way it is not just a syntactic restriction). In this case, for each type α, list''.cons is constructing a new type. (Of course, this was also occurring in list' but this was partially occluded by the fact that it's isomorphic to list.)

Is this the correct understanding?