Lazy Linearity for a Core Functional Language
I’m very proud to announce that “Lazy Linearity for a Core Functional Language”, a paper by myself and Bernardo Toninho, will be published at POPL 26! The extended version of the paper, which includes all proofs, is available here [arXiv, PDF]. The short-ish story: In 2023, for my Master’s thesis, I reached out to Arnaud Spiwack to discuss how Linear Types had been implemented in GHC. I wanted to research compiler optimisations made possible by linearity. Arnaud was quick to tell me: “Well yes, but you can’t!“ “Even though Haskell is linearly typed, Core isn’t!”1 Linearity is ignored in Core because, as soon as it’s optimised, previously valid linear programs become invalid. It turns out that traditional linear type systems are too syntactic, or strict, about…
