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

λA:U1,μT:U2,(nil:T)+(cons:ATT)\lambda A:U_1,\mu T:U_2, (\mathsf{nil}:T) + (\mathsf{cons}:A\to T\to T)

and biglist is

μT:U1U2,(nil:A:U1, T  A)+(cons:A:U1, AT  AT  A)\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

λA:U,μT:U,(nil:T)+(cons:ATT)\lambda A:U_{\ell},\mu T:U_{\ell}, (\mathsf{nil}:T) + (\mathsf{cons}:A\to T\to T)

and biglist is

μT:UUS,(nil:A:U,T  A)+(cons:A:U,AT  AT  A)\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:UA\,:\,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:Ul A : U_l has type UlU_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 uu or (|) 00 or (|) the successor of a universe level SS \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 uu, the constant 00, an SS 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: Dec 20 2023 at 11:08 UTC