一句话：提出 Linear Core，将线性资源语义从语法出现扩展到惰性求值语义，并证明其可靠性及优化保持线性。
在线性类型语言中，消费线性资源传统上等同于资源在程序中的语法出现。但在非严格求值下，语法出现不一定意味着执行时会使用该资源；Haskell 的优化编译器又会大幅重写源程序，常破坏语法线性却保持语义。本文提出 Linear Core，一种静态接受惰性线性语义的系统，适用于 GHC Core 等惰性语言。作者证明 Linear Core 是可靠的，能保证线性资源使用，并证明多个优化变换在 Linear Core 中保持线性，而在 Core 中不成立。系统已实现为编译器插件，并针对包括 linear-base 在内的重度使用线性的库进行了验证。
Traditionally, in linearly typed languages, consuming a linear resource is synonymous with its syntactic occurrence in the program. However, under the lens of non-strict evaluation, linearity can be further understood semantically, where a syntactic occurrence of a resource does not necessarily entail using that resource when the program is executed. While this distinction has been largely unexplored, it turns out to be inescapable in Haskell’s optimising compiler, which heavily rewrites the source program in ways that break syntactic linearity but preserve the program’s semantics. We introduce Linear Core, a novel system which accepts the lazy semantics of linearity statically and is suitable for lazy languages such as the Core intermediate language of the Glasgow Haskell Compiler. We prove that Linear Core is sound, guaranteeing linear resource usage, and that multiple optimising transformations preserve linearity in Linear Core while failing to do so in Core. We have implemented Linear Core as a compiler plugin to validate the system against linearity-heavy libraries, including linear-base .
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{MesquitaT26,
title = {Lazy Linearity for a Core Functional Language},
author = {Rodrigo Mesquita and Bernardo Toninho},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776711}
}