type of 'list'

Stream: new members

[Daniel Ever]

I apologize if that was covered before, but I'm now reading through Theorem proving in Lean and stumbled upon the 'list' thing. Why does 'list' has a type of Type u → Type u? Shouldn't the type of lists of elements of some type have its own type? If not, why it's so? The same seems to apply to 'prod' and some others. Thanks in advance.

[Arthur Paulino]

You might want to ask this in #new members

[Notification Bot]

This topic was moved here from #Lean for teaching > type of 'list' by Anne Baanen

[Kyle Miller]

list is the type constructor: given a type a, list a is the type of lists of elements of type a. list is a function so that you can create list types for any element type you want

[Logan Murphy]

This is what allows us to make, for instance, the types list ℕ and list string using a single definition of what a list is.

[Daniel Ever]

well, my question is why the type of lists of elements of type 'a' has the same type as elements of type 'a' itself? say, shouldn't natural numbers and lists of natural numbers have different types?

[Logan Murphy]

They do have different types -- list ℕ is not the same type as ℕ. They do, however, live in the same type universe. Is that what's confusing?

[Kyle Miller]

If nat : Type, then list nat : Type according to the type of list. They do have their own types, but the type of their types is Type. It's like how 22 : nat and 37 : nat but we don't conclude that 22 = 37.

[Logan Murphy]

If I have a function f : ℕ -> ℕ, all I know from the type signature is that if I give it a number, I get a number back. But the output is not necessarily the same number I gave it.

[Daniel Ever]

Logan Murphy said:

They do have different types -- list ℕ is not the same type as ℕ. They do, however, live in the same type universe. Is that what's confusing?

yep, I don't seem to get it right. if list \nat and \nat don't have the same type, then why does it show the same type 'Type' when I run #check ?

[Logan Murphy]

ℕ is a type, and so is bool, and so is list ℕ and so is list bool. These are all different things, but all have the same type.

[Daniel Ever]

Kyle Miller said:

If nat : Type, then list nat : Type according to the type of list. They do have their own types, but the type of their types is Type. It's like how 22 : nat and 37 : nat but we don't conclude that 22 = 37.

yeah, I get that, but 22 and 37 are 'the same' objects, while some natural number and a list of a natural numbers aren't exactly the same in many ways we may be interested in

[Daniel Ever]

Logan Murphy said:

ℕ is a type, and so is bool, and so is list ℕ and so is list bool. These are all different things, but they happen to all be the same type.

but why do natural numbers and lists of natural numbers have the same type? There should be a step of deduction I'm missing

[Kyle Miller]

Daniel Ever said:

yeah, I get that, but 22 and 37 are 'the same' objects, while some natural number and a list of a natural numbers aren't exactly the same in many ways we may be interested in

It seems that you might be jumping two levels in the type hierarchy here. It's not about "some natural number and a list of natural numbers," but rather "the type of natural numbers and the type of lists of natural numbers". One way nat and list nat are "the same" objects is that they're both inductive types, and they're both in Type.

[Arthur Paulino]

1 is of type nat
[1, 2, 3] is of type list nat

nat is a type, so nat is of type Type u for some universe u
list nat is also a type, so list nat is of type Type u, such that the type nat lives in u

It can get a bit awkward because we may not be accustomed to think about the type of a type

[Henrik Böving]

For me personally it has been much easier to let go off my usual idea of what a type is from regular languages like Java etc. when learning Lean. This is because in Lean everything has a type while in regular languages only values have a type.

Every natural number value is of type Nat, the type Nat is of type Type.
List is a type constructor so a function that takes in a type (the type of its members) and produces a new one (the type of lists with the members of the parameter type), written out its type is: Type u -> Type u. When we are working with Type as the type of members of the list (which is just an alias for Type 0) this turns out to be: Type 0 -> Type 0 or written a little shorter: Type -> Type. So now if we pass in the Nat type we get some type List Nat which itself has type Type.

So now both the Nat type and the List Nat type have type Type. However the nat values have type Nat and the lists that contain nats have type List Nat

[Daniel Ever]

Ok, that clears the confusion, thanks! Unfortunately I don't have any coding experience, so I have tough time trying to get through quite abstract reading materials.

Btw, perhaps anyone can suggest some soft intro to Lean more noob-friendly than Theorem proving in Lean and other manuals referenced on the official site?

[Arthur Paulino]

Hmm, Lean has a lot of features so an adequate material will depend on what you're struggling with in the most fundamental level. Are you used to the functional paradigm? Dependent types? Theorem proving? What's your background?

