We’re delighted to announce that Rodrigo’s paper on the theory for extending GHC Core to cover linear types has been accepted at POPL 2026, and will be presented in January. Read more background on Rodrigo’s blog, or check out the extended version of the paper on arXiv!
Lazy Linearity for a Core Functional Language
Rodrigo Mesquita, Bernardo Toninho
POPL 2026 (PDF)
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.