Lazy Linearity for a Core Functional Language
Rodrigo Mesquita and Bernardo Toninho
传统上,在线性类型语言中,消耗线性资源与其在程序中的句法发生同义。 然而,在非严格评估的视角下,线性性可以在语义上进一步理解,其中资源的句法发生并不一定意味着在执行程序时使用该资源。 虽然这种区别在很大程度上尚未探索,但在Haskell的优化编译器中却是不可避免的,该编译器在很大程度上重写了源程序,从而打破了语法线性度,但保留了程序的语义。 我们引入了线性核心(Linear Core),这是一种新颖的系统,它静态地接受线性的懒惰语义,适用于懒惰的语言,如格拉斯哥哈斯卡尔编译器的核心中间语言。 我们证明 Linear Core 是健全的,保证了线性资源的使用,并且多个优化转换保留了 Linear Core 中的线性度,同时在 Core 中未能这样做。 我们已经实现了线性核心作为编译器插件,以验证系统对抗线性重库,包括线性基。
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 sou...
