Zulip Chat Archive

Stream: general

Topic: Universe levels in inductive types

Julius Marozas (Dec 16 2021 at 18:50):

Hi all,
I was playing around with the definition of a list:

inductive {u} list (α : Sort u) : Sort u
| nil : list
| cons : α  list  list

where #print list shows the following.

inductive list : Sort u  Sort u
list.nil : Π {α : Sort u}, list α
list.cons : Π {α : Sort u}, α  list α  list α

So, I tried to redefine list without binding α\alpha (just like how #print shows it).

inductive {u} list : Sort u  Sort u
| nil : Π {α : Sort u}, list α
| cons : Π {α : Sort u}, α  list α  list α

But now I get an error: universe level of type_of(arg #1) of 'list.nil' is too big for the corresponding inductive datatype. I found that I can fix this by changing the type of list to be Sort u → Type u. But I am not sure why that's necessary, and why this doesn't break with the original definition.

Kyle Miller (Dec 16 2021 at 19:38):

@Julius Marozas The fix you found is equivalent to doing Sort u -> Sort (u + 1) (since Type u = Sort (u + 1) in general). Thinking about it in a computational way, the idea is that each constructor in an inductive type is expected to actually store its arguments so that you can later match and operate on them. Arguments to the type itself (the ones in the first line up to the colon) are not expected to be stored anywhere.

Your redefined list is one where each node keeps track of which type it's from, compared to the original where they don't. Recording types like this means the list must be in one universe higher -- otherwise list might be one of the types that can appear in one of the nodes, and impredicativity like that is not allowed ("predicativity" is that definitions can only ever refer to things that are defined before them; I guess the name "predicate" stuck, but only for one-argument Prop-valued functions).

Since each node knows the type of its element, you can easily go to fully heterogeneous lists, though there's not much you can really do with a list like this other than compute its length:

inductive {u} list : Sort (u+1)
| nil : list
| cons : Π {α : Sort u}, α  list  list

Eric Wieser (Dec 16 2021 at 19:56):

That's isomorphic to list (sigma $ @id (Sort u)), right?

Julius Marozas (Dec 16 2021 at 20:38):

@Kyle Miller Thanks for the explanation, it's much clearer now.
@Eric Wieser The code you provided doesn't seem to type check, maybe you meant this: list (sigma $ @id (Sort (u + 1)))?

Eric Wieser (Dec 16 2021 at 20:39):

Oh, I forgot that I wasn't allowed to put sorts in a list or sigma type

Eric Wieser (Dec 16 2021 at 20:39):

I might also mean list (sigma $ @id (Type u)) or list (psigma $ @id (Sort u))

Julius Marozas (Dec 16 2021 at 20:41):

Yeah, that seems to work. What's the point of having both psigma and sigma?

Eric Wieser (Dec 16 2021 at 20:42):

psigma causes annoying universe elaboration issues, apparently

Eric Wieser (Dec 16 2021 at 20:42):

Which aren't worth sufferring through for 90% of the cases when you know you only are dealing with Types

Julius Marozas (Dec 16 2021 at 20:45):

Interesting, do you have any examples of such cases, or documentation on this topic?

Eric Wieser (Dec 16 2021 at 20:50):

It would be great if someone could add a library note for this, so we could reference it from psigma and pprod

Yaël Dillies (Dec 16 2021 at 21:16):

I already hint at it in the module docs of data.sigma.basic

Last updated: Aug 03 2023 at 10:10 UTC