[Henrik Böving]

You could play the natural number game although its more of a "how does basic induction, rewriting and logic work in Lean" rather than an intro to Lean itself. My strategy with learning about stuff in Lean has been to keep pushing against the issue for quite a while (my definition of while here includes several days), try to read code that is related to my issue (although that does of course only work if you have at least basic understanding of Lean), ask people here in that order....aaaand usually it does work out although its of course a lengthy process at times :sweat_smile:

[Marc Huisinga]

Logic and Proof can be useful if you want to learn the basics of logic.
There's also The Hitchhiker's Guide to Logical Verification but I don't know what the prerequesites for it are.

[Daniel Ever]

I don't have any solid academic background. I do some economics stuff and occasionally teach some undergrad math (nothing harder than basic linear algrebra our multivariable calculus) to grown ups who most of the time work in IT, hence the idea to learn Lean in order to introduce them to proofs in a manner they might percieve easier to begin with.

I've played numbers game and did some exercises in the tutorials (those devoted to the basic theorems of analysis). However I feel that without the more fundamental understanding it all revolves around learning a handful of tactics which work in predefined structures and situations. That way it looks more like learning-by-doing, rather than understanding what you're doing and why it works.

[Arthur Paulino]

Check out this section of the community website: https://leanprover-community.github.io/learn.html#more-on-foundations

And of course, check out the whole page as it may contain material of your interest

[Arthur Paulino]

The idea of using Lean to teach new mathematical concepts can be a bit tricky. Maybe #Lean for teaching might contain valuable insights on that matter

[Daniel Ever]

Arthur Paulino said:

The idea of using Lean to teach new mathematical concepts can be a bit tricky. Maybe #Lean for teaching might contain valuable insights on that matter

thanks! been there, checked that) also I understand the possible drawbacks, it seems to me that being able to handle more abstract proofs at some point becomes way more efficient than trying to force your way through mostly calculational approaches which quickly become very unintuitive and cumbersome

[Arthur Paulino]

Daniel Ever said:

been there, checked that

Right! I forgot you first posted there :sweat_smile:

[Daniel Ever]

I mean all the resources you've mentioned, also I've watched some Youtube videos I could find, slowly trying to wrap my mind around it for some months so far)

[Julian Berman]

Daniel Ever said:

Kyle Miller said:

If nat : Type, then list nat : Type according to the type of list. They do have their own types, but the type of their types is Type. It's like how 22 : nat and 37 : nat but we don't conclude that 22 = 37.

yeah, I get that, but 22 and 37 are 'the same' objects, while some natural number and a list of a natural numbers aren't exactly the same in many ways we may be interested in

Type represents precisely the ways they are the same. If it helps, I think of this quite like the "real world". If I ask you what's in common between wheat and barley, you say "those are grains". If I say "piano and guitar", you say "instruments". If I say "wheat, barley, piano, and guitar", you get a bit confused, but we indeed have ways to classify these together, say "objects" or "matter". Sometimes indeed we do need to talk about these disparate objects together, so we have words for the less "tightly related" groups, or for groups of groups themselves. In programming languages, we do too, the way Lean calls the "group of groups" is Type, it's a way of referring to all of a set of different kinds of objects together, and there are things that are in common to every type, even if they're simple ones like "they have a name".

[Damiano Testa]

When I was starting to learn Lean, Kevin Buzzard recommended browsing through the book Learn you a Haskell. I had no idea of programming and found the book a great introduction to functional programming and, especially at the beginning, Lean (even though the book is about Haskell!).

[Adam Topaz]

So who will write the book "Lean you a Lean for great proofs!" ?

[Henrik Böving]

I was contemplating whether it would be worth it to provide an alternative intro to Theorem Proving in Lean 4 since Lean 4 is also meant for general purpose programming.

[Kevin Buzzard]

@Daniel Ever are you happy with the idea that the natural numbers are a set? And that the collection of all lists of natural numbers is also a set? Traditionally this is what people say, especially if they're used to mathematics being set up within a framework of set theory. That's all that's going on here, except that we say type not set.

I wrote a blog post when I was wrestling with all this stuff and trying to figure out what all this type thing was. I also wrote something about it as part of the notes for the course I'm teaching right now.

[Daniel Ever]

Kevin Buzzard said:

