Getting rid of universes

Stream: new members

[Nicolas Rolland]

How are universes different from stack size ?

Why can't we get a big amount of them, write unsafe paradoxical code, let the program increase the universe index at execution, crash once we reach a certain threshold.

[Edward van de Meent]

i'm sorry, i don't understand this question. maybe it would help if you first point out why universes are like stack size?

[Edward van de Meent]

because in my mind universes are merely a device to make the system typecheck.

[Edward van de Meent]

(and make sure you can't create an element of the Empty type and such)

[Nicolas Rolland]

I know it can avoid paradox, but at what cost ? I'd prefer my program to just crash if it finds one.

What I write is not paradoxical (distributor composition !), yet I have to pay the price of showing it isn't, and it causes big modularity pb when you have to modify some universe before, because you used some element after...

They are like stack size, as I understand them, in the sense that we are always proving we are below some amount (which can be - generally inferred - max (max ... ))

If there is a way out, I want it.

[Edward van de Meent]

an easy way out if all you're really concerned with is programming, is generally not making your definitions universe-polymorphic.

[Edward van de Meent]

if there is a specific issue you're running into where you'd like help, please post a #mwe

[Riccardo Brasca]

Note that one of the main use of Lean is as a theorem prover, to do mathematics, so we need a solid axiomatic framework.

[Robert Maxton]

Nicolas Rolland said:

How are universes different from stack size ?

Why can't we get a big amount of them, write unsafe paradoxical code, let the program increase the universe index at execution, crash once we reach a certain threshold.

Because having a program fail at runtime largely defeats the point of Lean? The entire point of all this complex dependent type theory and careful definitions is a static compile-time guarantees that your program is valid.

Also, it reflects a real mathematical fact, which is that no sort of collection can contain all copies of itself -- there is no set of all sets, no type of all types, no category of all categories, etc. If you don't track universes, then you can prove False, which would make Lean useless as a proof assistant.

[Luigi Massacci]

You actually can have a set of all sets, and even having it be a member of itself, but making that consistent also requires a rather intricate setup. Of course you need to make some changes to other axioms to keep the whole thing from collapsing. Proving the consistency of one such system was one of the major recent successes in lean!