# Zulip Chat Archive

## Stream: new members

### Topic: List is forced up a universe?

#### Ken Lee (Apr 19 2020 at 22:34):

#check list -- list : Type u_1 → Type u_1 namespace hidden inductive list : Type → Type | nil : Π A : Type, list A | append : Π A : Type, Π a : A, Π l : list A, list A /- universe level of type_of(arg #1) of 'hidden.list.nil' is too big for the corresponding inductive datatype -/ end hidden

Why is the `list`

pre-existing in Lean allowed to go from a universe to itself,

meanwhile when I try to define `list`

Lean tells me I need to go up a universe?

#### Reid Barton (Apr 19 2020 at 22:47):

The short answer is you put the type (`a`

in `list a`

) to the right of the colon.

#### Ken Lee (Apr 19 2020 at 22:50):

Reid Barton said:

The short answer is you put the type (

`a`

in`list a`

) to the right of the colon.

I'm not sure what you mean by "(`a`

in `list a`

)" ?

#### Reid Barton (Apr 19 2020 at 22:50):

I'm just trying to refer to the type that is the argument of `list`

.

#### Chris Hughes (Apr 19 2020 at 22:51):

I don't think it's directly because of that. It's because you have Types as arguments to your constructors, which you were forced to do by putting `list : Type -> Type`

instead of `list (A : Type) : Type`

#### Marc Huisinga (Apr 19 2020 at 22:52):

you'd want something like

inductive list (α : Type u) : Type u | nil : list | append : Π a : α, Π l : list, list

#### Ken Lee (Apr 19 2020 at 22:53):

Chris Hughes said:

I don't think it's directly because of that. It's because you have Types as arguments to your constructors, which you were forced to do by putting

`list : Type -> Type`

instead of`list (A : Type) : Type`

but surely `list (A : Type) : Type`

is just syntactic sugar for `list : Type -> Type`

?

#### Chris Hughes (Apr 19 2020 at 22:53):

If there are Type's as arguments to the constructors then it has to go up a universe, because this can be used to make very large Type, e.g.

inductive list : Type → Type | nil : Π A : Type, list unit

Here, there is a `list unit`

for every `Type`

, and the cardinality of `Type`

is strictly greater than any `Type`

, so if lean allowed this definition there would be a contradiction.

#### Chris Hughes (Apr 19 2020 at 22:54):

Ken Lee said:

but surely

`list (A : Type) : Type`

is just syntactic sugar for`list : Type -> Type`

?

It isn't

#### Reid Barton (Apr 19 2020 at 22:56):

I think in the type theory literature the variables before the colon are called parameters and the variables after the colon are called indices.

This is relevant even though it's about Coq: https://stackoverflow.com/questions/24600256/difference-between-type-parameters-and-indices

#### Chris Hughes (Apr 19 2020 at 22:57):

Putting `Type`

right of the colon allows you to define an inductive family, where you are defining many inductive `Types`

at the same time, one for each type and they can all be constructors to each other.

#### Chris Hughes (Apr 19 2020 at 22:58):

You can do stuff like this with inductive families.

inductive X : bool → Type | f : X tt → X ff | g : X ff → X tt

#### Chris Hughes (Apr 19 2020 at 23:00):

So you are defining two types `X ff`

and `X tt`

, and you can make an `X ff`

out of an `X tt`

. Both these types are empty incidentally.

#### Mario Carneiro (Apr 19 2020 at 23:02):

Ken Lee said:

but surely

`list (A : Type) : Type`

is just syntactic sugar for`list : Type -> Type`

?

To be clear, as far as the type of `list`

itself is concerned, this is true, but the location of the colon determines the difference between parameters and indices that is relevant to the axioms that define inductive types in lean, so these generally are not interchangeable.

#### Mario Carneiro (Apr 19 2020 at 23:04):

One could imagine a desugaring pass that notices if you always use the type argument the same way without varying it, and shifts the argument to be a parameter, but because there are ordering requirements between parameters and indices this may not always trigger, and in any case it gives the user less control (this also affects the statement of the recursion principle for the type)

#### Mario Carneiro (Apr 19 2020 at 23:08):

