Arrays in lean runtime

Stream: lean4

[Callan McGill]

I was wondering if arrays in the lean4 runtime are all boxed or if they used an optimal layout based on the argument type?

[James Gallicchio]

scalar arrays (e.g. Array Byte, Array Float, ...) have specialized array impls, but everything else is an array of lean_object*s. so if you have a generic function operating on generic arrays, everything will end up in a lean_object* box which may not be the optimal layout

[Callan McGill]

so just to check, if I used a something like Array.sequenceMap over a scalar array, that is going to produce reasonable code?

[James Gallicchio]

I have no clue :sweat_smile: a lot of things can get in the way of producing optimized bytecode. From what I've heard, getting leanc to produce a very optimized binary can be hard

[Mario Carneiro]

I don't think Array Byte has a specialized layout. (Instead there is a separate type ByteArray)

[Mario Carneiro]

Array A always has boxed cells

[Mario Carneiro]

Many array functions are @[specialize]d to the types they get used at though, so it's not always generic code

[Mario Carneiro]

the best way to find out is to just compile it and inspect the generated C code (which isn't too hard to follow once you get used to it)

[James Gallicchio]

Mario Carneiro said:

I don't think Array Byte has a specialized layout. (Instead there is a separate type ByteArray)

Ahh, I thought the type constructor itself was specialized. Sorry for the misinformation @Callan McGill

[Callan McGill]

No worries, it was otherwise useful info.

[Gabriel Ebner]

There are separate ByteArray and FloatArray types if you need unboxed arrays.