Daniel Ever are you happy with the idea that the natural numbers are a set? And that the collection of all lists of natural numbers is also a set? Traditionally this is what people say, especially if they're used to mathematics being set up within a framework of set theory. That's all that's going on here, except that we say type not set.

I wrote a blog post when I was wrestling with all this stuff and trying to figure out what all this type thing was. I also wrote something about it as part of the notes for the course I'm teaching right now.

1) yep, I am, though having both natural numbers and their lists displaying the same type is kinda awkward, but guess if any type has to belong to some higher type, we can find something common between numbers and lists to justify that

2) I've read most of the introductionary posts on your blog, but haven't heard of the second resource you've mentioned, will certainly give it a look, thanks!

[Kevin Buzzard]

I don't understand how you can say "I am happy that the collection of all natural numbers is a set, and that the collection of all lists of natural numbers is a set, but I am confused by the fact that in Lean the collection of all natural numbers is a type, and the collection of all lists of natural numbers is a type"

[Daniel Ever]

Kevin Buzzard said:

I don't understand how you can say "I am happy that the collection of all natural numbers is a set, and that the collection of all lists of natural numbers is a set, but I am confused by the fact that in Lean the collection of all natural numbers is a type, and the collection of all lists of natural numbers is a type"

my confusion arises from the fact that types aren't exactly sets and as far as I can get it, types assume some additional properties about its terms, unlike sets, which say nothing about the elements except for they belong to a set.

intuitively I don't see a lot in common between natural numbers and lists of natural numbers, so when they both are said to have the same type it rings a bell that something isn't right as I fail to think of properties that would be true both for natural numbers and for 'natural lists' which would justify them being typed the same.

[Kyle Miller]

The set of natural numbers and the set of lists of natural numbers both have elements, so those sets at least have that in common.

[Eric Rodriguez]

types don't really assume additional properties about their terms; if you know some category theory, we model the category of sets as the category of Types in Lean

[Eric Rodriguez]

now, a specific type (like ℕ) does assume sometihng about its elements, but so does the set ℕ

[Eric Rodriguez]

if you just say "ok give me a type" (in Lean, variables (a : Type)), you can't really say anything about it, apart from it exists, and maybe it has members

[Patrick Johnson]

The set of natural numbers and the set of lists of natural numbers have one thing in common: both are sets. So, they belong to the collection of all sets. You can think of Type as the collection of all sets, so it makes sense that it contains the set of natural numbers and the set of lists. Higher types, such as Type 1, Type 2, Type 3, etc, exist more or less just to prevent paradoxes.

[Patrick Johnson]

Note that this is just an analogy. Type nat is not the same as the univ set of naturals.

[Daniel Ever]

Eric Rodriguez said:

types don't really assume additional properties about their terms; if you know some category theory, we model the category of sets as the category of Types in Lean

ok, thanks! that's the idea about types I got from reading Ansten Klev's essay on the subject, prehaps I got it wrong, but for sets implying something about its members isn't a necessity.

say, we can have a set of continuos functions or prime numbers, but as well we may have a set made up of functions, numbers, crocodiles and hamburgers, while types don't allow that degree of flexibility

[Daniel Ever]

Patrick Johnson said:

The set of natural numbers and the set of lists of natural numbers have one thing in common: both are sets. So, they belong to the collection of all sets. You can think of Type as the collection of all sets, so it makes sense that it contains the set of natural numbers and the set of lists. Higher types, such as Type 1, Type 2, Type 3, etc, exist more or less just to prevent paradoxes.

may I ask what is implied by the 'univ' set of naturals?

[Kevin Buzzard]

Daniel Ever said:

say, we can have a set of continuos functions or prime numbers, but as well we may have a set made up of functions, numbers, crocodiles and hamburgers, while types don't allow that degree of flexibility

Sure they do. Here's a type which whose elements are either naturals, booleans, or functions from the naturals to the naturals:

inductive natural_or_boolean_or_function
| of_nat : ℕ → natural_or_boolean_or_function
| of_bool : bool → natural_or_boolean_or_function
| of_function (f : ℕ → ℕ) : natural_or_boolean_or_function

My mental model is that a type is just what a type theorist calls a set.

[Eric Rodriguez]

that is, in some ways, true. we have that if a : T₁, then a : T₂ is false unless T₁ = T₂. but you can build these up however you want; for example, you could do your type using the disjoint union Crocodiles ⊕ Functions ⊕ Numbers ⊕ Hamburgers; now a term of Crocodiles isn't a term of that disjoint union type, but you place a thin wrapper around it (sum.inl) and it is.

