Zulip Chat Archive

Stream: new members

Topic: List is forced up a universe?


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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)" ?

view this post on Zulip Reid Barton (Apr 19 2020 at 22:50):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Reid Barton (Apr 19 2020 at 23:11):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Reid Barton (Apr 19 2020 at 23:12):

Oh, hmm.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Apr 19 2020 at 23:22):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 19 2020 at 23:28):

right

view this post on Zulip 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

view this post on Zulip Chris Hughes (Apr 19 2020 at 23:29):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 19 2020 at 23:33):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Chris Hughes (Apr 19 2020 at 23:41):

What's BNF?

view this post on Zulip 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

view this post on Zulip Chris Hughes (Apr 19 2020 at 23:42):

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

view this post on Zulip Mario Carneiro (Apr 19 2020 at 23:42):

It is notation for what we would call an inductive type

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 19 2020 at 23:45):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 19 2020 at 23:49):

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

view this post on Zulip Marc Huisinga (Apr 20 2020 at 08:42):

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

view this post on Zulip 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

view this post on Zulip 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