square bracket indexing

Stream: lean4

[James Sully]

I'm confused about the square bracket indexing. Usually this notation implies constant time access to elements, but Lists are cons lists, for which indexing is usually linear time. Is there some optimization under the hood that makes it constant, or is it actually just linear?

[Kyle Miller]

It's linear. If you want constant-time accessing, there's Array, which looks like a List but it actually uses a block of contiguous memory.

They have different uses and have different runtime characteristics. List is a linked list so it supports sharing when you cons to the front, but Array has constant-time pushing to the end if the runtime detects there's no sharing.

[James Sully]

ok, thanks. I was thinking it might be an analogous situation to how Nat is optimized to not be as slow as one would naively assume