[Kevin Buzzard]

Once you get deeper into the theory you learn subtleties and how the concepts differ slightly, but if you are just a beginner then I think that modelling types as sets and sets as types is a productive point of view.

[Daniel Ever]

Kevin Buzzard said:

Once you get deeper into the theory you learn subtleties and how the concepts differ slightly, but if you are just a beginner then I think that modelling types as sets and sets as types is a productive point of view.

thanks for the guidelines, I've read and watched some materials which advocated for the radical shift of perception, saying that it's absolutely essential to understand why types are so unique and important, and why reverting to set-theoretical thinking makes all the new found intutionistic magic fade away.

[Kevin Buzzard]

Maybe if you have a CS background this is a productive point of view, but I teach Lean to mathematicians and I tell them all on day 1 that a Type is just what Lean calls a set and for now that's all they need to know. I think this is a useful model to begin with.

[Kevin Buzzard]

I should add that you just used the word "intutionistic", and discussions of various weak non-classical logics such as that and constructivism do not occur in my classes; we work with classical logic throughout. Again this reflects the background of the students I'm teaching.

[Daniel Ever]

@Eric Rodriguez thank you, I'll keep in mind that types can be used that way, finding something common in things that aren't exactly the same at the first glance

@Kevin Buzzard Indeed, my experience is shaped by lots of additional materials I have to browse through to make things a bit more clear, say, this type theory related course: http://www.cs.cmu.edu/~crary/317-f18/schedule.html and many others

In that way both Lean and type theory are usually seen as a development of constructionist ideas and it's highlighted that those ideas make it possible to efficiently verify all the proofs

[Eric Rodriguez]

mathlib is not constructivist, at all :)

[Kevin Buzzard]

Lean's core code contains nonconstructive axioms and these axioms are used everywhere in Lean's developments of mathematics. We are rejecting constructivism in our mathematics library and this is what makes it so much more powerful than many of the other libraries out there.

[Kevin Buzzard]

The decades-old computer science story that constructivism somehow makes mathematics more powerful is something which mathematicians saw through about 100 years ago. Since that time classical mathematics has produced milestone after milestone (Fermat's Last Theorem, the Poincare conjecture etc etc) and it is these sorts of results which we are longingly looking forward to here in the Lean mathematical community.

[Daniel Ever]

@Kevin Buzzard so, one could say that the guiding criteria for adopting some sort of foundations or general way of thinking among the math community mostly relies on its potential to produce new results, rather than some other aspects?

[Kevin Buzzard]

The theorem proving community contains many provers, and many communities of users, each with their own viewpoints, aims etc. As a resolutely classical mathematician myself, my aim has always been to grow mathlib as a classical library, with the model in my head that Type = set. There are people who use other theorem provers with other axioms and whose model of a type is some complex kind of topological space defined up to homotopy. I'm not speaking for those people. I'm talking only about my personal aim for the community's mathematics library, but I would say that there are many other contributors here who are equally happy to reject constructivism. I'm bringing this up now because if you are interested in constructivism then Lean might not be the prover for you -- or perhaps it's more accurate to say that Lean is perfectly happy to be constructive but you might not find much of a support group here when you get stuck.

[Daniel Ever]

@Kevin Buzzard I don't think my final goals make me competent enough to reason about the prefered logical paragidm, given that what exists now isn't in a need of an immediate replacing. However, some materials associated with automatic provers and type theory tend to present things that way, saying that type theory being adopted as the new foundations (with all the assumed features) is the only way for math to progress.

[Kevin Buzzard]

Well I work in a building full of people who are extremely skeptical about that idea, based on the fact that math has progressed very nicely for the last 2500 years without these automatic provers. One could regard the mathlib effort as some kind of attempt to at least get up to speed with the statements of modern mathematics.

[Daniel Ever]

@Kevin Buzzard in his video devoted to provers (and establishing the research center) Hoskinson mentioned that provers might aid the progress of math by allowing for an easier transfer of experience via libraries, since actual mathematicians are prone to dying and the ratio of an active career years to studying aren't very good.

perhaps you see the most potential in that regard?

[Kevin Buzzard]

We'll see what they end up doing. I am too cautious to predict the future. I just have genuine optimism that they will help mathematics somehow but I have only been in this area a few years. I suspect people have been saying all sorts of things about what theorem provers will or might do ever since theorem provers have existed.

[Daniel Ever]

ok, thanks for your time and replies, I'll certainly give it a thought and study the provided resources!