核心函数式语言中的惰性线性（Lazy Linearity）

《Proceedings of the ACM on Programming Languages》：Lazy Linearity for a Core Functional Language

线性资源在非严格评估中的语义与语法行为存在差异，Haskell优化编译器通过重写破坏语法线性性但保持语义。Linear Core系统静态保证线性资源使用，适用于Core中间语言，证明优化转换在Linear Core中有效而在原Core中无效，并实现为编译插件验证。

　　

摘要AI摘要

要查看此由AI生成的摘要，您必须具有高级访问权限。

了解更多登录

摘要

摘要

传统上，在线性类型语言中，消耗某种资源意味着该资源在程序中的语法出现。然而，在非严格求值的视角下，线性可以进一步从语义上进行理解：即资源在程序中的语法出现并不一定意味着在执行程序时必须使用该资源。尽管这一区别在很大程度上尚未被探索，但在Haskell的优化编译器中却不可避免。该编译器会大幅重写源代码，从而打破语法上的线性，但同时保持程序的语义。我们提出了Linear Core这一新系统，它能够静态地接受这种惰性（lazy）的线性语义，并适用于像Glasgow Haskell编译器的Core中间语言这样的惰性语言。我们证明了Linear Core是可靠的，能够保证资源使用的线性；同时，多种优化变换在Linear Core中能够保持线性，但在Core中则无法做到这一点。我们已将Linear Core实现为编译器插件，以验证其在处理依赖大量线性操作的库（包括linear-base）时的表现。

AI摘要

AI生成的摘要（实验性）

此摘要是由自动化工具生成的，并非由文章作者编写或审核的。它旨在帮助读者发现文章的相关性，并协助来自相关研究领域的读者理解文章内容。它旨在补充作者提供的摘要，后者仍是文章的官方总结。完整文章才是权威版本。点击此处了解更多。

点击此处对摘要的准确性、清晰度和实用性进行评论。您的反馈将有助于改进未来的版本。

要查看此由AI生成的通俗语言摘要，您必须具有高级访问权限。