Zulip Chat Archive

Stream: general

Topic: a finite infinite hierarchy of types

Luca Seemungal (Aug 22 2019 at 18:24):

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 (Aug 22 2019 at 18:37):

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 (Aug 22 2019 at 18:40):

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 (Aug 22 2019 at 18:47):

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

Simon Hudon (Aug 22 2019 at 18:48):

That would be why your memory runs out

Wojciech Nawrocki (Aug 22 2019 at 19:35):

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

Mario Carneiro (Aug 22 2019 at 21:51):

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 (Aug 23 2019 at 12:52):

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 (Aug 24 2019 at 01:23):

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.

Last updated: Dec 20 2023 at 11:08 UTC