namespace hidden inductive biglist : Type → Type 1 | nil {A : Type} : biglist A | cons {A : Type} (a : A) (l : biglist A) : biglist A inductive list (A : Type) : Type 1 | nil : list | cons (a : A) (l : list) : list #check @biglist.rec -- biglist.rec : -- Π {C : Π (a : Type), biglist a → Sort u_1}, -- (Π {A : Type}, C A biglist.nil) → -- (Π {A : Type} (a : A) (l : biglist A), C A l → C A (biglist.cons a l)) → Π {a : Type} (n : biglist a), C a n #check @list.rec -- list.rec : -- Π {A : Type} {C : list A → Sort u_1}, -- C list.nil → (Π (a : A) (l : list A), C l → C (list.cons a l)) → Π (n : list A), C n end hidden

#### Reid Barton (Apr 19 2020 at 23:11):

Hmm, so I guess `biglist`

lets you do "polymorphic recursion". Is that ever actually useful?

#### Mario Carneiro (Apr 19 2020 at 23:11):

note that `list.rec`

is a lot more convenient than `biglist.rec`

if you want to prove a statement about `list nat`

by induction

#### Mario Carneiro (Apr 19 2020 at 23:12):

`list.rec`

easily implies `biglist.rec`

but the reverse is not true (at least not without cast headaches)

#### Reid Barton (Apr 19 2020 at 23:12):

Oh, hmm.

#### Mario Carneiro (Apr 19 2020 at 23:13):

Other than that, these types are the same: `list`

and `biglist`

have the same type, as do `(big)list.nil`

and `(big)list.cons`

#### Ken Lee (Apr 19 2020 at 23:14):

I see! In `biglist`

there is a `\Pi {A : Type}`

at every minor premise(?)

By the way @Mario Carneiro I've been reading your notes on the Type Theory of Lean. Just got to typing judgements for inductive types, which was when I came across this question.

#### Mario Carneiro (Apr 19 2020 at 23:14):

Unfortunately, when you write inductive types in Coq style everything is right of the colon, so I notice this comes up in code translated from Coq

#### Mario Carneiro (Apr 19 2020 at 23:15):

@Ken Lee Yes, you can use the rules for inductive types in the paper to determine that this universe bumping is supposed to happen

#### Ken Lee (Apr 19 2020 at 23:18):

Mario Carneiro said:

Ken Lee Yes, you can use the rules for inductive types in the paper to determine that this universe bumping is supposed to happen

I have, which is why I was confused when Lean said it didn't have to happen

#### Ken Lee (Apr 19 2020 at 23:21):

Reid Barton said:

I think in the type theory literature the variables before the colon are called parameters and the variables after the colon are called indices.

This is relevant even though it's about Coq: https://stackoverflow.com/questions/24600256/difference-between-type-parameters-and-indices

So it looks like this is what I'm looking for. The difference between parameters and indices.

#### Mario Carneiro (Apr 19 2020 at 23:21):

In the notation of the paper, `list`

above is

$\lambda A:U_1,\mu T:U_2, (\mathsf{nil}:T) + (\mathsf{cons}:A\to T\to T)$

and `biglist`

is

$\mu T:U_1\to U_2, (\mathsf{nil}:\forall A:U_1,\ T\;A) + (\mathsf{cons}:\forall A:U_1,\ A\to T\;A\to T\;A)$

#### Mario Carneiro (Apr 19 2020 at 23:22):

parameters are denoted in the paper by having a free variable in the $\mu$-definition

#### Kevin Buzzard (Apr 19 2020 at 23:24):

@Chris Hughes didn't you once say to me that you wanted to read Mario's type theory notes? Note that Ken is reading them

#### Ken Lee (Apr 19 2020 at 23:27):

Mario Carneiro said:

In the notation of the paper,

`list`

is$\lambda A:U_{\ell},\mu T:U_{\ell}, (\mathsf{nil}:T) + (\mathsf{cons}:A\to T\to T)$

and

`biglist`

is$\mu T:U_{\ell}\to U_{S\ell}, (\mathsf{nil}:\forall A:U_{\ell},T\;A) + (\mathsf{cons}:\forall A:U_{\ell},A\to T\;A\to T\;A)$

Ahhhhhh so `list`

is an inductive definition per $A\,:\,U_{\ell}$, where as `biglist`

is just one inductive definition

#### Mario Carneiro (Apr 19 2020 at 23:28):

right

#### Ken Lee (Apr 19 2020 at 23:29):

and since the inductive definitions per $A : U_l$ has type $U_l$, `list`

is indeed type `Type u_l -> Type u_l`

#### Chris Hughes (Apr 19 2020 at 23:29):

Last time I tried reading Mario's paper I was completely intimidated by the notation.

#### Kenny Lau (Apr 19 2020 at 23:30):

