Lazy Linearity for a Core Functional Language
Rodrigo Mesquita, Bernardo Toninho
TL;DR
The paper addresses how linear resources should be tracked in languages with non-strict evaluation, where syntactic linearity can be misleading after optimisations. It introduces Linear Core, a lazy, semantically aware core language with usage environments, WHNF-based case rules, irrelevance, and tagging to guarantee linear resource usage. The authors prove soundness, type safety, and that key Core-to-Core optimisations preserve linearity, and they validate the approach by implementing a GHC plugin that checks intermediate Core against linearity. This work enables linear resource guarantees in optimising compilers for lazy languages and provides a path toward integrating semantic linearity into Core and potentially into Haskell itself.
Abstract
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.