一句话：提出源类型与内存类型双视角以精确控制 ADT 内存布局，并给出构造/析构与模式匹配的正确编译算法。
代数数据类型（ADT）已在主流语言中普及，但其抽象会隐藏值的确切内存布局，导致底层编程中难以使用，Rust 对内存表示的控制也很有限。本文提出一种基于双视角的数据布局规范方法：源类型在其余代码中提供高层描述，内存类型则提供对内存布局的完全控制。两个视角通过专门的有效性判据相联系，既便于正确性推理，也支持操作内存视图的优化。作者给出将构造器、析构器（包括模式匹配）编译到低层内存表示的算法，并证明其正确性；在工具 ribbit 中实现并编译到 LLVM IR，给出了初步实验结果。
Initially present only in functional languages such as OCaml and Haskell, Algebraic Data Types (ADTs) have now become pervasive in mainstream languages, providing nice data abstractions and an elegant way to express functions through pattern matching. Unfortunately, ADTs remain seldom used in low-level programming. One reason is that their increased convenience comes at the cost of abstracting away the exact memory layout of values. Even Rust, which tries to optimize data layout, severely limits control over memory representation. In this article, we present a new approach to specify the data layout of rich data types based on a dual view: a source type, providing a high-level description available in the rest of the code, along with a memory type, providing full control over the memory layout. This dual view allows for better reasoning about memory layout, both for correctness, with dedicated validity criteria linking the two views, and for optimizations that manipulate the memory view. We then provide algorithms to compile constructors and destructors, including pattern matching, to their low-level memory representation. We prove our compilation algorithms correct, implement them in a tool called ribbit that compiles to LLVM IR, and show some early experimental results.
@article{paperbot1909,
title = {Bit-Stealing Made Legal: Compilation for Custom Memory Representations of Algebraic Data Types},
author = {Thaïs Baudon and Gabriel Radanne and Laure Gonnord},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {ICFP},
year = {2023},
doi = {10.1145/3607858}
}