Lazy Linearity for a Core Functional Language

TL;DR

This paper introduces Linear Core, a system for lazy languages like Haskell, ensuring linear resource usage semantics are preserved during program optimization, addressing the gap between syntactic and semantic linearity.

Contribution

Linear Core is a novel system that statically models lazy linearity, guaranteeing linear resource usage and preserving linearity through compiler optimizations.

Findings

Linear Core is sound and guarantees linear resource usage.

Transformations in Linear Core preserve linearity, unlike in standard Core.

Implementation as a compiler plugin validates effectiveness with linearity-heavy libraries.

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.