I think if you stare at the notation for one minute then eventually you will discover that the notation stares back at you

#### Mario Carneiro (Apr 19 2020 at 23:32):

I think it is important to make sense of what the `inductive`

command does to have a term that denotes an inductive definition (here the $\mu$ binder). Otherwise, you might think that lean has an infinite and ever growing set of axioms and it would be difficult to understand the whole that way

#### Mario Carneiro (Apr 19 2020 at 23:33):

other than that, the notation really is lean in latex font

#### Mario Carneiro (Apr 19 2020 at 23:39):

Would there be a demand for a type theory primer more in the style of https://coq.github.io/doc/master/refman/language/cic.html ? That is a bit less symbol heavy and more tutorialized. I don't know if I could write something like that but I would be happy to collaborate with one of the educators around here

#### Chris Hughes (Apr 19 2020 at 23:40):

Even the very first notation is very hard to understand. What does this mean? Screenshot-2020-04-20-at-00.39.50.png

#### Ken Lee (Apr 19 2020 at 23:41):

Chris Hughes said:

Even the very first notation is very hard to understand. What does this mean? Screenshot-2020-04-20-at-00.39.50.png

it's just BNF. See : https://en.wikipedia.org/wiki/Backus%E2%80%93Naur_form

#### Chris Hughes (Apr 19 2020 at 23:41):

What's BNF?

#### Mario Carneiro (Apr 19 2020 at 23:41):

My main goal with chapter 2 of the thesis especially was to get all the axioms together in one place, as quickly, precisely, and compactly as possible, as a source for future formalization work. As a result it asks a lot from the reader, and in particular familiarity with BNF and "big fraction" notation

#### Chris Hughes (Apr 19 2020 at 23:42):

Okay. At least I know what it's called now, that should help a lot.

#### Mario Carneiro (Apr 19 2020 at 23:42):

It is notation for what we would call an inductive type

#### Kenny Lau (Apr 19 2020 at 23:43):

the first line means "a universe level ($\ell$) is either a universe level $u$ or ($|$) $0$ or ($|$) the successor of a universe level $S \ell$ or etc

#### Mario Carneiro (Apr 19 2020 at 23:44):

the first line says that $\ell$ is a variable denoting a syntactic class (that we would call `level`

), which can be a variable $u$, the constant $0$, an $S$ followed by a level expression, or the max or imax of two level expressions

#### Mario Carneiro (Apr 19 2020 at 23:44):

It exactly matches lean's `level`

, except that lean has an additional `mvar`

constructor that we omit because we aren't formalizing unelaborated terms

#### Kenny Lau (Apr 19 2020 at 23:45):

how close are we from building Lean in Lean (without violating Second Incompleteness)?

#### Ken Lee (Apr 19 2020 at 23:48):

Mario Carneiro said:

My main goal with chapter 2 of the thesis especially was to get all the axioms together in one place, as quickly, precisely, and compactly as possible, as a source for future formalization work. As a result it asks a lot from the reader, and in particular familiarity with BNF and "big fraction" notation

I was initially reading from Coq's site. But I got stuck at the triad of positivities Coq needed to define inductive definitions. Then I found your paper. I enjoyed its compactness and felt like I benefited from unpacking it.

#### Mario Carneiro (Apr 19 2020 at 23:48):

I had some work on a lean typechecker from maybe 2 years ago, which had some difficulty managing dependence on the environment, as well as the more recent lean in MM0 definition (https://github.com/digama0/mm0/blob/master/examples/lean.mm1), which can easily be ported to lean

#### Mario Carneiro (Apr 19 2020 at 23:49):

"lean in MM0" is directly based on the thesis description

#### Marc Huisinga (Apr 20 2020 at 08:42):

@Mario Carneiro do you have plans to publish your thesis eventually?

#### Mario Carneiro (Apr 20 2020 at 08:48):

I suppose? I'm not very good at finding journals for this kind of thing, and it's already served its main purpose, which was to get me a masters degree. It will probably live in preprint-like state for a while yet

#### Patrick Massot (Apr 20 2020 at 10:57):

Mario Carneiro said:

Would there be a demand for a type theory primer more in the style of https://coq.github.io/doc/master/refman/language/cic.html ? That is a bit less symbol heavy and more tutorialized. I don't know if I could write something like that but I would be happy to collaborate with one of the educators around here

I think people have already answered this question many time, but internet storage is cheap so let's do it again: YES.

Last updated: May 16 2021 at 22:14 UTC