Lean中Unboxed类型：Array Point连续内存分配及编译优化问询

问题描述 #

在Lean中定义如下结构体：

structure Point where
  x : Float
  y : Float

当使用Array Point时，运行时每个Point实例会在堆上单独分配，数组的连续内存区域仅存储指向这些实例的指针。

想了解两个问题：

• 是否可以让Lean编译器将整个数组（包含所有Point实例）分配在单个连续内存区域中，类似C++或Rust的实现方式（类似Haskell的Data.Vector.Unboxed）？
• Lean编译器是否会自动执行这类转换优化？如果会，触发条件是什么？

解答 #

1. 实现连续内存存储的方法 #

可以通过**不可装箱类型（unboxed types）**和专用容器Std.Vector.Unboxed实现连续内存布局，这和Haskell的Data.Vector.Unboxed功能一致。

首先需要让你的Point结构体支持不可装箱特性，只需为其派生Unbox类型类即可：

structure Point where
  x : Float
  y : Float
deriving Unbox

之后使用Std.Vector.Unboxed来存储Point实例，它会将所有Point的x和y值连续存储在一块内存区域中，而非存储指向每个Point的指针，行为完全等价于C++的std::vector<Point>或Rust的Vec<Point>：

def examplePoints : Std.Vector.Unboxed Point :=
  Std.Vector.Unboxed.push (Std.Vector.Unboxed.push Std.Vector.Unboxed.empty ⟨1.0, 2.0⟩) ⟨3.0, 4.0⟩

2. 自动优化的情况 #

Lean编译器不会自动将普通Array Point优化为连续内存布局。普通Array是通用容器，设计用于存储任意类型，默认采用指针数组的存储方式，以兼容多态性和复杂类型的存储需求。

在局部代码中，如果编译器能证明结构体是仅包含原始类型、无堆分配子对象的小型结构，可能会进行栈上分配的优化，但这仅影响单个实例的存储位置，不会改变Array本身的全局内存布局——Array始终会存储指向实例的指针。

若要实现连续内存存储，必须显式使用Std.Vector.Unboxed这类专用容器，同时确保结构体实现了Unbox类型类。

内容的提问来源于stack exchange，提问作者eyelash