List is forced up a universe?

Stream: new members

[Ken Lee]

#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]

The short answer is you put the type (a in list a) to the right of the colon.

[Ken Lee]

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]

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

[Chris Hughes]

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]

you'd want something like

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

[Ken Lee]

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]

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]

Ken Lee said:

but surely list (A : Type) : Type is just syntactic sugar for list : Type -> Type?

It isn't

[Reid Barton]

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]

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]

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]

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]

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]

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]

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]

Hmm, so I guess biglist lets you do "polymorphic recursion". Is that ever actually useful?

[Mario Carneiro]

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]

list.rec easily implies biglist.rec but the reverse is not true (at least not without cast headaches)

[Reid Barton]

Oh, hmm.

[Mario Carneiro]

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]

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]

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]

@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]

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]

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]

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]

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

[Kevin Buzzard]

@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]

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]

right

[Ken Lee]

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]

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

[Kenny Lau]

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]

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]

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

[Mario Carneiro]

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]

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]

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]

What's BNF?

[Mario Carneiro]

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]

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

[Mario Carneiro]

It is notation for what we would call an inductive type

[Kenny Lau]

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]

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]

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]

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

[Ken Lee]

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]

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]

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

[Marc Huisinga]

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

[Mario Carneiro]

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]

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.