a finite infinite hierarchy of types

Stream: general

[Luca Seemungal]

Hi, I'm very new. "Theorem Proving in Lean" has the statement "Lean’s underlying foundation has an infinite hierarchy of types", but if I type

#check Type 87172

my Lean server crashes. Why is this? My computer says it's a segfault (SIGSEGV)

[Floris van Doorn]

Interesting. I need to make the number a couple of orders of maginute larger for my Lean server to crash.

Of course, in practice this never matters, because you rarely work in a specific type universe higher than, say, Type 3.

[Luca Seemungal]

I'm going to go ahead and assume this is some sort of hardware (RAM?) limitation. My machine is an old laptop from 2009 and I don't have anything else to test this on at the moment.

[Simon Hudon]

I think you're right. I'm under the impression that the specific universes are encoded using unary numerals

[Simon Hudon]

That would be why your memory runs out

[Wojciech Nawrocki]

Yes, they are something like a linked list (with 87172 nodes in this case) iirc

[Mario Carneiro]

A linked list with 87172 nodes in it isn't that large... There must be hundreds or thousands of them to exhaust memory, and even so a segfault is not the best way to indicate this

[Wojciech Nawrocki]

You're right Mario, even with 16-byte nodes (pointer + some data) it would only be about 1Mib, so it shouldn't crash (but would be slow, since that's still a long list). Some of the code is here.

[Keeley Hoek]

I don't know anything about how it works, but at some point there was some custom allocation going on for various objects in lean, and if that's still happening it could just be that the custom allocator ran out of memory pages and just tried to keep going.